| 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, Some 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
+ Tactics.decompose ~mk_fresh_name_callback ()
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| 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.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) ->
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)
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,[]
*)
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},
+ (*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