Mysaa/mpri-2.4-project-2023-2024
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Implemented solver for easy cases

Browse Source
This commit is contained in:
Mysaa 2024-03-11 20:15:09 +01:00
parent 5ed12f0cdf
commit 35d0bd817e
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 48 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
src/Solver.ml
View File

@ -37,9 +37,8 @@ module Make (T : Utils.Functor) = struct
| NErr of 'e
| NDo of ('a, 'e) Constraint.t T.t
let eval (type a e) ~log (env : env) (c0 : (a, e) Constraint.t)
: log * env * (a, e) normal_constraint
=
let eval : type a e. bool -> env -> (a, e) Constraint.t -> log * env * (a, e) normal_constraint
= fun log env0 c0 ->
let add_to_log, get_log =
if log then make_logger c0
else ignore, (fun _ -> [])
@ -57,6 +56,50 @@ module Make (T : Utils.Functor) = struct
(You can also tweak this code temporarily to print stuff on
stderr right away if you need dirtier ways to debug.)
*)
Utils.not_yet "Solver.eval" (env, c0, add_to_log, get_log)
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 -> Utils.not_yet "NDo" (act)
end
| MapErr(c, f) ->
begin match (evalc c) with
| NRet a -> NRet a
| NErr e -> NErr (f e)
| NDo act -> Utils.not_yet "NDo" (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 act -> Utils.not_yet "NDo" (act)
end
| NErr e -> NErr e
| NDo act -> Utils.not_yet "NDo" (act)
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)) -> NErr (Clash(x,y))
| 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) -> _
| Do(act) -> NDo act
in
let out = evalc c0 in
(get_log (), !env, out)
end