| `Unfold what -> Tactics.unfold ~pattern what
| `Whd -> Tactics.whd ~pattern)
| GrafiteAst.Reflexivity _ -> Tactics.reflexivity
- | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos
| GrafiteAst.Replace (_, pattern, with_what) ->
Tactics.replace ~pattern ~with_what
| GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
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 = {
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.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