diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml index dd679da..4a49b18 100644 --- a/ocaml/Resolution.ml +++ b/ocaml/Resolution.ml @@ -21,6 +21,9 @@ let guard c x = if c then return x else [] Useful functions ======================================== *) +let remove_double list = + List.fold_left (fun l a -> if not(List.mem a l) then (a::l) else l) [] list + (* 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 @@ -68,7 +71,7 @@ let apply_ray id sub = (* 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 + | 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 *) @@ -99,6 +102,25 @@ let rec term_to_ray (term : term) = | Var id -> (Var(id) : ray) | Func(f, r) -> Func(f, Npol, List.map (fun a -> term_to_ray a) r) +(* convert a star to a string*) +let rec star_to_string star = + match star with + | [] -> "" + | h::t -> term_to_string (ray_to_term h) ^ "\n" ^ (star_to_string t) + +(*print a star*) +let print_star star = + print_string (star_to_string star) + +(*convert a constellation to a string*) +let rec const_to_string const = + match const with + | [] -> "" + | h::t -> (star_to_string h) ^ "---------- \n" ^ (const_to_string t) + +(*print a constellation*) +let print_const const = + print_string (const_to_string const) (* ======================================== Constellation graph ======================================== *) @@ -123,18 +145,30 @@ let link_to_string dg = | ((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 eq_to_string eq = 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);; + | ((r1, r2))::[] -> ("(" ^ term_to_string (ray_to_term r1) ^ " = " ^ term_to_string (ray_to_term r2) ^ ")") + | ((r1, r2))::t -> ("(" ^ term_to_string (ray_to_term r1) ^ " = " ^ term_to_string (ray_to_term r2) ^ ")") ^ "\n" ^ (aux t) + in aux eq;; + + +let print_eq eq = + print_string (eq_to_string eq) let clean_dgraph g = List.filter (fun a -> a <> []) g + (* 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 (clean_dgraph dg));; + (* _________ Examples _________ *) let make_const_pol pol c = Func (c, pol, []) let make_const c = make_const_pol Npol c @@ -157,7 +191,7 @@ let make_const_add n m = let constellation = make_const_add 1 3 ;; -print_dgraph (dgraph constellation) ;; +(*print_dgraph (dgraph constellation) ;;*) (* token is a couple of a family number and a star number in the constellation *) type token = int * int @@ -184,7 +218,7 @@ let link_to_eq prob = (* removes prob rays from stars *) let star_postfilter star prob = let (prob_a, prob_b) = List.split prob in - List.filter (fun a -> not(List.mem a prob_a || List.mem a prob_b )) star + List.filter (fun a -> not(List.mem a prob_a) && not(List.mem a prob_b )) star (* 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) toklist graph const prob fstar checked_stars = @@ -194,82 +228,48 @@ let divide_token (fam, n_star) toklist graph const prob fstar checked_stars = [] -> Some (tokl,prob_aux,star_aux,checked_stars_aux,fam) | ((i, j),(ri,rj))::tl -> if fam > (List.length prob_aux) || prob_aux = [] then (* We check if the family number is the same as the number of equations lists in prob. If it's superior, we add a new list in prob instead of filling the first equation list because it means we're treating a new family *) - if Option.is_some ((solve (link_to_eq [(ri, rj)])) []) then + if Option.is_some (*((solve (link_to_eq [(ri, rj)])) [])*)(dual_check ri rj) then aux tl ((fam, j)::tokl) ([(ri, rj)]::prob_aux) ( (( star_filter const ((i, j),(ri,rj)) [] ))::star_aux ) (i::checked_stars_aux) else None else - if Option.is_some (solve (link_to_eq ((ri, rj)::(List.hd prob_aux))) []) then (* We made sure prob_aux head would not be empty*) + if Option.is_some (solve (link_to_eq ((ri, rj)::(List.nth prob_aux fam))) []) then (* We made sure prob_aux head would not be empty*) + let _ = Printf.printf "ri=%s rj=%s \n" (term_to_string (ray_to_term ri)) (term_to_string (ray_to_term rj)) in aux tl ((fam, j)::tokl) (((ri, rj)::(List.hd prob_aux))::(List.tl prob_aux)) ( (( star_filter const ((i, j),(ri,rj)) (List.hd prob_aux) )@(List.hd star_aux))::(List.tl star_aux) ) (i::checked_stars_aux) (*We use List.hd because the current family we're working on should be the current first*) - else None + else + let _ = Printf.printf "equation list= \n %s \n last added equation: \n%s = %s" (eq_to_string((ri, rj)::(List.nth prob_aux fam))) (term_to_string (ray_to_term ri)) (term_to_string (ray_to_term rj)) in + None in if links = [] then Some (toklist,prob,fstar,n_star::checked_stars,fam) else aux links toklist prob fstar checked_stars (* should be deterministic exec, graph shouldn't be empty, takes a constellation and a list of stars that are gonna be beginning points *) +(* Start_star_list, the second argument, should not be empty*) +(* checked_stars is probabbly now be useless, to be removed*) let exec const start_star_list = let const_ext = extends_varname_const const in let graph = List.flatten (clean_dgraph (dgraph const_ext)) in let max_fam = List.length start_star_list in - let rec aux (toklist,prob,star,checked_stars,current_fam) = + let rec aux (toklist,prob,star,checked_stars,current_fam) = (*toklist is a list of tokens (int of family number and the number of a star), prob is the current list of equations, current_fam is the current family number *) begin match toklist with | [] -> (*let gen_token = List.filter (fun ((i,_),(_,_)) -> not( List.mem i checked_stars)) graph in *) - if current_fam = max_fam then star,prob + if current_fam = max_fam-1 then star,prob else aux ([(current_fam+1, List.nth start_star_list (current_fam+1))], prob, star, checked_stars, current_fam+1) | h::t -> aux (Option.get (divide_token h t graph const_ext prob star checked_stars)) end - in let ((i,_),(_,_)) = (List.hd graph) + (*in let ((i,_),(_,_)) = (List.hd graph)*) + in if start_star_list = [] then + failwith "star_star_list is empty" + else + let i = List.hd start_star_list in let (constf, prob_tmp) = aux ([(0,i)],[],[],[],0) in let probf = List.rev prob_tmp + (*in let _ = Printf.printf "prob = %s \n" (eq_to_string (List.hd probf))*) in let indexed_final_const = index_constellation constf - in List.map (fun (fam_star, a) -> let fam_prob = List.nth probf fam_star - in substit_star (star_postfilter a fam_prob) (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq fam_prob) [])))) indexed_final_const + in List.map (fun (fam_star, a) -> + let fam_prob = List.nth probf fam_star + in let substit_list = (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq fam_prob) []))) + in substit_star (remove_double (star_postfilter a fam_prob)) substit_list) indexed_final_const (* test constellation non-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 ;; - -(* TODO : -faire un filtre post application, const_filter -*) - -(* not flattened graph ver. : -(* 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 fstar checked_stars = - match g with - | [] -> Some (toklist,prob,fstar,checked_stars,fam) - | h::t -> let links = List.filter (fun ((i, _),(_, _)) -> i = n_star) h in - let rec aux2 l tokl prob2 star2 checked_stars2 = - match l with - | [] -> Some (tokl,prob2,star2,checked_stars2,fam) - | ((i, j),(ri,rj))::tl -> - if fam > (List.length prob2) || prob2 = [] then (* We check if the family number is the same as the number of equations lists in prob. If it's superior, we add a new list in prob instead of filling the first equation list *) - if Option.is_some ((solve (link_to_eq [(ri, rj)])) []) then - aux2 tl ((fam, j)::tokl) ([(ri, rj)]::prob2) ( (( star_filter const ((i, j),(ri,rj)) [] ))::star2 ) (i::checked_stars2) - else None - else - if Option.is_some (solve (link_to_eq ((ri, rj)::(List.hd prob2))) []) then (* *) - aux2 tl ((fam, j)::tokl) (((ri, rj)::(List.hd prob2))::(List.tl prob2)) ( (( star_filter const ((i, j),(ri,rj)) (List.hd prob2) )@(List.hd star2))::(List.tl star2) ) (i::checked_stars2) (*We use List.hd becasue the current family we're working on should be the current first*) - else None - in if links = [] then aux t toklist prob fstar checked_stars else aux2 links toklist prob fstar checked_stars - in aux graph [] [] [] [] - -(* should be deterministic exec, graph shouldn't be empty *) -let exec const = - let const_ext = extends_varname_const const in - let graph = clean_dgraph (dgraph const_ext) in - let rec aux (toklist,prob,star,checked_stars,current_fam) = - begin match toklist with - | [] -> let gen_token = List.filter (fun ((i,_),(_,_)) -> not( List.mem i checked_stars)) (List.flatten graph) in - if gen_token = [] then star,prob - else let ((i,_),(_,_)) = (List.hd gen_token) in aux ([(current_fam+1,i)],prob,star,checked_stars,current_fam+1) - | h::t -> aux (Option.get (divide_token h graph const_ext)) - end - in let ((i,_),(_,_)) = (List.hd (List.hd graph)) - in let (constf, prob_tmp) = aux ([(0,i)],[],[],[],0) - in let probf = List.rev prob_tmp - in let indexed_final_const = index_constellation constf - in List.map (fun (fam_star, a) -> let fam_prob = List.nth probf fam_star - in substit_star (star_postfilter a fam_prob) (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq fam_prob) [])))) indexed_final_const - -*) \ No newline at end of file +(*print_dgraph (dgraph test);; +exec test ;;*) \ No newline at end of file diff --git a/ocaml/StellarCircuits.ml b/ocaml/StellarCircuits.ml index 4717ebb..4de4bac 100644 --- a/ocaml/StellarCircuits.ml +++ b/ocaml/StellarCircuits.ml @@ -1,6 +1,6 @@ -open Circuits +(*open Circuits open Resolution - +*) (* ============================================ Stellar Circuits ============================================ *) @@ -53,4 +53,9 @@ let prop_logic : constellation = [ [call_cor Pos (make_const "0") (make_const "1") (make_const "1")]; [call_cor Pos (make_const "1") (make_const "0") (make_const "1")]; [call_cor Pos (make_const "1") (make_const "1") (make_const "1")] -] \ No newline at end of file +] + +let test2 = (const_of_circuit (make_em_circ 1));; +let testprop = ((const_of_circuit (make_em_circ 1))@[[Func("or", Pos, [Func("0", Npol, []); Func("1", Npol, []); Func("1", Npol, [])])];[Func("neg",Pos, [Func("1", Npol, []); Func("0", Npol, [])])]]);; + +let extest2 = exec test2 [0];; \ No newline at end of file diff --git a/ocaml/Unification.ml b/ocaml/Unification.ml index 95a3cc3..e1877b5 100644 --- a/ocaml/Unification.ml +++ b/ocaml/Unification.ml @@ -13,12 +13,13 @@ type equation = term * term let rec term_to_string t = match t with | Var id -> id + | Func(f, []) -> f | Func(f, tl) -> f ^ "(" ^ - let rec aux2 vl = - match vl with - | [] -> "" - | h::[] -> term_to_string h - | h::t -> (term_to_string h) ^ "," ^ (aux2 t) + let rec aux2 vl = + match vl with + | [] -> "" + | h::[] -> term_to_string h + | h::t -> (term_to_string h) ^ "," ^ (aux2 t) in (aux2 tl) ^ ")" let print_term t = @@ -83,12 +84,12 @@ let rec solve eq sub = | [] -> Some sub | (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 *) + | (Func(f, fs), Func(g, gs))::t -> if f = g then (solve ((List.combine fs gs)@t) sub) else (*failwith (Printf.sprintf "f=%s g=%s" f g)*) None (* If f and g are not equal, the equation can't be solved *) and elim id term eq sub = - if occurs id term then None (* If that's the cas, we would have something like x = f(x) which can't be solved *) + if occurs id term then (*failwith (Printf.sprintf "id=%s is in term" id)*) None (* If that's the case, we would have something like x = f(x) which can't be solved *) 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)) (* We apply the sigma_xy substitution and we add it to the solution list *) + solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) ((List.map (fun (i, t) -> (i, substit t sigma_xy)) sub)@sigma_xy) (* We apply the sigma_xy substitution to the equations and the solution list and we add it to the solution list *) (* ======================================== Tests