Fix bug in dangerous_conv with arity of arguments of matches.

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9e164e6e674bed1185175c5460a69ab93da5172e..2400fb81b8c6874b297f0d663e26d18f51211a35 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -5,6 +5,13 @@ open Num
 
 let bomb = ref(`Var(-1,-666));;
 
+(*
+ The number of arguments which can applied to numbers
+ safely, depending on the encoding of numbers.
+ For Scott's encoding, two.
+*)
+let num_more_args = 2;;
+
 type problem =
  { freshno: int
  ; div: i_var option (* None = bomb *)
@@ -24,7 +31,7 @@ let all_terms p =
 let sum_arities p =
  let rec aux = function
  | `N _ -> 0
- | `Var(_,ar) -> if ar = min_int then 0 else (assert (ar >= 0); ar)
+ | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
  | `Lam(_,t) -> aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args)
  | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many args
@@ -214,7 +221,7 @@ prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst));
  let p = {p with freshno; div; conv; ps} in
  ( (* check if double substituting a variable *)
   if List.exists (fun (x',_) -> x = x') sigma
-   then failwithProblem p "Variable replaced twice"
+   then failwithProblem p ("Variable "^ string_of_var x ^"replaced twice")
  );
  let p = {p with sigma = sigma@[x,inst]} in
  let p = super_simplify p in
@@ -240,8 +247,8 @@ let rec dangerous arities showstoppers =
       (match t with
           `N _ -> List.iter (dangerous arities showstoppers) args
         | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args
-        | `Var(x,_) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *)
-        | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *)
+        | `Var(x,_) -> dangerous_inert arities showstoppers x args num_more_args
+        | `I((x,_),args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) num_more_args
       )
   | `I((k,_),args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0
 
@@ -265,8 +272,8 @@ let rec dangerous_conv arities showstoppers =
       (match t with
           `N _ -> concat_map (dangerous_conv arities showstoppers) args
         | `Match _ as t -> dangerous_conv arities showstoppers t @ concat_map (dangerous_conv arities showstoppers) args
-        | `Var(x,_) -> dangerous_inert_conv arities showstoppers x args 2 (* 2 coming from Scott's encoding *)
-        | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *)
+        | `Var(x,_) -> dangerous_inert_conv arities showstoppers x args 2
+        | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args') (List.length args + 2)
       )
   | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) 0
 
@@ -275,8 +282,9 @@ and dangerous_inert_conv arities showstoppers k args more_args =
  if List.mem k showstoppers then k :: concat_map free_vars args else
  try
   let arity = arity_of arities k in
-  prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var k ^ " listlenargs=" ^ (string_of_int (List.length args)) );
-  if List.length args + more_args > arity then k :: concat_map free_vars args else []
+prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args);
+  if more_args > 0 (* match argument*) && List.length args = arity then []
+  else if List.length args + more_args > arity then k :: concat_map free_vars args else []
  with
   Not_found -> []
 
@@ -308,8 +316,9 @@ let rec edible arities div ps conv showstoppers =
     let dangerous_conv =
      List.map (dangerous_conv 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 l))) dangerous_conv;
+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 l))) dangerous_conv;
+
     let showstoppers' = showstoppers @ List.concat dangerous_conv in
     let showstoppers' = sort_uniq (match div with
      | None -> showstoppers'
@@ -487,7 +496,8 @@ let auto_instantiate (n,p) =
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
-         [] -> assert false
+         [] ->
+         assert false
        | x::_ ->
           prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
           x)