X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=83c1b1dab20be45651ca6ead3406f005f173c7b9;hb=refs%2Fheads%2Fstrong_simple_measure;hp=dbad9e0f70bc57fdc0abaa86cd911d8ce44db57f;hpb=e5abe00727322a6c39c53e5e87ab0d22a2968a7d;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index dbad9e0..83c1b1d 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -3,7 +3,7 @@ open Util.Vars
 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
@@ -11,7 +11,10 @@ let bomb = ref(`Var(-1,-666));;
  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
@@ -36,7 +39,7 @@ let label_of_problem {label} = label;;
 let string_of_var l x =
  try
   List.nth l x
- with Failure "nth" -> "`" ^ string_of_int x
+ with Failure _ -> "`" ^ string_of_int x
 ;;
 let string_of_term p t = print ~l:p.var_names (t :> nf);;
 
@@ -77,6 +80,7 @@ let problem_measure p = sum_arities p;;
 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" ([
@@ -88,10 +92,10 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
    ) 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
   @ [""])
 ;;
 
@@ -336,22 +340,22 @@ let rec edible ({div; conv; ps} as p) arities showstoppers =
            aux showstoppers xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps in
-
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
-  List.map (dangerous_conv p arities showstoppers) (conv :> nf list) in
+            aux (sort_uniq (h::showstoppers)) ps
+  in
+    let showstoppers = sort_uniq (aux showstoppers ps) in
+    let dangerous_conv =
+     List.map (dangerous_conv p arities showstoppers) (conv :> nf list) 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 showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
-  | None -> showstoppers'
-  | Some div ->
-    if List.exists ((=) (hd_of_i_var div)) showstoppers'
-    then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+    let showstoppers' = showstoppers @ List.concat dangerous_conv in
+    let showstoppers' = sort_uniq (match div with
+     | None -> showstoppers'
+     | Some div ->
+       if List.exists ((=) (hd_of_i_var div)) showstoppers'
+       then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+    if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
 ;;
 
 let precompute_edible_data {ps; div} xs =
@@ -399,8 +403,8 @@ let critical_showstoppers p =
   let showstoppers_eat = List.filter
     (fun x -> not (List.mem x showstoppers_step))
     showstoppers_eat in
-List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+  List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+  List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
   p, showstoppers_step, showstoppers_eat
   ;;
 
@@ -432,21 +436,8 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
   | 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 =
@@ -482,8 +473,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
   `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");
@@ -510,7 +499,16 @@ let compute_special_k tms =
      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) =
@@ -537,36 +535,6 @@ 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
@@ -664,21 +632,6 @@ let optimize_numerals p =
   replace_in_sigma (List.rev perm) p.sigma
 ;;
 
-let env_of_sigma freshno sigma should_explode =
- let rec aux n =
-  if n > freshno then
-   []
-  else
-   let e = aux (n+1) in
-   (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
- in aux 0
-;;
 (* ************************************************************************** *)
 
 type result = [
@@ -709,7 +662,6 @@ let solve p =
  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
@@ -723,28 +675,28 @@ let solve p =
   (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' = Pure.env_of_sigma freshno sigma' 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
   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));
@@ -767,3 +719,14 @@ let problem_of (label, div, conv, ps, var_names) =
    [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
  {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
 ;;
+
+(* assert_depends solves the problem, and checks if the result was expected *)
+let assert_depends x =
+ let c = String.sub (label_of_problem x) 0 1 in
+ match solve x with
+ | `Unseparable s when c = "!" ->
+    failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | `Separable _  when c = "?" ->
+    failwith ("assert_depends: separable.")
+ | _ -> () in
+Problems.main (assert_depends ++ problem_of);