From f4f050696e66b8604d9f0ff8173afe03addf74d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 12 Dec 2005 14:06:26 +0000 Subject: [PATCH] fixed undo support for coercions inside records --- helm/ocaml/extlib/hExtlib.ml | 10 ++ helm/ocaml/extlib/hExtlib.mli | 1 + helm/ocaml/grafite2/grafiteEngine.ml | 79 ++++++++++- helm/ocaml/grafite2/matitaSync.ml | 32 +---- helm/ocaml/grafite2/matitaSync.mli | 4 +- helm/ocaml/library/.depend | 11 +- helm/ocaml/library/Makefile | 1 + helm/ocaml/library/cicCoercion.ml | 154 ++++++++++++++++++++++ helm/ocaml/library/cicCoercion.mli | 31 +++++ helm/ocaml/library/coercDb.ml | 7 + helm/ocaml/library/coercDb.mli | 8 +- helm/ocaml/library/coercGraph.ml | 187 +-------------------------- helm/ocaml/library/coercGraph.mli | 12 +- helm/ocaml/library/librarySync.ml | 95 +++++++++++++- helm/ocaml/library/librarySync.mli | 16 +++ 15 files changed, 409 insertions(+), 239 deletions(-) create mode 100644 helm/ocaml/library/cicCoercion.ml create mode 100644 helm/ocaml/library/cicCoercion.mli diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index a0f9d8d6c..99e6609ec 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -134,6 +134,16 @@ let list_concat ?(sep = []) = | hd :: tl -> aux ([sep; hd] @ acc) tl in aux [] + +let rec list_findopt f l = + let rec aux = function + | [] -> None + | x::tl -> + (match f x with + | None -> aux tl + | Some _ as rc -> rc) + in + aux l (** {2 File predicates} *) diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index 6416afcaf..c0538bfab 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -72,6 +72,7 @@ val list_uniq: ?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on lists *) val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*) +val list_findopt: ('a -> 'b option) -> 'a list -> 'b option (** {2 Debugging & Profiling} *) diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml index 00470b9fc..d4a16d2d6 100644 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ b/helm/ocaml/grafite2/grafiteEngine.ml @@ -369,10 +369,18 @@ type 'a eval_executable = } type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit } + +let coercion_moo_statement_of uri = + GrafiteAst.Coercion + (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) let eval_coercion status ~add_composites coercion = let uri = CicUtil.uri_of_term coercion in - let status = MatitaSync.add_coercion status ~add_composites uri in + let basedir = Helm_registry.get "matita.basedir" in + let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in + let moo_content = coercion_moo_statement_of uri in + let status = GrafiteTypes.add_moo_content [moo_content] status in + let status = MatitaSync.add_coercion status uri compounds in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} let eval_tactical ~disambiguate_tactic status tac = @@ -448,6 +456,69 @@ let eval_tactical ~disambiguate_tactic status tac = let eval_comment status c = status +(* since the record syntax allows to declare coercions, we have to put this + * information inside the moo *) +let add_coercions_of_record_to_moo obj lemmas status = + let attributes = CicUtil.attributes_of_obj obj in + let is_record = function `Class (`Record att) -> Some att | _-> None in + match HExtlib.list_findopt is_record attributes with + | None -> status + | Some fields -> + let is_a_coercion uri = + try + let obj,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + let attrs = CicUtil.attributes_of_obj obj in + List.mem (`Class `Projection) attrs + with Not_found -> assert false + in + (* looking at the fields we can know the 'wanted' coercions, but not the + * actually generated ones. So, only the intersection between the wanted + * and the actual should be in the moo as coercion, while everithing in + * lemmas should go as aliases *) + let wanted_coercions = + HExtlib.filter_map + (function + | (name,true) -> + Some + (UriManager.uri_of_string + (GrafiteTypes.qualify status name ^ ".con")) + | _ -> None) + fields + in + prerr_endline "wanted coercions:"; + List.iter + (fun u -> prerr_endline (UriManager.string_of_uri u)) + wanted_coercions; + let coercions, moo_content = + List.split + (HExtlib.filter_map + (fun uri -> + let is_a_wanted_coercion = + List.exists (UriManager.eq uri) wanted_coercions in + if is_a_coercion uri && is_a_wanted_coercion then + Some (uri, coercion_moo_statement_of uri) + else + None) + lemmas) + in + List.iter + (fun u -> prerr_endline (UriManager.string_of_uri u)) + coercions; + let status = GrafiteTypes.add_moo_content moo_content status in + List.fold_left + (fun status uri -> + MatitaSync.add_coercion status uri []) + status coercions + +let add_obj uri obj status = + let basedir = Helm_registry.get "matita.basedir" in + let lemmas = LibrarySync.add_obj uri obj basedir in + let status = + {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects} in + let status = MatitaSync.add_obj uri obj lemmas status in + status, lemmas + let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd -> let status,cmd = disambiguate_command status cmd in let cmd,notation_ids' = CicNotation.process_notation cmd in @@ -519,7 +590,8 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt "Proof not completed! metasenv is not empty!"); let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in - MatitaSync.add_obj uri obj + let status, _lemmas = add_obj uri obj status in + (* should we assert lemmas = [] ? *) {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} | GrafiteAst.Coercion (loc, coercion, add_composites) -> eval_coercion status ~add_composites coercion @@ -616,7 +688,8 @@ let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opt raise (GrafiteTypes.Command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv)); - MatitaSync.add_obj uri obj + let status, lemmas = add_obj uri obj status in + let status = add_coercions_of_record_to_moo obj lemmas status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} } and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex -> diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml index 0f019a692..ee5d84278 100644 --- a/helm/ocaml/grafite2/matitaSync.ml +++ b/helm/ocaml/grafite2/matitaSync.ml @@ -114,10 +114,7 @@ let add_aliases_for_object status uri = | Cic.Variable _ | Cic.CurrentProof _ -> assert false -let add_obj uri obj status = - let basedir = Helm_registry.get "matita.basedir" in - let lemmas = LibrarySync.add_obj uri obj basedir in - let status = {status with objects = uri::status.objects} in +let add_obj uri obj lemmas status = List.fold_left add_alias_for_constant (add_aliases_for_object status uri obj) lemmas @@ -125,26 +122,9 @@ let add_obj = let profiler = HExtlib.profile "add_obj" in fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status -let add_coercion status ~add_composites uri = - let basedir = Helm_registry.get "matita.basedir" in - let compounds = CoercGraph.add_coercion uri in - let status = - if add_composites then - (List.iter (fun (u,_) -> - prerr_endline (UriManager.string_of_uri u)) compounds; - List.fold_left (fun s (uri,o) -> add_obj uri o s) status compounds ) - else - status - in - let status = - {status with coercions = uri :: List.map fst compounds @ status.coercions} - in - let statement_of name = - GrafiteAst.Coercion - (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in - let moo_content = [statement_of (UriManager.name_of_uri uri)] in - let status = GrafiteTypes.add_moo_content moo_content status in - List.fold_left add_alias_for_constant status (List.map fst compounds) +let add_coercion status uri compounds = + let status = {status with coercions = uri :: status.coercions} in + List.fold_left add_alias_for_constant status compounds module OrderedUri = struct @@ -185,13 +165,13 @@ let time_travel ~present ~past = in let debug_list = ref [] in List.iter - (fun uri -> CoercGraph.remove_coercion uri) + (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; List.iter LibrarySync.remove_obj objs_to_remove; List.iter CicNotation.remove_notation notation_to_remove let init () = - CoercGraph.remove_all (); + LibrarySync.remove_all_coercions (); LibraryObjects.reset_defaults (); { aliases = DisambiguateTypes.Environment.empty; diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli index 6161a6a0d..bc744f862 100644 --- a/helm/ocaml/grafite2/matitaSync.mli +++ b/helm/ocaml/grafite2/matitaSync.mli @@ -24,11 +24,11 @@ *) val add_obj: - UriManager.uri -> Cic.obj -> + UriManager.uri -> Cic.obj -> UriManager.uri list -> GrafiteTypes.status -> GrafiteTypes.status val add_coercion: - GrafiteTypes.status -> add_composites:bool -> UriManager.uri -> + GrafiteTypes.status -> UriManager.uri -> UriManager.uri list -> GrafiteTypes.status val time_travel: diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend index 0e1060c9e..5054959da 100644 --- a/helm/ocaml/library/.depend +++ b/helm/ocaml/library/.depend @@ -1,3 +1,4 @@ +cicCoercion.cmi: coercDb.cmi cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi cicRecord.cmo: cicRecord.cmi @@ -8,12 +9,14 @@ libraryDb.cmo: libraryDb.cmi libraryDb.cmx: libraryDb.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi +cicCoercion.cmo: coercDb.cmi cicCoercion.cmi +cicCoercion.cmx: coercDb.cmx cicCoercion.cmi coercGraph.cmo: coercDb.cmi coercGraph.cmi coercGraph.cmx: coercDb.cmx coercGraph.cmi -librarySync.cmo: libraryDb.cmi coercGraph.cmi cicRecord.cmi cicElim.cmi \ - librarySync.cmi -librarySync.cmx: libraryDb.cmx coercGraph.cmx cicRecord.cmx cicElim.cmx \ - librarySync.cmi +librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \ + cicElim.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: libraryDb.cmx coercGraph.cmx coercDb.cmx cicRecord.cmx \ + cicElim.cmx cicCoercion.cmx librarySync.cmi libraryNoDb.cmo: libraryNoDb.cmi libraryNoDb.cmx: libraryNoDb.cmi libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \ diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index 581709b2c..74a61aed5 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ + cicCoercion.mli \ coercGraph.mli \ librarySync.mli \ libraryNoDb.mli \ diff --git a/helm/ocaml/library/cicCoercion.ml b/helm/ocaml/library/cicCoercion.ml new file mode 100644 index 000000000..981baffce --- /dev/null +++ b/helm/ocaml/library/cicCoercion.ml @@ -0,0 +1,154 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +(* given the new coercion uri from src to tgt returns the list + * of new coercions to create. hte list elements are + * (source, list of coercions to follow, target) + *) +let get_closure_coercions src tgt uri coercions = + let eq_carr s t = + try + CoercDb.eq_carr s t + with + | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false + in + match src,tgt with + | CoercDb.Uri _, CoercDb.Uri _ -> + let c_from_tgt = + List.filter (fun (f,_,_) -> eq_carr f tgt) coercions + in + let c_to_src = + List.filter (fun (_,t,_) -> eq_carr t src) coercions + in + (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ + (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ + (List.fold_left ( + fun l (s,_,u1) -> + ((List.map (fun (_,t,u2) -> + (s,[u1;uri;u2],t) + )c_from_tgt)@l) ) + [] c_to_src) + | _ -> [] (* do not close in case source or target is not an indty ?? *) +;; + +let obj_attrs = [`Class `Coercion; `Generated] + +(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) +let generate_composite_closure c1 c2 univ = + let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in + let rec mk_rels n = + match n with + | 0 -> [] + | _ -> (Cic.Rel n) :: (mk_rels (n-1)) + in + let rec compose k = + function + | Cic.Prod (name,src,tgt) -> + let name = + match name with + | Cic.Anonymous -> Cic.Name "x" + | _ -> name + in + Cic.Lambda (name,src,compose (k+1) tgt) + | Cic.Appl (he::tl) -> + Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) + | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) + in + let c = compose 0 c1_ty in + let c_ty,univ = + try + CicTypeChecker.type_of_aux' [] [] c univ + with CicTypeChecker.TypeCheckerFailure s as exn -> + debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" + (CicPp.ppterm c) (Lazy.force s))); + raise exn + in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types c_ty + in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in + obj,univ +;; + +(* removes from l the coercions that are in !coercions *) +let filter_duplicates l coercions = + List.filter ( + fun (src,_,tgt) -> + not (List.exists (fun (s,t,u) -> + CoercDb.eq_carr s src && + CoercDb.eq_carr t tgt) + coercions)) + l + +(* given a new coercion uri from src to tgt returns + * a list of (new coercion uri, coercion obj, universe graph) + *) +let close_coercion_graph src tgt uri = + (* check if the coercion already exists *) + let coercions = CoercDb.to_list () in + let todo_list = get_closure_coercions src tgt uri coercions in + let todo_list = filter_duplicates todo_list coercions in + let new_coercions = + List.map ( + fun (src, l , tgt) -> + match l with + | [] -> assert false + | he :: tl -> + let first_step = + Cic.Constant ("", + Some (CoercDb.term_of_carr (CoercDb.Uri he)), + Cic.Sort Cic.Prop, [], obj_attrs) + in + let o,_ = + List.fold_left (fun (o,univ) coer -> + match o with + | Cic.Constant (_,Some c,_,[],_) -> + generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri + coer)) univ + | _ -> assert false + ) (first_step, CicUniv.empty_ugraph) tl + in + let name_src = CoercDb.name_of_carr src in + let name_tgt = CoercDb.name_of_carr tgt in + let name = name_tgt ^ "_of_" ^ name_src in + let buri = UriManager.buri_of_uri uri in + let c_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) + | _ -> assert false + in + ((src,tgt,c_uri,named_obj)) + ) todo_list + in + new_coercions +;; + diff --git a/helm/ocaml/library/cicCoercion.mli b/helm/ocaml/library/cicCoercion.mli new file mode 100644 index 000000000..c9eaf0aac --- /dev/null +++ b/helm/ocaml/library/cicCoercion.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* This module implements the Coercions transitive closure *) + +val close_coercion_graph: + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list + diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml index bc3d2a745..ac5067585 100644 --- a/helm/ocaml/library/coercDb.ml +++ b/helm/ocaml/library/coercDb.ml @@ -79,3 +79,10 @@ let get_carr uri = src, tgt with Not_found -> assert false (* uri must be a coercion *) +let term_of_carr = function + | Uri u -> CicUtil.term_of_uri u + | Sort s -> Cic.Sort s + | Term _ -> assert false + + + diff --git a/helm/ocaml/library/coercDb.mli b/helm/ocaml/library/coercDb.mli index 970d2b98a..9e8bf5e9c 100644 --- a/helm/ocaml/library/coercDb.mli +++ b/helm/ocaml/library/coercDb.mli @@ -24,7 +24,11 @@ *) - (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **) + (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync + * + * and may be merged with CicCoercion... + * + * **) (** XXX WARNING: non-reentrant *) @@ -51,4 +55,4 @@ val find_coercion: val is_a_coercion: UriManager.uri -> bool val get_carr: UriManager.uri -> coerc_carr * coerc_carr - +val term_of_carr: coerc_carr -> Cic.term diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml index 3862fcccc..b3176d093 100644 --- a/helm/ocaml/library/coercGraph.ml +++ b/helm/ocaml/library/coercGraph.ml @@ -34,7 +34,6 @@ type coercion_search_result = let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () - (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion src tgt = try @@ -75,188 +74,6 @@ let look_for_coercion src tgt = let tgt_uri = CoercDb.coerc_carr_of_term tgt in look_for_coercion src_uri tgt_uri -(* given the new coercion uri from src to tgt returns the list - * of new coercions to create. hte list elements are - * (source, list of coercions to follow, target) - *) -let get_closure_coercions src tgt uri coercions = - let eq_carr s t = - try - CoercDb.eq_carr s t - with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false - in - match src,tgt with - | CoercDb.Uri _, CoercDb.Uri _ -> - let c_from_tgt = - List.filter (fun (f,_,_) -> eq_carr f tgt) coercions - in - let c_to_src = - List.filter (fun (_,t,_) -> eq_carr t src) coercions - in - (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ - (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ - (List.fold_left ( - fun l (s,_,u1) -> - ((List.map (fun (_,t,u2) -> - (s,[u1;uri;u2],t) - )c_from_tgt)@l) ) - [] c_to_src) - | _ -> [] (* do not close in case source or target is not an indty ?? *) -;; - -let obj_attrs = [`Class `Coercion; `Generated] - -(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure c1 c2 univ = - let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in - let rec mk_rels n = - match n with - | 0 -> [] - | _ -> (Cic.Rel n) :: (mk_rels (n-1)) - in - let rec compose k = - function - | Cic.Prod (name,src,tgt) -> - let name = - match name with - | Cic.Anonymous -> Cic.Name "x" - | _ -> name - in - Cic.Lambda (name,src,compose (k+1) tgt) - | Cic.Appl (he::tl) -> - Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) - | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) - in - let c = compose 0 c1_ty in - let c_ty,univ = - try - CicTypeChecker.type_of_aux' [] [] c univ - with CicTypeChecker.TypeCheckerFailure s as exn -> - debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) (Lazy.force s))); - raise exn - in - let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types c_ty - in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in - obj,univ -;; - -(* removes from l the coercions that are in !coercions *) -let filter_duplicates l coercions = - List.filter ( - fun (src,_,tgt) -> - not (List.exists (fun (s,t,u) -> - CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt) - coercions)) - l - -let term_of_carr = function - | CoercDb.Uri u -> CicUtil.term_of_uri u - | CoercDb.Sort s -> Cic.Sort s - | CoercDb.Term _ -> assert false - -(* given a new coercion uri from src to tgt returns - * a list of (new coercion uri, coercion obj, universe graph) - *) -let close_coercion_graph src tgt uri = - (* check if the coercion already exists *) - let coercions = CoercDb.to_list () in - let todo_list = get_closure_coercions src tgt uri coercions in - let todo_list = filter_duplicates todo_list coercions in - let new_coercions = - List.map ( - fun (src, l , tgt) -> - match l with - | [] -> assert false - | he :: tl -> - let first_step = - Cic.Constant ("", - Some (term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs) - in - let o,_ = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (term_of_carr (CoercDb.Uri - coer)) univ - | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl - in - let name_src = CoercDb.name_of_carr src in - let name_tgt = CoercDb.name_of_carr tgt in - let name = name_tgt ^ "_of_" ^ name_src in - let buri = UriManager.buri_of_uri uri in - let c_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - let named_obj = - match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) - | _ -> assert false - in - ((src,tgt,c_uri,named_obj)) - ) todo_list - in - new_coercions -;; - -let coercion_hashtbl = UriManager.UriHashtbl.create 3 - -let add_coercion 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 - UriManager.UriHashtbl.add coercion_hashtbl uri - (List.map (fun (_,_,uri,_) -> uri) new_coercions); - CoercDb.add_coercion (src_uri,tgt_uri,uri); - List.iter - (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) - new_coercions; - List.map (fun (_,_,uri,o) -> uri,o) new_coercions - - -let remove_coercion uri = - try - let res = UriManager.UriHashtbl.find coercion_hashtbl uri in - UriManager.UriHashtbl.remove coercion_hashtbl uri; - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); - List.iter - (fun u -> - CoercDb.remove_coercion - (fun (_,_,u1) -> UriManager.eq u u1)) - res; - with - Not_found -> () - -let remove_all () = - CoercDb.remove_coercion (fun (_,_,u1) -> true) - let is_a_coercion t = try let uri = CicUtil.uri_of_term t in @@ -266,13 +83,13 @@ let is_a_coercion t = let source_of t = try let uri = CicUtil.uri_of_term t in - term_of_carr (fst (CoercDb.get_carr uri)) + CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) let target_of t = try let uri = CicUtil.uri_of_term t in - term_of_carr (snd (CoercDb.get_carr uri)) + CoercDb.term_of_carr (snd (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) (* EOF *) diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli index b21fb96be..1923a964a 100644 --- a/helm/ocaml/library/coercGraph.mli +++ b/helm/ocaml/library/coercGraph.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* This module implements the Query interface to the Coercion Graph *) + type coercion_search_result = | SomeCoercion of Cic.term | NoCoercion @@ -32,17 +34,7 @@ type coercion_search_result = val look_for_coercion : Cic.term -> Cic.term -> coercion_search_result -(* it returns the list of composite coercions *) -(* composite coercions are always declared as such; they are added to the *) -(* CoercDb adding them to the library is left to the caller *) -val add_coercion: - UriManager.uri -> - (UriManager.uri * Cic.obj) list - -val remove_coercion: UriManager.uri -> unit - val is_a_coercion: Cic.term -> bool val source_of: Cic.term -> Cic.term val target_of: Cic.term -> Cic.term -val remove_all: unit -> unit diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 707b355b0..2690349bc 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -27,6 +27,14 @@ exception AlreadyDefined of UriManager.uri let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 +(* uri |--> (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib) + * + * in case of remove_coercion uri, the first component is removed from the + * coercion DB, while the second is passed to remove_obj (and is not [] only if + * add_coercion is called with add_composites + * *) +let coercion_hashtbl = UriManager.UriHashtbl.create 3 + let merge_coercions obj = let module C = Cic in let rec aux2 = (fun (u,t) -> u,aux t) @@ -221,7 +229,7 @@ let remove_single_obj uri = HExtlib.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); ignore (LibraryDb.remove_uri uri); - CoercGraph.remove_coercion uri; + (*CoercGraph.remove_coercion uri;*) CicEnvironment.remove_obj uri) to_remove @@ -243,6 +251,82 @@ let generate_elimination_principles ~basedir uri = List.iter remove_single_obj !uris; raise exn +(* COERICONS ***********************************************************) + +let remove_all_coercions () = + UriManager.UriHashtbl.clear coercion_hashtbl; + CoercDb.remove_coercion (fun (_,_,u1) -> true) + +let add_coercion ~basedir ~add_composites uri = + let coer_ty,_ = + let coer = CicUtil.term_of_uri uri in + CicTypeChecker.type_of_aux' [] [] coer 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 + * + * Currently only (_:T1)T2 is supported. + * should we saturate it with metas in case we insert it? + * + *) + let extract_last_two_p ty = + let rec aux = function + | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> + assert false + (* not implemented: 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 = CicCoercion.close_coercion_graph src_uri tgt_uri uri in + let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in + (* update the DB *) + List.iter + (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) + new_coercions; + CoercDb.add_coercion (src_uri, tgt_uri, uri); + (* add the composites obj and they eventual lemmas *) + let lemmas = + if add_composites then + List.fold_left + (fun acc (_,_,uri,obj) -> + add_single_obj ~basedir uri obj; + uri::acc) + composite_uris new_coercions + else + [] + in + (* store that composite_uris are related to uri. the first component is the + * stuff in the DB while the second is stuff for remove_obj *) + UriManager.UriHashtbl.add coercion_hashtbl uri + (composite_uris,if add_composites then composite_uris else []); + lemmas + +let remove_coercion uri = + try + let (composites_in_db, composites_in_lib) = + UriManager.UriHashtbl.find coercion_hashtbl uri + in + UriManager.UriHashtbl.remove coercion_hashtbl uri; + CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); + (* remove from the DB *) + List.iter + (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1)) + composites_in_db; + (* remove composites from the lib *) + List.iter remove_single_obj composites_in_lib + with + Not_found -> () (* mhh..... *) + + let generate_projections ~basedir uri fields = let uris = ref [] in let projections = CicRecord.projections_of uri (List.map fst fields) in @@ -257,12 +341,8 @@ let generate_projections ~basedir uri fields = add_single_obj ~basedir uri obj; let composites = - if coercion then - (* this is _NOT_ the place for THIS!!! *) - (* MOO HANDLING IS MISSING *) - let toadd = CoercGraph.add_coercion uri in - List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd; - List.map fst toadd + if coercion then + add_coercion ~basedir ~add_composites:true uri else [] in @@ -321,3 +401,4 @@ let remove_obj uri = Not_found -> [] (*assert false*) in List.iter remove_single_obj (uri::uris) + diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli index 1400b081b..43ac34da3 100644 --- a/helm/ocaml/library/librarySync.mli +++ b/helm/ocaml/library/librarySync.mli @@ -34,3 +34,19 @@ val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list (* Warning: it does not remove the dependencies on the object and on its *) (* auxiliary lemmas! *) val remove_obj: UriManager.uri -> unit + +(* Informs the library that [uri] is a coercion. *) +(* This can generate some composite coercions that, if [add_composites] *) +(* is true are added to the library. *) +(* The list of added objects is returned. *) +val add_coercion: + basedir:string -> add_composites:bool -> UriManager.uri -> + UriManager.uri list + +(* inverse of add_coercion, removes both the eventually created composite *) +(* coercions and the information that [uri] and the composites are coercion *) +val remove_coercion: UriManager.uri -> unit + +(* mh... *) +val remove_all_coercions: unit -> unit + -- 2.39.2