X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=7b669ca3789880e524c6d6870d1111a64999cfba;hb=a34071ed728b8de44b198de4e73a52207557ed81;hp=821da4c331b055d084393359dcac4c9fa1a44f05;hpb=744a6d34d9a52e406d4ab9786d8ab19a2b0091d0;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 821da4c..7b669ca 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -3,14 +3,19 @@ open Util.Vars open Pure open Num -let bomb = ref(`Var(-1,-666));; - (* The number of arguments which can applied to numbers safely, depending on the encoding of numbers. For Scott's encoding, two. *) let num_more_args = 2;; +let _very_verbose = false;; + +let verbose s = + if _very_verbose then prerr_endline s +;; + +let convergent_dummy = `N(-1);; type discriminating_set = (int * nf) list;; @@ -22,10 +27,36 @@ type problem = ; sigma: (int * nf) list (* the computed substitution *) ; deltas: discriminating_set ref list (* collection of all branches *) ; initialSpecialK: int + ; label : string + ; var_names : string list (* names of the original free variables *) ; trail: discriminating_set list list };; +let label_of_problem {label} = label;; + +(* exceptions *) +exception Pacman +exception Bottom +exception Backtrack of string + +let first bound p var f = + let p = {p with trail = (List.map (!) p.deltas)::p.trail} in + let rec aux i = + if i > bound then + raise (Backtrack ("no more alternatives for " ^ string_of_var var)) + else + try + f p i + with Backtrack s -> +prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ "); + List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ; +prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i); + aux (i+1) + in + aux 1 + + let all_terms p = (match p.div with None -> [] | Some t -> [(t :> i_n_var)]) @ p.conv @@ -48,21 +79,21 @@ let string_of_measure = string_of_int;; let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); - prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||"); - let nl = "\n " in - let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in + prerr_string ("\n(* DISPLAY PROBLEM (" ^ p.label ^ " - " ^ label ^ ") "); + let nl = "\n" in + let deltas = String.concat (nl^" ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno - ^nl^"\b> DISCRIMINATING SETS (deltas)" - ^nl^deltas^(if deltas = "" then "" else nl) - ^"\b (* DIVERGENT *)" ^ nl - ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\" ") ^ nl - ^"\b (* CONVERGENT *) [" ^ nl - ^ String.concat " " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + "measure="^string_of_measure(problem_measure p) (* ^ " freshno = " ^ string_of_int freshno*) + ^ nl ^ " Discriminating sets (deltas):" + ^ nl ^ " " ^ deltas ^ (if deltas = " " then "" else nl) ^ "*)" + ^"(* DIVERGENT *)" ^ nl + ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl + ^" (* CONVERGENT *) [" ^ nl ^ " " + ^ String.concat "\n " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ (if conv = [] then "" else nl) - ^ "\b> NUMERIC" ^ nl - ^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) - ^ nl + ^ "] (* NUMERIC *) [" ^ nl ^ " " + ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) + ^ nl ^ "] [\"*\"];;" ^ nl ;; @@ -85,28 +116,28 @@ let make_fresh_vars p arities = let simple_expand_match ps = let rec aux_nob level = function - | #i_num_var as t -> aux_i_num_var level t + | #i_num_var as t -> (aux_i_num_var level t :> nf) | `Lam(b,t) -> `Lam(b,aux (level+1) t) | `Pacman as t -> t and aux level = function | `Bottom as t -> t - | #nf_nob as t -> aux_nob level t + | #nf_nob as t -> aux_nob level t and aux_i_num_var level = function | `Match(u,v,bs_lift,bs,args) as torig -> - let u = aux_i_num_var level u in + let (u : i_num_var) = aux_i_num_var level u in bs := List.map (fun (n, x) -> n, aux 0 x) !bs; (try (match u with | #i_n_var as u -> - let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *) - in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in + let i = index_of ~eq:eta_eq (lift (-level) u) (ps :> nf list) in (* can raise Not_found *) + let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in if t <> torig then - aux level (t :> nf) - else raise Not_found + aux_i_num_var level t + else raise Not_found | _ -> raise Not_found) with Not_found -> - mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args)) - | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args)) + cast_to_i_num_var (mk_appl (`Match(u,v,bs_lift,bs,[])) (List.map (aux_nob level) args))) + | `I(v,args) -> cast_to_i_num_var (mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args))) | `N _ | `Var _ as t -> t in aux_i_num_var 0 ;; @@ -116,22 +147,34 @@ let fixpoint f = ;; let rec super_simplify_ps ps = + fixpoint (List.map (fun x -> cast_to_i_n_var (simple_expand_match ps (x :> i_num_var)))) +;; + +let rec super_simplify_ps_with_match ps = fixpoint (List.map (cast_to_i_num_var ++ (simple_expand_match ps))) ;; let super_simplify ({div; ps; conv} as p) = - let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in - let conv = super_simplify_ps ps (p.conv :> i_num_var list) in + let ps = super_simplify_ps p.ps p.ps in + let conv = super_simplify_ps ps p.conv in let div = option_map (fun div -> - let divs = super_simplify_ps p.ps ([div] :> i_num_var list) in + let divs = super_simplify_ps p.ps ([div] :> i_n_var list) in List.hd divs) div in - {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv} + {p with div=option_map cast_to_i_var div; ps; conv} + +let cast_to_ps_with_match = + function + #i_num_var as y -> (y : i_num_var) + | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps") + | t -> + prerr_endline (print (t :> nf)); + assert false (* algorithm failed *) let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) = let len_ps = List.length ps in (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) - let rec aux ((freshno,acc_ps,acc_new_ps) as acc) = + let rec aux_ps ((freshno,acc_ps,acc_new_ps) as acc) = function | [] -> acc | t::todo_ps -> @@ -139,33 +182,43 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) let freshno,new_t,acc_new_ps = - expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t + try + expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t + with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom in ps") in - aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps + aux_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps (* cut&paste from aux above *) - and aux' ps ((freshno,acc_conv,acc_new_ps) as acc) = + and aux_conv ps ((freshno,acc_conv,acc_new_ps) as acc) = function | [] -> acc | t::todo_conv -> -(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = subst false false x inst (t :> nf) in + (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) + let t = subst false false x inst (t :> nf) in (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*) - let freshno,new_t,acc_new_ps = + let freshno,new_t,acc_new_ps = + try expand_match (freshno,ps,acc_new_ps) t - in - aux' ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv + with Pacman -> freshno,convergent_dummy,acc_new_ps + | Bottom -> raise (Backtrack "Bottom in conv") in + aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv (* cut&paste from aux' above *) - and aux'' ps (freshno,acc_new_ps) = + and aux_div ps (freshno,acc_new_ps) = function | None -> freshno, None, acc_new_ps | Some t -> let t = subst false false x inst (t :> nf) in - let freshno,new_t,acc_new_ps = - expand_match (freshno,ps,acc_new_ps) t - in - freshno,Some new_t,acc_new_ps + try + let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in + (* backtrack if it is a number or a variable *) + match new_t with + | `N _ -> raise (Backtrack "div=`N") + | `Var _ + | `I _ as new_t -> freshno, Some(new_t), acc_new_ps + with + | Bottom -> freshno, None, acc_new_ps + | Pacman -> raise (Backtrack "div=PAC") and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with @@ -175,12 +228,12 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) match u with | `N i -> acc_new_ps,i | _ -> - let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in - let super_simplified_ps = super_simplify_ps ps ps in + let ps = List.map (fun t -> cast_to_ps_with_match (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in + let super_simplified_ps = super_simplify_ps_with_match ps ps in (*prerr_endline ("CERCO u:" ^ print (fst u :> nf)); List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps; List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*) - match index_of_opt ~eq:eta_eq super_simplified_ps u with + match index_of_opt ~eq:eta_eq super_simplified_ps (u :> i_num_var) with Some i -> acc_new_ps, i | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps in @@ -195,16 +248,17 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*) expand_match (freshno,acc_ps,acc_new_ps) t - | `Lam _ | `Pacman -> assert false (* loose typing *) - | `Bottom -> assert false (* algorithm invariant *) + | `Lam _ -> assert false (* algorithm invariant/loose typing *) + | `Bottom -> raise Bottom + | `Pacman -> raise Pacman | #i_n_var as x -> let x = simple_expand_match (acc_ps@acc_new_ps) x in - freshno,cast_to_i_num_var x,acc_new_ps in + freshno,cast_to_i_n_var x,acc_new_ps in + + let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) ps in + let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) conv in + let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) in - let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in - let freshno,conv,new_ps = aux' old_ps (freshno,[],new_ps) (conv :> i_num_var list) in - let freshno,div,new_ps = aux'' old_ps (freshno,new_ps) (div :> i_num_var option) in - let div = option_map cast_to_i_var div in let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in let conv = List.map cast_to_i_n_var conv in (let l = Array.to_list (Array.init (freshno + 1) string_of_var) in @@ -224,7 +278,7 @@ exception Dangerous let arity_of arities k = let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in - let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | _ -> assert false in + let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in arity + if pos = -1 then - 1 else 0 ;; @@ -400,20 +454,10 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst)); then p else let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in - let p, bomb' = make_fresh_var p (-666) in - (if !bomb <> `Var (-1,-666) then - failwithProblem p - ("Bomb was duplicated! It was " ^ string_of_nf !bomb ^ - ", tried to change it to " ^ string_of_nf bomb')); - bomb := bomb'; - prerr_endline ("Just created bomb var: " ^ string_of_nf !bomb); let x = hd_of_i_var div in - let inst = make_lams !bomb n in - prerr_endline ("# INST (div): " ^ string_of_var x ^ " := " ^ string_of_nf inst); - let p = {p with div=None} in - (* subst_in_problem (hd_of_i_var div) inst p in *) - {p with sigma=p.sigma@[x,inst]} in - let dangerous_conv = showstoppers_conv in + let inst = make_lams `Bottom n in + subst_in_problem x inst p in + let dangerous_conv = showstoppers_conv in let _ = prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv)); List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))) dangerous_conv; in let conv = @@ -424,10 +468,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let _ = List.find (fun h -> hd_of t = Some h) showstoppers in t) with Not_found -> match hd_of t with - | None -> assert (t = `N ~-1); t + | None -> assert (t = convergent_dummy); t | Some h -> prerr_endline ("FREEZING " ^ string_of_var h); - `N ~-1 (* convergent dummy*) + convergent_dummy ) (List.combine showstoppers_conv p.conv) in List.iter (fun bs -> @@ -448,16 +492,19 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) else `Continue p + +let safe_arity_of_var p x = + (* Compute the minimum number of arguments when x is in head + position at p.div or p.ps *) + let aux = function + | `Var(y,_) -> if x = y then 0 else max_int + | `I((y,_),args) -> if x = y then Listx.length args else max_int + | _ -> max_int in + let tms = ((match p.div with None -> [] | Some t -> [(t :> i_n_var)]) @ p.ps) in + List.fold_left (fun acc t -> Pervasives.min acc (aux t)) max_int tms +;; + let instantiate p x perm n = - (if hd_of_i_var (cast_to_i_var !bomb) = x - then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!")); - let arity_of_x = max_arity_tms x (all_terms p) in - (if arity_of_x = None then failwithProblem p "step on var non occurring in problem"); - let arity_of_x = Util.option_get(arity_of_x) in - (if arity_of_x = min_int then failwithProblem p "step on fake variable"); - (if arity_of_x <= 0 then failwithProblem p "step on var of non-positive arity"); - (if perm < 1 || perm > arity_of_x then - failwithProblem p ("Tried to permutate variable "^ string_of_var x ^" beyond its max arity")); let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in let arities = Array.to_list (Array.make (n+1) min_int) in let p,vars = make_fresh_vars p arities in @@ -527,7 +574,10 @@ let choose_step (n,p) = prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); x with - Not_found -> x in + Not_found -> + let arity_of_x = max_arity_tms x (all_terms p) in + assert (Util.option_get arity_of_x > 0); + x in (* Instantiate in decreasing order of compute_special_k 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s let x = @@ -545,25 +595,8 @@ in*) if special_k < n then prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@"); let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in - x,arity_of_x,special_k - -exception Backtrack - -let first bound p var f = - let p = {p with trail = (List.map (!) p.deltas)::p.trail} in - let rec aux i = - if i > bound then - (prerr_endline (">>>>>>>>>>>>>>>>>> BACKTRACKING ON "^ string_of_var var ^" J="^ string_of_int i ^" <<<<<<<<<<<<<<<<<<"); - raise Backtrack) - else - try - f p i - with - Backtrack -> - List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ; - aux (i+1) - in - aux 1 + let safe_arity_of_x = safe_arity_of_var p x in + x, min arity_of_x safe_arity_of_x, special_k let rec auto_eat (n,p) = prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; @@ -658,7 +691,7 @@ let optimize_numerals p = replace_in_sigma (List.rev perm) p.sigma ;; -let env_of_sigma freshno sigma should_explode = +let env_of_sigma freshno sigma = let rec aux n = if n > freshno then [] @@ -667,154 +700,119 @@ let env_of_sigma freshno sigma should_explode = (try e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[] with - Not_found -> - if should_explode && n = hd_of_i_var (cast_to_i_var !bomb) - then ([], (let f t = Pure.A(t,t) in f (Pure.L (f (Pure.V 0)))), []) - else ([],Pure.V n,[]))::e + Not_found -> ([],Pure.V n,[]))::e in aux 0 ;; +(* ************************************************************************** *) + +type response = [ + | `CompleteSeparable of string + | `CompleteUnseparable of string + | `Uncomplete +] + +type result = [ + `Complete | `Uncomplete +] * [ + | `Separable of (int * Num.nf) list + | `Unseparable of string +] + +let run p = + Console.print_hline(); + prerr_endline (string_of_problem "main" p); + let p_finale = auto p p.initialSpecialK in + let freshno,sigma = p_finale.freshno, p_finale.sigma in + prerr_endline ("------- ------ measure=. \n "); + let l = Array.to_list (Array.init (freshno + 1) string_of_var) in + List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; -prerr_endline "########## main ##########";; - -(* Commands: - v ==> v := \a. a k1 .. kn \^m.0 - + ==> v := \^k. numero for every v such that ... - * ==> tries v as long as possible and then +v as long as possible -*) -let main problems = - let rec aux ({ps} as p) n l = - if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then begin - p - end else - let _ = prerr_endline (string_of_problem "main" p) in - let x,l = - match l with - | cmd::l -> cmd,l - | [] -> read_line (),[] in - let cmd = - if x = "+" then - `DoneWith - else if x = "*" then - `Auto - else - `Step x in - match cmd with - | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *) - | `Step x -> assert false - (* let x = var_of_string x in - aux (instantiate p x 1 n) n l *) - | `Auto -> aux (auto p n) n l - in - List.iter - (fun (p,n,cmds) -> - Console.print_hline(); - bomb := `Var (-1,-666); - let p_finale = aux p n cmds in - let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline ("------- ------\n "); - (* prerr_endline (string_of_problem "Original problem" p); *) - prerr_endline "---------------------"; - let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - prerr_endline (" BOMB == " ^ print ~l !bomb); - prerr_endline "---------------------"; - List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; -(* - prerr_endline "----------------------"; - let ps = - List.fold_left (fun ps (x,inst) -> - (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *) - (* In this non-recursive version, the intermediate states may containt Matchs *) - List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps) - (p.ps :> i_num_var list) sigma in - prerr_endline (string_of_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno}); - List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; -*) - prerr_endline "-------------------"; - let sigma = optimize_numerals p_finale in (* optimize numerals *) - let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; - prerr_endline "------------------"; - let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in - let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in - let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in - let sigma = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in - (*let ps_ok = List.fold_left (fun ps (x,inst) -> - List.map (Pure.subst false x inst) ps) ps sigma in*) - let e = env_of_sigma freshno sigma true in - let e' = env_of_sigma freshno sigma false in + prerr_endline "-------------------"; + let sigma = optimize_numerals p_finale in (* optimize numerals *) + let l = Array.to_list (Array.init (freshno + 1) string_of_var) in + List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; + + prerr_endline "------------------"; + let scott_of_nf t = ToScott.scott_of_nf (t :> nf) in + let div = option_map scott_of_nf p.div in + let conv = List.map scott_of_nf p.conv in + let ps = List.map scott_of_nf p.ps in + + let sigma' = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in + let e' = env_of_sigma freshno sigma' in + + prerr_endline "-----------------"; + (function Some div -> + print_endline (Pure.print div); + let t = Pure.mwhd (e',div,[]) in + prerr_endline ("*:: " ^ (Pure.print t)); + assert (t = Pure.B) + | None -> ()) div; + List.iter (fun n -> + verbose ("_::: " ^ (Pure.print n)); + let t = Pure.mwhd (e',n,[]) in + verbose ("_:: " ^ (Pure.print t)); + assert (t <> Pure.B) + ) conv ; + List.iteri (fun i n -> + verbose ((string_of_int i) ^ "::: " ^ (Pure.print n)); + let t = Pure.mwhd (e',n,[]) in + verbose ((string_of_int i) ^ ":: " ^ (Pure.print t)); + assert (t = Scott.mk_n i) + ) ps ; + prerr_endline "-------- --------"; + p_finale.sigma +;; -(* - prerr_endline "------------------"; -let rec print_e e = - "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]" -in - prerr_endline (print_e e); - List.iter (fun (t,t_ok) -> - prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok); - (*assert (Pure.unwind (e,t,[]) = t_ok)*) - ) (List.combine ps ps_ok); -*) - prerr_endline "-----------------"; - (function Some div -> - print_endline (Pure.print div); - let t = Pure.mwhd (e',div,[]) in - prerr_endline ("*:: " ^ (Pure.print t)); - prerr_endline (print !bomb); - assert (t = ToScott.scott_of_nf (!bomb:>nf)) - | None -> ()) div; - List.iter (fun n -> - prerr_endline ("_::: " ^ (Pure.print n)); - let t = Pure.mwhd (e,n,[]) in - prerr_endline ("_:: " ^ (Pure.print t)) - ) conv ; - List.iteri (fun i n -> - prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n)); - let t = Pure.mwhd (e,n,[]) in - prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t)); - assert (t = Scott.mk_n i) - ) ps ; - prerr_endline "-------- --------" - ) problems - -(********************** problems *******************) - -let zero = `Var(0,0);; - -let append_zero = - function - | `I _ - | `Var _ as i -> cast_to_i_n_var (mk_app i zero) - | _ -> assert false +let solve (p, todo) = + let completeness, to_run = + match todo with + | `CompleteUnseparable s -> `Complete, `False s + | `CompleteSeparable _ -> `Complete, `True + | `Uncomplete -> `Uncomplete, `True in + match to_run with + | `False s -> completeness, `Unseparable s + | `True -> + try + let sigma = run p in + completeness, `Separable sigma + with + | Backtrack _ -> completeness, `Unseparable "backtrack" ;; -type t = problem * int * string list;; - -let magic_conv ~div ~conv ~nums cmds = - let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in - let all_tms, var_names = parse' all_tms in - let div, (tms, conv) = match div with - | None -> None, list_cut (List.length nums, all_tms) - | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in - - if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv) - then ( - prerr_endline "--- TEST SKIPPED ---"; - {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0; trail=[]}, 0, [] - ) else - let tms = sort_uniq ~compare:eta_compare tms in - let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) - (* casts *) - let div = option_map cast_to_i_var div in - let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in - let tms = List.map cast_to_i_n_var tms in - - let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) - let freshno = List.length var_names in - let deltas = - let dummy = `Var (max_int / 2, -666) in - [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - let trail = [] in - {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail}, special_k, cmds +let check p = + (* TODO check if there are duplicates in p.ps + before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *) + (* FIXME what about initial fragments? *) + if (let rec f = function + | [] -> false + | hd::tl -> List.exists (eta_eq hd) tl || f tl in + f p.ps) + then `CompleteUnseparable "ps contains duplicates" + (* check if div occurs somewhere in ps@conv *) + else if (match p.div with + | None -> true + | Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv)) + ) && false (* TODO no bombs && pacmans *) + then `CompleteSeparable "no bombs, pacmans and div" + else if false (* TODO bombs or div fuori da lambda in ps@conv *) + then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" + else if p.div = None + then `CompleteSeparable "no div" + else `Uncomplete ;; -let magic strings cmds = magic_conv None [] strings cmds;; +let problem_of (label, div, conv, ps, var_names) = + (* TODO: replace div with bottom in problem??? *) + let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ ps @ conv in + if all_tms = [] then failwith "problem_of: empty problem"; + let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in + let freshno = List.length var_names in + let deltas = + let dummy = `Var (max_int / 2, -666) in + [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in + let trail = [] in + let sigma = [] in + let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK; trail; var_names; label} in + p, check p +;;