X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=83c1b1dab20be45651ca6ead3406f005f173c7b9;hb=9d007f52d02d23ed95d28c7b805b65bbdc47de6a;hp=9395daa7e0998eca7c8f9bd2a3ccca8be25f164e;hpb=18e8638888e5e47d755a6c7c4bff37a1a6ec026b;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9395daa..83c1b1d 100644
--- 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);;
 
@@ -719,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);