X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=43a2f8174a74a1cad4696523908e8a4575f6933e;hb=a5da590cb272fbe6d8e00b781ac40422ae1b816a;hp=6c5bb4a9a5b07f9eb815bcf7e3d391fb44bd2935;hpb=f4d71b463ae8510e80a40cf4df475d19fab3df2c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 6c5bb4a9a..43a2f8174 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+let ppterm = 
+  ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ -> 
+       let _ = inside_fix in assert false)
+;;
+let set_ppterm f = ppterm := f;;
+
 module C = NCic 
 module Ref = NReference
 
@@ -19,8 +25,8 @@ let debug_print = fun _ -> ();;
 let lift_from k n =
  let rec liftaux k = function
     | C.Rel m as t -> if m < k then t else C.Rel (m + n)
-    | C.Meta (i,(m,l)) as t when k <= m ->
-       if n = 0 then t else C.Meta (i,(m+n,l))
+    | C.Meta (i,(m,(C.Irl 0 as l))) when k <= m+1 -> C.Meta (i,(m,l))
+    | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
     | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
     | C.Meta (i,(m,l)) -> 
        let lctx = NCicUtils.expand_local_context l in
@@ -36,6 +42,7 @@ let lift ?(from=1) n t =
   else lift_from from n t
 ;;
 
+
 (* subst t1 t2                                                          *)
 (*  substitutes [t1] for [Rel 1] in [t2]                                *)
 (*  if avoid_beta_redexes is true (default: false) no new beta redexes  *)
@@ -53,16 +60,14 @@ let rec psubst ?(avoid_beta_redexes=false) map_arg args =
       | n when n < k -> t
       | n (* k <= n < k+nargs *) ->
        (try lift (k-1) (map_arg (List.nth args (n-k)))
-        with Failure _ -> assert false))
+        with Failure _ | Invalid_argument _ -> assert false))
    | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
        if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
-   | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m -> 
-       if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+   | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
    | C.Meta (i,(m,l)) -> 
       let lctx = NCicUtils.expand_local_context l in
-      (* 1-nargs < k-m, when <= 0 is still reasonable because we will
-       * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
-      C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+       C.Meta (i,(0, 
+         C.Ctx (HExtlib.sharing_map (fun x -> substaux k (lift m x)) lctx)))
    | C.Implicit _ -> assert false (* was identity *)
    | C.Appl (he::tl) as t ->
       (* Invariant: no Appl applied to another Appl *)
@@ -88,10 +93,10 @@ let rec psubst ?(avoid_beta_redexes=false) map_arg args =
 let subst ?avoid_beta_redexes arg = 
   psubst ?avoid_beta_redexes (fun x -> x)[arg];;
 
-(* subst_meta (n, Some [t_1 ; ... ; t_n]) t                                  *)
+(* subst_meta (n, C.Ctx [t_1 ; ... ; t_n]) t                                 *)
 (*  returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
 (*  [t_i] is lifted as usual when it crosses an abstraction                  *)
-(* subst_meta (n, Non) t -> lift n t                                         *)
+(* subst_meta (n, (C.Irl _ | C.Ctx [])) t | -> lift n t                      *)
 let subst_meta = function 
   | m, C.Irl _ 
   | m, C.Ctx [] -> lift m