anchor.diff:      (* ----------------------------------------------------------------------- *)
   
       let meson_expand rules ((g, ancestors), ((insts, offset, size) as tup)) cont = 
  -        let pr = fst g
  -        let newancestors = insertan insts g ancestors
  -        let newstate = (g, newancestors), tup
  -        try 
  -            if !meson_prefine && pr > 0
  -            then failwith "meson_expand"
  -            else 
  -                let arules =
  -                    assoc pr ancestors
  -                    |> Option.getOrFailWith "find"
  -                meson_expand_cont 0 arules newstate cont
  -        with
  -        | Cut as e ->
  -            nestedFailwith e "meson_expand"
  -        | Failure _ -> 
  -            try 
  -                let crules = 
  -                    filter (fun ((h, _), _) -> length h <= size) (assoc pr rules |> Option.getOrFailWith "find")
  -                meson_expand_cont offset crules newstate cont
  -            with
  -            | Cut as e ->
  -                nestedFailwith e "meson_expand"
  -            | Failure _ as e ->
  -                nestedFailwith e "meson_expand"
  +        choice { 
  +            let pr = fst g
  +            let! newancestors = insertan insts g ancestors
  +            let newstate = (g, newancestors), tup
  +            let v =
  +                try 
  +                    if !meson_prefine && pr > 0 then 
  +                        failwith "meson_expand"
  +                    else 
  +                        let arules = assoc pr ancestors |> Option.getOrFailWith "find"
  +                        Choice.result <| meson_expand_cont 0 arules newstate cont
  +                with
  +                | Cut as e -> 
  +                    Choice.nestedFailwith e "meson_expand"
  +                | Failure _ -> 
  +                    try 
  +                        let crules = filter (fun ((h, _), _) -> length h <= size) (assoc pr rules |> Option.getOrFailWith "find")
  +                        Choice.result <| meson_expand_cont offset crules newstate cont
  +                    with
  +                    | Cut as e -> 
  +                        Choice.nestedFailwith e "meson_expand"
  +                    | Failure _ as e -> 
  +                        Choice.nestedFailwith e "meson_expand"
  +            return! v 
  +        }
   
       (* ----------------------------------------------------------------------- *)
       (* Simple Prolog engine organizing search and backtracking.                *)
  
positive.code:             vcounter := 0
  
          let fol_of_var v = 
              let currentvars = !vstore
              match assoc v currentvars with
              | Some x -> x
              | None ->
                  let n = inc_vcounter()
                  vstore := (v, n) :: currentvars
                  n
  
          let hol_of_var v =
              match rev_assoc v !vstore with
              | Some x -> x
              | None ->
                  rev_assoc v (!gstore)
                  |> Option.getOrFailWith "find"
  
          let hol_of_bumped_var v = 
              try 
                  hol_of_var v
              with
              | Failure _ -> 
                  let v' = v % offinc
                  let hv' = hol_of_var v'
                  let gv = genvar(Choice.get <| type_of hv')
                  gstore := (gv, v) :: (!gstore)
                  gv
  
          reset_vars, fol_of_var, hol_of_bumped_var
  
  
negative.code:                         expand_goals depth (lgoals, (insts, offset, lsize)) 
                              (cacheconts
                                   (fun (lg', (i, off, n)) -> 
                                       expand_goals depth (rgoals, (i, off, n + rsize)) 
                                           (cacheconts(fun (rg', ztup) -> cont(lg' @ rg', ztup)))))
                      with
                      | Failure _ -> 
                          expand_goals depth (rgoals, (insts, offset, lsize)) 
                              (cacheconts(fun (rg', (i, off, n)) -> 
                                       expand_goals depth (lgoals, (i, off, n + rsize)) (cacheconts(fun (lg', ((_, _, fsize) as ztup)) -> 
                                                                                                 if n + rsize <= lsize + fsize then 
                                                                                                     failwith 
                                                                                                         "repetition of demigoal pair"
                                                                                                 else cont(lg' @ rg', ztup)))))
                  else 
                      match gl with
                      | g :: gs -> 
                          expand_goal depth (g, tup) 
                              (cacheconts
                                   (fun (g', stup) -> 
                                   expand_goals depth (gs, stup) (cacheconts(fun (gs', ftup) -> cont(g' :: gs', ftup))))) 
                          |> Choice.toOption
                      | _ -> None // failwith "expand_goal: Unhandled case."
          
          fun g maxdep maxinf cont -> expand_goal maxdep (g, ([], 2 * offinc, maxinf)) cont
  
      (* ----------------------------------------------------------------------- *)
      (* With iterative deepening of inferences or depth.                        *)
  