X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=43a2f8174a74a1cad4696523908e8a4575f6933e;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;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..43a2f8174 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -11,40 +11,28 @@
 
 (* $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
+
 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.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
-    | 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)) -> 
+    | C.Rel m as t -> if m < k then t else C.Rel (m + n)
+    | 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
-       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)
-   *)
+       C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
+    | C.Implicit _ -> (* was the identity *) assert false
+    | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t
  in
  liftaux k
 ;;
@@ -54,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  *)
@@ -61,101 +50,55 @@ let lift ?(from=1) n t =
 (*  well typed and avoid_beta_redexes is true.                          *)
 (*  map_arg is ReductionStrategy.from_env_for_unwind when psubst is     *)
 (*  used to implement nCicReduction.unwind'                             *)
-let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = 
+let rec psubst ?(avoid_beta_redexes=false) 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)
-   *)
+   | C.Rel n as t ->
+      (match n with
+      | n when n >= (k+nargs) ->
+         if nargs <> 0 then C.Rel (n - nargs) else t
+      | n when n < k -> t
+      | n (* k <= n < k+nargs *) ->
+       (try lift (k-1) (map_arg (List.nth args (n-k)))
+        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 (_,(m,(C.Irl l))) as t when k > l + m -> t
+   | C.Meta (i,(m,l)) -> 
+      let lctx = NCicUtils.expand_local_context l in
+       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 *)
+      let rec avoid he' = function
+        | [] -> he'
+        | arg::tl' as args->
+            (match he' with
+            | C.Appl l -> C.Appl (l@args)
+            | C.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 Obj.magic [Obj.magic arg] bo) tl'
+            | _ -> if he == he' && args == tl then t else C.Appl (he'::args))
+      in
+      let tl = HExtlib.sharing_map (substaux k) tl in
+      avoid (substaux k he) tl
+   | t -> NCicUtils.map (fun _ k -> k + 1) k substaux t
  in
   substaux 1
 ;;
 
 let subst ?avoid_beta_redexes arg = 
-  psubst ?avoid_beta_redexes true 0 (fun x -> x)[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, NCic.Irl _ 
-  | m, NCic.Ctx [] -> lift m 
-  | m, NCic.Ctx l  -> psubst false m (fun x -> x) l 
+  | m, C.Irl _ 
+  | m, C.Ctx [] -> lift m 
+  | m, C.Ctx l  -> psubst (lift m) l 
 ;;