Use of standard OCaml syntax

[helm.git] / matita / components / ng_refiner / nCicMetaSubst.ml

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index f1fa293b338e866d2042dcbbb4ee6f0ae5b32bc9..d51ce368582efc41e1084bb84e780ad4bd7d041c 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -47,10 +47,13 @@ let outside exc_opt =
 exception MetaSubstFailure of string Lazy.t
 exception Uncertain of string Lazy.t
 
-let newmeta,maxmeta = 
+let newmeta,maxmeta,pushmaxmeta,popmaxmeta = 
   let maxmeta = ref 0 in
+  let pushedmetas = ref [] in
   (fun () -> incr maxmeta; !maxmeta),
-  (fun () -> !maxmeta)
+  (fun () -> !maxmeta),
+  (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0),
+  (fun () -> match !pushedmetas with [] -> assert false | _hd::tl -> pushedmetas := tl)
 ;;
 
 exception NotFound of [`NotInTheList | `NotWellTyped];;
@@ -218,7 +221,7 @@ and restrict status metasenv subst i (restrictions as orig) =
         let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
         let new_subst = 
           subst_entry_j :: List.map 
-            (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
+            (fun ((n,_) as orig) -> if i = n then subst_entry_i else orig) subst
         in
         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         metasenv, new_subst, j, diff
@@ -247,7 +250,7 @@ and restrict status metasenv subst i (restrictions as orig) =
           pp (lazy ("BBB: dopo metasenv\n" ^  NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         List.map 
-          (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
+          (fun ((n,_) as orig) -> if i = n then metasenv_entry else orig) 
           metasenv,
         subst_entry :: subst, j, diff
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
@@ -260,18 +263,20 @@ and restrict status metasenv subst i (restrictions as orig) =
 ;;
 
 let rec is_flexible status context ~subst = function 
-  | NCic.Meta (i,_) ->
+  | NCic.Meta (i,lc) ->
+       (try 
+          let _,_,t,_ = NCicUtils.lookup_subst i subst in
+          let t = NCicSubstitution.subst_meta status lc t in
+          is_flexible status context ~subst t
+        with NCicUtils.Subst_not_found _ -> true)
+  | NCic.Appl (NCic.Meta (i,lc) :: args)-> 
       (try 
-        let _,_,t,_ = List.assoc i subst in
-        is_flexible status context ~subst t
-      with Not_found -> true)
-  | NCic.Appl (NCic.Meta (i,_) :: args)-> 
-      (try 
-        let _,_,t,_ = List.assoc i subst in
+        let _,_,t,_ = NCicUtils.lookup_subst i subst in
+        let t = NCicSubstitution.subst_meta status lc t in
         is_flexible status context ~subst 
           (NCicReduction.head_beta_reduce status ~delta:max_int 
             (NCic.Appl (t :: args)))
-      with Not_found -> true)
+      with NCicUtils.Subst_not_found _ -> true)
    (* this is a cheap whd, it only performs zeta-reduction.
     * 
     * it works when the **omissis** disambiguation algorithm
@@ -385,7 +390,7 @@ let delift status ~unify metasenv subst context n l t =
              if not clear then ms
              else 
                metasenv, 
-               (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
+               (i,([],c,t,ty)) :: List.filter (fun (j,_) -> i <> j) subst
            in
            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
          with NCicUtils.Subst_not_found _ ->
@@ -513,10 +518,14 @@ let delift status ~unify metasenv subst context n l t =
         NCicUtils.Meta_not_found _ ->
          (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
          assert (n = -1); res
+      | NCicTypeChecker.TypeCheckerFailure msg ->
+         HLog.error "----------- Problem with Dependent Types ----------";
+         HLog.error (Lazy.force msg) ;
+         HLog.error "---------------------------------------------------";
+         raise (NotFound `NotWellTyped)
       | TypeNotGood
       | NCicTypeChecker.AssertFailure _
-      | NCicReduction.AssertFailure _
-      | NCicTypeChecker.TypeCheckerFailure _ ->
+      | NCicReduction.AssertFailure _ ->
          raise (NotFound `NotWellTyped))
    with NotFound reason ->
       (* This is the case where we fail even first order unification. *)
@@ -563,7 +572,7 @@ let extend_meta metasenv n =
   | NCic.Implicit (`Typeof _) -> 
       let mk_meta context kind =
         let metasenv, _, ty, _ = mk_meta metasenv context kind in
-        (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
+        (n, (attrs, cc, ty)) :: List.filter (fun (x,_) -> x <> n) metasenv, ty
       in
       (match NCicUntrusted.kind_of_meta attrs with
        | `IsSort