...

[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 abc9eae6a03aa7e7b6cc9aef17dfd0f8457dbccc..188d4dc207ff4bf8e4f47d4bf28d8407b12be214 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -547,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
+;;