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
| 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
| 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
| 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
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
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
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
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 = {
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
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)
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,[]
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!"))
(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;
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);
("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
projects / helm.git / blobdiff