+ | 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)
+ | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
+ IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
+ id2 = IDENT ; RPAREN ->
+ GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
+ | just =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | params = auto_params -> `Auto params] ;
+ cont=by_continuation ->
+ (match cont with
+ BYC_done -> GrafiteAst.Bydone (loc, just)
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ GrafiteAst.AndElim (loc, just, 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" ; IDENT "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" ; 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)
+ (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
+ | IDENT "conclude";
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
+ | IDENT "obtain" ; name = IDENT;
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
+ | SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+ ]
+];
+ auto_fixed_param: [
+ [ IDENT "paramodulation"
+ | IDENT "depth"
+ | IDENT "width"
+ | IDENT "size"
+ | IDENT "timeout"
+ | IDENT "library"
+ | IDENT "type"
+ ]
+];
+ auto_params: [
+ [ params =
+ LIST0 [
+ i = auto_fixed_param -> i,""
+ | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
+ string_of_int v | v = IDENT -> v ] -> i,v ];
+ tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
+ (match tl with Some l -> l | None -> []),
+ params
+ ]
+];
+ by_continuation: [
+ [ WEPROVED; 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)
+ | WEPROVED; 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)
+ | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+ BYC_wehaveand (id1,t1,id2,t2)