some bits of reduction, reusing psubst

[helm.git] / helm / software / components / ng_kernel / nCicSubstitution.ml

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 4f5e25ecce91be0764fc841ee5bf423bdea7a317..1439544b35a73a760dcc57071f5abbaac9f465e5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -61,7 +61,9 @@ let lift ?(from=1) n t =
 (*  if avoid_beta_redexes is true (default: false) no new beta redexes  *)
 (*  are generated. WARNING: the substitution can diverge when t2 is not *)
 (*  well typed and avoid_beta_redexes is true.                          *)
-let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = 
+(*  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 nargs = List.length args in
  let rec substaux k = function
     | NCic.Sort _ 
@@ -71,10 +73,12 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
        | 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) (List.nth args (n-k)) 
+        (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
          with Failure _ -> assert false))
-    | NCic.Meta (_,(m,_)) as t when m >= k + nargs - 1 -> t
-    | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
+    | 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
@@ -93,7 +97,10 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
              (match he with
              | NCic.Appl l -> NCic.Appl (l@args)
              | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
-                 avoid (psubst ~avoid_beta_redexes true 0 [arg] bo) tl
+                 (* 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
@@ -105,7 +112,8 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
   substaux 1
 ;;
 
-let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];;
+let subst ?avoid_beta_redexes arg = 
+  psubst ?avoid_beta_redexes true 0 (fun x -> x)[arg];;
 
 (* subst_meta (n, Some [t_1 ; ... ; t_n]) t                                  *)
 (*  returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
@@ -114,5 +122,5 @@ let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];;
 let subst_meta = function 
   | m, NCic.Irl _ 
   | m, NCic.Ctx [] -> lift m 
-  | m, NCic.Ctx l  -> psubst false m l 
+  | m, NCic.Ctx l  -> psubst false m (fun x -> x) l 
 ;;