+ (* Produzioni Aggiunte *)
+ | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+ GrafiteAst.Assume (loc, id, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']->
+ GrafiteAst.Suppose (loc, t, id, t1)
+ | IDENT "by" ; t = [t' = tactic_term -> Some t' | SYMBOL "_" -> None];
+ cont=by_continuation ->
+ (match cont with
+ None -> GrafiteAst.Bydone (loc, t)
+ | Some (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ GrafiteAst.We_need_to_prove (loc, t, id, t1)
+ | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
+ | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Byinduction(loc, t, id)
+ | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
+ GrafiteAst.Thesisbecomes(loc, t)
+ | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
+ SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
+ GrafiteAst.Case(loc,id,params)
+ | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term ->
+ GrafiteAst.Let1 (loc, id, t, t1)
+ | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ->
+ GrafiteAst.Bywehave (loc, t, t1, id, t2, id1)
+ | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
+ GrafiteAst.RewritingStep(loc, Some termine, t1, t2)
+ | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2)
+ ]
+];
+ by_continuation: [
+ [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> Some (ty,id,t1)
+ | IDENT "done" -> None