...

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index c7d66dd06b4122e6e228410dada0dcf8081e9667..188d4dc207ff4bf8e4f47d4bf28d8407b12be214 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -155,7 +155,7 @@ exception NotInTheList;;
 let position n (shift, lc) =
   match lc with
   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
-  | NCic.Irl len -> n - shift
+  | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->
       let rec aux k = function 
          | [] -> raise NotInTheList
@@ -190,7 +190,7 @@ let mk_restricted_irl shift len restrictions =
 exception Occur;;
 
 let rec force_does_not_occur metasenv subst restrictions t =
- let rec aux k (metasenv, subst as  ms) = function
+ let rec aux k ms = function
     | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
     | NCic.Meta (n, l) as orig ->
        (* we ignore the subst since restrict will take care of already
@@ -222,7 +222,7 @@ let rec force_does_not_occur metasenv subst restrictions t =
            restrict metasenv subst n restrictions_for_n 
          in
            (metasenv, subst), NCic.Meta (newmeta, l')
-    | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
+    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
  in
    aux 0 (metasenv,subst) t 
 
@@ -276,7 +276,7 @@ and restrict metasenv subst i restrictions =
         let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
         metasenv,
         subst_entry_j :: List.map 
-          (fun (n,x) as orig -> if i = n then subst_entry_i else orig) subst,
+          (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst,
         j
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
             ("Cannot restrict the context of the metavariable ?%d over "^^
@@ -298,7 +298,7 @@ and restrict metasenv subst i restrictions =
         let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
         let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
         List.map 
-          (fun (n,x) as orig -> if i = n then metasenv_entry else orig) 
+          (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
           metasenv,
         subst_entry :: subst, j
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
@@ -355,11 +355,10 @@ let delift metasenv subst context n l t =
                   in
                   (metasenv, subst), 
                   NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
-              | NCic.Irl len, NCic.Irl len1 when shift = 0 -> ms, orig
-              | NCic.Irl len, NCic.Irl len1 ->
+              | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
+              | NCic.Irl _, NCic.Irl _ ->
                    ms, NCic.Meta (i, (shift1 - shift, lc1))
               | _ -> 
-                  let to_be_restricted = ref [] in
                   let lc1 = NCicUtils.expand_local_context lc1 in
                   let rec deliftl tbr j ms = function
                     | [] -> ms, tbr, []
@@ -380,7 +379,7 @@ let delift metasenv subst context n l t =
                     let metasenv, subst, newmeta = 
                       restrict metasenv subst i to_be_r in
                     (metasenv, subst), NCic.Meta(newmeta,l1))
-    | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
+    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
    try aux 0 (metasenv,subst) t
    with NotInTheList ->
@@ -395,11 +394,13 @@ let delift metasenv subst context n l t =
         ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
         shift) (NCicUtils.expand_local_context lc))))))
       in
+      let shift, lc = l in
+      let lc = NCicUtils.expand_local_context lc in
+      let l = List.map (NCicSubstitution.lift shift) lc in
        if
          List.exists
-          (function
-              Some t -> CicUtil.is_meta_closed (apply_subst subst t)
-            | None -> true) l
+          (fun t -> NCicUntrusted.metas_of_term subst context t = [])
+            l
        then
         raise (Uncertain msg)
        else
@@ -546,3 +547,30 @@ let delift_rels subst metasenv n t =
   delift_rels_from subst metasenv 1 n t
 *) 
 
+let mk_meta ?name metasenv context ty = 
+  let n = newmeta () in
+  let len = List.length context in
+  let menv_entry = (n, (name, context, ty)) in
+  menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len))
+;;
+
+let saturate ?(delta=0) metasenv context ty goal_arity =
+ assert (goal_arity >= 0);
+  let rec aux metasenv = function
+   | NCic.Prod (name,s,t) ->
+       let metasenv1, arg = mk_meta ~name:name metasenv context s in            
+       let t, metasenv1, args, pno = 
+           aux metasenv1 (NCicSubstitution.subst arg t) 
+       in
+       if pno + 1 = goal_arity then
+         ty, metasenv, [], goal_arity+1
+       else
+         t, metasenv1, arg::args, pno+1
+   | ty ->
+        match NCicReduction.whd context ty ~delta with
+        | NCic.Prod _ as ty -> aux metasenv ty
+        | ty -> ty, metasenv, [], 0
+  in
+  let res, newmetasenv, arguments, _ = aux metasenv ty in
+  res, newmetasenv, arguments
+;;