X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=67eb10a651553956f3798ef5800377115905434b;hb=810bbac9ad50436ada9f2f5a9b069b3f59e079ab;hp=3d05948b1be1d5af2f659c7dddf3080e4073c069;hpb=518d6cfee0f99668a84f3b6b3a7572f93b1de91b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 3d05948b1..67eb10a65 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -15,36 +15,15 @@ let debug_print = fun _ -> ();;
 
 let lift_from k n =
  let rec liftaux k = function
-    | NCic.Rel m as t ->
-       if m < k then t
-       else NCic.Rel (m + n)
-    | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l))
+    | NCic.Rel m as t -> if m < k then t else NCic.Rel (m + n)
+    | NCic.Meta (i,(m,l)) as t when k <= m ->
+       if n = 0 then t else NCic.Meta (i,(m+n,l))
     | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
     | NCic.Meta (i,(m,l)) -> 
        let lctx = NCicUtils.expand_local_context l in
-       NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx)))
+       NCic.Meta (i, (m, NCic.Ctx (NCicUtils.sharing_map (liftaux (k-m)) lctx)))
     | NCic.Implicit _ -> (* was the identity *) assert false
-    | t -> NCicUtils.map liftaux ((+) 1) k t
-   (*
-    | NCic.Const _ 
-    | NCic.Sort _ as t -> t
-    | NCic.Rel m ->
-       if m < k then NCic.Rel m
-       else NCic.Rel (m + n)
-    | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l))
-    | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
-    | NCic.Meta (i,(m,l)) -> 
-       let lctx = NCicUtils.expand_local_context l in
-       NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx)))
-    | NCic.Implicit _ -> (* was the identity *) assert false
-    | NCic.Prod (n,s,t) -> NCic.Prod (n, liftaux k s, liftaux (k+1) t)
-    | NCic.Lambda (n,s,t) -> NCic.Lambda (n, liftaux k s, liftaux (k+1) t)
-    | NCic.LetIn (n,ty,te,t) -> 
-       NCic.LetIn (n, liftaux k ty, liftaux k te, liftaux (k+1) t)
-    | NCic.Appl l -> NCic.Appl (List.map (liftaux k) l)
-    | NCic.Match (r,outty,t,pl) ->
-       NCic.Match (r,liftaux k outty,liftaux k t, List.map (liftaux k) pl)
-   *)
+    | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t
  in
  liftaux k
 ;;
@@ -64,85 +43,41 @@ let lift ?(from=1) n t =
 let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = 
  let nargs = List.length args in
  let rec substaux k = function
-    | NCic.Rel n as t ->
-       (match n with
-       | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t
-       | n when n < k -> t
-       | n (* k <= n < k+nargs *) ->
-        (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
-         with Failure _ -> assert false))
-    | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
-        if delift then NCic.Meta (i,(m-nargs,l)) else t
-    | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> 
-        if delift then NCic.Meta (i,(m-nargs,irl)) else t
-    | NCic.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 ] *)
-       NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
-    | NCic.Implicit _ -> assert false (* was identity *)
-    | NCic.Appl (he::tl) ->
-       (* Invariant: no Appl applied to another Appl *)
-       let rec avoid he = function
-         | [] -> he
-         | arg::tl as args->
-             (match he with
-             | NCic.Appl l -> NCic.Appl (l@args)
-             | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
-                 (* map_arg is here \x.x, Obj magic is needed because 
-                  * we don't have polymorphic recursion w/o records *)
-                 avoid (psubst 
-                   ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl
-             | _ as he -> NCic.Appl (he::args))
-       in
-       let tl = List.map (substaux k) tl in
-       avoid (substaux k he) tl
-    | NCic.Appl _ -> assert false
-    | t -> NCicUtils.map substaux ((+) 1) k t
-   (*
-    | NCic.Sort _ 
-    | NCic.Const _ as t -> t
-    | NCic.Rel n as t ->
-       (match n with
-       | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t
-       | n when n < k -> t
-       | n (* k <= n < k+nargs *) ->
-        (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
-         with Failure _ -> assert false))
-    | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
-        if delift then NCic.Meta (i,(m-nargs,l)) else t
-    | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> 
-        if delift then NCic.Meta (i,(m-nargs,irl)) else t
-    | NCic.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 ] *)
-       NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
-    | NCic.Implicit _ -> assert false (* was identity *)
-    | NCic.Prod (n,s,t) -> NCic.Prod (n, substaux k s, substaux (k + 1) t)
-    | NCic.Lambda (n,s,t) -> NCic.Lambda (n, substaux k s, substaux (k + 1) t)
-    | NCic.LetIn (n,ty,te,t) -> 
-       NCic.LetIn (n, substaux k ty, substaux k te, substaux (k + 1) t)
-    | NCic.Appl (he::tl) ->
-       (* Invariant: no Appl applied to another Appl *)
-       let rec avoid he = function
-         | [] -> he
-         | arg::tl as args->
-             (match he with
-             | NCic.Appl l -> NCic.Appl (l@args)
-             | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
-                 (* map_arg is here \x.x, Obj magic is needed because 
-                  * we don't have polymorphic recursion w/o records *)
-                 avoid (psubst 
-                   ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl
-             | _ as he -> NCic.Appl (he::args))
-       in
-       let tl = List.map (substaux k) tl in
-       avoid (substaux k he) tl
-    | NCic.Appl _ -> assert false
-    | NCic.Match (r,outt,t,pl) ->
-       NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
-   *)
+   | NCic.Rel n as t ->
+      (match n with
+      | n when n >= (k+nargs) ->
+         if delift && nargs <> 0 then NCic.Rel (n - nargs) else t
+      | n when n < k -> t
+      | n (* k <= n < k+nargs *) ->
+       (try lift (k-1+lift_args) (map_arg (List.nth args (n-k)))
+        with Failure _ -> assert false))
+   | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
+       if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
+   | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> 
+       if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
+   | NCic.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 ] *)
+      NCic.Meta (i,(m, NCic.Ctx (NCicUtils.sharing_map (substaux (k-m)) lctx)))
+   | NCic.Implicit _ -> assert false (* was identity *)
+   | NCic.Appl (he::tl) as t ->
+      (* Invariant: no Appl applied to another Appl *)
+      let rec avoid he' = function
+        | [] -> he'
+        | arg::tl' as args->
+            (match he' with
+            | NCic.Appl l -> NCic.Appl (l@args)
+            | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
+                (* map_arg is here \x.x, Obj magic is needed because 
+                 * we don't have polymorphic recursion w/o records *)
+                avoid (psubst 
+                  ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl'
+            | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args))
+      in
+      let tl = NCicUtils.sharing_map (substaux k) tl in
+      avoid (substaux k he) tl
+   | t -> NCicUtils.map (fun _ k -> k + 1) k substaux t
  in
   substaux 1
 ;;