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 <[email protected]>

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
 

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. *)

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. *)
 

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

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
 
 <YOUR SYNTAX ERROR MESSAGE HERE>
 
+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
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
 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 [ # ]
 ##

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