From 35d0bd817e2d68c434fb8abb427fb5e85ac89ec2 Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Mon, 11 Mar 2024 20:15:09 +0100
Subject: [PATCH] Implemented solver for easy cases

---
 src/Solver.ml | 53 ++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 48 insertions(+), 5 deletions(-)

diff --git a/src/Solver.ml b/src/Solver.ml
index 268a96f..fc2890a 100644
--- a/src/Solver.ml
+++ b/src/Solver.ml
@@ -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