X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=e9aa59dce7094eac40af0f8373cdd7410ecfe570;hb=b2e89f8c6a89ad675718acdf35cdd0abfafaad5a;hp=8f080d57ef4dbc9a8140ee3c16b50d166a73e514;hpb=8392da1be43d50073e2d51bae917dcc570431a78;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 8f080d5..e9aa59d 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;; @@ -26,7 +31,11 @@ type problem = ; trail: discriminating_set list list };; +(* exceptions *) +exception Pacman +exception Bottom exception Backtrack of string +exception Fail of string let first bound p var f = let p = {p with trail = (List.map (!) p.deltas)::p.trail} in @@ -35,10 +44,9 @@ let first bound p var f = raise (Backtrack ("no more alternatives for " ^ string_of_var var)) else try - f p i - with - Backtrack s -> -prerr_endline ("!!BACKTRACK!! " ^ s); + 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) @@ -68,21 +76,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 (" ^ 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 "\n " (List.map (fun t -> "(* _: *) " ^ (if t = `N (-1) then "PAC;" 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 + ^ "] (* NUMERIC *) [" ^ nl ^ " " ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) - ^ nl + ^ nl ^ "] [\"*\"];;" ^ nl ;; @@ -150,7 +158,7 @@ let super_simplify ({div; ps; conv} as p) = let cast_to_ps = function #i_num_var as y -> (y : i_num_var) - | `Bottom | `Pacman -> raise (Backtrack "foo") + | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps") | t -> prerr_endline (print (t :> nf)); assert false (* algorithm failed *) @@ -159,7 +167,7 @@ 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 -> @@ -167,33 +175,38 @@ 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 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(cast_to_i_var new_t),acc_new_ps + with Bottom -> freshno, None, acc_new_ps + | Pacman -> raise (Backtrack "Pacman in div") and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t = match t with @@ -224,15 +237,16 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif (*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 _ -> assert false (* algorithm invariant/loose typing *) - | `Bottom | `Pacman -> raise (Backtrack "BOT or PAC in toplevel numeric positioon") + | `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 - 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 freshno,old_ps,new_ps = aux_ps (freshno,[],[]) (ps :> i_num_var list) in + let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) (conv :> i_num_var list) in + let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) 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 @@ -428,20 +442,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 = @@ -452,10 +456,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 -> @@ -477,8 +481,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) `Continue p 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 @@ -668,7 +670,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 [] @@ -677,114 +679,85 @@ 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 ;; -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; +let solve p = + if List.for_all (function `N _ -> true | _ -> false) p.ps && p.div = None + then (prerr_endline "Initial problem is already completed, nothing to do") + else ( + Console.print_hline(); + prerr_endline (string_of_problem "main" p); + let p_finale = + try + auto p p.initialSpecialK + with Backtrack _ -> raise (Fail "Unsolvable problem, apparently") in + let freshno,sigma = p_finale.freshno, p_finale.sigma in + prerr_endline ("------- ------ measure=. \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 "---------------------"; *) + 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 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 "------------------"; + prerr_endline "------------------"; let rec print_e e = - "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) 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 (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 + 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 "-------- --------" + ) +;; (********************** problems *******************) @@ -797,9 +770,7 @@ let append_zero = | _ -> assert false ;; -type t = problem * int * string list;; - -let magic_conv ~div ~conv ~nums cmds = +let problem_of ~div ~conv ~nums = 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 @@ -809,14 +780,27 @@ let magic_conv ~div ~conv ~nums cmds = 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, [] + {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0; trail=[]} ) 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 div = + match div with + | None | Some `Bottom -> None + | Some (`I _ as t) -> Some t + | _ -> raise (Fail "div is not an inert or BOT in the initial problem") in + let conv = Util.filter_map ( + function + | #i_n_var as t -> Some t + | `Lam _ -> None + | _ -> raise (Fail "A term in conv is not i_n_var") + ) conv in + let tms = List.map ( + function + | #i_n_var as y -> y + | _ -> raise (Fail "A term in num is not 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 @@ -824,7 +808,13 @@ let magic_conv ~div ~conv ~nums cmds = 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 + {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} ;; -let magic strings cmds = magic_conv None [] strings cmds;; +let should_fail f = + try + solve (f ()); + failwith "The problem should have failed" + with Fail _ -> + prerr_endline "The problem failed, as expected" +;;