exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
-exception Macro of
- GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
+ (GrafiteAst.command) disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
- disambiguator_input ->
+(* (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) *)
+ GrafiteAst.statement disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
}
type 'a eval_command =
{ec_go: 'term 'obj.
disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
+ (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
options -> GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
+ GrafiteAst.command disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.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 -> GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
+ options -> GrafiteTypes.status -> GrafiteAst.comment disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
}
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
+ GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
options ->
- GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
+ GrafiteTypes.status -> GrafiteAst.code disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
}
status,`New []
;;
+(* Not used
let eval_ng_punct (_text, _prefix_len, punct) =
match punct with
| GrafiteAst.Dot _ -> NTactics.dot_tac
| GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
| GrafiteAst.Wildcard _ -> NTactics.wildcard_tac
| GrafiteAst.Merge _ -> NTactics.merge_tac
-;;
+;; *)
let eval_ng_tac tac =
let rec aux f (text, prefix_len, tac) =
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
let status,uris =
match cmd with
- | GrafiteAst.Drop loc -> raise Drop
- | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
- (* Old Include command is not recursive; new one is *)
+ | GrafiteAst.Include (loc, baseuri) ->
+ (* Old Include command is not recursive; new one is
let status =
if new_or_old = `OldAndNew then
let moopath_rw, moopath_r =
eval_from_moo.efm_go status moopath
else
status
- in
+ in *)
let status =
NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
status in
let status =
GrafiteTypes.add_moo_content
- [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+ [GrafiteAst.Include (loc,baseuri)] status
in
status,`New []
| GrafiteAst.Print (_,_) -> status,`New []
| GrafiteAst.Set (loc, name, value) -> status, `New []
-(* GrafiteTypes.set_option status name value,[] *)
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
in
status,uris
} and eval_executable = {ee_go = fun ~disambiguate_command
-~disambiguate_macro opts status (text,prefix_len,ex) ->
+ opts status (text,prefix_len,ex) ->
match ex with
| GrafiteAst.NTactic (_(*loc*), tacl) ->
if status#ng_mode <> `ProofMode then
eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
| GrafiteAst.NCommand (_, cmd) ->
eval_ncommand opts status (text,prefix_len,cmd)
- | GrafiteAst.Macro (loc, macro) ->
- raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
| GrafiteAst.NMacro (loc, macro) ->
raise (NMacro (loc,macro))
let status,lemmas =
eval_ast.ea_go
~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
- ~disambiguate_macro:(fun _ _ -> assert false)
status ast
in
assert (lemmas=`New []);
status)
status moo
} and eval_ast = {ea_go = fun ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) status
+?(do_heavy_checks=false) status
(text,prefix_len,st)
->
let opts = { do_heavy_checks = do_heavy_checks ; } in
match st with
| GrafiteAst.Executable (_,ex) ->
eval_executable.ee_go ~disambiguate_command
- ~disambiguate_macro opts status (text,prefix_len,ex)
+ opts status (text,prefix_len,ex)
| 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) ->