1) mk_meta now returns also the index of the created meta

[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 4c44221ad0dc5e1845b039773e647ba7cb92679d..3f2f43df09d30d1449ec0ea2828be8b1276c0c0b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -342,34 +342,32 @@ let delift metasenv subst context n l t =
 ;;
 
 let mk_meta ?name metasenv context ty = 
-  match ty with
-  | `Typeless ->
-    let n = newmeta () in
-    let ty = NCic.Implicit (`Typeof n) in
-    let menv_entry = (n, (name, context, ty)) in
-    menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty
-  | `Type 
-  | `Term ->
-    let context_for_ty = if ty = `Type then [] else context in
-    let n = newmeta () in
-    let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in
-    let m = newmeta () in
-    let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in
-    let menv_entry = (m, (name, context, ty)) in
-    menv_entry :: ty_menv_entry :: metasenv, 
-      NCic.Meta (m, (0,NCic.Irl (List.length context))), ty
+  let tyof = function Some s -> Some ("typeof_"^s) | None -> None in
+  let rec mk_meta name n metasenv context = function
   | `WithType 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)), ty
+    menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
+  | `Sort ->
+    let ty = NCic.Implicit (`Typeof n) in
+    mk_meta (tyof name) n metasenv [] (`WithType ty)
+  | `Type ->
+    let metasenv, _, ty, _ = 
+      mk_meta (tyof name) (newmeta ()) metasenv context `Sort in
+    mk_meta name n metasenv context (`WithType ty)
+  | `Term ->
+    let metasenv, _, ty, _ = 
+      mk_meta (tyof name) (newmeta ()) metasenv context `Type in
+    mk_meta name n metasenv context (`WithType ty)
+  in
+    mk_meta name (newmeta ()) metasenv context ty
 ;;
 
-let saturate ?(delta=0) metasenv context ty goal_arity =
+let saturate ?(delta=0) metasenv subst context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
-   | NCic.Prod (name,s,t) ->
-       let metasenv1, arg,_ = 
+   | NCic.Prod (name,s,t) as ty ->
+       let metasenv1, _, arg,_ = 
           mk_meta ~name:name metasenv context (`WithType s) in            
        let t, metasenv1, args, pno = 
            aux metasenv1 (NCicSubstitution.subst arg t) 
@@ -379,7 +377,7 @@ let saturate ?(delta=0) metasenv context ty goal_arity =
        else
          t, metasenv1, arg::args, pno+1
    | ty ->
-        match NCicReduction.whd context ty ~delta with
+        match NCicReduction.whd ~subst context ty ~delta with
         | NCic.Prod _ as ty -> aux metasenv ty
         | ty -> ty, metasenv, [], 0
   in