A new very simple example for recursive functions. Still bugged, but getting

[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 67bada94989b41a4631158f3f3abd18a190a1541..1439544b35a73a760dcc57071f5abbaac9f465e5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -61,24 +61,29 @@ 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 _ 
+    | 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) (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
         * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
        NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
-    | NCic.Sort _ as t -> t
     | 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)
@@ -92,20 +97,23 @@ 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
        avoid (substaux k he) tl
     | NCic.Appl _ -> assert false
-    | NCic.Const _ as t -> t
     | NCic.Match (r,outt,t,pl) ->
        NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
  in
   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 
 ;;