From 8f881ad4c57f6888b2d4fb4a369f1fc8c2973418 Mon Sep 17 00:00:00 2001 From: Julia Date: Wed, 20 Apr 2022 22:56:09 +0200 Subject: [PATCH] dgraph ocaml --- ocaml/Resolution.ml | 128 +++++++++++++++++++++++++++++++++++++++++++ ocaml/Unification.ml | 74 ++++++++++--------------- 2 files changed, 156 insertions(+), 46 deletions(-) create mode 100644 ocaml/Resolution.ml diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml new file mode 100644 index 0000000..e023d4f --- /dev/null +++ b/ocaml/Resolution.ml @@ -0,0 +1,128 @@ +open Unification + +(* ======================================== + Definitions + ======================================== *) + +type pol = Pos | Neg | Npol +type ray = Var of id | Func of (id * pol * ray list) +type star = ray list +type constellation = star list +type graph = (int * int) * (ray * ray) list + +(* List monad *) +let return x = [x] (*plongement dans la monade de liste*) +let (>>=) xs k = List.flatten (List.map k xs) +let guard c x = if c then return x else [] + +(* ======================================== + Useful functions + ======================================== *) + +(* 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 + ======================================== *) + +(* Makes a dgraph from a constellation *) +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)) + +(* Convert a link to a string to be printable *) + +let link_to_string dg = + let rec aux dgl = + match dgl with + | [] -> "" + | ((i,j),(r1, r2))::[] -> ("(" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" ^ "," ^ "(" ^ term_to_string (ray_to_term r1) ^ ", " ^ term_to_string (ray_to_term r2) ^ ")") + | ((i,j),(r1, r2))::t -> ("(" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" ^ "," ^ "(" ^ term_to_string (ray_to_term r1) ^ ", " ^ term_to_string (ray_to_term r2) ^ ")") ^ "+" ^ (aux t) + in aux dg ;; + +(* Print a dgraph *) + +let print_dgraph dg = + let rec aux dgl = + match dgl with + | [] -> "" + | h::[] -> (link_to_string h) + | h::t -> (link_to_string h) ^ "\n" ^ aux t + in print_string (aux dg);; + +(* _________ Examples _________ *) +let y = Var("y") +let x = Var("x") +let z = Var("z") +let r = Var("r") +let zero = Func("0", Npol, []) +let s x = Func("s", Npol, [x]) +let add p x y z = Func("add", p, [x;y;z]) + +(* Convert int to term *) +let rec enat i = + if i = 0 then Func("0", Npol, []) else s (enat (i-1)) + +(* makes the constellation corresponding to an addition *) +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 diff --git a/ocaml/Unification.ml b/ocaml/Unification.ml index 3d29f73..ab6e1bd 100644 --- a/ocaml/Unification.ml +++ b/ocaml/Unification.ml @@ -1,8 +1,7 @@ open List (* ======================================== Definitions - ======================================== - *) + ======================================== *) type id = string type term = Var of id | Func of (id * term list) @@ -10,9 +9,7 @@ type term = Var of id | Func of (id * term list) type subst = id * term list type equation = term * term -(* -Affiche un term -*) +(* Affiche un term *) let print_term t = let rec aux t = @@ -27,9 +24,7 @@ let print_term t = in (aux2 tl) ^ ")" in print_string (aux t) -(* -Fonction de comparaison entre deux termes sur l'ordre lexicographique -*) +(* Fonction de comparaison entre deux termes sur l'ordre lexicographique *) let rec compare_term t1 t2 = match t1, t2 with @@ -40,27 +35,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 -*) +(* indom regarde si une variable est dans le domaine d'une substitution *) 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 regarde si une variable apparaît dans un 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 ajoute un suffixe à toutes les variables *) let rec extends_varname t ext = match t with @@ -68,9 +57,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 renvoie la liste de toutes les variables d'un term *) let rec vars t = match t with @@ -81,21 +68,36 @@ let rec vars t = Substitution ======================================== *) -(* -apply applique une substitution à une variable -*) +(* apply applique une substitution à une variable *) 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 applique une substitution sur un terme *) let rec substit trm sub = match trm with | Var id -> apply id sub | Func(f,tl) -> Func(f,List.map (fun a -> substit a sub) tl) + (* ======================================== + Unification + ======================================== *) + +(* Résout une liste d'équations *) + +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*) + +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 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 *) + (* ======================================== Tests ======================================== *) @@ -130,31 +132,11 @@ apply "x" subd ;; print_term terme ;; print_term (substit terme subd) ;; - (* ======================================== - Unification - ======================================== *) - -(*Résout une liste d'équations, à modifier avec option*) - -let rec solve eq sub = - match eq with - | [] -> sub - | (Var(x), term)::t -> if Var(x) = term then solve t sub else elim x term t sub - | (term, Var(x))::t -> elim x term t sub - | (Func(f, fs), Func(g, gs))::t -> if f = g then solve ((List.combine fs gs)@t) sub else [] - -and elim id term eq sub = - if eq = [] then sub - else if occurs id term then [] - else let sigma_xy = [(id, term)] in - solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub) - let melina = Var("Melina") let sieg = Var("Sieg") let hyetta = Var("Hyetta") let adeline = Var("Adeline") -let terme = Func("f",[x; v; Func("g",[z; y])]) ;; let terme3 = Func("f",[ melina ; sieg; Func("g",[Func("h",[hyetta]); adeline])]) ;; solve [(terme,terme3)] [] ;; \ No newline at end of file