BIG FAT COMMIT REGARDING COERCIONS:

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 9e524b377fc68e2cb300d2efb13b871b74551894..2de83bc4078b569613b2b922fc9dc0e791ba75a2 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -414,8 +414,8 @@ type 'a eval_executable =
 type 'a eval_from_moo =
  { efm_go: GT.status -> string -> GT.status }
       
-let coercion_moo_statement_of uri =
-  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let coercion_moo_statement_of arity uri =
+  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
 
 let refinement_toolkit = {
   RefinementTool.type_of_aux' = 
@@ -440,11 +440,12 @@ let refinement_toolkit = {
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
   
-let eval_coercion status ~add_composites uri =
+let eval_coercion status ~add_composites uri arity =
  let status,compounds =
-  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
+  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity 
+ in
  let moo_content = 
-   List.map coercion_moo_statement_of (uri::compounds)
+   List.map (coercion_moo_statement_of arity) (uri::compounds)
  in
  let status = GT.add_moo_content moo_content status in
   {status with GT.proof_status = GT.No_proof},
@@ -551,7 +552,11 @@ let add_coercions_of_record_to_moo obj lemmas status =
           let obj,_ = 
             CicEnvironment.get_cooked_obj  CicUniv.empty_ugraph uri in
           let attrs = CicUtil.attributes_of_obj obj in
-          List.mem (`Class `Coercion) attrs
+          try 
+            match List.find 
+             (function `Class (`Coercion _) -> true | _-> false) attrs
+            with `Class (`Coercion n) -> true,n | _ -> assert false
+          with Not_found -> false,0            
         with Not_found -> assert false
       in
       (* looking at the fields we can know the 'wanted' coercions, but not the 
@@ -561,9 +566,9 @@ let add_coercions_of_record_to_moo obj lemmas status =
       let wanted_coercions = 
         HExtlib.filter_map 
           (function 
-            | (name,true) -> 
+            | (name,true,arity) -> 
                Some 
-                 (UriManager.uri_of_string 
+                 (arity, UriManager.uri_of_string 
                    (GT.qualify status name ^ ".con"))
             | _ -> None) 
           fields
@@ -576,13 +581,22 @@ let add_coercions_of_record_to_moo obj lemmas status =
         List.split
           (HExtlib.filter_map 
             (fun uri ->
-              let is_a_wanted_coercion = 
-                List.exists (UriManager.eq uri) wanted_coercions 
+              let is_a_wanted_coercion,arity_wanted = 
+                try
+                  let arity,_ = 
+                    List.find (fun (n,u) -> UriManager.eq u uri) 
+                      wanted_coercions
+                  in
+                  true, arity
+                with Not_found -> false, 0
               in
-              if is_a_coercion uri || is_a_wanted_coercion then
-                Some (uri, coercion_moo_statement_of uri)
+              let is_a_coercion, arity_coercion = is_a_coercion uri in
+              if is_a_coercion then
+                Some (uri, coercion_moo_statement_of arity_coercion uri)
+              else if is_a_wanted_coercion then
+                Some (uri, coercion_moo_statement_of arity_wanted uri)
               else
-                None) 
+                None)
             lemmas)
       in
       (*prerr_endline "actual coercions:";
@@ -681,8 +695,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status, lemmas = add_obj uri obj status in
        {status with GT.proof_status = GT.No_proof},
         uri::lemmas
-  | GrafiteAst.Coercion (loc, uri, add_composites) ->
-     eval_coercion status ~add_composites uri
+  | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
+     eval_coercion status ~add_composites uri arity
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with