X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=8f080d57ef4dbc9a8140ee3c16b50d166a73e514;hb=8392da1be43d50073e2d51bae917dcc570431a78;hp=927cfe6544fb5c6f4adba3157f6cb855e850059f;hpb=e1177d88d7ff54d6cb16d711103c5c71aaccdcc6;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 927cfe6..8f080d5 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -147,6 +147,14 @@ let super_simplify ({div; ps; conv} as p) =
     List.hd divs) div in
   {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv}
 
+let cast_to_ps =
+ function
+    #i_num_var as y -> (y : i_num_var)
+  | `Bottom | `Pacman -> raise (Backtrack "foo")
+  | t ->
+    prerr_endline (print (t :> nf));
+    assert false (* algorithm failed *)
+
 let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) =
  let len_ps = List.length ps in
 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
@@ -195,7 +203,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
          match u with
          | `N i -> acc_new_ps,i
          | _ ->
-            let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
+            let ps = List.map (fun t -> cast_to_ps (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
             let super_simplified_ps = super_simplify_ps ps ps in
 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;