New handling of substitution:

[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.ml

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 41f0589453e7521bcdd091c67e5968e28f482c76..748307013f27168f25e7ba8ee4ea04064a5df3ef 100644 (file)
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -28,7 +28,6 @@
 (* where n = List.length [canonical_context]                             *)
 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
- let canonical_context_length = List.length canonical_context in
   let rec aux =
    function
       (_,[]) -> []
@@ -39,45 +38,54 @@ let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
 
 (* Returns the first meta whose number is above the *)
 (* number of the higher meta.                       *)
-let new_meta metasenv =
+let new_meta metasenv subst =
   let rec aux =
    function
-      None,[] -> 1
-    | Some n,[] -> n
-    | None,(n,_,_)::tl -> aux (Some n,tl)
-    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+      None, [] -> 1
+    | Some n, [] -> n
+    | None, n::tl -> aux (Some n,tl)
+    | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
   in
-   1 + aux (None,metasenv)
+  let indexes = 
+    (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst)
+  in
+  1 + aux (None, indexes)
 
-let mk_implicit metasenv context =
-  let newmeta = new_meta metasenv in
+let mk_implicit metasenv subst context =
+  let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
   let irl = identity_relocation_list_for_metavariable context in
+    (* in the following mk_* functions we apply substitution to canonical
+    * context since we have the invariant that the metasenv has already been
+    * instantiated with subst *)
+  let context = CicMetaSubst.apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []);
     newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
    newmeta + 2)
 
-let mk_implicit_type metasenv context =
-  let newmeta = new_meta metasenv in
+let mk_implicit_type metasenv subst context =
+  let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
+  let context = CicMetaSubst.apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
    newmeta + 1)
 
-let mk_implicit_sort metasenv =
-  let newmeta = new_meta metasenv in
+let mk_implicit_sort metasenv subst =
+  let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta)
   (* TASSI: ?? *)
 
-let n_fresh_metas metasenv context n = 
+let n_fresh_metas metasenv subst context n = 
   if n = 0 then metasenv, []
   else 
     let irl = identity_relocation_list_for_metavariable context in
-    let newmeta = new_meta metasenv in
+    let context = CicMetaSubst.apply_subst_context subst context in
+    let newmeta = new_meta metasenv subst in
     let newuniv = CicUniv.fresh () in
     let rec aux newmeta n = 
       if n = 0 then metasenv, [] 
@@ -90,9 +98,10 @@ let n_fresh_metas metasenv context n =
         Cic.Meta(newmeta+2,irl)::l in
     aux newmeta n
       
-let fresh_subst metasenv context uris = 
+let fresh_subst metasenv subst context uris = 
   let irl = identity_relocation_list_for_metavariable context in
-  let newmeta = new_meta metasenv in
+  let context = CicMetaSubst.apply_subst_context subst context in
+  let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
   let rec aux newmeta = function
       [] -> metasenv, [] 
@@ -105,7 +114,7 @@ let fresh_subst metasenv context uris =
           (uri,Cic.Meta(newmeta+2,irl))::l in
     aux newmeta uris
 
-let expand_implicits metasenv context term =
+let expand_implicits metasenv subst context term =
   let rec aux metasenv context = function
     | (Cic.Rel _) as t -> metasenv, t
     | (Cic.Sort _) as t -> metasenv, t
@@ -125,14 +134,14 @@ let expand_implicits metasenv context term =
         let metasenv', l' = do_local_context metasenv context l in
         metasenv', Cic.Meta (n, l')
     | Cic.Implicit (Some `Type) ->
-        let (metasenv', idx) = mk_implicit_type metasenv context in
+        let (metasenv', idx) = mk_implicit_type metasenv subst context in
         let irl = identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)
     | Cic.Implicit (Some `Closed) ->
-        let (metasenv', idx) = mk_implicit metasenv [] in
+        let (metasenv', idx) = mk_implicit metasenv subst [] in
         metasenv', Cic.Meta (idx, [])
     | Cic.Implicit None ->
-        let (metasenv', idx) = mk_implicit metasenv context in
+        let (metasenv', idx) = mk_implicit metasenv subst context in
         let irl = identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)
     | Cic.Cast (te, ty) ->