moved psubst and list to the new iterators, result not very impressing

from the #lines point of view

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 1439544b35a73a760dcc57071f5abbaac9f465e5..3d05948b1be1d5af2f659c7dddf3080e4073c069 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -1,27 +1,13 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
 
 (* $Id$ *)
 
@@ -29,6 +15,17 @@ 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 ->
@@ -47,6 +44,7 @@ let lift_from k n =
     | 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)
+   *)
  in
  liftaux k
 ;;
@@ -66,6 +64,42 @@ 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 ->
@@ -108,6 +142,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args =
     | NCic.Appl _ -> assert false
     | NCic.Match (r,outt,t,pl) ->
        NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
+   *)
  in
   substaux 1
 ;;