X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=456dd5b9ec96ae9b62ee68c185067f97cfaa3d5d;hb=eeb6d213aac0f064babcb31ad6250be842d952b5;hp=21cd5cad24220009184b0e5b5e8b4e1784e372bb;hpb=2c7cb84589a53b27d30f2d3ae6333bb175d0d7d8;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 21cd5ca..456dd5b 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -6,6 +6,7 @@ open Num
 (* exceptions *)
 exception Pacman
 exception Bottom
+exception Lambda
 exception Backtrack of string
 
 (*
@@ -14,7 +15,10 @@ exception Backtrack of string
  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
@@ -58,7 +62,7 @@ let first bound p var f =
    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 p.var_names var^" i="^string_of_int i);
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
      aux (i+1)
  in
   aux 1
@@ -87,6 +91,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" ([
@@ -98,10 +103,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
   @ [""])
 ;;
 
@@ -208,7 +213,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
       let freshno,new_t,acc_new_ps =
        try
         expand_match (freshno,ps,acc_new_ps) t
-       with Pacman -> freshno,convergent_dummy,acc_new_ps
+       with Pacman | Lambda -> 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
 
@@ -257,7 +262,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
          let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
 (*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 *)
+   | `Lam _ -> raise Lambda (* assert false (* algorithm invariant/loose typing *) *)
    | `Bottom -> raise Bottom
    | `Pacman -> raise Pacman
    | #i_n_var as x ->
@@ -556,7 +561,7 @@ let compute_special_k tms =
  | `Bottom
  | `Pacman
  | `Var _ -> 0 in
- Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
 
 let choose_step p =