exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
type 'a disambiguator_input = string * int * 'a
(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyRule (_, 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
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
options ->
GrafiteTypes.status ->
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations) =
+let coercion_moo_statement_of (uri,arity, saturations,_) =
GrafiteAst.Coercion
(HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
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
* information inside the moo *)
let add_coercions_of_record_to_moo obj lemmas status =
let attributes = CicUtil.attributes_of_obj obj in
- let is_record = function `Class (`Record att) -> Some att | _-> None in
+ let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
match HExtlib.list_findopt is_record attributes with
| None -> status,[]
| Some fields ->
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)
status,[]
| GrafiteAst.Print (_,"proofterm") ->
let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
- prerr_endline (Auto.pp_proofterm p);
+ prerr_endline (Auto.pp_proofterm (Lazy.force p));
status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Qed loc ->
(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,[],attrs) in
+ let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
let status, lemmas = add_obj uri obj status in
{status with
GrafiteTypes.proof_status = GrafiteTypes.No_proof},
"\nPlease use a variant."));
end;
let _subst = [] in
- let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in
+ let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
} 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) ->