From 27ce29cfef1e71c00ee19d2c00c9f425f9efb031 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 10 Jul 2006 17:07:24 +0000 Subject: [PATCH] improved coercions support: - multiple coercions from the same carrier are allowed - coercions are hidden from the proof too - a new function to print proof in text mode added --- components/acic_content/acic2content.ml | 25 ++- components/acic_content/acic2content.mli | 3 + components/acic_content/termAcicContent.ml | 3 +- components/acic_content/termAcicContent.mli | 1 - components/cic_unification/cicRefine.ml | 165 +++++++++++++------- components/content_pres/.depend | 2 + components/content_pres/Makefile | 1 + components/content_pres/boxPp.ml | 8 +- components/content_pres/boxPp.mli | 8 +- components/content_pres/cicNotationLexer.ml | 2 +- components/content_pres/objPp.ml | 30 ++++ components/content_pres/objPp.mli | 27 ++++ components/grafite_engine/grafiteEngine.ml | 24 +-- components/library/cicCoercion.ml | 152 ++++++++++++------ components/library/coercDb.ml | 41 +++-- components/library/coercDb.mli | 2 +- components/library/coercGraph.ml | 51 +++--- components/library/coercGraph.mli | 2 +- components/library/librarySync.ml | 113 ++++++++------ 19 files changed, 446 insertions(+), 214 deletions(-) create mode 100644 components/content_pres/objPp.ml create mode 100644 components/content_pres/objPp.mli diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index e72d466d5..23d644786 100644 --- a/components/acic_content/acic2content.ml +++ b/components/acic_content/acic2content.ml @@ -44,6 +44,8 @@ let conclude_prefix = "concl:";; let premise_prefix = "prem:";; let lemma_prefix = "lemma:";; +let hide_coercions = ref true;; + (* e se mettessi la conversione di BY nell'apply_context ? *) (* sarebbe carino avere l'invariante che la proof2pres generasse sempre prove con contesto vuoto *) @@ -500,13 +502,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types else raise Not_a_proof | C.AAppl (id,li) -> - (try rewrite + (try coercion + seed li ~ids_to_inner_types ~ids_to_inner_sorts + with NotApplicable -> + try rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> - try transitivity + try transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> let subproofs, args = @@ -795,6 +800,22 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = } | _ -> raise NotApplicable +and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts = + match li with + | ((Cic.AConst _) as he)::tl + | ((Cic.AMutInd _) as he)::tl + | ((Cic.AMutConstruct _) as he)::tl when + CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && + !hide_coercions -> + let rec last = + function + [] -> assert false + | [t] -> t + | _::tl -> last tl + in + acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl) + | _ -> raise NotApplicable + and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in diff --git a/components/acic_content/acic2content.mli b/components/acic_content/acic2content.mli index e1dfb82de..32ce68859 100644 --- a/components/acic_content/acic2content.mli +++ b/components/acic_content/acic2content.mli @@ -31,3 +31,6 @@ val annobj2content : val map_sequent : Cic.annconjecture -> Cic.annterm Content.conjecture + +val hide_coercions: bool ref + diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml index a25730e4d..7948f2654 100644 --- a/components/acic_content/termAcicContent.ml +++ b/components/acic_content/termAcicContent.ml @@ -66,7 +66,6 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) -let hide_coercions = ref true;; let ast_of_acic0 term_info acic k = let k = k term_info in @@ -123,7 +122,7 @@ let ast_of_acic0 term_info acic k = | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) -> if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && - !hide_coercions + !Acic2content.hide_coercions then let rec last = function diff --git a/components/acic_content/termAcicContent.mli b/components/acic_content/termAcicContent.mli index 214d7f5d2..49358bfce 100644 --- a/components/acic_content/termAcicContent.mli +++ b/components/acic_content/termAcicContent.mli @@ -23,7 +23,6 @@ * http://helm.cs.unibo.it/ *) -val hide_coercions: bool ref (** {2 Persistant state handling} *) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 90643164d..48ae522f4 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -261,6 +261,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = + let try_coercion t subst metasenv context ugraph coercion_tgt c = + let coerced = Cic.Appl[c;t] in + try + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context coerced ugraph + in + let newt, tty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv ugraph newt coercion_tgt + in + Some (newt, tty, subst, metasenv, ugraph) + with + | RefineFailure _ | Uncertain _ -> None + in let module C = Cic in let module S = CicSubstitution in let module U = UriManager in @@ -392,15 +405,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion c -> - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context (Cic.Appl[c;t]) - ugraph in - let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph - newt coercion_tgt - in - newt, tty, subst, metasenv, ugraph) + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (try_coercion + t subst metasenv context ugraph coercion_tgt) + candidates + in + match selected with + | Some x -> x + | None -> + enrich localization_tbl t + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context + subst t context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ + " that is not a sort")))) in let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -439,15 +462,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CoercGraph.look_for_coercion coercion_src coercion_tgt in match boh with - | CoercGraph.SomeCoercion c -> - let newt,_,subst',metasenv',ugraph1 = - type_of_aux subst' metasenv' context (Cic.Appl[c;s']) - ugraph1 in - let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion context subst' metasenv' - ugraph1 newt coercion_tgt - in - newt, tty, subst', metasenv', ugraph1 | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl s' @@ -465,6 +479,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (try_coercion + s' subst' metasenv' context ugraph1 coercion_tgt) + candidates + in + match selected with + | Some x -> x + | None -> + enrich localization_tbl s' + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst s' context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ + " that is not a sort"))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -1100,31 +1132,33 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let tgt_carr = CicMetaSubst.apply_subst subst ty in (match CoercGraph.look_for_coercion source_carr tgt_carr with - | CoercGraph.SomeCoercion c -> - let newt = - match c with - Cic.Appl l -> Cic.Appl (l @ [head]) - | _ -> Cic.Appl [c;head] + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun c -> + let newt = + match c with + | Cic.Appl l -> Cic.Appl (l @ [head]) + | _ -> Cic.Appl [c;head] + in + (try + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + Some (newt, ty, subst, metasenv, ugraph) + with RefineFailure _ | Uncertain _ -> None)) + candidates in - (try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in - debug_print - (lazy - ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); - newt, ty, subst, metasenv, ugraph - with - RefineFailure _ -> - prerr_endline ("#### Coercion not packed (Refine_failure): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); - assert false - | Uncertain _ -> - prerr_endline ("#### Coercion not packed (Uncerctain case): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); + (match selected with + | Some x -> x + | None -> + prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t); assert false) | _ -> assert false) (* the composite coercion must exist *) else @@ -1238,29 +1272,40 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion c -> - try - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - (Cic.Appl[c;hete]) ugraph in - let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt tgt_carr in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - newt, subst, metasenv, ugraph - with _ -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun c -> + try + let t = Cic.Appl[c;hete] in + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context + t ugraph + in + let newt, _, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv + ugraph newt tgt_carr + in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety s ugraph + in + Some (newt, subst, metasenv, ugraph) + with Uncertain _ | RefineFailure _ -> None) + candidates + in + (match selected with + | Some x -> x + | None -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst hety context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn) + (* "\nReason: " ^ Lazy.force e*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> diff --git a/components/content_pres/.depend b/components/content_pres/.depend index 60e25ecd8..d16c75a76 100644 --- a/components/content_pres/.depend +++ b/components/content_pres/.depend @@ -30,6 +30,8 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi +objPp.cmo: content2pres.cmi boxPp.cmi objPp.cmi +objPp.cmx: content2pres.cmx boxPp.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index 980e8c25a..5613ff9ff 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -12,6 +12,7 @@ INTERFACE_FILES = \ cicNotationPres.mli \ boxPp.mli \ content2pres.mli \ + objPp.mli \ sequent2pres.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/components/content_pres/boxPp.ml b/components/content_pres/boxPp.ml index 7a2fa9912..2957a3975 100644 --- a/components/content_pres/boxPp.ml +++ b/components/content_pres/boxPp.ml @@ -93,7 +93,7 @@ let fixed_rendering s = let s_len = String.length s in (fun _ -> s_len, [s]) -let render_to_strings size markup = +let render_to_strings choose_action size markup = let max_size = max_int in let rec aux_box = function @@ -101,7 +101,7 @@ let render_to_strings size markup = | Box.Space _ -> fixed_rendering string_space | Box.Ink _ -> fixed_rendering string_ink | Box.Action (_, []) -> assert false - | Box.Action (_, hd :: _) -> aux_box hd + | Box.Action (_, l) -> aux_box (choose_action l) | Box.Object (_, o) -> aux_mpres o | Box.H (attrs, children) -> let spacing = want_spacing attrs in @@ -236,6 +236,6 @@ let render_to_strings size markup = in snd (aux_mpres markup size) -let render_to_string size markup = - String.concat "\n" (render_to_strings size markup) +let render_to_string choose_action size markup = + String.concat "\n" (render_to_strings choose_action size markup) diff --git a/components/content_pres/boxPp.mli b/components/content_pres/boxPp.mli index 6b7c3cec8..fe05e24d9 100644 --- a/components/content_pres/boxPp.mli +++ b/components/content_pres/boxPp.mli @@ -24,10 +24,14 @@ *) (** @return rows list of rows *) -val render_to_strings: int -> CicNotationPres.markup -> string list +val render_to_strings: + (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> + int -> CicNotationPres.markup -> string list (** helper function * @return s, concatenation of the return value of render_to_strings above * with newlines as separators *) -val render_to_string: int -> CicNotationPres.markup -> string +val render_to_string: + (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> + int -> CicNotationPres.markup -> string diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml index 67340d37a..fb459a94e 100644 --- a/components/content_pres/cicNotationLexer.ml +++ b/components/content_pres/cicNotationLexer.ml @@ -125,7 +125,7 @@ let _ = ("<>", <:unicode>); (":=", <:unicode>); ] -let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+ +let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ let regexp uri = ("cic:/" | "theory:/") (* schema *) diff --git a/components/content_pres/objPp.ml b/components/content_pres/objPp.ml new file mode 100644 index 000000000..1eb47dbab --- /dev/null +++ b/components/content_pres/objPp.ml @@ -0,0 +1,30 @@ +(* 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 obj_to_string n obj = + let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in + let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in + let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in + BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) diff --git a/components/content_pres/objPp.mli b/components/content_pres/objPp.mli new file mode 100644 index 000000000..e007c6e7c --- /dev/null +++ b/components/content_pres/objPp.mli @@ -0,0 +1,27 @@ +(* 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/ + *) + +val obj_to_string: int -> Cic.obj -> string + diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ad5423b3e..ebe7df369 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -423,8 +423,10 @@ let refinement_toolkit = { let eval_coercion status ~add_composites uri = let status,compounds = GrafiteSync.add_coercion ~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 + let moo_content = + List.map coercion_moo_statement_of (uri::compounds) + in + let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, compounds @@ -517,7 +519,7 @@ 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 `Projection) attrs + List.mem (`Class `Coercion) attrs with Not_found -> assert false in (* looking at the fields we can know the 'wanted' coercions, but not the @@ -534,8 +536,7 @@ let add_coercions_of_record_to_moo obj lemmas status = | _ -> None) fields in - (* - prerr_endline "wanted coercions:"; + (*prerr_endline "wanted coercions:"; List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) wanted_coercions; *) @@ -544,17 +545,22 @@ let add_coercions_of_record_to_moo obj lemmas status = (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 + 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 - (* prerr_endline "actual coercions:"; + (*prerr_endline "actual coercions:"; + List.iter + (fun u -> prerr_endline (UriManager.string_of_uri u)) + coercions; + prerr_endline "lemmas was:"; List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - coercions; *) + lemmas; *) let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 7e36ac1aa..9a9ddb62b 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -42,19 +42,31 @@ let get_closure_coercions src tgt uri coercions = match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> let c_from_tgt = - List.filter (fun (f,_,_) -> eq_carr f tgt) coercions + List.filter + (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) + coercions in let c_to_src = - List.filter (fun (_,t,_) -> eq_carr t src) coercions + List.filter + (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt)) + 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) + (HExtlib.flatten_map + (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ + (HExtlib.flatten_map + (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ + (HExtlib.flatten_map + (fun (s,_,u1l) -> + HExtlib.flatten_map + (fun (_,t,u2l) -> + HExtlib.flatten_map + (fun u1 -> + List.map + (fun u2 -> (s,[u1;uri;u2],t)) + u2l) + u1l) + c_from_tgt) + c_to_src) | _ -> [] (* do not close in case source or target is not an indty ?? *) ;; @@ -169,13 +181,50 @@ let generate_composite_closure rt c1 c2 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) -> + fun (src,l1,tgt) -> + not (List.exists (fun (s,t,l2) -> CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt) + CoercDb.eq_carr t tgt && + try + List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2 + with + | Invalid_argument "List.for_all2" -> false) coercions)) l +let mangle s t l = + (*List.fold_left + (fun s x -> s ^ "_" ^ x) + (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*) + s ^ "_OF_" ^ t +;; + +exception ManglingFailed of string + +let number_if_already_defined buri name = + let rec aux n = + let suffix = if n > 0 then string_of_int n else "" in + let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in + try + let _ = Http_getter.resolve ~writable:true uri in + if Http_getter.exists uri then + begin + HLog.warn ("Uri " ^ uri ^ " already exists."); + if n < 10 then aux (n+1) else + raise + (ManglingFailed + ("Unable to give an altenative name to " ^ + buri ^ "/" ^ name ^ ".con")) + end + else + UriManager.uri_of_string uri + with + | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri + | Http_getter_types.Unresolvable_URI _ -> assert false + in + aux 0 +;; + (* given a new coercion uri from src to tgt returns * a list of (new coercion uri, coercion obj, universe graph) *) @@ -184,44 +233,45 @@ let close_coercion_graph rt src tgt uri = 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 = - HExtlib.filter_map ( - fun (src, l , tgt) -> - try - (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 rt c - (CoercDb.term_of_carr (CoercDb.Uri coer)) univ + try + let new_coercions = + HExtlib.filter_map ( + fun (src, l , tgt) -> + try + (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 rt 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 by = List.map UriManager.name_of_uri l in + let name = mangle name_tgt name_src by in + let buri = UriManager.buri_of_uri uri in + let c_uri = number_if_already_defined buri name in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) | _ -> 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 - Some ((src,tgt,c_uri,named_obj))) - with UnableToCompose -> None - ) todo_list - in - new_coercions + in + Some ((src,tgt,c_uri,named_obj))) + with UnableToCompose -> None + ) todo_list + in + new_coercions + with ManglingFailed s -> HLog.error s; [] ;; diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index 8b7982ea0..25bdab180 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -72,28 +72,51 @@ let eq_carr src tgt = let to_list () = !db -let add_coercion c = - db := c :: !db - -let remove_coercion p = - db := List.filter (fun u -> not(p u)) !db +let rec myfilter p = function + | [] -> [] + | (s,t,l)::tl -> + let l = List.filter (fun u -> not (p (s,t,u))) l in + if l = [] then myfilter p tl else (s,t,l)::myfilter p tl +;; + +let remove_coercion p = db := myfilter p !db;; let find_coercion f = - List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db) + List.flatten + (List.map + (fun (_,_,x) -> x) + (List.filter (fun (s,t,_) -> f (s,t)) !db)) +;; -let is_a_coercion u = - List.exists (fun (_,_,x) -> UriManager.eq x u) !db +let is_a_coercion u = + List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db +;; let get_carr uri = try - let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in + let src, tgt, _ = + List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db + in 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 +;; +let add_coercion (src,tgt,u) = + let f s t = eq_carr s src && eq_carr t tgt in + let where = List.filter (fun (s,t,_) -> f s t) !db in + let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in + match where with + | [] -> db := (src,tgt,[u]) :: !db + | (src,tgt,l)::tl -> + assert (tl = []); (* not sure, this may be a feature *) + db := (src,tgt,u::l)::tl @ rest +;; + diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index 1f5df8933..95dd96c0b 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -45,7 +45,7 @@ val name_of_carr: coerc_carr -> string val to_list: unit -> - (coerc_carr * coerc_carr * UriManager.uri) list + (coerc_carr * coerc_carr * UriManager.uri list) list val add_coercion: coerc_carr * coerc_carr * UriManager.uri -> unit diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index 06d7a12d3..6d7a670ef 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -28,7 +28,7 @@ open Printf;; type coercion_search_result = - | SomeCoercion of Cic.term + | SomeCoercion of Cic.term list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t @@ -65,34 +65,29 @@ let look_for_coercion src tgt = (CoercDb.name_of_carr src) (CoercDb.name_of_carr tgt))); None - | [u] -> + | _::_ -> debug_print (lazy ( - sprintf ":-) TROVATA 1 coercion da %s a %s: %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - Some u - | u::_ -> - debug_print (lazy ( - sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + sprintf ":-) TROVATE %d coercion(s) da %s a %s" (List.length l) (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - Some u + (CoercDb.name_of_carr tgt))); + Some l in (match uri with None -> NoCoercion - | Some u -> - let c = CicUtil.term_of_uri u in - let arity = arity_of c in - let args = mk_implicits (arity - 1) in - let newt = - match args with - [] -> c - | _ -> Cic.Appl (c::args) + | Some ul -> + let cl = List.map CicUtil.term_of_uri ul in + let arityl = List.map arity_of cl in + let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in + let newtl = + List.map2 + (fun args c -> + match args with + | [] -> c + | _ -> Cic.Appl (c::args)) + argsl cl in - SomeCoercion newt) + SomeCoercion newtl) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed @@ -131,10 +126,14 @@ let generate_dot_file () = in let conclusion = " } \n" in let data = List.fold_left - (fun acc (src,tgt,c) -> - acc ^ CoercDb.name_of_carr src ^ " -> " ^ - CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ - "\"];\n") "" l + (fun acc (src,tgt,cl) -> + List.fold_left + (fun acc c -> + acc ^ CoercDb.name_of_carr src ^ " -> " ^ + CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ + "\"];\n") + acc cl) + "" l in preamble ^ data ^ conclusion diff --git a/components/library/coercGraph.mli b/components/library/coercGraph.mli index 283d8a484..691bafd4c 100644 --- a/components/library/coercGraph.mli +++ b/components/library/coercGraph.mli @@ -26,7 +26,7 @@ (* This module implements the Query interface to the Coercion Graph *) type coercion_search_result = - | SomeCoercion of Cic.term + | SomeCoercion of Cic.term list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 413cc986c..a59294aaa 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -217,60 +217,75 @@ let add_coercion ~add_composites refinement_toolkit uri = in aux ty in + let already_in = + List.exists + (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul) + (CoercDb.to_list ()) + in let ty_src, ty_tgt = extract_last_two_p coer_ty in let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in - let new_coercions = - CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr 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; - if - List.exists - (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr) - (CoercDb.to_list ()) - then - begin - assert (new_coercions = []); - [] - end + if not add_composites then + (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) else - begin - CoercDb.add_coercion (src_carr, tgt_carr, 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 uri obj refinement_toolkit; - 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 *) - (* - prerr_endline ("adding: " ^ - string_of_bool add_composites ^ UriManager.string_of_uri uri); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composite_uris; - *) - UriManager.UriHashtbl.add coercion_hashtbl uri - (composite_uris,if add_composites then composite_uris else []); - lemmas - end + let new_coercions = + CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri + in + let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in + if already_in then + (* this if starts here just to be sure the closure function works fine *) + begin + assert (new_coercions = []); + HLog.warn + (UriManager.string_of_uri uri ^ + " is already declared as a coercion! skipping..."); + [] + end + else + begin + (* update the DB *) + List.iter + (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) + new_coercions; + CoercDb.add_coercion (src_carr, tgt_carr, 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 uri obj refinement_toolkit; + uri::acc) + [] 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 *) + (* + prerr_endline ("adding: " ^ + string_of_bool add_composites ^ UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composite_uris; + *) + UriManager.UriHashtbl.add coercion_hashtbl uri + (composite_uris,if add_composites then composite_uris else []); + (* + prerr_endline ("lemmas:"); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + lemmas; + prerr_endline ("lemmas END");*) + lemmas + end +;; let remove_coercion uri = try let (composites_in_db, composites_in_lib) = UriManager.UriHashtbl.find coercion_hashtbl uri in - prerr_endline ("removing: " ^UriManager.string_of_uri uri); + (*prerr_endline ("removing: " ^UriManager.string_of_uri uri); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composites_in_db; + composites_in_db;*) UriManager.UriHashtbl.remove coercion_hashtbl uri; CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); (* remove from the DB *) @@ -297,7 +312,15 @@ let generate_projections refinement_toolkit uri fields = add_single_obj uri obj refinement_toolkit; let composites = if coercion then - add_coercion ~add_composites:true refinement_toolkit uri + begin + prerr_endline ("composite for " ^ UriManager.string_of_uri uri); + let x = add_coercion ~add_composites:true refinement_toolkit uri + in + prerr_endline ("are: "); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; + prerr_endline "---"; + x + end else [] in @@ -336,7 +359,7 @@ let add_obj refinement_toolkit uri obj = | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ generate_elimination_principles uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit uri obj; + uris := !uris @ generate_inversion refinement_toolkit uri obj; let rec get_record_attrs = function | [] -> None -- 2.39.2