X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=4c177fee76d3c6245ec47091af00f15427c733a7;hb=8ae990161006978a019f0afda4ff8d56a78d1fd0;hp=4539029af26e1b6d276904701c2a414d81693cc7;hpb=be292a08ee0c8792b21105952626da05d5f645b9;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 4539029af..4c177fee7 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -56,16 +56,21 @@ 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.Cases (_, what, names) -> + Tactics.cases_intros ~mk_fresh_name_callback:(namer_of names) + what | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id @@ -75,20 +80,16 @@ let tactic_of_ast ast = | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = LibraryDb.instance () in + | GrafiteAst.Decompose (_, names) -> let mk_fresh_name_callback = namer_of names in - Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what - | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) + Tactics.decompose ~mk_fresh_name_callback () + | GrafiteAst.Demodulate _ -> + Tactics.demodulate + ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Destruct (_,term) -> Tactics.destruct term - | GrafiteAst.Elim (_, what, using, depth, names) -> + | GrafiteAst.Elim (_, pattern, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what + pattern | GrafiteAst.ElimType (_, what, using, depth, names) -> Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what @@ -146,8 +147,8 @@ let tactic_of_ast ast = | GrafiteAst.Reflexivity _ -> Tactics.reflexivity | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what - | GrafiteAst.Rewrite (_, direction, t, pattern) -> - EqualityTactics.rewrite_tac ~direction ~pattern t + | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> + EqualityTactics.rewrite_tac ~direction ~pattern t names | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring | GrafiteAst.Split _ -> Tactics.split @@ -158,20 +159,27 @@ let tactic_of_ast ast = | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1 | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) -> - Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) t ty id t1 + Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe t ty id t1 | GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove t id t2 - | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) t + | GrafiteAst.Bydone (_, t) -> + Declarative.bydone ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe t + | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> + Declarative.we_proceed_by_cases_on t t1 | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> Declarative.we_proceed_by_induction_on t t1 | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) -> - Declarative.existselim t id1 t1 id2 t2 + Declarative.existselim ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> - Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) termine t1 t2 cont + Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) + ~universe:status.GrafiteTypes.universe termine t1 t2 cont let classify_tactic tactic = match tactic with @@ -304,7 +312,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 @@ -317,7 +325,7 @@ prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) let proof, opened_goals = if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty = proof in + let uri, metasenv_after_tactic, t, ty, attrs = proof in (* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) let reordered_metasenv, opened_goals = reorder_metasenv @@ -325,7 +333,7 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, t, ty in + let proof' = uri, reordered_metasenv, t, ty, attrs in (* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) proof', opened_goals end @@ -410,7 +418,7 @@ type 'a eval_executable = type 'a eval_from_moo = { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } -let coercion_moo_statement_of arity uri = +let coercion_moo_statement_of (uri,arity) = GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity) let refinement_toolkit = { @@ -436,16 +444,17 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri arity = +let eval_coercion status ~add_composites uri arity baseuri = let status,compounds = GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity + baseuri in let moo_content = - List.map (coercion_moo_statement_of arity) (uri::compounds) + List.map coercion_moo_statement_of ((uri,arity)::compounds) in let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - compounds + List.map fst compounds let eval_tactical ~disambiguate_tactic status tac = let apply_tactic = apply_tactic ~disambiguate_tactic in @@ -588,9 +597,9 @@ let add_coercions_of_record_to_moo obj lemmas status = in let is_a_coercion, arity_coercion = is_a_coercion uri in if is_a_coercion then - Some (uri, coercion_moo_statement_of arity_coercion uri) + Some (uri, coercion_moo_statement_of (uri,arity_coercion)) else if is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of arity_wanted uri) + Some (uri, coercion_moo_statement_of (uri,arity_wanted)) else None) lemmas) @@ -617,8 +626,25 @@ 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 + (GrafiteTypes.get_string_option status "baseuri") | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] @@ -636,18 +662,32 @@ 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 + let _,_,p,_, _ = GrafiteTypes.get_current_proof status in print_endline (AutoTactic.pp_proofterm p); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = + let uri, metasenv, bo, ty, attrs = match status.GrafiteTypes.proof_status with - | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | GrafiteTypes.Proof (None, metasenv, body, ty) -> + | GrafiteTypes.Proof (Some uri, metasenv, body, ty, attrs) -> + uri, metasenv, body, ty, attrs + | GrafiteTypes.Proof (None, metasenv, body, ty, attrs) -> raise (GrafiteTypes.Command_error ("Someone allows to start a theorem without giving the "^ "name/uri. This should be fixed!")) @@ -660,9 +700,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (GrafiteTypes.Command_error "Proof not completed! metasenv is not empty!"); let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name,Some bo,ty,[],[]) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) 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}, + (*CSC: I throw away the arities *) uri::lemmas | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; @@ -710,7 +752,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> + | Cic.CurrentProof (_,metasenv',bo,ty,_, attrs) -> let name = UriManager.name_of_uri uri in if not(CicPp.check name ty) then HLog.error ("Bad name: " ^ name); @@ -742,7 +784,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ("Theorem already proved: " ^ UriManager.string_of_uri x ^ "\nPlease use a variant.")); end; - let initial_proof = (Some uri, metasenv', bo, ty) in + let initial_proof = (Some uri, metasenv', bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof