From d32caf307007a8592ceaced8ef659002f923811e Mon Sep 17 00:00:00 2001
From: julia <juliavonkreutzer@courriel>
Date: Fri, 29 Apr 2022 09:33:03 +0200
Subject: [PATCH] adding string_to_term and a first version of exec

---
 ocaml/Resolution.ml  | 50 +++++++++++++++++++++++++++++++++++++++++---
 ocaml/Unification.ml | 39 +++++++++++++++++-----------------
 2 files changed, 67 insertions(+), 22 deletions(-)

diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml
index e023d4f..01b1065 100644
--- a/ocaml/Resolution.ml
+++ b/ocaml/Resolution.ml
@@ -123,6 +123,50 @@ let rec enat i =
 let make_const_add n m = 
   [[add Pos zero y y]; [add Neg x y z; add Pos (s x) y (s z)]; [add Neg (enat n) (enat m) r; r]] 
 
-let constellation = make_const_add 3 1 ;;
-
-print_dgraph (dgraph constellation) ;;
\ No newline at end of file
+let constellation = make_const_add 1 3 ;;
+
+print_dgraph (dgraph constellation) ;;
+
+(* test constellation cyclique déterministe *)
+(*let boucle = [[Func("c", Neg, [x]) ; Func("c", Pos, [x])]]
+print_dgraph (dgraph boucle);; *)
+
+(* exec graph *)
+
+let exec graph const = 
+  let rec aux graph sol = 
+    match graph with
+    | [] -> Some sol
+    | h::tail -> 
+      let rec aux2 glink sol = 
+        match glink, sol with
+        | [], _ -> aux tail sol
+        | ((i,j),(ri, rj))::t,(Some sola, solb) ->
+        aux2 t (solve [(substit (ray_to_term ri) sola,substit (ray_to_term rj) sola)] sola, (List.filter (fun a -> a <> ri) (List.nth const i))@solb )
+        | (_,(None,_)) -> None
+        in aux2 h sol
+  in aux graph (Some [],[]) ;;
+
+  (* Exec where it just keeps the last equation and re-tries to solve it as a whole instead of applying the solution of the previous equation *)
+
+  let exec2 graph const = 
+    let rec aux graph sol = 
+      match graph with
+      | [] -> Some sol
+      | h::tail -> 
+        let rec aux2 glink sol = 
+          match glink, sol with
+          | [], _ -> aux tail sol
+          | ((i,j),(ri, rj))::t,(Some sola, solb) ->
+          aux2 t (let eq = ((ray_to_term ri),(ray_to_term rj))::sola in 
+            if (solve eq []) = None then 
+              failwith "marchpo"
+            else Some eq,
+            (List.filter (fun a -> a <> ri) (List.nth const i))@solb )
+          | (_,(None,_)) -> None
+          in aux2 h sol
+    in aux graph (Some [],[]) ;;
+  
+
+exec (dgraph constellation) constellation;;
+exec2 (dgraph constellation) constellation;;
\ No newline at end of file
diff --git a/ocaml/Unification.ml b/ocaml/Unification.ml
index ab6e1bd..4015f84 100644
--- a/ocaml/Unification.ml
+++ b/ocaml/Unification.ml
@@ -9,22 +9,23 @@ type term = Var of id | Func of (id * term list)
 type subst = id * term list
 type equation = term * term
 
-(* Affiche un term *)
+(* convert a term to a string *)
 
-let print_term t =
-   let rec aux t =
+let rec term_to_string t =
    match t with
    | Var id -> id
    | Func(f, tl) -> f ^ "(" ^
      let rec aux2 vl =
       match vl with
       | [] -> ""
-      | h::[] -> aux h
-      | h::t -> (aux h) ^ "," ^ (aux2 t) 
+      | h::[] -> term_to_string h
+      | h::t -> (term_to_string h) ^ "," ^ (aux2 t) 
       in (aux2 tl) ^ ")"
-   in print_string (aux t)
 
-(* Fonction de comparaison entre deux termes sur l'ordre lexicographique *)
+let print_term t =
+  print_string (term_to_string t)
+
+(* Compare to terms *)
 
 let rec compare_term t1 t2 =
    match t1, t2 with
@@ -35,21 +36,21 @@ let rec compare_term t1 t2 =
    else if comp < 0 then -1 
    else List.compare compare_term fs gs
 
-(* indom regarde si une variable est dans le domaine d'une substitution *)
+(* Look if there's a var to be substituted in the term in the substitution environment *)
 
 let rec indom t sl = 
   match t with
   | Var id -> List.exists (fun (a,_) -> a = id ) sl
   | Func(_, tl) -> List.exists (fun a -> indom a sl) tl
 
-(* occurs regarde si une variable apparaît dans un term *)
+(* occurs checks if given var is in term *)
 
 let rec occurs id t =
   match t with
   | Var i -> i = id 
   | Func(_, tl) -> List.exists (fun a -> occurs id a) tl
 
-(* extends_varname ajoute un suffixe à toutes les variables *)
+(* extends_varname adds suffix to all var names of a term *)
 
 let rec extends_varname t ext =
   match t with
@@ -57,7 +58,7 @@ let rec extends_varname t ext =
   | Func(f, tl) -> Func(f, List.map (fun a -> extends_varname a ext) tl)
 
 
-(* vars renvoie la liste de toutes les variables d'un term *)
+(* vars gives a list of all vars in a term *)
 
 let rec vars t =
   match t with
@@ -68,11 +69,11 @@ let rec vars t =
       Substitution
      ======================================== *)
 
-(* apply applique une substitution à une variable *)
+(* apply applies a substitution to a var *)
 
 let apply id sub = let (_,s) = try List.find (fun (a,_) -> a = id ) sub with Not_found -> (id,Var(id)) in s
 
-(* subst applique une substitution sur un terme *)
+(* subst applies all possible substition from an environment to a term *)
 
 let rec substit trm sub =
   match trm with
@@ -83,20 +84,20 @@ let rec substit trm sub =
       Unification
      ======================================== *)
 
-(* Résout une liste d'équations *)
+(* Solves an equation list by returning solution list *)
 
 let rec solve eq sub = 
   match eq with
   | [] -> Some sub
-  | (Var(x), term)::t -> if Var(x) = term then Some (solve t sub) else Some (elim x term t sub) (* Si x = x c'est une équation inutile, on passe donc à la suite *)
-  | (term, Var(x))::t -> Some (elim x term t sub) (*Inutile de vérifier si term = Var(x) ici car c'est déjà vérifié à la ligne ci-dessus*)
-  | (Func(f, fs), Func(g, gs))::t -> if f = g then Some (solve ((List.combine fs gs)@t) sub) else None (*si f et g ne sont pas égaux, on ne peut pas résoudre l'équation*)
+  | (Var(x), term)::t -> if Var(x) = term then (solve t sub) else (elim x term t sub) (* If x = x it's a useless equation *)
+  | (term, Var(x))::t -> (elim x term t sub) (*It's useless to check if term = Var(x) because it would be the same case as above *)
+  | (Func(f, fs), Func(g, gs))::t -> if f = g then (solve ((List.combine fs gs)@t) sub) else None (* If f and g are not equal, the equation can't be solved *)
 
 and elim id term eq sub =
   if eq = [] then Some sub
-  else if occurs id term then None (* l'équation n'est pas soluble, car on aurait quelque chose de la forme x = f(x) *)
+  else if occurs id term then None (* If that's the cas, we would have something like x = f(x) which can't be solved *)
   else let sigma_xy = [(id, term)] in
-  Some (solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub)) (* On substitue toutes les occurences d'id dans le système d'équation et on ajoute cette solution au système *)
+  (solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub)) (* We apply the sigma_xy substitution and we add it to the solution list *)
 
   (* ========================================
       Tests