moved coercion to library (work in progress)

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index 2058ba37aae5f5496de0726ba408f0359c5c2114..f3687789b4ffef162f9c341c14fae13008529b9a 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -124,7 +124,7 @@ let eq_metadata = (=)
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 2
+let magic = 3
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -135,7 +135,7 @@ type ('term,'obj) command =
       (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Coercion of loc * 'term
+  | Coercion of loc * 'term * bool (* add composites *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj

diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml
index 36b54694d4092ea450806a4cd0de459c61995716..28f42ca6d5eb4e7f1bc7a234598aa5138ca44919 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.ml
+++ b/helm/ocaml/grafite/grafiteAstPp.ml
@@ -218,7 +218,8 @@ let pp_command = function
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)
+  | Coercion (_,term, _do_composites) ->
+     sprintf "coercion %s" (pp_term_ast term)
   | Alias (_,s) -> pp_alias s
   | Obj (_,obj) -> CicNotationPp.pp_obj obj
   | Default (_,what,uris) ->
@@ -286,7 +287,8 @@ let pp_cic_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
-  | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
+  | Coercion (_,term,_add_composites) ->
+     sprintf "coercion %s" (CicPp.ppterm term)
   | Set _
   | Alias _
   | Default _

diff --git a/helm/ocaml/grafite/grafiteParser.ml b/helm/ocaml/grafite/grafiteParser.ml
index ea83367a88b804409dfa779051cac43697adb089..90198052f4f8b1bd880e175cc89e0a7d8efd1a5c 100644 (file)
--- a/helm/ocaml/grafite/grafiteParser.ml
+++ b/helm/ocaml/grafite/grafiteParser.ml
@@ -475,9 +475,9 @@ EXTEND
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
     | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true)
     | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true)
     | IDENT "alias" ; spec = alias_spec ->
         GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->

diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile
index 224a8d2ddf0a921cfd61e86806cd4fc63fdd925d..c22a61976a4f5a1a04c6235b1c45cf49d81d1b2f 100644 (file)
--- a/helm/ocaml/library/Makefile
+++ b/helm/ocaml/library/Makefile
@@ -7,8 +7,8 @@ INTERFACE_FILES = \
        libraryMisc.mli \
        libraryDb.mli \
        coercDb.mli \
-       coercGraph.mli \
        librarySync.mli \
+       coercGraph.mli \
        libraryClean.mli \
        $(NULL)
 IMPLEMENTATION_FILES = \

diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml
index d99fc6f798f67f72ccbee796adc50b8bd0db1474..77c449e0480f58f9f7044e4e3d18f92b48f0cf72 100644 (file)
--- a/helm/ocaml/library/coercGraph.ml
+++ b/helm/ocaml/library/coercGraph.ml
@@ -207,4 +207,61 @@ let close_coercion_graph src tgt uri =
   new_coercions_obj
 ;;
 
+let coercion_hashtbl = UriManager.UriHashtbl.create 3
+
+let add_coercion ~basedir ~add_composites uri =
+ let coer_ty,_ =
+  CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
+   CicUniv.empty_ugraph 
+ in
+  (* we have to get the source and the tgt type uri
+   * in Coq syntax we have already their names, but
+   * since we don't support Funclass and similar I think
+   * all the coercion should be of the form
+   * (A:?)(B:?)T1->T2
+   * So we should be able to extract them from the coercion type
+   *)
+  let extract_last_two_p ty =
+    let rec aux = function
+      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
+      | Cic.Prod( _, src, tgt) -> src, tgt
+      | _ -> assert false
+    in
+    aux ty
+  in
+  let ty_src,ty_tgt = extract_last_two_p coer_ty in
+  let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+  let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+  let new_coercions = close_coercion_graph src_uri tgt_uri uri in
+  let uris = ref [] in
+   if add_composites then
+    try
+     let lemmas =
+      List.fold_left
+       (fun lemmas (uri,o,_) ->
+         let lemmas' = LibrarySync.add_obj ~basedir uri o in
+          uris := uri :: !uris;
+          uri::lemmas'@lemmas
+       ) [] new_coercions;
+     in
+      UriManager.UriHashtbl.add coercion_hashtbl uri !uris;
+      lemmas
+    with
+     exn ->
+      List.iter LibrarySync.remove_obj !uris;
+      raise exn    
+   else
+    []
+
+let remove_coercion uri =
+ let uris =
+  try
+   let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
+    UriManager.UriHashtbl.remove coercion_hashtbl uri;
+    res
+   with
+    Not_found -> assert false
+ in
+  List.iter LibrarySync.remove_obj uris
+
 (* EOF *)

diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli
index fcbed3497313fd840b81d36000d5e3eef7d3dd6a..bd562414ee0e457c16240738ed3208c5dd03a521 100644 (file)
--- a/helm/ocaml/library/coercGraph.mli
+++ b/helm/ocaml/library/coercGraph.mli
@@ -32,8 +32,10 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
-(* also adds them to the Db *)
-val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
-    (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+(* it returns the list of composite coercions and their auxiliary lemmas  *)
+(* composite coercions are always declared as such; they are added to the *)
+(* library only on demand (i.e. not when processing a .moo)               *)
+val add_coercion:
+ basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list
 
+val remove_coercion: UriManager.uri -> unit

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index 4aa9669472aba78437c4d48852e5e61d831f3402..db5239454f06dc60e109eb524dd375a44b3e0ba6 100644 (file)
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -220,8 +220,10 @@ let add_obj uri obj ~basedir =
 let remove_obj uri =
  let uris =
   try
-   UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri
+   let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
+    UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
+    res
   with
-   Not_found -> []
+   Not_found -> assert false
  in
   List.iter remove_single_obj (uri::uris)