From 60143c901773b686d261f770ea69c4029f16c3b2 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 10 Feb 2023 17:05:00 +0100 Subject: [PATCH] Add mutually recursive definition support for AE (#129) * Add mutually recursive definition support for AE * Replace the function mut_fun_def_rec by the function defs * Add support for mutually recursive predicates * Poetry * Add support for functions and predicates in the same group * changes * code cleanup * some more code cleanup --------- Co-authored-by: Guillaume Bury --- CHANGES.md | 2 + src/interface/stmt.ml | 29 +++++------ src/languages/ae/ast.ml | 5 +- src/languages/ae/parser.mly | 37 ++++++++----- src/languages/ae/syntax.messages | 52 ++++++++++++------- src/standard/statement.ml | 5 -- tests/parsing/ae/pass/dune | 38 ++++++++++++++ tests/parsing/ae/pass/flags.dune | 0 tests/parsing/ae/pass/test-mut-fun_def_1.ae | 21 ++++++++ .../ae/pass/test-mut-fun_def_1.expected | 0 tests/parsing/ae/pass/test-mut-pred_def_1.ae | 21 ++++++++ .../ae/pass/test-mut-pred_def_1.expected | 0 tests/typing/pass/ae/adts/dune | 19 ++++++- tests/typing/pass/ae/adts/rec_defs.ae | 21 ++++++++ tests/typing/pass/ae/adts/rec_defs.expected | 0 15 files changed, 193 insertions(+), 57 deletions(-) create mode 100644 tests/parsing/ae/pass/dune create mode 100644 tests/parsing/ae/pass/flags.dune create mode 100644 tests/parsing/ae/pass/test-mut-fun_def_1.ae create mode 100644 tests/parsing/ae/pass/test-mut-fun_def_1.expected create mode 100644 tests/parsing/ae/pass/test-mut-pred_def_1.ae create mode 100644 tests/parsing/ae/pass/test-mut-pred_def_1.expected create mode 100644 tests/typing/pass/ae/adts/rec_defs.ae create mode 100644 tests/typing/pass/ae/adts/rec_defs.expected diff --git a/CHANGES.md b/CHANGES.md index 3bfe59334..368ab31e1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -27,6 +27,8 @@ v0.8.1 definitions are always recursive (PR#123) - Add `parse_raw_lazy` to parse a string into a lazy list of statements (PR#125) +- Add support for mutually recursive functions and predicates + in Alt-ergo's native language (PR#129) ### Typing diff --git a/src/interface/stmt.ml b/src/interface/stmt.ml index 005d9a57f..14a84614c 100644 --- a/src/interface/stmt.ml +++ b/src/interface/stmt.ml @@ -88,10 +88,13 @@ module type Logic = sig statements to import. *) val include_ : ?loc:location -> string -> id list -> t - (** Inlcude directive. [include file l] means to include in the current scope + (** Include directive. [include file l] means to include in the current scope the directives from file [file] that appear in [l]. If [l] is the empty list, all directives should be imported. *) + val defs : ?loc:location -> ?attrs:term list -> t list -> t + (** Pack a list of mutually recursive definitions into a single statement. *) + (** {2 Alt-ergo Statements} *) val logic : ?loc:location -> ac:bool -> id list -> term -> t @@ -113,6 +116,13 @@ module type Logic = sig val rec_types : ?loc:location -> t list -> t (** Pack together a list of mutually recursive type definitions. *) + val pred_def : ?loc:location -> id -> term list -> term list -> term -> t + (** Symbol definition. [pred_def p vars args body] means that "p(args) = (body : bool)", + i.e [p] is a predicate symbol with arguments [args], and which returns the value + [body] which is of type [bool]. The predicate can also be a top-level predicate in + which case it doesn't have arguments and it just returns the value of the body which + means "p = (body : bool)". *) + val axiom : ?loc:location -> id -> term -> t (** Create a axiom. *) @@ -195,20 +205,8 @@ module type Logic = sig i.e f is a function symbol with arguments [args], and which returns the value [body] which is of type [ret]. *) - val fun_def_rec : ?loc:location -> id -> term list -> term list -> term -> term -> t - (** Symbol definition. [fun_def_rec f vars args ret body] means that "f(args) = (body : ret)", - i.e f is a recursive function symbol with arguments [args], and which returns the value - [body] which is of type [ret]. *) - - val pred_def : ?loc:location -> id -> term list -> term list -> term -> t - (** Symbol definition. [pred_def p vars args body] means that "p(args) = (body : bool)", - i.e [p] is a predicate symbol with arguments [args], and which returns the value - [body] which is of type [bool]. The predicate can also be a top-level predicate in - which case it doesn't have arguments and it just returns the value of the body which - means "p = (body : bool)". *) - val funs_def_rec : ?loc:location -> (id * term list * term list * term * term) list -> t - (** Define a list of mutually recursive functions. Each functions has the same + (** Define a list of mutually recursive functions. Each function has the same definition as in [fun_def] *) val get_proof : ?loc:location -> unit -> t @@ -281,9 +279,6 @@ module type Logic = sig (** Packs a list of mutually recursive inductive type declarations into a single statement. *) - val defs : ?loc:location -> ?attrs:term list -> t list -> t - (** Packs a list of mutually recursive definitions into a single statement. *) - val rewrite : ?loc:location -> ?attrs:term list -> term -> t (** Declare a rewrite rule, i.e a universally quantified equality or equivalence that can be oriented according to a specific ordering. *) diff --git a/src/languages/ae/ast.ml b/src/languages/ae/ast.ml index 3ce6af5dd..aad2cf7cf 100644 --- a/src/languages/ae/ast.ml +++ b/src/languages/ae/ast.ml @@ -197,12 +197,15 @@ module type Statement = sig val record_type : ?loc:location -> id -> term list -> (id * term) list -> t (** Record type definition. *) - val fun_def_rec : ?loc:location -> id -> term list -> term list -> term -> term -> t + val fun_def : ?loc:location -> id -> term list -> term list -> term -> term -> t (** Function definition. *) val pred_def : ?loc:location -> id -> term list -> term list -> term -> t (** Predicate definition. *) + val defs : ?loc:location -> ?attrs:term list -> t list -> t + (** Pack a list of mutually recursive definitions into a single statement. *) + val abstract_type : ?loc:location -> id -> term list -> t (** Create a new abstract type, quantified over the given type variables. *) diff --git a/src/languages/ae/parser.mly b/src/languages/ae/parser.mly index ecb268cbf..8a9521d9e 100644 --- a/src/languages/ae/parser.mly +++ b/src/languages/ae/parser.mly @@ -516,6 +516,28 @@ rewriting_list: | e=lexpr PV l=rewriting_list { e :: l } +function_def: + | FUNC f=raw_named_ident + LEFTPAR args=separated_list(COMMA, logic_binder) RIGHTPAR + COLON ret_ty=primitive_type EQUAL body=lexpr + { let loc = L.mk_pos $startpos $endpos in + S.fun_def ~loc f [] args ret_ty body } + +predicate_def: + | PRED p=raw_named_ident EQUAL body=lexpr + { let loc = L.mk_pos $startpos $endpos in + S.pred_def ~loc p [] [] body } + + | PRED p=raw_named_ident + LEFTPAR args=separated_list(COMMA, logic_binder) RIGHTPAR EQUAL body=lexpr + { let loc = L.mk_pos $startpos $endpos in + S.pred_def ~loc p [] args body } + +function_or_predicate_def: + | s=function_def + | s=predicate_def + { s } + decl: | THEORY id=decl_ident EXTENDS ext=decl_ident EQUAL l=theory_elt* END { let loc = L.mk_pos $startpos $endpos in @@ -537,20 +559,9 @@ decl: { let loc = L.mk_pos $startpos $endpos in S.logic ~loc ~ac args ty } - | FUNC f=raw_named_ident - LEFTPAR args=separated_list(COMMA, logic_binder) RIGHTPAR - COLON ret_ty=primitive_type EQUAL body=lexpr - { let loc = L.mk_pos $startpos $endpos in - S.fun_def_rec ~loc f [] args ret_ty body } - - | PRED p=raw_named_ident EQUAL body=lexpr + | l=separated_nonempty_list(AND, function_or_predicate_def) { let loc = L.mk_pos $startpos $endpos in - S.pred_def ~loc p [] [] body } - - | PRED p=raw_named_ident - LEFTPAR args=separated_list(COMMA, logic_binder) RIGHTPAR EQUAL body=lexpr - { let loc = L.mk_pos $startpos $endpos in - S.pred_def ~loc p [] args body } + S.defs ~loc l } | AXIOM name=decl_ident COLON body=lexpr { let loc = L.mk_pos $startpos $endpos in diff --git a/src/languages/ae/syntax.messages b/src/languages/ae/syntax.messages index cfc10d584..c259d3ba3 100644 --- a/src/languages/ae/syntax.messages +++ b/src/languages/ae/syntax.messages @@ -3369,8 +3369,8 @@ file: PRED XOR ## ## Ends in an error in state: 308. ## -## decl -> PRED . raw_named_ident EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] -## decl -> PRED . raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED . raw_named_ident EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] +## predicate_def -> PRED . raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED @@ -3382,8 +3382,8 @@ file: PRED ID COMMA ## ## Ends in an error in state: 309. ## -## decl -> PRED raw_named_ident . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] -## decl -> PRED raw_named_ident . LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED raw_named_ident . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] +## predicate_def -> PRED raw_named_ident . LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident @@ -3401,7 +3401,7 @@ file: PRED ID LEFTPAR XOR ## ## Ends in an error in state: 310. ## -## decl -> PRED raw_named_ident LEFTPAR . loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED raw_named_ident LEFTPAR . loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident LEFTPAR @@ -3413,7 +3413,7 @@ file: PRED ID LEFTPAR RIGHTPAR XOR ## ## Ends in an error in state: 313. ## -## decl -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR @@ -3425,7 +3425,7 @@ file: PRED ID LEFTPAR RIGHTPAR EQUAL XOR ## ## Ends in an error in state: 314. ## -## decl -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL @@ -3437,7 +3437,6 @@ file: PRED ID LEFTPAR RIGHTPAR EQUAL ID RIGHTSQ ## ## Ends in an error in state: 315. ## -## decl -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] ## lexpr -> lexpr . PLUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . MINUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . TIMES lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] @@ -3458,6 +3457,7 @@ file: PRED ID LEFTPAR RIGHTPAR EQUAL ID RIGHTSQ ## lexpr -> lexpr . NOTEQ lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . HAT LEFTBR INTEGER COMMA INTEGER RIGHTBR [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . AT lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] +## predicate_def -> PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR EQUAL lexpr @@ -3525,7 +3525,7 @@ file: PRED ID EQUAL XOR ## ## Ends in an error in state: 322. ## -## decl -> PRED raw_named_ident EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## predicate_def -> PRED raw_named_ident EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident EQUAL @@ -3537,7 +3537,6 @@ file: PRED ID EQUAL ID RIGHTSQ ## ## Ends in an error in state: 323. ## -## decl -> PRED raw_named_ident EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] ## lexpr -> lexpr . PLUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . MINUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . TIMES lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] @@ -3558,6 +3557,7 @@ file: PRED ID EQUAL ID RIGHTSQ ## lexpr -> lexpr . NOTEQ lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . HAT LEFTBR INTEGER COMMA INTEGER RIGHTBR [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . AT lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] +## predicate_def -> PRED raw_named_ident EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## PRED raw_named_ident EQUAL lexpr @@ -3778,7 +3778,7 @@ file: FUNC XOR ## ## Ends in an error in state: 345. ## -## decl -> FUNC . raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC . raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC @@ -3790,7 +3790,7 @@ file: FUNC ID EQUAL ## ## Ends in an error in state: 346. ## -## decl -> FUNC raw_named_ident . LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident . LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC raw_named_ident @@ -3808,7 +3808,7 @@ file: FUNC ID LEFTPAR XOR ## ## Ends in an error in state: 347. ## -## decl -> FUNC raw_named_ident LEFTPAR . loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR . loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC raw_named_ident LEFTPAR @@ -3820,7 +3820,7 @@ file: FUNC ID LEFTPAR RIGHTPAR XOR ## ## Ends in an error in state: 349. ## -## decl -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR . COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR . COLON primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR @@ -3832,7 +3832,7 @@ file: FUNC ID LEFTPAR RIGHTPAR COLON XOR ## ## Ends in an error in state: 350. ## -## decl -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON . primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON . primitive_type EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON @@ -3844,7 +3844,7 @@ file: FUNC ID LEFTPAR RIGHTPAR COLON ID XOR ## ## Ends in an error in state: 351. ## -## decl -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type . EQUAL lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## primitive_type -> primitive_type . ty_ident [ ID EQUAL ] ## ## The known suffix of the stack is as follows: @@ -3857,7 +3857,7 @@ file: FUNC ID LEFTPAR RIGHTPAR COLON ID EQUAL XOR ## ## Ends in an error in state: 352. ## -## decl -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL . lexpr [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## ## The known suffix of the stack is as follows: ## FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL @@ -3869,7 +3869,7 @@ file: FUNC ID LEFTPAR RIGHTPAR COLON ID EQUAL ID RIGHTSQ ## ## Ends in an error in state: 353. ## -## decl -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## function_def -> FUNC raw_named_ident LEFTPAR loption(separated_nonempty_list(COMMA,logic_binder)) RIGHTPAR COLON primitive_type EQUAL lexpr . [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM AND ] ## lexpr -> lexpr . PLUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . MINUS lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] ## lexpr -> lexpr . TIMES lexpr [ XOR TYPE TIMES THEORY SLASH RIGHTARROW REWRITING PRED POWDOT POW PLUS PERCENT OR NOTEQ MINUS LT LRARROW LOGIC LE HAT GT GOAL GE FUNC EQUAL EOF AXIOM AT AND ] @@ -3979,9 +3979,21 @@ file: AXIOM ID COLON ID RIGHTSQ +file: PRED ID EQUAL ID AND XOR +## +## Ends in an error in state: 363. +## +## separated_nonempty_list(AND,function_or_predicate_def) -> function_or_predicate_def AND . separated_nonempty_list(AND,function_or_predicate_def) [ TYPE THEORY REWRITING PRED LOGIC GOAL FUNC EOF AXIOM ] +## +## The known suffix of the stack is as follows: +## function_or_predicate_def AND +## + + + file: LOGIC ID COLON PROP XOR ## -## Ends in an error in state: 361. +## Ends in an error in state: 367. ## ## list(decl) -> decl . list(decl) [ EOF ] ## @@ -3993,7 +4005,7 @@ file: LOGIC ID COLON PROP XOR input: XOR ## -## Ends in an error in state: 363. +## Ends in an error in state: 369. ## ## input' -> . input [ # ] ## diff --git a/src/standard/statement.ml b/src/standard/statement.ml index 481c3337a..de23a6135 100644 --- a/src/standard/statement.ml +++ b/src/standard/statement.ml @@ -498,11 +498,6 @@ let fun_def ?loc id vars params ret_ty body = def ?loc id ~vars ~params ret_ty body ] -let fun_def_rec ?loc id vars params ret_ty body = - mk_defs ?loc ~recursive:true [ - def ?loc id ~vars ~params ret_ty body - ] - let pred_def ?loc id vars params body = let attrs = [Term.const ?loc Id.predicate_def] in let ret_ty = Term.prop ?loc () in diff --git a/tests/parsing/ae/pass/dune b/tests/parsing/ae/pass/dune new file mode 100644 index 000000000..0cb0aacb2 --- /dev/null +++ b/tests/parsing/ae/pass/dune @@ -0,0 +1,38 @@ +; File auto-generated by gentests.ml + +; Auto-generated part begin +; Test for test-mut-fun_def_1.ae +; Full mode test + +(rule + (target test-mut-fun_def_1.full) + (deps (:input test-mut-fun_def_1.ae)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes 0 + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff test-mut-fun_def_1.expected test-mut-fun_def_1.full))) + + +; Test for test-mut-pred_def_1.ae +; Full mode test + +(rule + (target test-mut-pred_def_1.full) + (deps (:input test-mut-pred_def_1.ae)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes 0 + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff test-mut-pred_def_1.expected test-mut-pred_def_1.full))) + + +; Auto-generated part end diff --git a/tests/parsing/ae/pass/flags.dune b/tests/parsing/ae/pass/flags.dune new file mode 100644 index 000000000..e69de29bb diff --git a/tests/parsing/ae/pass/test-mut-fun_def_1.ae b/tests/parsing/ae/pass/test-mut-fun_def_1.ae new file mode 100644 index 000000000..b87aa9368 --- /dev/null +++ b/tests/parsing/ae/pass/test-mut-fun_def_1.ae @@ -0,0 +1,21 @@ +type t = + A + | B of { us : u } + +and u = + C + | D of { us1 : t } + +function f(x: t) : int = + match x with + | A -> 1 + | B(y) -> (1 + g(y)) +end + +and function g(y1: u) : int = + match y1 with + | C -> 1 + | D(x) -> (1 + f(x)) +end + +goal size : (f(B(D(A))) = 3) diff --git a/tests/parsing/ae/pass/test-mut-fun_def_1.expected b/tests/parsing/ae/pass/test-mut-fun_def_1.expected new file mode 100644 index 000000000..e69de29bb diff --git a/tests/parsing/ae/pass/test-mut-pred_def_1.ae b/tests/parsing/ae/pass/test-mut-pred_def_1.ae new file mode 100644 index 000000000..2b90f3714 --- /dev/null +++ b/tests/parsing/ae/pass/test-mut-pred_def_1.ae @@ -0,0 +1,21 @@ +type t = + A + | B of { us : u } + +and u = + C + | D of { us1 : t } + +predicate f(x: t) = + match x with + | A -> true + | B(y) -> g(y) +end + +and predicate g(y1: u) = + match y1 with + | C -> false + | D(x) -> not f(x) +end + +goal size : (f(B(D(A))) = false) diff --git a/tests/parsing/ae/pass/test-mut-pred_def_1.expected b/tests/parsing/ae/pass/test-mut-pred_def_1.expected new file mode 100644 index 000000000..e69de29bb diff --git a/tests/typing/pass/ae/adts/dune b/tests/typing/pass/ae/adts/dune index 2b0d7b6cb..85fa14f8f 100644 --- a/tests/typing/pass/ae/adts/dune +++ b/tests/typing/pass/ae/adts/dune @@ -27,7 +27,7 @@ (package dolmen_bin) (action (chdir %{workspace_root} (with-outputs-to %{target} - (with-accepted-exit-codes (or 0 (not 0)) + (with-accepted-exit-codes 0 (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) (rule (alias runtest) @@ -35,4 +35,21 @@ (action (diff length.expected length.full))) +; Test for rec_defs.ae +; Full mode test + +(rule + (target rec_defs.full) + (deps (:input rec_defs.ae)) + (package dolmen_bin) + (action (chdir %{workspace_root} + (with-outputs-to %{target} + (with-accepted-exit-codes (or 0 (not 0)) + (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune})))))) +(rule + (alias runtest) + (package dolmen_bin) + (action (diff rec_defs.expected rec_defs.full))) + + ; Auto-generated part end diff --git a/tests/typing/pass/ae/adts/rec_defs.ae b/tests/typing/pass/ae/adts/rec_defs.ae new file mode 100644 index 000000000..a86f1eefc --- /dev/null +++ b/tests/typing/pass/ae/adts/rec_defs.ae @@ -0,0 +1,21 @@ +type t = + A + | B of { us : u } + +and u = + C + | D of { us1 : t } + +function f(x: t) : int = + match x with + | A -> 1 + | B(y) -> if g(y) then 2 else 3 +end + +and predicate g(y1: u) = + match y1 with + | C -> true + | D(x) -> f(x) = 1 +end + +goal size : (f(B(D(A))) = 3) diff --git a/tests/typing/pass/ae/adts/rec_defs.expected b/tests/typing/pass/ae/adts/rec_defs.expected new file mode 100644 index 000000000..e69de29bb