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: /// Returns an error if the variable is not an integer.
  /// Returns no clause if the variable is not initialised.
  /// Takes the environment of active global variables.
  let hsfModelVariables (svars : VarMap) : Result<Horn, Error> =
      let vpars =
          svars
          |> Map.toSeq
          |> Seq.map
              (function
  
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)
  
  