open Printf
+let is_a_variant obj =
+ match obj with
+ | Cic.Constant(_,_,_,_,attrs) ->
+ List.exists (fun x -> x = `Flavour `Variant) attrs
+ | _ -> false
+
let uris_for_inductive_type uri obj =
match obj with
| Cic.InductiveDefinition(types,_,_,_) ->
([],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.empty_ugraph in
-(* prop filtering
- let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_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 ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph 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
(universe,status)
in
+ let uris_to_index =
+ if is_a_variant obj then []
+ else (uris_for_inductive_type uri obj) @ lemmas
+ in
let universe,status =
List.fold_left add_to_universe
(status.GrafiteTypes.universe,status)
- ((uris_for_inductive_type uri obj)@lemmas) in
+ 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 compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity 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 add_coercion ~pack_coercion_obj ~add_composites status uri arity
+ saturations baseuri
+=
+ 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 init () =
- LibrarySync.remove_all_coercions ();
- LibraryObjects.reset_defaults ();
- {
+let initial_status lexicon_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;
+ ng_status = GrafiteTypes.CommandMode lexicon_status;
}
+
+
+let init baseuri =
+ CoercDb.restore CoercDb.empty_coerc_db;
+ LibraryObjects.reset_defaults ();
+ initial_status baseuri
+ ;;
+let pop () =
+ LibrarySync.pop ();
+ LibraryObjects.pop ()
+;;
+
+let push () =
+ LibrarySync.push ();
+ LibraryObjects.push ()
+;;
+