end else
FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-let tactic_of_ast ast =
+let tactic_of_ast status ast =
let module PET = ProofEngineTypes in
match ast with
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
+ ~universe:status.GrafiteTypes.universe
| GrafiteAst.Assumption _ -> Tactics.assumption
| GrafiteAst.Auto (_,params) ->
AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())
+ ~universe:status.GrafiteTypes.universe
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
let proof = GrafiteTypes.get_current_proof status in
let proof_status = proof, goal in
let needs_reordering, always_opens_a_goal = classify_tactic tactic in
- let tactic = tactic_of_ast tactic in
+ let tactic = tactic_of_ast status tactic in
(* apply tactic will change the lexicon_status ... *)
(* prerr_endline "apply_tactic bassa"; *)
let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
let status,uris =
match cmd with
+ | GrafiteAst.Index (loc,None,uri) ->
+ assert false (* TODO: for user input *)
+ | GrafiteAst.Index (loc,Some key,uri) ->
+ let universe = Universe.index
+ status.GrafiteTypes.universe key (CicUtil.term_of_uri uri) in
+ let status = {status with GrafiteTypes.universe = universe} in
+(* debug
+ let msg =
+ let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
+ ("candidates for " ^ (CicPp.ppterm key) ^ " = " ^
+ (String.concat "\n" (List.map CicPp.ppterm candidates)))
+ in
+ prerr_endline msg;
+*)
+ let status = GrafiteTypes.add_moo_content [cmd] status in
+ status,[]
| GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
eval_coercion status ~add_composites uri arity
| GrafiteAst.Default (loc, what, uris) as cmd ->
raise (IncludedFileNotCompiled (moopath_rw,baseuri))
in
let status = eval_from_moo.efm_go status moopath in
+(* debug
+ let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
+ let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+ let nat = Cic.MutInd(nat_uri,0,[]) in
+ let zero = Cic.MutConstruct(nat_uri,0,1,[]) in
+ let succ = Cic.MutConstruct(nat_uri,0,2,[]) in
+ let fake= Cic.Meta(-1,[]) in
+ let term= Cic.Appl [Cic.Const (lt_uri,[]);zero;Cic.Appl[succ;zero]] in let msg =
+ let candidates = Universe.get_candidates status.GrafiteTypes.universe term in
+ ("candidates for " ^ (CicPp.ppterm term) ^ " = " ^
+ (String.concat "\n" (List.map CicPp.ppterm candidates)))
+ in
+ prerr_endline msg;
+*)
status,[]
| GrafiteAst.Print (_,"proofterm") ->
let _,_,p,_ = GrafiteTypes.get_current_proof status in
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some bo,ty,[],[]) in
let status, lemmas = add_obj uri obj status in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ {status with
+ GrafiteTypes.proof_status = GrafiteTypes.No_proof},
uri::lemmas
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
Setoids.add_relation id a aeq refl sym trans;
open Printf
+let uris_for_inductive_type uri obj =
+ match obj with
+ | Cic.InductiveDefinition(types,_,_,_) ->
+ let suri = UriManager.string_of_uri uri in
+ let uris,_ =
+ List.fold_left
+ (fun (acc,i) (_,_,_,constructors)->
+ let is = string_of_int i in
+ let newacc,_ =
+ List.fold_left
+ (fun (acc,j) _ ->
+ let js = string_of_int j in
+ UriManager.uri_of_string
+ (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1)
+ (acc,1) constructors
+ in
+ newacc,i+1)
+ ([],1) types
+ in uris
+ | _ -> [uri]
+
let add_obj refinement_toolkit uri obj status =
let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
- {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
+ 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 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 universe,status =
+ List.fold_left add_to_universe
+ (status.GrafiteTypes.universe,status)
+ ((uris_for_inductive_type uri obj)@lemmas) in
+ {status with
+ GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
+ GrafiteTypes.universe = universe},
lemmas
let add_coercion refinement_toolkit ~add_composites status uri arity =
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 (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
+ List.iter LibrarySync.remove_obj objs_to_remove
let init () =
LibrarySync.remove_all_coercions ();
options = GrafiteTypes.no_options;
objects = [];
coercions = [];
+ universe = Universe.empty;
}
projects / helm.git / commitdiff