- delift_type_wrt_term fixed in many ways

  - as a side effect let in expty propagation works
  - as a side effect lambda_intros now works
- is_flexible (delift) improved in case: (? args) ---subst---> (\lambda .?) args

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 496648f55a90460fa8fc23a297927d258e59785e..421194abdb02b3a4431149b995e6b7493e104248 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -207,11 +207,18 @@ and restrict metasenv subst i restrictions =
 ;;
 
 let rec flexible_arg context subst = function 
-  | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> 
+  | NCic.Meta (i,_) ->
       (try 
         let _,_,t,_ = List.assoc i subst in
         flexible_arg context subst t
       with Not_found -> true)
+  | NCic.Appl (NCic.Meta (i,_) :: args)-> 
+      (try 
+        let _,_,t,_ = List.assoc i subst in
+        flexible_arg context subst 
+          (NCicReduction.head_beta_reduce ~delta:max_int 
+            (NCic.Appl (t :: args)))
+      with Not_found -> true)
    (* this is a cheap whd, it only performs zeta-reduction.
     * 
     * it works when the **omissis** disambiguation algorithm

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 58036784f634e8e8427f3c86d4987ac0fce35d0b..f46487aabda862068115d907c62809c7701f4db0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -242,7 +242,7 @@ let rec typeof rdb
          | Some x -> 
              let m, s, x = 
                NCicUnification.delift_type_wrt_terms 
-                 rdb metasenv subst context x [t]
+               rdb metasenv subst context x [t]
              in
                m, s, Some x
        in

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 5669b1abcd9bd4d500e220ae4c1d462fc067961f..7395aa7ac7cd7679ea69f4f09ce62e4a97e3a092 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -135,10 +135,9 @@ let is_locked n subst =
    with NCicUtils.Subst_not_found _ -> false
 ;;
 
-let rec mk_irl =
- function
-    0 -> []
-  | n -> NCic.Rel n :: mk_irl (n-1)
+let rec mk_irl stop base =
+  if base > stop then []
+  else (NCic.Rel base) :: mk_irl stop (base+1) 
 ;;
 
 (* the argument must be a term in whd *)
@@ -168,15 +167,16 @@ let rec lambda_intros rdb metasenv subst context t args =
        metasenv, subst, bo
    | (arg,ty)::tail ->
        pp(lazy("arg{ " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  ":" ^
+         NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  " : " ^
          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
        let metasenv, subst, telescopic_ty = 
          if processed_args = [] then metasenv, subst, ty else
          let _ = pp(lazy("delift")) in
-         delift_type_wrt_terms rdb metasenv subst context_of_args ty 
-           (List.rev processed_args)
+         delift_type_wrt_terms rdb metasenv subst context 
+           (NCicSubstitution.lift n ty)
+           (List.map (NCicSubstitution.lift n) (List.rev processed_args))
        in
-       pp(lazy("arg}"));
+       pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
        let name = "HBeta"^string_of_int n in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
@@ -743,6 +743,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
  (*D*)  in outside true; rc with exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
+  let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
   let (metasenv, subst), t =
    try
     NCicMetaSubst.delift 
@@ -753,8 +754,7 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx (args @ 
-        List.rev (mk_irl (List.length context)))) t
+      metasenv subst context 0 (0,NCic.Ctx lc) t
    with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
   in
    metasenv, subst, t

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 13de7f4433337c21babf78856df4686091d94b4e..86f5fae1aafa86d8285d5149de8affa0c82d7a9a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -25,9 +25,13 @@ val unify :
 (* this should be moved elsewhere *)
 val fix_sorts: NCic.term -> NCic.term
 
+(* delift_type_wrt_terms st m s c t args
+ *   lift t (length args) 
+ *      [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ]
+ *)      
 val delift_type_wrt_terms:
   #NRstatus.status -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
-  NCic.term -> NCic.term list ->
+  NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term