109 lines
3.6 KiB
OCaml
109 lines
3.6 KiB
OCaml
(*
|
|
As explained in the README.md ("Abstracting over an effect"),
|
|
this module as well as other modules is parametrized over
|
|
an arbitrary effect [T : Functor].
|
|
*)
|
|
|
|
module Make (T : Utils.Functor) = struct
|
|
module Constraint = Constraint.Make(T)
|
|
module SatConstraint = SatConstraint.Make(T)
|
|
module ConstraintSimplifier = ConstraintSimplifier.Make(T)
|
|
module ConstraintPrinter = ConstraintPrinter.Make(T)
|
|
|
|
type env = Unif.Env.t
|
|
type log = PPrint.document list
|
|
|
|
let make_logger c0 =
|
|
let logs = Queue.create () in
|
|
let c0_erased = SatConstraint.erase c0 in
|
|
let add_to_log env =
|
|
let doc =
|
|
c0_erased
|
|
|> ConstraintSimplifier.simplify env
|
|
|> ConstraintPrinter.print_sat_constraint
|
|
in
|
|
Queue.add doc logs
|
|
in
|
|
let get_log () =
|
|
logs |> Queue.to_seq |> List.of_seq
|
|
in
|
|
add_to_log, get_log
|
|
|
|
(** See [../README.md] ("High-level description") or [Solver.mli]
|
|
for a description of normal constraints and
|
|
our expectations regarding the [eval] function. *)
|
|
type ('a, 'e) normal_constraint =
|
|
| NRet of 'a Constraint.on_sol
|
|
| NErr of 'e
|
|
| NDo of ('a, 'e) Constraint.t T.t
|
|
|
|
let eval (type a e) ~log (env0 : env) (c0 : (a, e) Constraint.t)
|
|
: log * env * (a, e) normal_constraint
|
|
=
|
|
let add_to_log, get_log =
|
|
if log then make_logger c0
|
|
else ignore, (fun _ -> [])
|
|
in
|
|
(* We recommend calling the function [add_to_log] above
|
|
whenever you get an updated environment. Then call
|
|
[get_log] at the end to get a list of log message.
|
|
|
|
$ dune exec -- minihell --log-solver foo.test
|
|
|
|
will show a log that will let you see the evolution
|
|
of your input constraint (after simplification) as
|
|
the solver progresses, which is useful for debugging.
|
|
|
|
(You can also tweak this code temporarily to print stuff on
|
|
stderr right away if you need dirtier ways to debug.)
|
|
*)
|
|
let env = ref env0 in
|
|
let rec evalc : type aa ee. (aa,ee) Constraint.t -> (aa, ee) normal_constraint =
|
|
function
|
|
| Ret(a) -> NRet a
|
|
| Err(e) -> NErr e
|
|
| Map(c, f) ->
|
|
begin match (evalc c) with
|
|
| NRet a -> NRet (fun ctx -> (f (a ctx)))
|
|
| NErr e -> NErr e
|
|
| NDo act -> NDo (T.map (fun c -> Constraint.Map(c,f)) act)
|
|
end
|
|
| MapErr(c, f) ->
|
|
begin match (evalc c) with
|
|
| NRet a -> NRet a
|
|
| NErr e -> NErr (f e)
|
|
| NDo act -> NDo (T.map (fun c -> Constraint.MapErr(c,f)) act)
|
|
end
|
|
| Conj(c,d) ->
|
|
begin match (evalc c) with
|
|
| NRet a ->
|
|
begin match (evalc d) with
|
|
| NRet b -> NRet (fun ctx -> (a ctx,b ctx))
|
|
| NErr e -> NErr e
|
|
| NDo act2 -> NDo (T.map (fun d -> Constraint.Conj(c,d)) act2)
|
|
end
|
|
| NErr e -> NErr e
|
|
| NDo act1 -> NDo (T.map (fun c -> Constraint.Conj(c,d)) act1)
|
|
end
|
|
| Eq(x,y) ->
|
|
begin match (Unif.unify (!env) x y) with
|
|
| Ok(a) ->
|
|
env := a;
|
|
add_to_log (!env);
|
|
NRet (fun _ -> ()) (* We return unit *)
|
|
| Error(Clash(x,y)) ->
|
|
let xt,yt = Decode.decode (!env) x, Decode.decode (!env) y in
|
|
NErr(Clash(xt,yt))
|
|
| Error(Cycle(x)) -> NErr (Cycle(x))
|
|
end
|
|
| Exist(x,s,c) ->
|
|
env := Unif.Env.add x s !env;
|
|
add_to_log (!env);
|
|
evalc c
|
|
| Decode(v) -> NRet (fun _ -> Decode.decode (!env) v)
|
|
| Do(act) -> NDo act
|
|
in
|
|
let out = evalc c0 in
|
|
(get_log (), !env, out)
|
|
end
|