X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=e9aa59dce7094eac40af0f8373cdd7410ecfe570;hb=b2e89f8c6a89ad675718acdf35cdd0abfafaad5a;hp=583d99eb89ca9f77777cd6a653f0cda135f61d95;hpb=4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 583d99e..e9aa59d 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -9,6 +9,13 @@ open Num 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;; @@ -28,6 +35,7 @@ type problem = 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,11 +43,10 @@ let first bound p var f = if i > bound then raise (Backtrack ("no more alternatives for " ^ string_of_var var)) else - try(try + try f p i - with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom")) with Backtrack s -> -prerr_endline ("!!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) @@ -79,7 +86,7 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = ^"(* 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 = `N (-1) then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + ^ String.concat "\n " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ (if conv = [] then "" else nl) ^ "] (* NUMERIC *) [" ^ nl ^ " " ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) @@ -151,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 *) @@ -168,7 +175,9 @@ 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_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps @@ -178,11 +187,13 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) | [] -> acc | t::todo_conv -> (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*) - let t = try - subst false false x inst (t :> nf) - with Pacman -> `N(-1) in (* DUMMY CONVERGENT *) + 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,ps,acc_new_ps) t in + let freshno,new_t,acc_new_ps = + try + expand_match (freshno,ps,acc_new_ps) t + 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 *) @@ -195,6 +206,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*) 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 @@ -444,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 -> @@ -671,103 +683,81 @@ let env_of_sigma freshno sigma = 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(); - 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 "---------------------"; - 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 "------------------"; + 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; - 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 + 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 + 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)); - assert (t = Pure.B) - | 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 *******************) @@ -780,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 @@ -792,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 @@ -807,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" +;;