From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 14:43:50 +0000 (+0000) Subject: moved coercion to library (work in progress) X-Git-Tag: make_still_working~8060 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=785d58938cfe252fc078a2ca7d4c7d8bfc83cdc8;p=helm.git moved coercion to library (work in progress) --- diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index 2058ba37a..f3687789b 100644 --- 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 36b54694d..28f42ca6d 100644 --- 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 ea83367a8..90198052f 100644 --- 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 224a8d2dd..c22a61976 100644 --- 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 d99fc6f79..77c449e04 100644 --- 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 fcbed3497..bd562414e 100644 --- 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 4aa966947..db5239454 100644 --- 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)