From 84e6cbe962c9a534be48542c098d7bb0d90be9a1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Jan 2009 10:54:34 +0000 Subject: [PATCH] many changes regarding coercions: - new `prefer coercion foo` command to reorder the list of coercions associated with a src >-> tgt pair - rewritten coercions undoing mechanism - coercion composition fixed (generates more coercions) - librarySync rewritten, procedures to generate derived lemmas (eliminators, invertion lemmas, ...) are hooks registerd by other modules that can thus live anywhere (also in tactics/ like the one for inversion) - manual fixed to talk about the new command - coercions graph is drawn together with a list of coercions that makes their precedence visible (and can be altered with the prefer coercion command) - dump-moo fixed to print coercions - removed `Coercion attribute in XML files (YOU NEED TO RECOMPILE) --- helm/software/components/cic/cic.ml | 3 +- helm/software/components/cic/cicParser.ml | 7 - helm/software/components/cic/cicUtil.ml | 10 - helm/software/components/cic/cicUtil.mli | 1 - .../components/cic_disambiguation/.depend | 4 +- .../components/cic_proof_checking/.depend | 6 +- .../components/cic_unification/cicRefine.ml | 5 - .../components/cic_unification/coercGraph.ml | 49 +- .../components/cic_unification/coercGraph.mli | 4 - .../software/components/grafite/grafiteAst.ml | 5 +- .../components/grafite/grafiteAstPp.ml | 2 + .../components/grafite/grafiteMarshal.ml | 2 + .../grafite_engine/grafiteEngine.ml | 145 ++---- .../grafite_engine/grafiteEngine.mli | 1 - .../components/grafite_engine/grafiteSync.ml | 63 +-- .../components/grafite_engine/grafiteSync.mli | 13 +- .../components/grafite_engine/grafiteTypes.ml | 12 +- .../grafite_engine/grafiteTypes.mli | 11 +- .../grafite_parser/grafiteDisambiguate.ml | 140 +++--- .../grafite_parser/grafiteParser.ml | 2 + helm/software/components/library/.depend | 17 +- helm/software/components/library/.depend.opt | 17 +- helm/software/components/library/Makefile | 6 +- helm/software/components/library/cicElim.ml | 28 ++ helm/software/components/library/cicElim.mli | 14 +- helm/software/components/library/cicFix.ml | 69 +++ .../library/{refinementTool.ml => cicFix.mli} | 19 +- helm/software/components/library/cicRecord.ml | 47 ++ .../software/components/library/cicRecord.mli | 4 +- helm/software/components/library/coercDb.ml | 11 +- helm/software/components/library/coercDb.mli | 3 + .../components/library/librarySync.ml | 463 +++++------------- .../components/library/librarySync.mli | 33 +- .../components/tactics/closeCoercionGraph.ml | 16 +- helm/software/components/tactics/fourierR.ml | 4 +- .../components/tactics/inversion_principle.ml | 165 ++++--- .../tactics/inversion_principle.mli | 26 + helm/software/matita/.depend | 4 +- helm/software/matita/applyTransformation.ml | 2 +- .../formal_topology/overlap/categories.ma | 5 + .../formal_topology/overlap/o-algebra.ma | 8 +- .../overlap/o-basic_topologies.ma | 4 +- .../overlap/o-concrete_spaces.ma | 7 +- .../overlap/relations_to_o-algebra.ma | 14 +- helm/software/matita/dist/ChangeLog | 7 +- helm/software/matita/dump_moo.ml | 4 +- helm/software/matita/help/C/sec_commands.xml | 25 + helm/software/matita/matita.lang | 1 + helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaInit.ml | 6 +- helm/software/matita/matitacLib.ml | 6 +- 51 files changed, 694 insertions(+), 828 deletions(-) create mode 100644 helm/software/components/library/cicFix.ml rename helm/software/components/library/{refinementTool.ml => cicFix.mli} (59%) diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml index 53b4ef62b..9a4f4b0de 100644 --- a/helm/software/components/cic/cic.ml +++ b/helm/software/components/cic/cic.ml @@ -67,8 +67,7 @@ type object_flavour = ] type object_class = - [ `Coercion of int - | `Elim of sort (** elimination principle; if sort is Type, the universe is + [ `Elim of sort (** elimination principle; if sort is Type, the universe is * not relevant *) | `Record of (string * bool * int) list (** inductive type that encodes a record; the arguments are diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index 30e7a0b38..3962323a1 100644 --- a/helm/software/components/cic/cicParser.ml +++ b/helm/software/components/cic/cicParser.ml @@ -694,13 +694,6 @@ let end_element ctxt tag = let class_modifiers = pop_class_modifiers ctxt in push ctxt (match pop_tag_attrs ctxt with - | ["value", "coercion"] -> Obj_class (`Coercion 0) - | ("value", "coercion")::["arity",n] - | ("arity",n)::["value", "coercion"] -> - let arity = try int_of_string n with Failure _ -> - parse_error "\"arity\" must be an integer" - in - Obj_class (`Coercion arity) | ["value", "elim"] -> (match class_modifiers with | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort) diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index c5061c62f..8fa982859 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -216,16 +216,6 @@ let attributes_of_obj = function let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj) -let arity_of_composed_coercion obj = - let attrs = attributes_of_obj obj in - try - let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in - match tag with - | `Class (`Coercion n) -> n - | _-> assert false - with Not_found -> 0 -;; - let projections_of_record obj uri = let attrs = attributes_of_obj obj in try diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli index f6087be52..66fbebe47 100644 --- a/helm/software/components/cic/cicUtil.mli +++ b/helm/software/components/cic/cicUtil.mli @@ -54,7 +54,6 @@ val id_of_annterm: Cic.annterm -> Cic.id val params_of_obj: Cic.obj -> UriManager.uri list val attributes_of_obj: Cic.obj -> Cic.attribute list val projections_of_record: Cic.obj -> UriManager.uri -> UriManager.uri list -val arity_of_composed_coercion: Cic.obj -> int val is_generated: Cic.obj -> bool (** mk_rels [howmany] [from] diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index 9fd0c6639..e9bd1168f 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,6 +1,6 @@ -disambiguateChoices.cmo: disambiguateChoices.cmi -disambiguateChoices.cmx: disambiguateChoices.cmi cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi number_notation.cmo: disambiguateChoices.cmi number_notation.cmx: disambiguateChoices.cmx diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index 5669c0845..5d83fd0f3 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -22,5 +22,7 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ freshNamesGenerator.cmi freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ freshNamesGenerator.cmi -cicDischarge.cmo: cicTypeChecker.cmi cicEnvironment.cmi cicDischarge.cmi -cicDischarge.cmx: cicTypeChecker.cmx cicEnvironment.cmx cicDischarge.cmi +cicDischarge.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicEnvironment.cmi \ + cicDischarge.cmi +cicDischarge.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicEnvironment.cmx \ + cicDischarge.cmi diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 45b2bce8f..7b472a851 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1192,11 +1192,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let selected = HExtlib.list_findopt (fun (metasenv,last,c) _ -> - match c with - | c when not (CoercGraph.is_composite c) -> - debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); - None - | c -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last head ugraph in debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index e54b3a847..0b0db09d9 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -91,7 +91,13 @@ let look_for_coercion_carr metasenv subst context src tgt = else let l = CoercDb.find_coercion - (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) + (fun (s,t) -> + CoercDb.eq_carr s src && + match t, tgt with + | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop + | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set + | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true + | _ -> CoercDb.eq_carr t tgt) in pp_l "precise" l; (match l with @@ -130,12 +136,37 @@ let source_of t = ;; let generate_dot_file () = + let l = CoercDb.to_list () in let module Pp = GraphvizPp.Dot in let buf = Buffer.create 10240 in let fmt = Format.formatter_of_buffer buf in Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] ~edge_attrs:["fontsize", "10"] fmt; - let l = CoercDb.to_list () in + if l <> [] then + Format.fprintf fmt "subgraph cluster_rest { style=\"filled\"; + color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n" + (" + + + "^ + String.concat "" + (List.map + (fun (src,tgt,ul) -> + let src_name = CoercDb.string_of_carr src in + let tgt_name = CoercDb.string_of_carr tgt in + let names = List.map (fun (u,_,_) -> UriManager.name_of_uri u) ul in + "") + (List.sort (fun (x,y,_) (x1,y1,_) -> + let rc = compare x x1 in + if rc = 0 then compare y y1 else rc) l)) + ^ "
SourceTargetArrows
" ^ src_name ^ "" ^ tgt_name ^ "" ^ + String.concat "," names ^ "
") + (String.concat ";" + (List.flatten (List.map (fun (s,t,_) -> + let src_name = CoercDb.string_of_carr s in + let tgt_name = CoercDb.string_of_carr t in + [ "\""^src_name^"\""; "\""^tgt_name^"\"" ] + ) l))); let pp_description carr = match carr with | CoercDb.Uri uri -> @@ -166,20 +197,6 @@ let generate_dot_file () = Buffer.contents buf ;; -let is_composite t = - try - let uri = - match t with - | Cic.Appl (he::_) -> CicUtil.uri_of_term he - | _ -> CicUtil.uri_of_term t - in - match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with - | Cic.Constant (_,_, _, _, attrs),_ -> - List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs - | _ -> false - with Invalid_argument _ -> false -;; - let coerced_arg l = match l with | [] | [_] -> None diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index 6c6ef2b50..3bc6273c3 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -40,10 +40,6 @@ val look_for_coercion : Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term -> Cic.term -> coercion_search_result -(* checks if term is a constant or - * a constant applyed that is marked with (`Class `Coercion) *) -val is_composite: Cic.term -> bool - val source_of: Cic.term -> Cic.term val generate_dot_file: unit -> string diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index c861a1a45..474294495 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -150,13 +150,14 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 14 +let magic = 15 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) | Coercion of loc * 'term * bool (* add_obj *) * int (* arity *) * int (* saturations *) - | UnificationHint of (loc * 'term) + | PreferCoercion of loc * 'term + | UnificationHint of loc * 'term | Default of loc * string * UriManager.uri list | Drop of loc | Include of loc * string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 0399e4ca3..9e3ea3b5a 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -313,6 +313,8 @@ let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri | Coercion (_, t, do_composites, i, j) -> pp_coercion ~term_pp t do_composites i j + | PreferCoercion (_,t) -> + "prefer coercion " ^ term_pp t | UnificationHint (_,t) -> "unification hint " ^ term_pp t | Default (_,what,uris) -> pp_default what uris diff --git a/helm/software/components/grafite/grafiteMarshal.ml b/helm/software/components/grafite/grafiteMarshal.ml index 836f592b0..48525aed5 100644 --- a/helm/software/components/grafite/grafiteMarshal.ml +++ b/helm/software/components/grafite/grafiteMarshal.ml @@ -44,6 +44,8 @@ let rehash_cmd_uris = | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) + | GrafiteAst.PreferCoercion (loc, uri) -> + GrafiteAst.PreferCoercion (loc, CicUtil.rehash_term uri) | GrafiteAst.Coercion (loc, uri, close, arity, saturations) -> GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations) | GrafiteAst.Index (loc, key, uri) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 7cf3897fa..c6bebbc39 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -470,51 +470,51 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = GrafiteAst.Coercion (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) -let refinement_toolkit = { - RefinementTool.type_of_aux' = - (fun ?localization_tbl e c t u -> - let saved = !CicRefine.insert_coercions in - CicRefine.insert_coercions:= false; - let rc = - try - let t, ty, metasenv, ugraph = - CicRefine.type_of_aux' ?localization_tbl e c t u in - RefinementTool.Success (t, ty, metasenv, ugraph) - with - | CicRefine.RefineFailure s - | CicRefine.Uncertain s - | CicRefine.AssertFailure s -> RefinementTool.Exception s - in - CicRefine.insert_coercions := saved; - rc); - RefinementTool.ppsubst = CicMetaSubst.ppsubst; - RefinementTool.apply_subst = CicMetaSubst.apply_subst; - RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; - RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; - } - let eval_unification_hint status t = (* XXX no undo *) NCicUnifHint.add_user_provided_hint t; status,[] ;; +let add_coercions_of_lemmas lemmas status = + let moo_content = + HExtlib.filter_map + (fun uri -> + match CoercDb.is_a_coercion (Cic.Const (uri,[])) with + | None -> None + | Some (_,tgt,_,sat,_) -> + let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in + Some (coercion_moo_statement_of (uri,arity,sat,0))) + lemmas + in + let status = GrafiteTypes.add_moo_content moo_content status in + {status with GrafiteTypes.coercions = CoercDb.dump () }, + lemmas + let eval_coercion status ~add_composites uri arity saturations = let uri = try CicUtil.uri_of_term uri with Invalid_argument _ -> raise (Invalid_argument "coercion can only be constants/constructors") in - let status,compounds = - GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity - saturations (GrafiteTypes.get_baseuri status) - in - let moo_content = - List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds) + let status, lemmas = + GrafiteSync.add_coercion ~add_composites + ~pack_coercion_obj:CicRefine.pack_coercion_obj + status uri arity saturations (GrafiteTypes.get_baseuri status) in + let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in + let status = GrafiteTypes.add_moo_content [moo_content] status in + add_coercions_of_lemmas lemmas status + +let eval_prefer_coercion status c = + let uri = + try CicUtil.uri_of_term c + with Invalid_argument _ -> + raise (Invalid_argument "coercion can only be constants/constructors") in - let status = GrafiteTypes.add_moo_content moo_content status in - {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - List.map (fun u,_,_,_ -> u) compounds + let status = GrafiteSync.prefer_coercion status uri in + let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in + let status = GrafiteTypes.add_moo_content [moo_content] status in + status, [] module MatitaStatus = struct @@ -570,82 +570,7 @@ let eval_tactical status tac = in 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 x _ = match x with `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.oblivion_ugraph uri in - let attrs = CicUtil.attributes_of_obj obj in - 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 - let buri = GrafiteTypes.get_baseuri status 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,arity) -> - Some - (arity, UriManager.uri_of_string (buri ^ "/" ^ 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,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 - let is_a_coercion, arity_coercion = is_a_coercion uri in - if is_a_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0)) - else if is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0)) - else - None) - lemmas) - in - (*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)) - lemmas; *) - let status = GrafiteTypes.add_moo_content moo_content status in - {status with - GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, - lemmas - -let add_obj uri obj status = - let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in - status, lemmas +let add_obj = GrafiteSync.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj let rec eval_command = {ec_go = fun ~disambiguate_command opts status (text,prefix_len,cmd) -> @@ -668,6 +593,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status *) let status = GrafiteTypes.add_moo_content [cmd] status in status,[] + | GrafiteAst.PreferCoercion (loc, coercion) -> + eval_prefer_coercion status coercion | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> eval_coercion status ~add_composites uri arity saturations | GrafiteAst.UnificationHint (loc, t) -> @@ -798,7 +725,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status CicMetaSubst.ppmetasenv [] metasenv)); let status, lemmas = add_obj uri obj status in let status,new_lemmas = - add_coercions_of_record_to_moo obj lemmas status + add_coercions_of_lemmas lemmas status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, uri::new_lemmas@lemmas diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index 1dabfaaa1..993ccda71 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -57,4 +57,3 @@ val eval_ast : (* the new status and generated objects, if any *) GrafiteTypes.status * UriManager.uri list -val refinement_toolkit: RefinementTool.kit diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index b6b9f7e5a..c1b23c928 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -53,33 +53,19 @@ let uris_for_inductive_type uri obj = ([],1) types in uris | _ -> [uri] +;; -let add_obj refinement_toolkit uri obj status = - let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in +let add_obj ~pack_coercion_obj uri obj status = + let lemmas = LibrarySync.add_obj ~pack_coercion_obj uri obj in let add_to_universe (universe,status) uri = let term = CicUtil.term_of_uri uri in let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in -(* prop filtering - let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.oblivion_ugraph in - prerr_endline (CicPp.ppterm term); - prerr_endline (CicPp.ppterm sort); - let tkeys = - if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty - else [] - in -*) let tkeys = Universe.keys [] ty in let index_cmd = List.map (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)) tkeys in -(* prop filtering - let universe = - if sort = Cic.Sort(Cic.Prop) then - Universe.index_term_and_unfolded_term universe [] term ty - else universe -*) let universe = Universe.index_term_and_unfolded_term universe [] term ty in let status = GrafiteTypes.add_moo_content index_cmd status in @@ -87,7 +73,7 @@ let add_obj refinement_toolkit uri obj status = in let uris_to_index = if is_a_variant obj then [] - else (uris_for_inductive_type uri obj)@lemmas + else (uris_for_inductive_type uri obj) @ lemmas in let universe,status = List.fold_left add_to_universe @@ -95,27 +81,25 @@ let add_obj refinement_toolkit uri obj status = uris_to_index in {status with - GrafiteTypes.objects = uri::status.GrafiteTypes.objects; + GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects; GrafiteTypes.universe = universe}, lemmas -let add_coercion refinement_toolkit ~add_composites status uri arity +let add_coercion ~pack_coercion_obj ~add_composites status uri arity saturations baseuri = - let compounds = - LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity - saturations baseuri in - {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions}, - compounds - -module OrderedUri = -struct - type t = UriManager.uri * string - let compare (u1, _) (u2, _) = UriManager.compare u1 u2 -end - -module UriSet = Set.Make (OrderedUri) + let lemmas = + LibrarySync.add_coercion ~add_composites ~pack_coercion_obj + uri arity saturations baseuri in + { status with GrafiteTypes.coercions = CoercDb.dump () ; + objects = lemmas @ status.GrafiteTypes.objects + }, + lemmas +let prefer_coercion s u = + CoercDb.prefer u; + { s with GrafiteTypes.coercions = CoercDb.dump () } + (** @return l2 \ l1 *) let uri_list_diff l2 l1 = let module S = UriManager.UriSet in @@ -127,25 +111,22 @@ let uri_list_diff l2 l1 = let time_travel ~present ~past = let objs_to_remove = uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in - let coercions_to_remove = - uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions - in - List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove; - List.iter LibrarySync.remove_obj objs_to_remove + List.iter LibrarySync.remove_obj objs_to_remove; + CoercDb.restore past.GrafiteTypes.coercions; +;; let initial_status baseuri = { GrafiteTypes.moo_content_rev = []; proof_status = GrafiteTypes.No_proof; -(* options = GrafiteTypes.no_options; *) objects = []; - coercions = []; + coercions = CoercDb.empty_coerc_db; universe = Universe.empty; baseuri = baseuri; } let init baseuri = - LibrarySync.remove_all_coercions (); + CoercDb.restore CoercDb.empty_coerc_db; LibraryObjects.reset_defaults (); initial_status baseuri ;; diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli index aa2749979..be455ea1e 100644 --- a/helm/software/components/grafite_engine/grafiteSync.mli +++ b/helm/software/components/grafite_engine/grafiteSync.mli @@ -24,22 +24,25 @@ *) val add_obj: - RefinementTool.kit -> + pack_coercion_obj:(Cic.obj -> Cic.obj) -> UriManager.uri -> Cic.obj -> GrafiteTypes.status -> GrafiteTypes.status * UriManager.uri list val add_coercion: - RefinementTool.kit -> + pack_coercion_obj:(Cic.obj -> Cic.obj) -> add_composites:bool -> GrafiteTypes.status -> UriManager.uri -> int -> int -> string (* baseuri *) -> - GrafiteTypes.status * (UriManager.uri * int * int * int) list - (* URI, arity, saturations, cpos *) + GrafiteTypes.status * UriManager.uri list + +val prefer_coercion: + GrafiteTypes.status -> UriManager.uri -> GrafiteTypes.status val time_travel: present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit - (* also resets the imperative part of the status *) + (* also resets the imperative part of the status + * init: the baseuri of the current script *) val init: string -> GrafiteTypes.status (* diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 71fd19f94..244ce615f 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -44,21 +44,11 @@ type proof_status = (* Status in which the proof could be while it is being processed by the * engine. No status entering/exiting the engine could be in it. *) -(* REMOVE -module StringMap = Map.Make (String) -type option_value = - | String of string - | Int of int -*) -(* type options = option_value StringMap.t *) -(* let no_options = StringMap.empty *) - type status = { moo_content_rev: GrafiteMarshal.moo; proof_status: proof_status; -(* options: options; *) objects: UriManager.uri list; - coercions: UriManager.uri list; + coercions: CoercDb.coerc_db; universe:Universe.universe; baseuri: string; } diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index ce988944b..95f65f360 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -42,20 +42,11 @@ type proof_status = | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv -(* -type option_value = - | String of string - | Int of int -type options -val no_options: options -*) - type status = { moo_content_rev: GrafiteMarshal.moo; proof_status: proof_status; (** logical status *) -(* options: options; *) objects: UriManager.uri list; (** in-scope objects *) - coercions: UriManager.uri list; (** defined coercions *) + coercions: CoercDb.coerc_db; universe:Universe.universe; (** universe of terms used by auto *) baseuri: string; } diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index c5cfa3b29..9f63a5d8f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -41,7 +41,7 @@ let singleton msg = function | l, _ -> let debug = Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" - msg (List.length l) + msg (List.length l) in HLog.debug debug; assert false @@ -343,7 +343,7 @@ let rec disambiguate_tactic metasenv,GrafiteAst.AutoBatch (loc,params) | GrafiteAst.Cases (loc, what, pattern, idents) -> let metasenv,what = disambiguate_term context metasenv what in - let pattern = disambiguate_pattern pattern in + let pattern = disambiguate_pattern pattern in metasenv,GrafiteAst.Cases (loc, what, pattern, idents) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term with_what in @@ -381,20 +381,20 @@ let rec disambiguate_tactic metasenv, term :: terms in let metasenv, terms = List.fold_right map terms (metasenv, []) in - metasenv, GrafiteAst.Destruct(loc, Some terms) + metasenv, GrafiteAst.Destruct(loc, Some terms) | GrafiteAst.Destruct (loc, None) -> metasenv,GrafiteAst.Destruct(loc,None) | GrafiteAst.Exact (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Exact (loc, cic) | GrafiteAst.Elim (loc, what, Some using, pattern, specs) -> - let metasenv,what = disambiguate_term context metasenv what in + let metasenv,what = disambiguate_term context metasenv what in let metasenv,using = disambiguate_term context metasenv using in - let pattern = disambiguate_pattern pattern in + let pattern = disambiguate_pattern pattern in metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs) | GrafiteAst.Elim (loc, what, None, pattern, specs) -> - let metasenv,what = disambiguate_term context metasenv what in - let pattern = disambiguate_pattern pattern in + let metasenv,what = disambiguate_term context metasenv what in + let pattern = disambiguate_pattern pattern in metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs) | GrafiteAst.ElimType (loc, what, Some using, specs) -> let metasenv,what = disambiguate_term context metasenv what in @@ -470,94 +470,94 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Assume (loc, id, cic) | GrafiteAst.Suppose (loc, term, id, term') -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = - match term' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.Suppose (loc, cic, id, cic') + let metasenv,cic' = + match term' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.Suppose (loc, cic, id, cic') | GrafiteAst.Bydone (loc,just) -> let metasenv,just = disambiguate_just disambiguate_term context metasenv just in - metasenv,GrafiteAst.Bydone (loc, just) + metasenv,GrafiteAst.Bydone (loc, just) | GrafiteAst.We_need_to_prove (loc,term,id,term') -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = - match term' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic') + let metasenv,cic' = + match term' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic') | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') -> let metasenv,just = disambiguate_just disambiguate_term context metasenv just in let metasenv,cic' = disambiguate_term context metasenv term' in - let metasenv,cic'' = - match term'' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'') + let metasenv,cic'' = + match term'' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'') | GrafiteAst.We_proceed_by_cases_on (loc, term, term') -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = disambiguate_term context metasenv term' in - metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic') + let metasenv,cic' = disambiguate_term context metasenv term' in + metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic') | GrafiteAst.We_proceed_by_induction_on (loc, term, term') -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = disambiguate_term context metasenv term' in - metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic') + let metasenv,cic' = disambiguate_term context metasenv term' in + metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic') | GrafiteAst.Byinduction (loc, term, id) -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Byinduction(loc, cic, id) + metasenv,GrafiteAst.Byinduction(loc, cic, id) | GrafiteAst.Thesisbecomes (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Thesisbecomes (loc, cic) + metasenv,GrafiteAst.Thesisbecomes (loc, cic) | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) -> - let metasenv,just = + let metasenv,just = disambiguate_just disambiguate_term context metasenv just in let metasenv,cic' = disambiguate_term context metasenv term1 in - let cic''= disambiguate_lazy_term term2 in - metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'') + let cic''= disambiguate_lazy_term term2 in + metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'') | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) -> - let metasenv,just = + let metasenv,just = disambiguate_just disambiguate_term context metasenv just in - let metasenv,cic'= disambiguate_term context metasenv term1 in - let metasenv,cic''= disambiguate_term context metasenv term2 in - metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'') + let metasenv,cic'= disambiguate_term context metasenv term1 in + let metasenv,cic''= disambiguate_term context metasenv term2 in + metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'') | GrafiteAst.Case (loc, id, params) -> let metasenv,params' = - List.fold_right - (fun (id,term) (metasenv,params) -> + List.fold_right + (fun (id,term) (metasenv,params) -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,(id,cic)::params - ) params (metasenv,[]) - in - metasenv,GrafiteAst.Case(loc, id, params') + metasenv,(id,cic)::params + ) params (metasenv,[]) + in + metasenv,GrafiteAst.Case(loc, id, params') | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) -> let metasenv,cic = - match term1 with - None -> metasenv,None - | Some (start,t) -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some (start,t) in - let metasenv,cic'= disambiguate_term context metasenv term2 in + match term1 with + None -> metasenv,None + | Some (start,t) -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some (start,t) in + let metasenv,cic'= disambiguate_term context metasenv term2 in let metasenv,cic'' = - match term3 with + match term3 with | `SolveWith term -> - let metasenv,term = disambiguate_term context metasenv term in + let metasenv,term = disambiguate_term context metasenv term in metasenv, `SolveWith term - | `Auto params -> + | `Auto params -> let metasenv, params = disambiguate_auto_params metasenv params in metasenv,`Auto params - | `Term t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,`Term t + | `Term t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,`Term t | `Proof as t -> metasenv,t in - metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) + metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let uri = @@ -700,26 +700,32 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= | GrafiteAst.Index(loc,key,uri) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in + disambiguate_term None text prefix_len lexicon_status_ref [] in let disambiguate_term_option metasenv = - function + function None -> metasenv,None - | Some t -> + | Some t -> let metasenv,t = disambiguate_term metasenv t in - metasenv, Some t + metasenv, Some t in let metasenv,key = disambiguate_term_option metasenv key in !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri) + | GrafiteAst.PreferCoercion (loc,t) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = + disambiguate_term None text prefix_len lexicon_status_ref [] in + let metasenv,t = disambiguate_term metasenv t in + !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t) | GrafiteAst.Coercion (loc,t,b,a,s) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in + disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) | GrafiteAst.UnificationHint (loc, t) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in + disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t) | GrafiteAst.Default _ diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index cf2a6f95b..4da1d4477 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -698,6 +698,8 @@ EXTEND let composites = match composites with None -> true | Some _ -> false in GrafiteAst.Coercion (loc, t, composites, arity, saturations) + | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> + GrafiteAst.PreferCoercion (loc, t) | IDENT "unification"; IDENT "hint"; t = tactic_term -> GrafiteAst.UnificationHint (loc, t) | IDENT "record" ; (params,name,ty,fields) = record_spec -> diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index fefbf93ec..a9f24f814 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,11 +1,6 @@ cicCoercion.cmi: coercDb.cmi -librarySync.cmi: refinementTool.cmo librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi -cicElim.cmo: cicElim.cmi -cicElim.cmx: cicElim.cmi -cicRecord.cmo: cicRecord.cmi -cicRecord.cmx: cicRecord.cmi libraryMisc.cmo: libraryMisc.cmi libraryMisc.cmx: libraryMisc.cmi libraryDb.cmo: libraryDb.cmi @@ -14,10 +9,14 @@ coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi cicCoercion.cmo: coercDb.cmi cicCoercion.cmi cicCoercion.cmx: coercDb.cmx cicCoercion.cmi -librarySync.cmo: refinementTool.cmo libraryDb.cmi coercDb.cmi cicRecord.cmi \ - cicElim.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \ - cicElim.cmx cicCoercion.cmx librarySync.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi +cicElim.cmo: librarySync.cmi cicElim.cmi +cicElim.cmx: librarySync.cmx cicElim.cmi +cicRecord.cmo: librarySync.cmi cicRecord.cmi +cicRecord.cmx: librarySync.cmx cicRecord.cmi +cicFix.cmo: librarySync.cmi cicFix.cmi +cicFix.cmx: librarySync.cmx cicFix.cmi libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ libraryClean.cmi libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt index d8ff04797..a9f24f814 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -1,11 +1,6 @@ cicCoercion.cmi: coercDb.cmi -librarySync.cmi: refinementTool.cmx librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi -cicElim.cmo: cicElim.cmi -cicElim.cmx: cicElim.cmi -cicRecord.cmo: cicRecord.cmi -cicRecord.cmx: cicRecord.cmi libraryMisc.cmo: libraryMisc.cmi libraryMisc.cmx: libraryMisc.cmi libraryDb.cmo: libraryDb.cmi @@ -14,10 +9,14 @@ coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi cicCoercion.cmo: coercDb.cmi cicCoercion.cmi cicCoercion.cmx: coercDb.cmx cicCoercion.cmi -librarySync.cmo: refinementTool.cmx libraryDb.cmi coercDb.cmi cicRecord.cmi \ - cicElim.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \ - cicElim.cmx cicCoercion.cmx librarySync.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi +cicElim.cmo: librarySync.cmi cicElim.cmi +cicElim.cmx: librarySync.cmx cicElim.cmi +cicRecord.cmo: librarySync.cmi cicRecord.cmi +cicRecord.cmx: librarySync.cmx cicRecord.cmi +cicFix.cmo: librarySync.cmi cicFix.cmi +cicFix.cmx: librarySync.cmx cicFix.cmi libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ libraryClean.cmi libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ diff --git a/helm/software/components/library/Makefile b/helm/software/components/library/Makefile index e3c921dd7..5b9dc226f 100644 --- a/helm/software/components/library/Makefile +++ b/helm/software/components/library/Makefile @@ -3,17 +3,17 @@ PREDICATES = INTERFACE_FILES = \ librarian.mli \ - cicElim.mli \ - cicRecord.mli \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ cicCoercion.mli \ librarySync.mli \ + cicElim.mli \ + cicRecord.mli \ + cicFix.mli \ libraryClean.mli \ $(NULL) IMPLEMENTATION_FILES = \ - refinementTool.ml \ $(INTERFACE_FILES:%.mli=%.ml) include ../../Makefile.defs diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml index 282383d78..9f3bda423 100644 --- a/helm/software/components/library/cicElim.ml +++ b/helm/software/components/library/cicElim.ml @@ -430,4 +430,32 @@ debug_print (lazy (CicPp.ppterm eliminator_body)); | _ -> failwith (sprintf "not an inductive definition (%s)" (UriManager.string_of_uri uri)) +;; +let generate_elimination_principles ~add_obj ~add_coercion uri obj = + match obj with + | Cic.InductiveDefinition (indTypes,_,_,attrs) -> + let _,inductive,_,_ = List.hd indTypes in + if not inductive then [] + else + let _,all_eliminators = + List.fold_left + (fun (i,res) _ -> + let elim sort = + try Some (elim_of ~sort uri i) + with Can_t_eliminate -> None + in + i+1, + HExtlib.filter_map + elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] @ res + ) (0,[]) indTypes + in + List.fold_left + (fun lemmas (uri,obj) -> add_obj uri obj @ uri::lemmas) + [] all_eliminators + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_elimination_principles;; diff --git a/helm/software/components/library/cicElim.mli b/helm/software/components/library/cicElim.mli index f1f84c92e..70c1c2167 100644 --- a/helm/software/components/library/cicElim.mli +++ b/helm/software/components/library/cicElim.mli @@ -23,19 +23,7 @@ * http://helm.cs.unibo.it/ *) - (** can't build the required elimination principle (e.g. elimination from Prop - * to Set *) -exception Can_t_eliminate - (** internal error while generating elimination principle *) exception Elim_failure of string Lazy.t -(** @param sort target sort -* @param uri inductive type uri -* @param typeno inductive type number -* @raise Failure -* @raise Can_t_eliminate -* @return Cic constant corresponding to the required elimination principle -* and its uri -*) -val elim_of: sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj +val init : unit -> unit diff --git a/helm/software/components/library/cicFix.ml b/helm/software/components/library/cicFix.ml new file mode 100644 index 000000000..21a2fdb20 --- /dev/null +++ b/helm/software/components/library/cicFix.ml @@ -0,0 +1,69 @@ +(* Copyright (C) 2004-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/ + *) + +(* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *) + +let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj = + match obj with + | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when + List.mem (`Flavour `MutualDefinition) attrs -> + (match bo with + Cic.Fix (_,funs) -> + snd ( + List.fold_right + (fun (name,idx,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n-1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.Fix (n-1,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + (n-1,lemmas @ uri::uris)) + funs (List.length funs,[])) + | Cic.CoFix (_,funs) -> + snd ( + List.fold_right + (fun (name,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n-1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.CoFix (n-1,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + (n-1,lemmas @ uri::uris)) + funs (List.length funs,[])) + | _ -> assert false) + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;; diff --git a/helm/software/components/library/refinementTool.ml b/helm/software/components/library/cicFix.mli similarity index 59% rename from helm/software/components/library/refinementTool.ml rename to helm/software/components/library/cicFix.mli index b78246987..de361cc7c 100644 --- a/helm/software/components/library/refinementTool.ml +++ b/helm/software/components/library/cicFix.mli @@ -1,4 +1,4 @@ -(* Copyright (C) 2006, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,19 +23,4 @@ * http://helm.cs.unibo.it/ *) -type type_of_rc = - | Success of Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph - | Exception of string Lazy.t - - (* these are the same functions of cic_unification/ (eventually wrapped) *) -type kit = { - type_of_aux': - ?localization_tbl:Stdpp.location Cic.CicHash.t -> - Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> - type_of_rc; - pack_coercion_obj: Cic.obj -> Cic.obj; - apply_subst: Cic.substitution -> Cic.term -> Cic.term ; - ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string; - ppmetasenv: Cic.substitution -> Cic.metasenv -> string; -} - +val init : unit -> unit diff --git a/helm/software/components/library/cicRecord.ml b/helm/software/components/library/cicRecord.ml index 5502f989e..e76ca9ca2 100644 --- a/helm/software/components/library/cicRecord.ml +++ b/helm/software/components/library/cicRecord.ml @@ -86,3 +86,50 @@ let projections_of uri field_names = in aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) | _ -> assert false +;; + +let generate_projections ~add_obj ~add_coercion (uri as orig_uri) obj = + match obj with + | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> [] + | Some fields -> + let uris = ref [] in + let projections = + projections_of uri (List.map (fun (x,_,_) -> x) fields) + in + List.iter2 + (fun (uri, name, bo) (_name, coercion, arity) -> + try + let ty, _ = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in + let attrs = [`Class `Projection; `Generated] in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + let lemmas1 = + if not coercion then [] else + add_coercion uri arity 0 (UriManager.buri_of_uri orig_uri) + in + uris := lemmas1 @ lemmas @ uri::!uris + with + CicTypeChecker.TypeCheckerFailure s -> + HLog.message ("Unable to create projection " ^ name ^ + " cause: " ^ Lazy.force s); + | CicEnvironment.Object_not_found uri -> + let depend = UriManager.name_of_uri uri in + HLog.message ("Unable to create projection " ^ name ^ + " because it requires " ^ depend) + ) projections fields; + !uris) + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_projections;; diff --git a/helm/software/components/library/cicRecord.mli b/helm/software/components/library/cicRecord.mli index b966f317c..de361cc7c 100644 --- a/helm/software/components/library/cicRecord.mli +++ b/helm/software/components/library/cicRecord.mli @@ -23,6 +23,4 @@ * http://helm.cs.unibo.it/ *) -(** projections_of [uri] returns uri * name * term *) -val projections_of: - UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list +val init : unit -> unit diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index 312c2f1e4..c8be370f2 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -50,6 +50,7 @@ type coerc_db = (* coercion_entry grouped by carrier with molteplicity *) let db = ref ([] : coerc_db) let dump () = !db let restore coerc_db = db := coerc_db +let empty_coerc_db = [] let rec coerc_carr_of_term t a = try @@ -78,8 +79,7 @@ let eq_carr ?(exact=false) src tgt = | Cic.Prod _, true -> false | Cic.Prod _, false -> coarse_eq | _ -> coarse_eq) - | Sort (Cic.Type _), Sort (Cic.Type _) -> true - | Sort src, Sort tgt when src = tgt -> true + | Sort _, Sort _ -> true | Fun _,Fun _ when not exact -> true (* only one Funclass *) | Fun i,Fun j when i = j -> true (* only one Funclass *) | _, _ -> false @@ -166,3 +166,10 @@ let add_coercion (src,tgt,u,saturations,cpos) = db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest ;; +let prefer u = + let prefer (s,t,l) = + let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in + s,t,lb@la + in + db := List.map prefer !db; +;; diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 130987df8..83e61dbfb 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -42,6 +42,7 @@ val to_list: (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list type coerc_db +val empty_coerc_db : coerc_db val dump: unit -> coerc_db val restore: coerc_db -> unit @@ -62,3 +63,5 @@ val find_coercion: (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list val is_a_coercion: Cic.term -> coercion_entry option + +val prefer: UriManager.uri -> unit diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index e6871b60e..1ca46db0b 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -25,21 +25,32 @@ (* $Id$ *) -let object_declaration_hook = ref (fun _ _ -> ());; -let set_object_declaration_hook f = - object_declaration_hook := f +let object_declaration_hook = ref [] +let add_object_declaration_hook f = + object_declaration_hook := f :: !object_declaration_hook exception AlreadyDefined of UriManager.uri -let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 +type coercion_decl = + UriManager.uri -> int (* arity *) -> + int (* saturations *) -> string (* baseuri *) -> + UriManager.uri list (* lemmas (new objs) *) -(* 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 stack = ref [];; + +let push () = + stack := CoercDb.dump () :: !stack; + CoercDb.restore CoercDb.empty_coerc_db; +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP from librarySync.ml") + | db :: tl -> + stack := tl; + CoercDb.restore db; +;; let uris_of_obj uri = let innertypesuri = UriManager.innertypesuri_of_uri uri in @@ -135,27 +146,37 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_single_obj uri obj refinement_toolkit = - let module RT = RefinementTool in +let remove_obj uri = + let derived_uris_of_uri uri = + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) + in + let uris_to_remove = + if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] + in + let files_to_remove = uri :: derived_uris_of_uri uri in + List.iter + (fun uri -> + (try + let file = Http_getter.resolve' ~local:true ~writable:true uri in + HExtlib.safe_remove file; + HExtlib.rmdir_descend (Filename.dirname file) + with Http_getter_types.Key_not_found _ -> ()); + ) files_to_remove ; + List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ; + CicEnvironment.remove_obj uri +;; + +let rec add_obj uri obj ~pack_coercion_obj = let obj = if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None - then refinement_toolkit.RT.pack_coercion_obj obj + then pack_coercion_obj obj else obj in let dbd = LibraryDb.instance () in - if CicEnvironment.in_library uri then - raise (AlreadyDefined uri) - else begin - (*CicUniv.reset_spent_time (); - let before = Unix.gettimeofday () in*) + if CicEnvironment.in_library uri then raise (AlreadyDefined uri); + begin (* ATOMIC *) typecheck_obj uri obj; (* 1 *) - (*let after = Unix.gettimeofday () in - let univ_time = CicUniv.get_spent_time () in - let total_time = after -. before in - prerr_endline - (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" - (univ_time *. 100. /. total_time) (total_time) (univ_time) - (UriManager.name_of_uri uri));*) let obj, ugraph, univlist = try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri with CicEnvironment.Object_not_found _ -> assert false @@ -165,11 +186,6 @@ let add_single_obj uri obj refinement_toolkit = try (*3*) let new_stuff = save_object_to_disk uri obj ugraph univlist in - (* EXPERIMENTAL: pretty print the object in natural language *) - (try !object_declaration_hook uri obj - with exc -> - prerr_endline ("Error: object_declaration_hook failed"^ - Printexc.to_string exc)); try HLog.message (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) @@ -182,92 +198,28 @@ let add_single_obj uri obj refinement_toolkit = with exc -> CicEnvironment.remove_obj uri; (* -1 *) raise exc - end - -let remove_single_obj uri = - let derived_uris_of_uri uri = - let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) - in - let uris_to_remove = - if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] - in - let files_to_remove = uri :: derived_uris_of_uri uri in - List.iter - (fun uri -> - (try - let file = Http_getter.resolve' ~local:true ~writable:true uri in - HExtlib.safe_remove file; - HExtlib.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - ) files_to_remove ; - List.iter - (fun uri -> - ignore (LibraryDb.remove_uri uri); - (*CoercGraph.remove_coercion uri;*) - ) uris_to_remove ; - CicEnvironment.remove_obj uri - -(*** GENERATION OF AUXILIARY LEMMAS ***) - -let generate_elimination_principles uri refinement_toolkit = - let uris = ref [] in - let elim i = - let elim sort = - try - let uri,obj = CicElim.elim_of ~sort uri i in - add_single_obj uri obj refinement_toolkit; - uris := uri :: !uris - with CicElim.Can_t_eliminate -> () - in - try - List.iter - elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - with exn -> - List.iter remove_single_obj !uris; - raise exn - in - let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in - match obj with - | Cic.InductiveDefinition (indTypes, _, _, _) -> - let counter = ref 0 in - List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes; - !uris - | _ -> - failwith (Printf.sprintf "not an inductive definition (%s)" - (UriManager.string_of_uri uri)) - -(* COERCIONS ***********************************************************) - -let remove_all_coercions () = - UriManager.UriHashtbl.clear coercion_hashtbl; - CoercDb.remove_coercion (fun _ -> true) - -let stack = ref [];; - -let h2l h = - UriManager.UriHashtbl.fold - (fun k v acc -> (k,v) :: acc) h [] -;; - -let push () = - stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack; - remove_all_coercions () -;; - -let pop () = - match !stack with - | [] -> raise (Failure "Unable to POP from librarySync.ml") - | (db,h) :: tl -> - stack := tl; - remove_all_coercions (); - CoercDb.restore db; - List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v) - h -;; + end; + let added = ref [] in + let add_obj_with_parachute u o = + added := u :: !added; + add_obj u o ~pack_coercion_obj in + let old_db = CoercDb.dump () in + try + List.fold_left + (fun lemmas f -> + f ~add_obj:add_obj_with_parachute + ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj) + uri obj @ lemmas) + [] !object_declaration_hook + with exn -> + List.iter remove_obj !added; + remove_obj uri; + CoercDb.restore old_db; + raise exn + (* /ATOMIC *) -let add_coercion ~add_composites refinement_toolkit uri arity saturations - baseuri +and + add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in @@ -320,37 +272,72 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations let already_in_obj src_carr tgt_carr uri obj = List.exists (fun (s,t,ul) -> + if not (CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr) + then false + else List.exists (fun u,_,_ -> - let bo = + let bo, ty = match obj with - | Cic.Constant (_, Some bo, _, _, _) -> bo - | _ -> assert false + | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty + | _ -> + (* this is not a composite coercion, thus the uri is valid *) + let bo = CicUtil.term_of_uri uri in + bo, + fst (CicTypeChecker.type_of_aux' [] [] bo + CicUniv.oblivion_ugraph) in - CoercDb.eq_carr s src_carr && - CoercDb.eq_carr t tgt_carr && - if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo - CicUniv.oblivion_ugraph) - then - (HLog.warn - ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^ - "it is a duplicate of " ^ UriManager.string_of_uri u); - true) - else - (HLog.warn + let are_body_convertible = + fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo + CicUniv.oblivion_ugraph) + in + if not are_body_convertible then + (HLog.warn ("Coercions " ^ - UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri - uri^" are not convertible, but are between the same nodes.\n"^ - "From now on unification can fail randomly."); - false)) + UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri + uri^" are not convertible, but are between the same nodes.\n"^ + "From now on unification can fail randomly."); + false) + else + match t, tgt_carr with + | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j) + | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j) + when not (CicUniv.eq i j) -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicUniv.string_of_universe j ^ " <> " ^ + CicUniv.string_of_universe i); false) + | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop + | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _) + | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true) + | CoercDb.Sort s1, CoercDb.Sort s2 -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ + CicPp.ppterm (Cic.Sort s2)); false) + | _ -> + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true)) ul) (CoercDb.to_list ()) in let cpos = no_args - arity - saturations - 1 in if not add_composites then + (ignore(already_in_obj src_carr tgt_carr uri + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri))); (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); - UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); - []) + [])) else let new_coercions = CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations @@ -360,211 +347,19 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj)) new_coercions in - let composite_uris = - List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions - in (* update the DB *) + ignore(already_in_obj src_carr tgt_carr uri + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri))); List.iter (fun (src,tgt,uri,saturations,_,_,cpos) -> CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) new_coercions; CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); (* add the composites obj and they eventual lemmas *) - let lemmas = - List.fold_left - (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> - add_single_obj uri obj refinement_toolkit; - (uri,arity,saturations,cpos)::acc) - [] new_coercions - 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,composite_uris); - (* - prerr_endline ("lemmas:"); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - lemmas; - prerr_endline ("lemmas END");*) - lemmas + (List.fold_left + (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> + add_obj uri obj pack_coercion_obj @ uri::acc) + [] new_coercions) ;; -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); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composites_in_db;*) - 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 -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *) - -let generate_projections refinement_toolkit uri fields = - let uris = ref [] in - let projections = - CicRecord.projections_of uri - (List.map (fun (x,_,_) -> x) fields) - in - try - List.iter2 - (fun (uri, name, bo) (_name, coercion, arity) -> - let saturations = 0 in - try - let ty, _ = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in - let attrs = [`Class `Projection; `Generated] in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj uri obj refinement_toolkit; - let composites = - if coercion then - begin -(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) - (*CSC: I think there is a bug here. The composite coercions - are not remembered in the .moo file. Thus they are re-generated - every time. Right? *) - let x = - add_coercion ~add_composites:true refinement_toolkit uri arity - saturations (UriManager.buri_of_uri uri) - in -(*prerr_endline ("are: "); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; - prerr_endline "---"; -*) - (*CSC: I throw the arity away. See comment above *) - List.map (fun u,_,_,_ -> u) x - end - else - [] - in - uris := uri :: composites @ !uris - with - CicTypeChecker.TypeCheckerFailure s -> - HLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s); - | CicEnvironment.Object_not_found uri -> - let depend = UriManager.name_of_uri uri in - HLog.message - ("Unable to create projection " ^ name ^ " because it requires " ^ - depend) - ) projections fields; - !uris - with exn -> - List.iter remove_single_obj !uris; - raise exn - -let build_inversion_principle = ref (fun a b -> assert false);; - -let generate_inversion refinement_toolkit uri obj = - List.map - (fun (ind_uri,ind_obj) -> - add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri) - (!build_inversion_principle uri obj) - -let - generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid -= - function - Cic.Fix (_,funs) -> - snd ( - List.fold_right - (fun (name,idx,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.Fix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - (add_single_obj uri obj refinement_toolkit; - (n-1,uri::uris))) - funs (List.length funs,[])) - | Cic.CoFix (_,funs) -> - snd ( - List.fold_right - (fun (name,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.CoFix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj uri obj refinement_toolkit; - (n-1,uri::uris) - ) funs (List.length funs,[])) - | _ -> assert false - -let add_obj refinement_toolkit uri obj = - add_single_obj uri obj refinement_toolkit; - let uris = ref [] in - let not_debug = not (Helm_registry.get_bool "matita.debug") in - try - begin - match obj with - | Cic.Constant (name,Some bo,_,_,attrs) when - List.mem (`Flavour `MutualDefinition) attrs -> - uris := - !uris @ - generate_sibling_mutual_definitions refinement_toolkit uri attrs - name bo - | Cic.Constant _ -> () - | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> - let _,inductive,_,_ = List.hd inductivefuns in - if inductive then - begin - uris := !uris @ - generate_elimination_principles uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit uri obj; - end ; - let rec get_record_attrs = - function - | [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - | None -> () (* not a record *) - | Some fields -> - uris := !uris @ - (generate_projections refinement_toolkit uri fields)) - | Cic.CurrentProof _ - | Cic.Variable _ -> assert false - end; - UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; - !uris - with - | exn when not_debug -> - List.iter remove_single_obj !uris; - raise exn - -let remove_obj uri = - let uris = - try - let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in - UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri; - res - with - Not_found -> [] (*assert false*) - in - List.iter remove_single_obj (uri::uris) - diff --git a/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli index 13a6479bd..bfab37330 100644 --- a/helm/software/components/library/librarySync.mli +++ b/helm/software/components/library/librarySync.mli @@ -25,22 +25,25 @@ exception AlreadyDefined of UriManager.uri -val set_object_declaration_hook : (UriManager.uri -> Cic.obj -> unit) -> unit +type coercion_decl = + UriManager.uri -> int (* arity *) -> + int (* saturations *) -> string (* baseuri *) -> + UriManager.uri list (* lemmas (new objs) *) -(* this is a pointer to the function which builds the inversion principle *) -val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref +(* the add_single_obj fun passed to the callback can raise AlreadyDefined *) +val add_object_declaration_hook : + (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) -> + add_coercion:coercion_decl -> + UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) (* it returns the list of the uris of the auxiliary lemmas generated *) val add_obj: - RefinementTool.kit -> - UriManager.uri -> Cic.obj -> + UriManager.uri -> Cic.obj -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> UriManager.uri list -(* inverse of add_obj; *) -(* Warning: it does not remove the dependencies on the object and on its *) -(* auxiliary lemmas! *) +(* removes an object (does not remove its associated lemmas) *) val remove_obj: UriManager.uri -> unit (* Informs the library that [uri] is a coercion. *) @@ -48,17 +51,9 @@ val remove_obj: UriManager.uri -> unit (* is true are added to the library. *) (* The list of added objects is returned. *) val add_coercion: - add_composites:bool -> - RefinementTool.kit -> UriManager.uri -> int (* arity *) -> - int (* saturations *) -> string (* baseuri *) -> - (UriManager.uri * int * int * int) list (* URI, arity, saturations, cpos *) - -(* 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 + add_composites:bool -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> coercion_decl -(* this is used when resetting, but the more gracefull push/pop can be used to - * suspend/resume an execution *) -val remove_all_coercions: unit -> unit +(* these just push/pop the coercions database, since the library is not + * pushable/poppable *) val push: unit -> unit val pop: unit -> unit diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 83d706542..ebf4cbc2a 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -89,8 +89,6 @@ let get_closure_coercions src tgt uri coercions = | _ -> [] (* do not close in case source or target is not an indty ?? *) ;; -let obj_attrs n = [`Class (`Coercion n); `Generated] - exception UnableToCompose (* generate_composite (c2 (c1 s)) in the universe graph univ @@ -364,7 +362,7 @@ let build_obj c univ arity = let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],[`Generated]) in obj,univ ;; @@ -403,15 +401,7 @@ let number_if_already_defined buri name l = let suffix = if n > 0 then string_of_int n else "" in let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in let uri = UriManager.uri_of_string suri in - let retry () = - if n < 100 then - begin - HLog.warn ("Uri " ^ suri ^ " already exists."); - aux (n+1) - end - else - err () - in + let retry () = if n < max_int then aux (n+1) else err () in if List.exists (UriManager.eq uri) l then retry () else try @@ -443,7 +433,7 @@ let close_coercion_graph src tgt uri saturations baseuri = | (he,saturations1,arity1) :: tl -> let first_step = Cic.Constant ("", Some (CicUtil.term_of_uri he), - Cic.Sort Cic.Prop, [], obj_attrs arity1), + Cic.Sort Cic.Prop, [], [`Generated]), saturations1, arity1,0 in diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml index 484497803..eb3201c58 100644 --- a/helm/software/components/tactics/fourierR.ml +++ b/helm/software/components/tactics/fourierR.ml @@ -439,8 +439,8 @@ let fourier_lineq lineq1 = let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> Hashtbl.iter (fun x c -> - try (Hashtbl.find hvar x;()) - with _-> nvar:=(!nvar)+1; + try ignore(Hashtbl.find hvar x) + with Not_found -> nvar:=(!nvar)+1; Hashtbl.add hvar x (!nvar); debug("aggiungo una var "^ string_of_int !nvar^" per "^ diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index 0f50116cb..ae0a48186 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -129,104 +129,103 @@ let rec build_theorem rightparam_tys arity_l (*arity_l only to name p's*) [(Cic.Rel 1)] uri typeno ) ;; -let build_inversion uri obj = - (*uri e obj of InductiveDefinition *) - let module PET = ProofEngineTypes in - let build_one typeno name nleft arity cons_list = - (*check if there are right parameters, else return void*) - if List.length (list_of_prod arity) = (nleft + 1) then - None +let build_inversion ~add_obj ~add_coercion uri obj = + match obj with + | Cic.InductiveDefinition (tys,_,nleft,attrs) -> + let _,inductive,_,_ = List.hd tys in + if not inductive then [] else - try - let arity_l = cut_last (list_of_prod arity) in - let rightparam_tys = cut_first nleft arity_l in - let theorem = build_theorem rightparam_tys arity_l arity cons_list - [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in - debug_print - (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); - let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem - CicUniv.oblivion_ugraph in - (*DEBUG*) debug_print - (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); - let buri = UriManager.buri_of_uri uri in - let inversor_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in - let goal = CicMkImplicit.new_meta metasenv [] in - let metasenv' = (goal,[],ref_theorem)::metasenv in - let attrs = [`Class (`InversionPrinciple); `Generated] in - let _subst = [] in - let proof= - (Some inversor_uri,metasenv',_subst, - lazy (Cic.Meta(goal,[])),ref_theorem, attrs) in - let _,applies = - List.fold_right - (fun _ (i,applies) -> - i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies) - cons_list (2,[]) - in - let proof1,gl1 = - PET.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ()) - (*if the number of applies is 1, we cannot use - thens, but then_*) - ~continuation: - (match (List.length applies) with - 0 -> (Inversion.private_inversion_tac (Cic.Rel 1)) - | 1 -> (Tacticals.then_ - ~start:(Inversion.private_inversion_tac - (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac - (Cic.Rel 2)) - ) - | _ -> (Tacticals.thens - ~start:(Inversion.private_inversion_tac - (Cic.Rel 1)) - ~continuations:applies - ) - )) - (proof,goal) - in - let metasenv,bo,ty, attrs = - match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs - in + let build_one typeno name nleft arity cons_list = + (*check if there are right parameters, else return void*) + if List.length (list_of_prod arity) = (nleft + 1) then + None + else + try + let arity_l = cut_last (list_of_prod arity) in + let rightparam_tys = cut_first nleft arity_l in + let theorem = build_theorem rightparam_tys arity_l arity cons_list + [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in + debug_print + (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem))); + let (ref_theorem,_,metasenv,_) = + CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in + (*DEBUG*) debug_print + (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem))); + let buri = UriManager.buri_of_uri uri in + let inversor_uri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in + let goal = CicMkImplicit.new_meta metasenv [] in + let metasenv' = (goal,[],ref_theorem)::metasenv in + let attrs = [`Class (`InversionPrinciple); `Generated] in + let _subst = [] in + let proof= + Some inversor_uri,metasenv',_subst, + lazy (Cic.Meta(goal,[])),ref_theorem, attrs in + let _,applies = + List.fold_right + (fun _ (i,applies) -> + i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies + ) cons_list (2,[]) in + let proof1,gl1 = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ()) + (*if the number of applies is 1, we cannot use + thens, but then_*) + ~continuation: + (match List.length applies with + 0 -> Inversion.private_inversion_tac (Cic.Rel 1) + | 1 -> + Tacticals.then_ + ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) + ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) + | _ -> + Tacticals.thens + ~start:(Inversion.private_inversion_tac (Cic.Rel 1)) + ~continuations:applies)) + (proof,goal) in + let _,metasenv,_subst,bo,ty, attrs = proof1 in assert (metasenv = []); Some - (inversor_uri, - Cic.Constant - (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) - with - Inversion.EqualityNotDefinedYet -> None - | CicRefine.RefineFailure ls -> + (inversor_uri, + Cic.Constant + (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[])) + with + Inversion.EqualityNotDefinedYet -> + HLog.warn "No default equality, no inversion principle"; + None + | CicRefine.RefineFailure ls -> HLog.warn ("CicRefine.RefineFailure during generation of inversion principle: " ^ Lazy.force ls) ; None - | CicRefine.Uncertain ls -> + | CicRefine.Uncertain ls -> HLog.warn ("CicRefine.Uncertain during generation of inversion principle: " ^ Lazy.force ls) ; None - | CicRefine.AssertFailure ls -> + | CicRefine.AssertFailure ls -> HLog.warn ("CicRefine.AssertFailure during generation of inversion principle: " ^ Lazy.force ls) ; None - in - match obj with - | Cic.InductiveDefinition (tys,_,nleft,_) -> - let counter = ref (List.length tys) in - List.fold_right - (fun (name,_,arity,cons_list) res -> - counter := !counter-1; - match build_one !counter name nleft arity cons_list with - | None -> res - | Some inv -> inv::res) - tys [] - |_ -> assert false - + in + let counter = ref (List.length tys) in + let all_inverters = + List.fold_right + (fun (name,_,arity,cons_list) res -> + counter := !counter-1; + match build_one !counter name nleft arity cons_list with + None -> res + | Some inv -> inv::res + ) tys [] + in + List.fold_left + (fun lemmas (uri,obj) -> add_obj uri obj @ uri :: lemmas + ) [] all_inverters + | _ -> [] ;; -let init () = ();; -LibrarySync.build_inversion_principle := build_inversion;; +let init () = + LibrarySync.add_object_declaration_hook build_inversion;; diff --git a/helm/software/components/tactics/inversion_principle.mli b/helm/software/components/tactics/inversion_principle.mli index 7cdf29c24..30335ed6c 100644 --- a/helm/software/components/tactics/inversion_principle.mli +++ b/helm/software/components/tactics/inversion_principle.mli @@ -1 +1,27 @@ +(* Copyright (C) 2002, 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://cs.unibo.it/helm/. + *) + +(* $Id: primitiveTactics.ml 9014 2008-09-26 08:03:47Z tassi $ *) val init: unit -> unit diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index 12790dd0e..8a6abcf5a 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -48,10 +48,10 @@ matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matitaMathView.cmi matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaAutoGui.cmi buildTimeConf.cmo applyTransformation.cmi + buildTimeConf.cmo applyTransformation.cmi matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaAutoGui.cmx buildTimeConf.cmx applyTransformation.cmx + buildTimeConf.cmx applyTransformation.cmx matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \ applyTransformation.cmi matitaScript.cmi diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index ac044cefe..e741ed70c 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -280,7 +280,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = in if real then do_it obj else let newuri = discharge_uri style uri in - let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in + let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in do_it obj with | TC.TypeCheckerFailure s -> diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma index 84cde74dd..e22402d9f 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma @@ -55,6 +55,7 @@ definition setoid1_of_setoid: setoid → setoid1. qed. coercion setoid1_of_setoid. +prefer coercion Type_OF_setoid. definition reflexive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x. definition symmetric2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x. @@ -85,6 +86,10 @@ definition setoid2_of_setoid1: setoid1 → setoid2. qed. coercion setoid2_of_setoid1. +prefer coercion Type_OF_setoid2. +prefer coercion Type_OF_setoid. +prefer coercion Type_OF_setoid1. +(* we prefer 0 < 1 < 2 *) interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y). interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y). diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index 8ff55d0d6..ca3d0379b 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -137,6 +137,8 @@ qed. interpretation "o-algebra binary meet" 'and a b = (fun21 ___ (binary_meet _) a b). +prefer coercion Type1_OF_OAlgebra. + definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O. intros; split; [ intros (p q); @@ -151,8 +153,6 @@ qed. interpretation "o-algebra binary join" 'or a b = (fun21 ___ (binary_join _) a b). -coercion Type1_OF_OAlgebra nocomposites. - lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q). (* next change to avoid universe inconsistency *) change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O); @@ -260,15 +260,17 @@ qed. coercion umorphism_setoid_OF_ORelation_setoid. lemma uncurry_arrows : ∀B,C. ORelation_setoid B C → B → C. -intros; apply ((fun11 ?? t) t1); +intros; apply (t t1); qed. coercion uncurry_arrows 1. +(* lemma hint6: ∀P,Q. Type_OF_setoid2 (hint5 P ⇒ hint5 Q) → unary_morphism1 P Q. intros; apply t; qed. coercion hint6. +*) notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}. notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index 873a9df60..68b9befb8 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -116,9 +116,9 @@ definition continuous_relation_comp: intros (o1 o2 o3 r s); constructor 1; [ apply (s ∘ r); | intros; - apply sym1; + apply sym1; change in match ((s ∘ r) U) with (s (r U)); - (**) unfold FunClass_1_OF_Type_OF_setoid2; + (**) unfold FunClass_1_OF_Type_OF_setoid21; unfold objs2_OF_basic_topology1; unfold hint; letin reduced := reduced; clearbody reduced; unfold uncurry_arrows in reduced ⊢ %; (**) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma index 57ec577ae..b00521633 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma @@ -92,11 +92,12 @@ definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → λCS1,CS2,c.rp ?? c. coercion rp''. -definition rp''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ + +definition rp''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝ λCS1,CS2,c.rp ?? c. coercion rp'''. -definition rp'''': ∀CS1,CS2.Type_OF_setoid2 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝ +definition rp'''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝ λCS1,CS2,c.rp ?? c. coercion rp''''. @@ -140,7 +141,7 @@ definition CSPA: category2. change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12); apply rule ASSOC; | intros; simplify; - change with (a ∘ id2 ? o1 = a); + change with (a ∘ id2 BP o1 = a); apply (id_neutral_right2 : ?); | intros; simplify; change with (id2 ? o2 ∘ a = a); diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma index e661fbfd0..856a7e0ae 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma @@ -108,7 +108,7 @@ lemma orelation_of_relation_preserves_equality: apply (. #‡(e‡#)); ] qed. -lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2). +lemma hint: ∀o1,o2:OA. Type_OF_setoid21 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2). intros; apply t; qed. coercion hint. @@ -136,12 +136,12 @@ lemma orelation_of_relation_preserves_identity: | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros; change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;] qed. - -lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T). +(* +lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid21 (arrows2 OA S T). intros; apply c; qed. coercion hint2. - +*) (* CSC: ???? forse un uncertain mancato *) lemma orelation_of_relation_preserves_composition: ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3. @@ -156,9 +156,11 @@ lemma orelation_of_relation_preserves_composition: split; [ assumption | exists; [apply w] split; assumption ] | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ] split; [ exists; [apply w] split; assumption | assumption ] - | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] + | unfold arrows1_OF_ORelation_setoid; + cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ] split; [ assumption | exists; [apply w] split; assumption ] - | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ] + | unfold arrows1_OF_ORelation_setoid in e; + cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ] split; [ exists; [apply w] split; assumption | assumption ] | whd; intros; apply f; exists; [ apply y] split; assumption; | cases f1; clear f1; cases x; clear x; apply (f w); assumption;] diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 804009ef5..46609ad4c 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,6 +1,9 @@ 0.5.7 - .../01/2009 - Pàdoa release - * declaring a coercion twice now makes it the first choice - (reordering) + * generation of derived lemmas rewritten to be based on hooks that + are triggered every definition + * composition of coercions fixed, more composite are generated + * undo mechanism for coercions remade, should work better + * new command "prefer coercion foo" to reorder coercions. * UTF-8 eq classes and virtuals described in the manual and consistently printed in the TeX/UTF-8 table * added a memory system for UTF-8 equivalence classes, so that diff --git a/helm/software/matita/dump_moo.ml b/helm/software/matita/dump_moo.ml index 54eaea4ba..6b8658abd 100644 --- a/helm/software/matita/dump_moo.ml +++ b/helm/software/matita/dump_moo.ml @@ -52,8 +52,8 @@ let _ = (fun cmd -> printf " %s\n%!" (GrafiteAstPp.pp_command - ~term_pp:(fun _ -> assert false) - ~obj_pp:(fun _ -> assert false) cmd)) + ~term_pp:(fun t -> CicPp.ppterm t) + ~obj_pp:(fun _ -> "OBJ") cmd)) commands; end) (List.rev !moos) diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index 102e375ad..19685bf90 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -100,6 +100,31 @@ + + prefer coercion + prefer coercion u + + + + Synopsis: + + + prefer coercion + (&uri; | &term;) + + + + + Action: + + The already declared coercion u + is preferred to other coercions with the same source and target. + + + + + + coercion coercion u with ariety saturation nocomposites diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index c76046c75..949d412a5 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -28,6 +28,7 @@ and as coercion + prefer nocomposites coinductive corec diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 9fa70e11f..b3963bf02 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -157,7 +157,7 @@ let _ = (fun cmd -> prerr_endline (GrafiteAstPp.pp_command - ~term_pp:(fun _ -> assert false) + ~term_pp:(fun t -> CicPp.ppterm t) ~obj_pp:(fun _ -> assert false) cmd)) (List.rev moo)); diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 2655798a9..f75cbcf48 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -280,4 +280,8 @@ let initialize_environment () = status := initialize_environment !status let _ = - Inversion_principle.init () + CicFix.init (); + Inversion_principle.init (); + CicRecord.init (); + CicElim.init () +;; diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index a9172cee5..ff9fb1d73 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -180,10 +180,10 @@ let activate_extraction baseuri fname = let f = open_out (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in - LibrarySync.set_object_declaration_hook - (fun _ obj -> + LibrarySync.add_object_declaration_hook + (fun ~add_obj ~add_coercion _ obj -> output_string f (CicExportation.ppobj baseuri obj); - flush f); + flush f; []); ;; let compile options fname = -- 2.39.2