anchor.diff:  open Starling.Backends.Z3
   open Starling.Optimiser.Graph
   
  -[<AutoOpen>] 
  +[<AutoOpen>]
   module Types =
       /// <summary>A Grasshopper variable shadowing a Starling variable.</summary>
       type ShadowVar =
  
positive.code: ﻿/// <summary>
  ///     Backend for emitting verification conditions in Grasshopper format
  /// </summary>
  module Starling.Backends.Grasshopper 
  
  open Chessie.ErrorHandling
  
  
negative.code:         // TODO(CaptainHayashi): is printType correct?
          | x -> Starling.Core.TypeSystem.Pretty.printType x
  
      let printTypedGrass (pVar : 'Var -> Doc) (var : CTyped<'Var>) : Doc =
          colonSep [ pVar (valueOf var); printType (typeOf var)]
  
      /// Prints a typed Var
      let printTypedVarGrass (v : TypedVar) : Doc =
          printTypedGrass String v
  
      /// Pretty-prints an arithmetic expression.
      let rec printIntExprG (pVar : 'Var -> Doc) (i : IntExpr<'Var>) : Doc =
          match i with
          | IVar c -> pVar c
          | IAdd xs -> infexpr "+" (printIntExprG pVar) xs
          | IMul xs -> infexpr "*" (printIntExprG pVar) xs
          | ISub xs -> infexpr "-" (printIntExprG pVar) xs
          | IDiv (x, y) -> infexpr "/" (printIntExprG pVar) [ x ; y ]
          | IMod (x, y) -> infexpr "%" (printIntExprG pVar) [ x ; y ]
          | IInt k -> String (sprintf "%i" k)
          | IIdx _ as x ->
              failwith
                  (sprintf
                      "[printIntExprG] Unimplemented for Grasshopper: %A"
                      x)
  
  
      /// Pretty-prints a Boolean expression.
      and printBoolExprG (pVar : 'Var -> Doc) (b : BoolExpr<'Var>) : Doc =
          match b with
          | BVar c -> pVar c
          | BTrue -> String "true"
          | BFalse -> String "false"
          | BAnd xs -> infexprV "&&" (printBoolExprG pVar) xs
          | BOr xs -> infexprV "||" (printBoolExprG pVar) xs
          | BImplies (x, y) ->
              /// Convert implications to disjunctive form
              printBoolExprG pVar (simp (BOr [BNot x; y]))
          | BNot (BEq (x, y)) -> infexpr "!=" (printExprG pVar) [x; y]
          | BNot x ->
              String "!" <+> (printBoolExprG pVar x) |> parened
          | BEq (x, y) -> infexpr "==" (printExprG pVar) [x; y]
          | BLt (x, y) -> infexpr "<" (stripTypeRec >> printIntExprG pVar) [x; y]
          | BLe (x, y) -> infexpr "<=" (stripTypeRec >> printIntExprG pVar) [x; y]
  