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 ())
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 ->
GrafiteTypes.status * UriManager.uri list
}
+type 'a eval_comment =
+ {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
+ disambiguate_command:
+ (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
+ GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
+ options -> GrafiteTypes.status ->
+ (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
+ GrafiteTypes.status * UriManager.uri list
+ }
+
type 'a eval_executable =
{ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
disambiguate_tactic:
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 ->
RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
}
-
+
+let eval_unification_hint status t =
+ (* XXX no undo *)
+ NCicUnifHint.add_user_provided_hint t;
+ status,[]
+;;
+
let eval_coercion status ~add_composites uri arity saturations =
let uri =
try CicUtil.uri_of_term uri
in
status
-let eval_comment status c = status
-
(* since the record syntax allows to declare coercions, we have to put this
* 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 ->
status,[]
| GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
eval_coercion status ~add_composites uri arity saturations
+ | GrafiteAst.UnificationHint (loc, t) ->
+ eval_unification_hint status t
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Executable (_,ex) ->
eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
~disambiguate_macro opts status (text,prefix_len,ex)
- | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[]
+ | GrafiteAst.Comment (_,c) ->
+ eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c)
+} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) ->
+ status, []
}
+;;
+
let eval_ast = eval_ast.ea_go