(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.AutoBatch (_,params) ->
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
- | GrafiteAst.Cases (_, what, (howmany, names)) ->
+ | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
- what
+ ~pattern what
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations) =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations)
+let coercion_moo_statement_of (uri,arity, saturations,_) =
+ GrafiteAst.Coercion
+ (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
let refinement_toolkit = {
RefinementTool.type_of_aux' =
}
let eval_coercion status ~add_composites uri arity saturations =
+ let uri =
+ try CicUtil.uri_of_term uri
+ with Invalid_argument _ ->
+ raise (Invalid_argument "coercion can only be constants/constructors")
+ in
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
saturations (GrafiteTypes.get_baseuri status)
in
let moo_content =
- List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
+ List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- List.map (fun u,_,_ -> u) compounds
+ List.map (fun u,_,_,_ -> u) compounds
module MatitaStatus =
struct
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
else
None)
lemmas)
} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
~disambiguate_macro opts status (text,prefix_len,ex) ->
match ex with
- | GrafiteAst.Tactic (_, Some tac, punct) ->
+ | GrafiteAst.Tactic (_(*loc*), Some tac, punct) ->
let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
let status = eval_tactical status (tactic_of_ast' tac) in
+ (* CALL auto on every goal, easy way of testing it
+ let auto =
+ GrafiteAst.AutoBatch
+ (loc, ([],["depth","2";"timeout","1";"type","1"])) in
+ (try
+ let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in
+ let _ = eval_tactical status (tactic_of_ast' auto) in
+ print_endline "GOOD"; ()
+ with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());
+ *)
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
| GrafiteAst.Tactic (_, None, punct) ->