X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=6d187432ae12ba7e73789d4af25719eedc6e637e;hb=d70d83df962621feeb0e674810a1b9583c7e5487;hp=f082fc23092d6aa1074e54426dbb4ad2994ac170;hpb=76735c56a213efa570fd98336aac2524ff4d36e5;p=helm.git

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index f082fc230..6d187432a 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -198,7 +198,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst) ->
@@ -274,11 +274,7 @@ let apply_subst_context subst context =
           let t' = apply_subst subst t in
           Some (n, Cic.Decl t') :: context
       | Some (n, Cic.Def (t, ty)) ->
-          let ty' =
-            match ty with
-            | None -> None
-            | Some ty -> Some (apply_subst subst ty)
-          in
+          let ty' = apply_subst subst ty in
           let t' = apply_subst subst t in
           Some (n, Cic.Def (t', ty')) :: context
       | None -> None :: context)
@@ -335,9 +331,7 @@ let ppcontext' ~metasenv ?(sep = "\n") subst context =
           (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
-          (match ty with
-              None -> "_"
-            | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context)
+          (ppterm_in_name_context ~metasenv subst ty name_context)
           (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context
        | None ->
           sprintf "%s_ :? _" (separate i), None::name_context
@@ -443,7 +437,8 @@ let rec force_does_not_occur subst to_be_restricted t =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
-    | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
+    | C.LetIn (name,so,ty,dest) ->
+       C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -515,14 +510,11 @@ let rec restrict subst to_be_restricted metasenv =
           force_does_not_occur subst to_be_restricted bo
         in
         let more_to_be_restricted, ty' =
-          match ty with
-          | None ->  more_to_be_restricted, None
-          | Some ty ->
-              let more_to_be_restricted', ty' =
-                force_does_not_occur subst to_be_restricted ty
-              in
-              more_to_be_restricted @ more_to_be_restricted',
-              Some ty'
+         let more_to_be_restricted', ty' =
+           force_does_not_occur subst to_be_restricted ty
+         in
+         more_to_be_restricted @ more_to_be_restricted',
+         ty'
         in
         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
   in
@@ -635,7 +627,14 @@ let delift n subst context metasenv l t =
 
  let module S = CicSubstitution in
   let l =
-   let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+   let (_, canonical_context, _) =
+    try
+     CicUtil.lookup_meta n metasenv
+    with CicUtil.Meta_not_found _ ->
+     raise (MetaSubstFailure (lazy
+      ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+       "declared in the metasenv")))
+    in
    List.map2 (fun ct lt ->
      match (ct, lt) with
      | None, _ -> None
@@ -653,13 +652,17 @@ let delift n subst context metasenv l t =
            (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
+                (try
+                  C.Rel ((position (m-k) l) + k)
+                 with
+                  NotInTheList ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
                 (*CSC: first order unification. Does it help or does it harm? *)
                 (*CSC: ANSWER: it hurts performances since it is possible to  *)
                 (*CSC: have an exponential explosion of the size of the proof.*)
                 (*CSC: However, without this bit of reduction some "apply" in *)
                 (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
-                deliftaux k (S.lift m t)
+                  deliftaux k (S.lift m t))
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)
              | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
@@ -708,7 +711,8 @@ let delift n subst context metasenv l t =
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
-     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+     | C.LetIn (n,s,ty,t) ->
+        C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
      | C.Const (uri,exp_named_subst) ->
         let exp_named_subst' =
@@ -849,10 +853,11 @@ let delift_rels_from subst metasenv k n =
        let s',subst,metasenv = liftaux subst metasenv k s in
        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
         C.Lambda (n,s',t'),subst,metasenv
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        let s',subst,metasenv = liftaux subst metasenv k s in
+       let ty',subst,metasenv = liftaux subst metasenv k ty in
        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
-        C.LetIn (n,s',t'),subst,metasenv
+        C.LetIn (n,s',ty',t'),subst,metasenv
     | C.Appl l ->
        let l',subst,metasenv =
         List.fold_right