anchor.diff:      >> lift List.ofSeq
   
   /// Generates an if-then-else, collapsing automatically in the case of true or false.
  -let ite i t e =
  +let ite (i : Literal) (t : Literal) (e : Literal) : Literal =
       match i with
       | True -> t
       | False -> e
       | _ -> ITE(i,t,e)
   
   /// Constructs a Horn literal for a Func.
  -let hsfFunc dvs env (func : MVFunc) =
  +let hsfFunc
  +  (definer : FuncToIndefiniteBoolDefiner)
  +  (sharedVars : VarMap)
  +  (func : MVFunc)
  +  : Result<Literal option, Error> =
       // 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
  +    definer
       |> (lookup func >> mapMessages (curry InconsistentFunc func))
       |> bind (function
  -             | Some df -> lift Some (predOfFunc env tryIntExpr func)
  +             | Some df -> lift Some (predOfFunc sharedVars tryIntExpr func)
                | None -> ok None)
   
   /// Constructs a Horn literal for a GFunc.
  -let hsfGFunc dvs env { Cond = c; Item = ms } =
  -    hsfFunc dvs env ms
  +let hsfGFunc
  +  (definer : FuncToIndefiniteBoolDefiner)
  +  (sharedVars : VarMap)
  +  ({ Cond = c; Item = ms } : GFunc<MarkedVar>)
  +  : Result<Literal option, Error> =
  +    hsfFunc definer sharedVars 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
  +let hsfConditionBody
  +  (definer : FuncToIndefiniteBoolDefiner)
  +  (sharedVars : VarMap)
  +  (weakestPre : GView<MarkedVar>)
  +  (command : MBoolExpr)
  +  : Result<Literal list, Error> =
  +    let weakestPreH =
  +        weakestPre
           |> Multiset.toFlatSeq
  -        |> Seq.map (hsfGFunc dvs env)
  +        |> Seq.map (hsfGFunc definer sharedVars)
           |> collect
           |> lift (Seq.choose id >> List.ofSeq)
   
  -    let semH = topLevelExpr sem
  -
  -    lift2 List.append psH semH
  +    let commandH = topLevelExpr command
  +
  +    lift2 List.append weakestPreH commandH
   
   /// 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}) =
  +let hsfTerm
  +  (definer : FuncToIndefiniteBoolDefiner)
  +  (sharedVars : VarMap)
  +  (name : string,
  +   {Cmd = c; WPre = w ; Goal = g}
  +     : Term<MBoolExpr, GView<MarkedVar>, MVFunc>)
  +  : Result<Horn list, Error> =
       lift2 (fun head body ->
              [ Comment (sprintf "term %s" name)
                Clause (Option.get head, body) ])
  -          (hsfFunc dvs env g)
  -          (hsfConditionBody dvs env w c)
  +          (hsfFunc definer sharedVars g)
  +          (hsfConditionBody definer sharedVars w c)
   
   /// Constructs a set of Horn clauses for all terms associated with a model.
  -let hsfModelTerms gs dvs =
  +let hsfModelTerms
  +  (sharedVars : VarMap)
  +  (definer : FuncToIndefiniteBoolDefiner)
  +  : Map<string, Term<MBoolExpr, GView<MarkedVar>, MVFunc>>
  +  -> Result<Horn list, Error> =
       Map.toSeq
  -    >> Seq.map (hsfTerm dvs gs)
  +    >> Seq.map (hsfTerm definer sharedVars)
       >> collect
       >> lift List.concat
   
   /// Constructs a HSF script for a model.
   let hsfModel
  -  ({ Globals = gs; ViewDefs = dvs; Axioms = xs }
  +  ({ Globals = sharedVars; ViewDefs = definer; 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
  +        let! vs = sharedVars |> hsfModelVariables
  +        let! ds = hsfModelViewDefs sharedVars definer |> lift Set.toList
  +        let! xs = hsfModelTerms sharedVars definer xs
           return vs :: List.append ds xs
       }
  
positive.code:  *)
  
  /// Generates a query_naming clause for a viewdef.
  let queryNaming { Name = n ; Params = ps } =
      QueryNaming { Name = n ; Params = List.map valueOf ps }
  
  /// Constructs a full constraint in HSF.
  /// The map of active globals should be passed as gs.
  /// Some is returned if the constraint is definite; None otherwise.
  let hsfModelViewDef svars
    : (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 svars 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 svars
    : FuncTable<VBoolExpr option> -> Result<Set<Horn>, Error> =
      Seq.map (hsfModelViewDef svars)
      >> collect
      >> lift (List.concat >> Set.ofSeq)
  
  
negative.code:  *)
  
  /// Converts a top-level Boolean expression to a list of Horn literals.
  let topLevelExpr : BoolExpr<MarkedVar> -> Result<Literal list, Error> =
      // The main difference here is that we model conjunctions directly as a
      // Horn literal list.
      function
  