various updates, removed proofs for now because they are the real bottleneck!!

[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 748307013f27168f25e7ba8ee4ea04064a5df3ef..a2d0a73d54bbf09ecf10da7b08a2512f9c42dbbf 100644 (file)
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -51,6 +51,10 @@ let new_meta metasenv 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 subst context =
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
@@ -58,7 +62,7 @@ let mk_implicit metasenv subst context =
     (* 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
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []);
@@ -68,7 +72,7 @@ let mk_implicit metasenv subst context =
 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
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
@@ -84,7 +88,7 @@ let n_fresh_metas metasenv subst context n =
   if n = 0 then metasenv, []
   else 
     let irl = identity_relocation_list_for_metavariable context in
-    let context = CicMetaSubst.apply_subst_context subst context 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 = 
@@ -100,7 +104,7 @@ let n_fresh_metas metasenv subst context n =
       
 let fresh_subst metasenv subst context uris = 
   let irl = identity_relocation_list_for_metavariable context in
-  let context = CicMetaSubst.apply_subst_context subst context 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
@@ -144,6 +148,7 @@ let expand_implicits metasenv subst context term =
         let (metasenv', idx) = mk_implicit metasenv subst context in
         let irl = identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)
+    | Cic.Implicit _ -> assert false
     | Cic.Cast (te, ty) ->
         let metasenv', ty' = aux metasenv context ty in
         let metasenv'', te' = aux metasenv' context te in
@@ -273,3 +278,36 @@ let expand_implicits metasenv subst context term =
   in
   aux metasenv context term
 
+let expand_implicits_in_obj metasenv subst =
+ function
+    Cic.Constant (name,bo,ty,params,attrs) ->
+     let metasenv,bo' =
+      match bo with
+         None -> metasenv,None
+       | Some bo ->
+          let metasenv,bo' = expand_implicits metasenv subst [] bo in
+           metasenv,Some bo' in
+     let metasenv,ty' = expand_implicits metasenv subst [] ty in
+      metasenv,Cic.Constant (name,bo',ty',params,attrs)
+  | Cic.CurrentProof (name,metasenv',bo,ty,params,attrs) ->
+     assert (metasenv' = []);
+     let metasenv,bo' = expand_implicits metasenv subst [] bo in
+     let metasenv,ty' = expand_implicits metasenv subst [] ty in
+      metasenv,Cic.CurrentProof (name,metasenv,bo',ty',params,attrs)
+  | Cic.InductiveDefinition (tyl,params,paramsno,attrs) ->
+     let metasenv,tyl =
+      List.fold_right
+       (fun (name,b,ty,cl) (metasenv,res) ->
+         let metasenv,ty' = expand_implicits metasenv subst [] ty in
+         let metasenv,cl' =
+          List.fold_right
+           (fun (name,ty) (metasenv,res) ->
+             let metasenv,ty' = expand_implicits metasenv subst [] ty in
+              metasenv,(name,ty')::res
+           ) cl (metasenv,[])
+         in
+          metasenv,(name,b,ty',cl')::res
+       ) tyl (metasenv,[])
+     in
+      metasenv,Cic.InductiveDefinition (tyl,params,paramsno,attrs)
+  | Cic.Variable _ -> assert false (* Not implemented *)