GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
GrafiteAst.Transitivity (loc, t)
+ (* Produzioni Aggiunte *)
+ | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+ GrafiteAst.Assume (loc, id, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Suppose (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.By_term_we_proved (loc, t, ty, id)
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.We_need_to_prove (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+ GrafiteAst.Bydone (loc, t)
]
];
atomic_tactical:
fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
fun ~include_paths status ->
- let path = DependenciesParser.baseuri_of_script ~include_paths fname in
+ let buri, fullpath =
+ DependenciesParser.baseuri_of_script ~include_paths fname
+ in
let status =
- LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
+ LexiconEngine.eval_command status
+ (LexiconAst.Include (iloc,buri,mode,fullpath))
in
status,
LSome
(GrafiteAst.Executable
(loc,GrafiteAst.Command
- (loc,GrafiteAst.Include (iloc,path))))
+ (loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
let status = LexiconEngine.eval_command status scom in