X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=d927411a1598dae8d06b599eb4a85deb520bb8e1;hb=0197354468e40860a3a104b9ea5b68854a22cfca;hp=e56a496a88cf83cc4eb8727a1f0b59274fd4a7eb;hpb=4674dd787b5141c8aa22339d497ba671f4435da5;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index e56a496..d927411 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);;
 
@@ -50,7 +53,7 @@ let measure_of_term, measure_of_terms =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
  | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
@@ -63,7 +66,7 @@ let count_fakevars p =
  let rec aux = function
  | `N _ -> 0
  | `Var(_,ar) -> if ar = min_int then 1 else 0
- | `Lam(_,t) -> aux t
+ | `Lam(_,t,g) -> assert (g = []); aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
  | `Match(u,v,_,_,args) -> aux (u :> nf) + aux (`Var v) + aux_many args
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
@@ -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
   @ [""])
 ;;
 
@@ -116,7 +120,7 @@ let make_fresh_vars p arities =
 let simple_expand_match ps =
  let rec aux level = function
   | #i_num_var as t -> (aux_i_num_var level t :> nf)
-  | `Lam(b,t) -> `Lam(b,aux (level+1) t)
+  | `Lam(b,t,g) -> assert (g = []); `Lam(b,aux (level+1) t,[])
  and aux_i_num_var level = function
   | `Match(u,v,bs_lift,bs,args) as torig ->
     let (u : i_num_var) = aux_i_num_var level u in
@@ -365,6 +369,11 @@ let precompute_edible_data {ps; div} xs =
    ) 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
@@ -404,11 +413,11 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv = edible p arities showstoppers in
-  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
+  let inedible, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
   let p =
   List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N(pos) in
+   let v = `N pos in
    let inst = make_lams v nargs in
 prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
    { p with sigma = p.sigma @ [hd,inst] }
@@ -425,31 +434,18 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
  let p = match p.div with
   | None -> p
   | Some div ->
-   if List.mem (hd_of_i_var div) showstoppers
+   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
-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 p.var_names) l))) dangerous_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 =
    List.map (function s,t ->
     try
      if s <> [] then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
-     let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
+     let _ = List.find (fun h -> hd_of t = Some h) inedible in
       t)
     with Not_found -> match hd_of t with
      | None -> assert (t = convergent_dummy); t
@@ -477,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");
@@ -492,20 +486,29 @@ let instantiate p x n =
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
  (* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[])) in
+ let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,-666),1,bs,[]),[]) in
  let p = {p with deltas=bs::p.deltas} in
  subst_in_problem x inst p
 ;;
 
 let compute_special_k tms =
  let rec aux k (t: nf) = Pervasives.max k (match t with
- | `Lam(b,t) -> aux (k + if b then 1 else 0) t
+ | `Lam(b,t,g) -> assert (g = []); aux (k + if b then 1 else 0) t
  | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
  | `Match(t, _, liftno, bs, args) ->
      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,g) -> assert (g = []); 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) =
@@ -532,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
@@ -642,7 +615,7 @@ let optimize_numerals p =
     | `N n -> `N (List.nth perm n)
     | `I _ -> assert false
     | `Var _ as t -> t
-    | `Lam(v,t) -> `Lam(v, aux t)
+    | `Lam(v,t,g) -> assert (g = []); `Lam(v, aux t,[])
     | `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
     in List.map (fun (n,t) -> (n,aux t))
   in
@@ -659,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 = [
@@ -704,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
@@ -718,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));
@@ -762,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);