open Pure
open Num
-let bomb = ref(`Var(-1,-666));;
+let divergent = ref(`Var(-1, -666));;
(*
The number of arguments which can applied to numbers
For Scott's encoding, two.
*)
let num_more_args = 2;;
+(* verbosity *)
let _very_verbose = false;;
+(** Display measure of every term when printing problem *)
+let _measure_of_terms = false;;
let verbose s =
if _very_verbose then prerr_endline s
let string_of_measure = string_of_int;;
let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
+ let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in
let deltas = String.concat ("\n# ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
let l = p.var_names in
String.concat "\n" ([
) else "# ";
"#";
"$" ^ p.label;
- (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
+ (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf));
]
- @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
- @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
+ @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv
+ @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps
@ [""])
;;
) xs)
;;
+(** Returns (p, showstoppers_step, showstoppers_eat) where:
+ - showstoppers_step are the heads occurring twice
+ in the same discriminating set
+ - showstoppers_eat are the heads in ps having different number
+ of arguments *)
let critical_showstoppers p =
let p = super_simplify p in
let hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
| Some div ->
if List.mem (hd_of_i_var div) inedible
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
- 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
+ else (divergent := `Var(hd_of_i_var div, -666); {p with div=None}) in
+ let dangerous_conv = showstoppers_conv in
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 p.var_names) l))) dangerous_conv;
let conv =
`Continue p
let instantiate p x 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");
(if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable");
List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
| `N _
| `Var _ -> 0
- ) in Listx.max (Listx.map (aux 0) tms)
+ ) in
+ let rec aux' top t = match t with
+ | `Lam(_,t) -> aux' false t
+ | `I((_,ar), tms) -> max ar
+ (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
+ | `Match(t, _, liftno, bs, args) ->
+ List.fold_left max 0 (List.map (aux' false) ((t :> nf)::(args :> nf list)@List.map snd !bs))
+ | `N _
+ | `Var _ -> 0 in
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
;;
let auto_instantiate (n,p) =
| x::_, _ ->
prerr_endline ("INSTANTIATING " ^ string_of_var p.var_names x);
x in
-(* Strategy that decreases the special_k to 0 first (round robin)
-1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
- let x =
- try
- match
- hd_of (List.find (fun t ->
- compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
- ) (all_terms p))
- with
- | None -> assert false
- | Some x ->
- prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var p.var_names x);
- x
- with
- 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 =
- try
- (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) (all_terms p))))) with
- None -> assert false
- | Some x ->
- prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
- x)
- with
- Not_found -> x
-in*)
let special_k =
compute_special_k (Listx.from_list (all_terms p :> nf list) )in
if special_k < n then
(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
;;
(* ************************************************************************** *)
match check p with
| Some s -> `Unseparable s
| None ->
- bomb := `Var(-1,-666);
Console.print_hline();
let p_finale = auto p p.initialSpecialK in
let freshno,sigma = p_finale.freshno, p_finale.sigma in
(string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
prerr_endline "---------<PURE>---------";
+ ToScott.bomb := !divergent;
let scott_of_nf t = ToScott.t_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, scott_of_nf inst) sigma in
- let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in
+ let e' = env_of_sigma freshno sigma' false in
+ let e'' = env_of_sigma freshno sigma' true in
prerr_endline "--------<REDUCE>---------";
- let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *)
(function
| Some div ->
print_endline (Pure.print div);
let t = Pure.mwhd (e',div,[]) in
prerr_endline ("*:: " ^ (Pure.print t));
- assert (t = pure_bomb)
+ assert (Pure.diverged t)
| None -> ()) div;
List.iter (fun n ->
verbose ("_::: " ^ (Pure.print n));
- let t = Pure.mwhd (e',n,[]) in
+ let t = Pure.mwhd (e'',n,[]) in
verbose ("_:: " ^ (Pure.print t));
- assert (t <> pure_bomb)
+ assert (not (Pure.diverged t))
) conv ;
List.iteri (fun i n ->
verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));
projects / fireball-separation.git / blobdiff