renamed Http_client to Http_user_agent to avoid clashes with Gerd's

[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 0fa33047f3e2adeab1b2f931746155cb3786cd2c..b6aa1df419b5c60a9d5ace639bf865eea6ed35ab 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,63 +38,87 @@ 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 apply_subst_context = CicMetaSubst.apply_subst_context;; *)
+(* questa o la precedente sembrano essere equivalenti come tempi *)
+let apply_subst_context _ context = context ;;
 
-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
-  ([ newmeta, [], Cic.Sort Cic.Type ;
+    (* 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 = 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
-  ([ newmeta, [], Cic.Sort Cic.Type ;
+let mk_implicit_type metasenv subst context =
+  let newmeta = new_meta metasenv subst in
+  let newuniv = CicUniv.fresh () in
+  let context = 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
-  ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta)
+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 = 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, [] 
       else
         let metasenv', l = aux (newmeta + 3) (n-1) in 
-        (newmeta, context, Cic.Sort Cic.Type)::
+       (* TASSI: ?? *)
+        (newmeta, context, Cic.Sort (Cic.Type newuniv))::
         (newmeta + 1, context, Cic.Meta (newmeta, irl))::
         (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
         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 = apply_subst_context subst context in
+  let newmeta = new_meta metasenv subst in
+  let newuniv = CicUniv.fresh () in
   let rec aux newmeta = function
       [] -> metasenv, [] 
     | uri::tl ->
        let metasenv', l = aux (newmeta + 3) tl in 
-         (newmeta, context, Cic.Sort Cic.Type)::
+         (* TASSI: ?? *)
+        (newmeta, context, Cic.Sort (Cic.Type newuniv))::
          (newmeta + 1, context, Cic.Meta (newmeta, irl))::
          (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
           (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
@@ -115,14 +138,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) ->