1) more sharing everywhere in NCicSubstitution

2) type of iterators in nCicUtils changed to take a NCic.hypothesis when
   crossing binders

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 3d05948b1be1d5af2f659c7dddf3080e4073c069..2be7f5871704457a10683e7fd673e76e834b3fc5 100644 (file)
--- 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+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
 ;;

diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml
index 87dc48aa58fb5dc3651cfbb4cd6f101019071ea7..707ea93b6f4a501c06d7d1535c99611751e1cfb1 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.ml
+++ b/helm/software/components/ng_kernel/nCicUtils.ml
@@ -36,16 +36,17 @@ let lookup_meta index metasenv =
   with Not_found -> raise (Meta_not_found index)
 ;;
 
-let fold f g acc k = function
+let fold g k f acc = function
+ | NCic.Meta _ -> assert false
  | NCic.Implicit _
  | NCic.Sort _
  | NCic.Const _
- | NCic.Meta _
  | NCic.Rel _ -> acc
+ | NCic.Appl [] | NCic.Appl [_] -> assert false
  | NCic.Appl l -> List.fold_left (f k) acc l
- | NCic.Prod (_,s,t)
- | NCic.Lambda (_,s,t) -> f (g k) (f k acc s) t
- | NCic.LetIn (_,ty,t,bo) -> f (g k) (f k (f k acc ty) t) bo
+ | NCic.Prod (n,s,t)
+ | NCic.Lambda (n,s,t) -> f (g (n,NCic.Decl s) k) (f k acc s) t
+ | NCic.LetIn (n,ty,t,bo) -> f (g (n,NCic.Def (t,ty)) k) (f k (f k acc ty) t) bo
  | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
 ;;
 
@@ -61,21 +62,27 @@ let sharing_map f l =
   if !unchanged then l else l1
 ;;
         
-let map f g k = function
+let map g k f = function
+ | NCic.Meta _ -> assert false
  | NCic.Implicit _
  | NCic.Sort _
  | NCic.Const _
- | NCic.Meta _
  | NCic.Rel _ as t -> t
- | NCic.Appl l -> NCic.Appl (sharing_map (f k) l)
+ | NCic.Appl [] | NCic.Appl [_] -> assert false
+ | NCic.Appl l as orig ->
+    (match sharing_map (f k) l with
+      | NCic.Appl l :: tl -> NCic.Appl (l@tl)
+      | l1 when l == l1 -> orig
+      | l1 -> NCic.Appl l1)
  | NCic.Prod (n,s,t) as orig ->
-     let s1 = f k s in let t1 = f (g k) t in
+     let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
      if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
  | NCic.Lambda (n,s,t) as orig -> 
-     let s1 = f k s in let t1 = f (g k) t in
+     let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
      if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
  | NCic.LetIn (n,ty,t,b) as orig -> 
-     let ty1 = f k ty in let t1 = f k t in let b1 = f (g k) b in
+     let ty1 = f k ty in let t1 = f k t in
+     let b1 = f (g (n,NCic.Def (t,ty)) k) b in
      if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1)
  | NCic.Match (r,oty,t,pl) as orig -> 
      let oty1 = f k oty in let t1 = f k t in let pl1 = sharing_map (f k) pl in
@@ -91,7 +98,7 @@ let is_closed t =
       | NCic.Rel n when n > k -> raise NotClosed
       | NCic.Meta (_, (s, NCic.Irl n)) when not (n+s <= k) -> raise NotClosed
       | NCic.Meta (_, (s, NCic.Ctx l)) -> List.iter (aux (k+s) ()) l 
-      | _ -> fold aux ((+) 1) () k t
+      | _ -> fold (fun _ k -> k + 1) k aux () t
     in 
       aux 0 () t; true
   with NotClosed -> false

diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli
index f7bf459188649f758f1f6fc50ed08cdfc2f09648..269603c65d0aa398f6a58f3b08817a065cae237f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUtils.mli
+++ b/helm/software/components/ng_kernel/nCicUtils.mli
@@ -28,14 +28,20 @@
 exception Subst_not_found of int
 exception Meta_not_found of int
 
+val sharing_map: ('a -> 'a) -> 'a list -> 'a list
+
 val expand_local_context : NCic.lc_kind -> NCic.term list
 
 val lookup_subst: int ->  NCic.substitution -> NCic.subst_entry
 val lookup_meta: int ->  NCic.metasenv -> NCic.conjecture
 
-(* both Meta agnostic, map attempts to preserve sharing.
+(* both functions raise "assert false" when a Meta is found
  * call the 'a->'a function when a binder is crossed *)
-val fold: ('a -> 'b -> NCic.term -> 'b) -> ('a -> 'a) -> 'b -> 'a -> NCic.term -> 'b
-val map: ('a -> NCic.term -> NCic.term) -> ('a -> 'a) -> 'a -> NCic.term -> NCic.term
+val fold:
+  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
+  ('k -> 'a -> NCic.term -> 'a) -> 'a -> NCic.term -> 'a
+val map:
+ (NCic.hypothesis -> 'k -> 'k) -> 'k ->
+ ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
 
 val is_closed: NCic.term -> bool