- 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)
]
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
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)
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
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]
-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
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
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));
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
;;
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"
+ ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
+ <TR><TD BGCOLOR=\"gray95\">Source</TD>
+ <TD BGCOLOR=\"gray95\">Target</TD>
+ <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
+ String.concat "</TR>"
+ (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
+ "<TR><TD>" ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
+ String.concat "," names ^ "</TD>")
+ (List.sort (fun (x,y,_) (x1,y1,_) ->
+ let rc = compare x x1 in
+ if rc = 0 then compare y y1 else rc) l))
+ ^ "</TR></TABLE></FONT>")
+ (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 ->
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
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
(** 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
| 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
| 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) ->
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
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) ->
*)
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) ->
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
(* the new status and generated objects, if any *)
GrafiteTypes.status * UriManager.uri list
-val refinement_toolkit: RefinementTool.kit
([],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
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
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
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
;;
*)
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
(*
(* 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;
}
| 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;
}
| l, _ ->
let debug =
Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
- msg (List.length l)
+ msg (List.length l)
in
HLog.debug debug; assert false
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
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
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 =
| 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 _
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 ->
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
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 \
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
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 \
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
| _ ->
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;;
* 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
--- /dev/null
+(* 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;;
--- /dev/null
+(* 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/
+ *)
+
+val init : unit -> unit
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;;
* 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
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
| 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
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;
+;;
(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
(coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
val is_a_coercion: Cic.term -> coercion_entry option
+
+val prefer: UriManager.uri -> unit
(* $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
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
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))
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
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
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)
-
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. *)
(* 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
+++ /dev/null
-(* Copyright (C) 2006, 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/
- *)
-
-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;
-}
-
| _ -> [] (* 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
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
;;
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
| (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
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 "^
[(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;;
+(* 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
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
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 ->
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.
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).
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);
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);
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}.
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));
- (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid2;
+ (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid21;
unfold objs2_OF_basic_topology1; unfold hint;
letin reduced := reduced; clearbody reduced;
unfold uncurry_arrows in reduced ⊢ %; (*</BAD>*)
λ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''''.
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);
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.
| 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.
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;]
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
(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)
</variablelist>
</para>
</sect1>
+ <sect1 id="command_prefer_coercion">
+ <title>prefer coercion</title>
+ <para><userinput>prefer coercion u</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para>
+ <emphasis role="bold">prefer coercion</emphasis>
+ (&uri; | &term;)
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>The already declared coercion <command>u</command>
+ is preferred to other coercions with the same source and target.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
<sect1 id="command_coercion">
<title>coercion</title>
<para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
<keyword>and</keyword>
<keyword>as</keyword>
<keyword>coercion</keyword>
+ <keyword>prefer</keyword>
<keyword>nocomposites</keyword>
<keyword>coinductive</keyword>
<keyword>corec</keyword>
(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));
status := initialize_environment !status
let _ =
- Inversion_principle.init ()
+ CicFix.init ();
+ Inversion_principle.init ();
+ CicRecord.init ();
+ CicElim.init ()
+;;
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 =
projects / helm.git / commitdiff