added support for "polymorphic" coercions

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index c55bf8d9ebecb5296304548c296d6f42a0b17426..26fc540d89224d7567081341554f75f7685cb273 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -392,11 +392,34 @@ type 'a eval_from_moo =
 let coercion_moo_statement_of uri =
   GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
 
+let refinement_toolkit = {
+  RefinementTool.type_of_aux' = 
+    (fun ?localization_tbl e c t u ->
+      let saved = !CicRefine.insert_coercions in 
+      CicRefine.insert_coercions:= false;
+      let rc = 
+        try 
+          let t, ty, metasenv, ugraph = 
+            CicRefine.type_of_aux' ?localization_tbl e c t u in
+          RefinementTool.Success (t, ty, metasenv, ugraph)
+        with
+        | CicRefine.RefineFailure s
+        | CicRefine.Uncertain s 
+        | CicRefine.AssertFailure s -> RefinementTool.Exception s
+      in
+      CicRefine.insert_coercions := saved;
+      rc);
+  RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+  RefinementTool.apply_subst = CicMetaSubst.apply_subst; 
+  RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
+  RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+  
 let eval_coercion status ~add_composites uri =
  let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
    prerr_endline "evaluating a coercion command";
-  GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+  GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
@@ -505,10 +528,11 @@ let add_coercions_of_record_to_moo obj lemmas status =
             | _ -> None) 
           fields
       in
+      (*
       prerr_endline "wanted coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        wanted_coercions;
+        wanted_coercions; *)
       let coercions, moo_content = 
         List.split
           (HExtlib.filter_map 
@@ -521,10 +545,10 @@ let add_coercions_of_record_to_moo obj lemmas status =
                 None) 
             lemmas)
       in
-      prerr_endline "actual coercions:";
+      (* prerr_endline "actual coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        coercions;
+        coercions; *)
       let status = GrafiteTypes.add_moo_content moo_content status in 
       {status with 
         GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
@@ -532,7 +556,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
 
 let add_obj uri obj status =
  let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
  status, lemmas 
       
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->