From 67cf4ce16c346991c8eda71576414f5c6324ab82 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Nov 2006 14:06:57 +0000 Subject: [PATCH] The status has been extended with a "universe", that is a discrimination-tree structure indexing all defined objects. The universe is functional (hope so). --- components/grafite_engine/grafiteEngine.ml | 39 ++++++++++++-- components/grafite_engine/grafiteSync.ml | 63 ++++++++++++++++++++-- components/grafite_engine/grafiteTypes.ml | 1 + components/grafite_engine/grafiteTypes.mli | 3 +- 4 files changed, 99 insertions(+), 7 deletions(-) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 4539029af..582ad112d 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -56,16 +56,18 @@ let namer_of names = 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 @@ -304,7 +306,7 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = 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 @@ -617,6 +619,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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 -> @@ -636,6 +654,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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 @@ -662,7 +694,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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; diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index 7b4bdfb5e..9581dc9d6 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -27,9 +27,65 @@ 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 = @@ -60,8 +116,8 @@ let time_travel ~present ~past = 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 (); @@ -72,4 +128,5 @@ let init () = options = GrafiteTypes.no_options; objects = []; coercions = []; + universe = Universe.empty; } diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml index 0d59e4b46..6e1c299e4 100644 --- a/components/grafite_engine/grafiteTypes.ml +++ b/components/grafite_engine/grafiteTypes.ml @@ -57,6 +57,7 @@ type status = { options: options; objects: UriManager.uri list; coercions: UriManager.uri list; + universe:Universe.universe; } let get_current_proof status = diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli index a8b86c276..b26c0ca21 100644 --- a/components/grafite_engine/grafiteTypes.mli +++ b/components/grafite_engine/grafiteTypes.mli @@ -53,7 +53,8 @@ type status = { proof_status: proof_status; (** logical status *) options: options; objects: UriManager.uri list; (** in-scope objects *) - coercions: UriManager.uri list; (** defined coercions *) + coercions: UriManager.uri list; (** defined coercions *) + universe:Universe.universe; (** universe of terms used by auto *) } val dump_status : status -> unit -- 2.39.2