New interesting example

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 311537a151c3409ace586ee7ef0982a2a2ed8ceb..83c1b1dab20be45651ca6ead3406f005f173c7b9 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -39,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);;
 
@@ -632,18 +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 -> ([], Pure.V n, []) ) :: e
- in aux 0
-;;
 (* ************************************************************************** *)
 
 type result = [
@@ -694,8 +682,7 @@ let solve p =
  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 in
- let e'' = env_of_sigma freshno sigma' true in
+ let e' = Pure.env_of_sigma freshno sigma' in
 
  prerr_endline "--------<REDUCE>---------";
  (function
@@ -707,7 +694,7 @@ let solve p =
    | 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 (not (Pure.diverged t))
  ) conv ;
@@ -732,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);