From 72474711d169ee0c84d57726a9a801e494941a37 Mon Sep 17 00:00:00 2001 From: Julia Date: Sun, 1 May 2022 21:45:02 +0200 Subject: [PATCH] fixed dgraph --- ocaml/Resolution.ml | 42 +++++++++++++----------------------------- ocaml/Unification.ml | 17 +++++------------ 2 files changed, 18 insertions(+), 41 deletions(-) diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml index 01b1065..e3c43d3 100644 --- a/ocaml/Resolution.ml +++ b/ocaml/Resolution.ml @@ -20,61 +20,45 @@ let guard c x = if c then return x else [] ======================================== *) (* Convert a pol and an id to a string, adding + or - before the id *) - let pol_to_string pol id = if pol = Pos then "+" ^ id else if pol = Neg then "-" ^ id else id (* Convert a ray (which is polarized) to a term *) - let rec ray_to_term r = match r with | Var id -> (Var(id) : term) | Func(id, pol, raylist) -> (Func(pol_to_string pol id, List.map ray_to_term raylist) : term) (* Invert polarization of a pol*) - let inv_pol pol = if pol = Pos then Neg else if pol = Neg then Pos else pol (* Invert the polarization of a ray to allow an easier Unification writing *) - let rec inv_pol_ray ray = match ray with | Func(id, pol, raylist) -> Func(id, inv_pol pol, List.map inv_pol_ray raylist) | _ -> ray (* Checks if a ray is polarised *) - let rec is_polarised r = match r with | Var id -> false | Func(_, p, r) -> (p <> Npol) || (List.fold_left (fun acc b -> (is_polarised b) || acc) false r) (* Checks if two rays are dual, meaning that after inverting polarization of one ray, the two rays can be unified *) - let dual_check r1 r2 = if (is_polarised r1 && is_polarised r2) then (solve [(extends_varname (ray_to_term (inv_pol_ray r1)) "0"), (extends_varname ((ray_to_term r2)) "1")] []) else None (* Create an index for a constellation *) - let index_constellation const = List.combine (List.init (List.length const) (fun a -> a)) const -(* Make a list of links between two stars using their indexes*) - -let are_linked (i, il) (j, jl) = - List.fold_left (fun link_list ray -> - List.fold_left (fun rl rs -> - let uni = dual_check ray rs in - if Option.is_some uni then ((i,j),(ray,rs))::rl else rl - ) [] jl ) [] il - (* ======================================== Constellation graph ======================================== *) @@ -83,11 +67,14 @@ let are_linked (i, il) (j, jl) = let dgraph const = let indexed_const = index_constellation const in indexed_const >>= fun (i, il) -> - indexed_const >>= fun (j, jl) -> - guard (j >= i) (are_linked (i, il) (j, jl)) + indexed_const >>= fun (j, jl) -> + il >>= fun r1 -> + jl >>= fun r2 -> + guard (j >= i) ( let uni = dual_check r1 r2 in + if Option.is_some uni then [((i,j),(r1,r2))] + else []) (* Convert a link to a string to be printable *) - let link_to_string dg = let rec aux dgl = match dgl with @@ -97,7 +84,6 @@ let link_to_string dg = in aux dg ;; (* Print a dgraph *) - let print_dgraph dg = let rec aux dgl = match dgl with @@ -127,12 +113,7 @@ 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 @@ -147,9 +128,8 @@ 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 *) - - let exec2 graph const = +(* 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 @@ -169,4 +149,8 @@ let exec graph const = exec (dgraph constellation) constellation;; -exec2 (dgraph constellation) constellation;; \ No newline at end of file +exec2 (dgraph constellation) constellation;; + +(* test constellation cyclique déterministe *) +let boucle = [ [Func("c", Neg, [x]); x] ; [Func("c", Pos, [Func("f", Npol, [y])]) ; Func("c", Npol, [x]) ] ] ;; +print_dgraph (dgraph boucle);; \ No newline at end of file diff --git a/ocaml/Unification.ml b/ocaml/Unification.ml index 4015f84..03a43da 100644 --- a/ocaml/Unification.ml +++ b/ocaml/Unification.ml @@ -10,7 +10,6 @@ type subst = id * term list type equation = term * term (* convert a term to a string *) - let rec term_to_string t = match t with | Var id -> id @@ -25,8 +24,7 @@ let rec term_to_string t = let print_term t = print_string (term_to_string t) -(* Compare to terms *) - +(* Compare two terms *) let rec compare_term t1 t2 = match t1, t2 with | Var(id1), Var(id2) -> String.compare id1 id2 @@ -37,21 +35,19 @@ let rec compare_term t1 t2 = else List.compare compare_term fs gs (* 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 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 adds suffix to all var names of a term *) +(* extends_varname adds suffix to all var names of a term *) let rec extends_varname t ext = match t with | Var id -> Var(id ^ ext) @@ -59,7 +55,6 @@ let rec extends_varname t ext = (* vars gives a list of all vars in a term *) - let rec vars t = match t with | Var id -> [id] @@ -70,11 +65,9 @@ let rec vars t = ======================================== *) (* 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 applies all possible substition from an environment to a term *) - let rec substit trm sub = match trm with | Var id -> apply id sub @@ -85,7 +78,6 @@ let rec substit trm sub = ======================================== *) (* Solves an equation list by returning solution list *) - let rec solve eq sub = match eq with | [] -> Some sub @@ -102,7 +94,7 @@ and elim id term eq sub = (* ======================================== Tests ======================================== *) - +(* let x = Var("x") let v = Var("v") let z = Var("z") @@ -140,4 +132,5 @@ let adeline = Var("Adeline") let terme3 = Func("f",[ melina ; sieg; Func("g",[Func("h",[hyetta]); adeline])]) ;; -solve [(terme,terme3)] [] ;; \ No newline at end of file +solve [(terme,terme3)] [] ;; +*) \ No newline at end of file