exec almost working as intended

ocaml/Resolution.ml

@@ -6,6 +6,8 @@ open Unification
 
 type pol = Pos | Neg | Npol
 type ray = Var of id | Func of (id * pol * ray list)
+(* alternative ray definition using terms *)
+(* type ray = PR of id * pol * ray | NR of term *)
 type star = ray list
 type constellation = star list
 type graph = (int * int) * (ray * ray) list
@@ -59,6 +61,44 @@ let dual_check r1 r2 =
 let index_constellation const = 
     List.combine (List.init (List.length const) (fun a -> a)) const
 
+(* apply_ray applies a substitution to a var of a ray*)
+let apply_ray id sub = 
+  let (_,s) = try List.find (fun (a,_) -> a = id ) sub with Not_found -> (id,Var(id)) in (s :ray)
+
+(* substit_ray applies all possible substition from an environment to a ray *)
+let rec substit_ray ray sub =
+  match ray with
+  | Var id -> apply_ray id sub
+  | Func(f, p, tl) -> Func(f, p, List.map (fun a -> substit_ray a sub) tl) 
+
+(* substit_star applies all possible substition from an environment to a star *)
+let substit_star star sub =
+  List.map (fun a -> substit_ray a sub) star
+
+(* substit_const applies all possible substition from an environment to a constellation *)
+let substit_const const sub =
+  List.map (fun a -> substit_star a sub) const
+
+(* extends_varname adds suffix to all var names of a ray *)  
+let rec extends_varname_ray t ext =
+  match t with
+  | Var id -> Var(id ^ ext)
+  | Func(f, p, tl) -> Func(f, p, List.map (fun a -> extends_varname_ray a ext) tl)
+
+(* extends_varname adds suffix to all var names of a star *)
+let extends_varname_star const ext =
+  List.map (fun a -> extends_varname_ray a ext) const
+
+(* extends_varname adds suffix to all var names of a constellation based on each star number after being indexed *)
+let extends_varname_const const =
+  List.map (fun (i,a) -> extends_varname_star a (string_of_int i)) (index_constellation const)
+
+(* convert a term to a ray *)
+let rec term_to_ray (term : term) =
+  match term with
+  | Var id -> (Var(id) : ray)
+  | Func(f, r) -> Func(f, Npol, List.map (fun a -> term_to_ray a) r)
+
 (* ========================================
      Constellation graph
    ======================================== *)
@@ -119,7 +159,7 @@ let constellation = make_const_add 1 3 ;;
 
 print_dgraph (dgraph constellation) ;;
 
-(* exec graph *)
+(* former try
 let exec graph const = 
   let rec aux graph sol = 
     match graph with
@@ -134,7 +174,7 @@ let exec graph const =
         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 *)
+ former try 
 let exec2 graph const = 
     let rec aux graph sol = 
       match graph with
@@ -153,41 +193,64 @@ let exec2 graph const =
           in aux2 h sol
     in aux graph (Some [],[]) ;;
 
+
+*)
 (* token is a couple of a family number and a star number in the constellation *)
 type token = int * int
 type process = token list
 
 (* get a star using its number in the list from a constellation *)
-let get_star i const =
+let get_star const i =
   List.nth const i
 
+(* Takes a constellation, a ray and a (ray,ray) list and extracts rays from stars number i (respectively j) that are  not ri (respectively rj) when ri (respectively rj) isn't in the prob list *)
+let star_filter const ((i, j),(ri,rj)) prob =
+  let (prob_a, prob_b) = List.split prob in
+  (if List.mem ri prob_a then 
+    []
+  else (List.filter (fun a -> a <> ri) (get_star const i))
+  )@( 
+  if List.mem rj prob_b then 
+    []
+  else (List.filter (fun a -> a <> rj) (get_star const j))
+  )
+
+(* convert the (ray,ray) list part of a link to an equation, converting its rays to terms *)
+let link_to_eq prob =
+  List.map (fun (ra, rb) -> (ray_to_term (inv_pol_ray ra)), ray_to_term rb) prob
+
 (* takes a token, a graph and a constellation and returns the list of tokens to check next and a list of solvable equation *)
 let divide_token (fam, n_star) graph const =
-  let rec aux g toklist prob =
+  let rec aux g toklist prob fstar =
     match g with
-    | [] -> Some (toklist,prob)
+    | [] -> Some (toklist,prob,fstar)
     | h::t -> let links = List.filter (fun ((i, _),(_, _)) -> i = n_star) h in
-        let rec aux2 l tokl probb =
+        let rec aux2 l tokl prob2 star2 =
           match l with
-          | [] -> Some (toklist,prob)
+          | [] -> Some (toklist,prob2,star2)
           | ((i, j),(ri,rj))::tl -> 
-              if Option.is_some (solve ((ray_to_term (inv_pol_ray ri), ray_to_term rj)::probb) []) then 
+              if Option.is_some (solve (link_to_eq (( ri, rj)::prob2)) []) then 
-                aux2 tl ((fam, j)::tokl) ((ray_to_term (inv_pol_ray ri), ray_to_term rj)::probb) 
+                aux2 tl ((fam, j)::tokl) ((ri, rj)::prob2) ( ( star_filter const ((i, j),(ri,rj)) prob2 )@star2 )
               else None
-        in if links = [] then aux t toklist prob else aux2 links toklist prob
+        in if links = [] then aux t toklist prob fstar else aux2 links toklist prob fstar
-  in aux graph [] []
+  in aux graph [] [] []
 
 (* should be deterministic exec, graph shouldn't be empty *)
 let exec const =
-  let graph = clean_dgraph (dgraph const) in
+  let const_ext = extends_varname_const const in
-  let rec aux (toklist,prob) =
+  let graph = clean_dgraph (dgraph const_ext) in
+  let rec aux (toklist,prob,star) =
     begin match toklist with
-      | [] -> prob
+      | [] -> star,prob
-      | h::t -> aux (Option.get (divide_token h graph const))
+      | h::t -> aux (Option.get (divide_token h graph const_ext))
     end              
-  in let ((i,_),(_,_)) = (List.hd (List.hd graph)) in aux ([(0,i)],[])
+  in let ((i,_),(_,_)) = (List.hd (List.hd graph)) in let (starf, probf) = aux ([(0,i)],[],[]) in substit_star starf (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq probf) [])))
 
 (* test constellation cyclique déterministe *)
 let test = [ [Func("c", Neg, [x]); x] ; [Func("c", Pos, [Func("f", Npol, [y])]) ; Func("c", Npol, [x]) ] ] ;;
 print_dgraph (dgraph test);;
 exec test ;;
+
+prob :
+
+let fgraph = List.flatten graph in