diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml index d1ae874..0ff9e9e 100644 --- a/ocaml/Resolution.ml +++ b/ocaml/Resolution.ml @@ -159,42 +159,6 @@ let constellation = make_const_add 1 3 ;; print_dgraph (dgraph constellation) ;; -(* former try -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 [],[]) ;; - - former try -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 [],[]) ;; - - -*) (* token is a couple of a family number and a star number in the constellation *) type token = int * int type process = token list @@ -220,45 +184,91 @@ 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 || 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) graph const = - let rec aux g toklist prob fstar = - match g with - | [] -> Some (toklist,prob,fstar) - | h::t -> let links = List.filter (fun ((i, _),(_, _)) -> i = n_star) h in - let rec aux2 l tokl prob2 star2 = - match l with - | [] -> Some (toklist,prob2,star2) - | ((i, j),(ri,rj))::tl -> - if Option.is_some (solve (link_to_eq (( ri, rj)::prob2)) []) then - 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 fstar else aux2 links toklist prob fstar - in aux graph [] [] [] +let divide_token (fam, n_star) toklist graph const prob fstar checked_stars = + let links = List.filter (fun ((i, _),(_, _)) -> i = n_star) graph in + let rec aux l tokl prob_aux star_aux checked_stars_aux = + match l with + [] -> 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 + 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*) + 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 + 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 *) 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) = + let graph = List.flatten (clean_dgraph (dgraph const_ext)) in + let rec aux (toklist,prob,star,checked_stars,current_fam) = begin match toklist with - | [] -> star,prob - | h::t -> aux (Option.get (divide_token h graph const_ext)) + | [] -> let gen_token = List.filter (fun ((i,_),(_,_)) -> not( List.mem i checked_stars)) 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 t graph const_ext prob star checked_stars)) end - in let ((i,_),(_,_)) = (List.hd (List.hd graph)) in let (starf, probf) = aux ([(0,i)],[],[]) in substit_star (star_postfilter starf probf) (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq probf) []))) - -(* test constellation cyclique déterministe *) + in let ((i,_),(_,_)) = (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 + +(* 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 -corriger la substitution qui ne fonctionne pas dans exec *) -(* prob : +(* 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 [] [] [] [] -let fgraph = List.flatten graph in *) \ No newline at end of file +(* 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