+ (* 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)
+ | "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
+ cont=by_continuation ->
+ let t' = match t with LNone _ -> None | LSome t -> Some t in
+ (match cont with
+ BYC_done -> GrafiteAst.Bydone (loc, t')
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ (* (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ GrafiteAst.We_need_to_prove (loc, t, id, t1)
+ | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
+ | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
+ | "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)
+ | start = OPT [
+ start =
+ [ IDENT "conclude" -> None
+ | IDENT "obtain" ; name = IDENT -> Some name ] ;
+ termine = tactic_term -> start, termine];
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "exact"; t=tactic_term -> `Term t
+ | IDENT "using"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, start, t1, t2, cont)
+ ]
+];
+ auto_params: [
+ [ params =
+ LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ];
+ tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] ->
+ (match tl with Some l -> l | None -> []),
+ params
+ ]
+];
+ 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] -> BYC_weproved (ty,Some id,t1)
+ | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
+ "done" -> BYC_weproved (ty,None,t1)
+ | "done" -> BYC_done
+ | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
+ IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
+ | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+ BYC_wehaveand (id1,t1,id2,t2)