anchor.diff:      open Starling.Core.View.Pretty
       open Starling.Core.Model.Pretty
   
  -    /// Decides whether to put brackets over the expression emission x,
  -    /// given its expression as the second argument.
  -    let maybeBracket xe x =
  +    /// <summary>
  +    ///     Given an expression and its Doc, potentially wrap the Doc
  +    ///     in brackets.
  +    /// </summary>
  +    /// <param name="xe">
  +    ///     The expression for which <paramref name="x"/> is a Doc.
  +    /// </param>
  +    /// <param name="x">
  +    ///     The document form of <paramref name="xe"/>.
  +    /// </param>
  +    /// <returns>
  +    ///     The Doc deriving from potentially bracketing
  +    ///     <paramref name="x"/>.
  +    /// </returns>
  +    let maybeBracket (xe : IntExpr<Var>) (x : Doc) : Doc =
           match xe with
           | SimpleInt -> x
           | CompoundInt -> parened x
   
       /// Emits an integral expression in Datalog syntax.
  -    let rec printInt : VIntExpr -> Doc =
  +    let rec printInt : IntExpr<Var> -> Doc =
           function
           | AVar c -> String c
           | AInt i -> sprintf "%d" i |> String
  
positive.code:     >> lift List.ofSeq
  
  /// Generates an if-then-else, collapsing automatically in the case of true or false.
  let ite i t e =
      match i with
      | True -> t
      | False -> e
      | _ -> ITE(i,t,e)
  
  /// Constructs a Horn literal for a Func.
  let hsfFunc dvs env (func : MVFunc) =
      // We check the defining views here, because anything not in the
      // defining views is to be held true.
      // Now that we're at the func level, finding the view is easy!
      dvs
      |> (lookup func >> mapMessages (curry InconsistentFunc func))
      |> bind (function
               | Some df -> lift Some (predOfFunc env tryIntExpr func)
               | None -> ok None)
  
  /// Constructs a Horn literal for a GFunc.
  let hsfGFunc dvs env { Cond = c; Item = ms } =
      hsfFunc dvs env ms
      |> (lift2 (fun cR -> Option.map (fun m -> ite cR m True))
                (boolExpr unmarkVar c))
  
  /// Constructs the body for a set of condition pair Horn clauses,
  /// given the defining views, preconditions and semantics clause.
  let hsfConditionBody dvs env ps sem =
      let psH =
          ps
          |> Multiset.toFlatSeq
          |> Seq.map (hsfGFunc dvs env)
          |> collect
          |> lift (Seq.choose id >> List.ofSeq)
  
      let semH = topLevelExpr sem
  
      lift2 List.append psH semH
  
  /// Constructs a series of Horn clauses for a term.
  /// Takes the environment of active global variables.
  let hsfTerm dvs env (name, {Cmd = c; WPre = w ; Goal = g}) =
      lift2 (fun head body ->
             [ Comment (sprintf "term %s" name)
               Clause (Option.get head, body) ])
            (hsfFunc dvs env g)
            (hsfConditionBody dvs env w c)
  
  /// Constructs a set of Horn clauses for all terms associated with a model.
  let hsfModelTerms gs dvs =
      Map.toSeq
      >> Seq.map (hsfTerm dvs gs)
      >> collect
      >> lift List.concat
  
  /// Constructs a HSF script for a model.
  let hsfModel
    ({ Globals = gs; ViewDefs = dvs; Axioms = xs }
       : Model<Term<MBoolExpr, GView<MarkedVar>, MVFunc>,
               FuncToIndefiniteBoolDefiner>)
    : Result<Horn list, Error> =
      trial {
          let! vs = gs |> hsfModelVariables
          let! ds = hsfModelViewDefs gs dvs |> lift Set.toList
          let! xs = hsfModelTerms gs dvs xs
          return vs :: List.append ds xs
      }
  
negative.code:  *)
  
  /// Generates a query_naming clause for a viewdef.
  let queryNaming ({ Name = n ; Params = ps } : DFunc) : Horn =
      QueryNaming { Name = n ; Params = List.map valueOf ps }
  
  /// Constructs a full constraint in HSF.
  /// The map of active globals should be passed as sharedVars.
  /// Some is returned if the constraint is definite; None otherwise.
  let hsfModelViewDef (sharedVars : VarMap)
    : (DFunc * VBoolExpr option) -> Result<Horn list, Error> =
      function
      | (vs, Some ex) ->
          lift2 (fun hd bd -> [Clause (hd, [bd]); Clause (bd, [hd])])
                (boolExpr makeHSFVar ex)
                (predOfFunc sharedVars ensureArith vs)
          |> lift (fun c -> queryNaming vs :: c)
      | (vs, None) -> ok [ queryNaming vs ]
  
  /// Constructs a set of Horn clauses for all definite viewdefs in a model.
  let hsfModelViewDefs (sharedVars : VarMap)
    : FuncToIndefiniteBoolDefiner -> Result<Set<Horn>, Error> =
      Seq.map (hsfModelViewDef sharedVars)
      >> collect
      >> lift (List.concat >> Set.ofSeq)
  
  