Added support for mutually recursive function and predicate definitio…

…ns (#549)

* Added support for mutually recursive fun/pred defs

* Use  `and function|predicate` instead of `with`
for mutually recursive function definitions

* Renaming:
- type_fun_aux_1 -> declare_fun
- type_fun_aux_2 -> define_fun
- with_recursive_def_opt -> and_recursive_def_opt

src/lib/frontend/parsed_interface.ml

@@ -58,6 +58,9 @@ let mk_logic loc is_ac named_idents ty =
 let mk_function_def loc named_ident args ty expr =
   Function_def (loc, named_ident, args, ty, expr)
 
+let mk_mut_rec_def l =
+  MutRecDefs l
+
 let mk_ground_predicate_def loc named_ident expr =
   Predicate_def (loc, named_ident, [], expr)
 

src/lib/frontend/parsed_interface.mli

@@ -48,6 +48,14 @@ val mk_non_ground_predicate_def :
   string * string ->
   (Loc.t * string * ppure_type) list -> lexpr -> decl
 
+val mk_mut_rec_def :
+  (Loc.t
+   * (string * string)
+   * (Loc.t * string * ppure_type) list
+   * ppure_type option
+   * lexpr
+  ) list -> decl
+
 val mk_goal : Loc.t -> string -> lexpr -> decl
 
 val mk_check_sat : Loc.t -> string -> lexpr -> decl

src/lib/frontend/typechecker.ml

@@ -2004,9 +2004,11 @@ let type_one_th_decl env e =
   | Check_sat(loc, _, _)
   | Predicate_def(loc,_,_,_)
   | Function_def(loc,_,_,_,_)
+  | MutRecDefs ((loc,_,_,_,_) :: _)
   | TypeDecl ((loc, _, _, _)::_)
   | Push (loc,_) | Pop (loc,_) ->
     Errors.typing_error WrongDeclInTheory loc
+  | MutRecDefs []
   | TypeDecl [] -> assert false
 
 let is_recursive_type =
@@ -2154,6 +2156,51 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
     assert (not is_recursive); (* Abstract types are not recursive *)
     acc, env
 
+let declare_fun env loc n ?ret_ty l  =
+  check_duplicate_params l;
+  let infix, ty  =
+    let l = List.map (fun (_,_,x) -> x) l in
+    match ret_ty with
+    | None | Some PPTbool ->
+      PPiff, PPredicate l
+    | Some ty ->
+      PPeq, PFunction(l,ty)
+  in
+  let mk_symb hs = Symbols.name hs ~kind:Symbols.Other in
+  let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *)
+  env, infix, tlogic
+
+let define_fun (acc, env) loc n l tlogic ?ret_ty infix e =
+  let l = List.map (fun (_,x,t) -> (x,t)) l in
+  let n = fst n in
+  let lvar = List.map (fun (x,_) -> {pp_desc=PPvar x;pp_loc=loc}) l in
+  let p = { pp_desc=PPapp(n,lvar) ; pp_loc=loc } in
+  let f = { pp_desc = PPinfix(p,infix,e) ; pp_loc = loc } in
+  let f = make_pred loc [] f l in
+  let f = type_form env f in
+  let t_typed, l_typed =
+    match tlogic with
+    | TPredicate args ->
+      Ty.Tbool, List.map2 (fun (x, _) ty -> x, Ty.shorten ty) l args
+    | TFunction (args, ret) ->
+      Ty.shorten ret, List.map2 (fun (x, _) ty -> x, Ty.shorten ty) l args
+  in
+  let td =
+    match ret_ty with
+    | None ->
+      Options.tool_req 1 "TR-Typing-LogicPred$_F$";
+      TPredicate_def(loc,n,l_typed,f)
+    | Some _ ->
+      Options.tool_req 1 "TR-Typing-LogicFun$_F$";
+      TFunction_def(loc,n,l_typed,t_typed,f)
+  in
+  let td_a = { c = td; annot=new_id () } in
+  (td_a, env)::acc, env
+
+let type_fun (acc, env) loc n l ?ret_ty e =
+  let env, infix, tlogic = declare_fun env loc n ?ret_ty l in
+  define_fun (acc, env) loc n l tlogic ?ret_ty infix e
+
 let rec type_decl (acc, env) d assertion_stack =
   Types.to_tyvars := MString.empty;
   match d with
@@ -2225,49 +2272,24 @@ let rec type_decl (acc, env) d assertion_stack =
     let f = alpha_renaming_env env f in
     type_and_intro_goal acc env Sat n f, env
 
-  | Predicate_def(loc,n,l,e)
-  | Function_def(loc,n,l,_,e) ->
-    check_duplicate_params l;
-    let infix, ty  =
-      let l = List.map (fun (_,_,x) -> x) l in
-      match d with
-      | Function_def(_,_,_,PPTbool,_) ->
-        (* cast functions that returns bools into predicates *)
-        PPiff, PPredicate l
-      | Function_def(_,_,_,t,_) ->
-        PPeq, PFunction(l,t)
-      | Predicate_def _ ->
-        PPiff, PPredicate l
-      | _ -> assert false
+  | MutRecDefs l ->
+    let rev_l, env =
+      List.fold_left (
+        fun (acc, env) (loc,n,l,ret_ty,e) ->
+          let env, infix, tlogic = declare_fun env loc n ?ret_ty l in
+          (loc, n, l, tlogic, ret_ty, infix, e) :: acc, env
+      ) ([], env) l
     in
-    let l = List.map (fun (_,x,t) -> (x,t)) l in
-    let mk_symb hs = Symbols.name hs ~kind:Symbols.Other in
-    let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *)
-    let n = fst n in
-
-    let lvar = List.map (fun (x,_) -> {pp_desc=PPvar x;pp_loc=loc}) l in
-    let p = {pp_desc=PPapp(n,lvar) ; pp_loc=loc } in
-    let f = { pp_desc = PPinfix(p,infix,e) ; pp_loc = loc } in
-    let f = make_pred loc [] f l in
-    let f = type_form env f in
-    let t_typed, l_typed =
-      match tlogic with
-      | TPredicate args ->
-        Ty.Tbool, List.map2 (fun (x, _) ty -> x, Ty.shorten ty) l args
-      | TFunction (args, ret) ->
-        Ty.shorten ret, List.map2 (fun (x, _) ty -> x, Ty.shorten ty) l args
-    in
-    let td =
-      match d with
-      | Function_def _ ->
-        Options.tool_req 1 "TR-Typing-LogicFun$_F$";
-        TFunction_def(loc,n,l_typed,t_typed,f)
-      | _ ->
-        Options.tool_req 1 "TR-Typing-LogicPred$_F$";
-        TPredicate_def(loc,n,l_typed,f)
-    in
-    let td_a = { c = td; annot=new_id () } in
-    (td_a, env)::acc, env
+    List.fold_left (
+      fun (acc, env) (loc, n, l, tlogic, ret_ty, infix, e) ->
+        define_fun (acc, env) loc n l tlogic ?ret_ty infix e
+    ) (acc, env) (List.rev rev_l)
+
+  | Predicate_def(loc,n,l,e) ->
+    type_fun (acc, env) loc n l e
+
+  | Function_def(loc,n,l,ret_ty,e) ->
+    type_fun (acc, env) loc n l ~ret_ty e
 
   | TypeDecl [] ->
     assert false

src/lib/structures/parsed.ml

@@ -268,6 +268,9 @@ type decl =
   | Function_def of
       Loc.t * (string * string) *
       (Loc.t * string * ppure_type) list * ppure_type * lexpr
+  | MutRecDefs of
+      (Loc.t * (string * string) *
+       (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list
   | TypeDecl of type_decl list
   | Push of Loc.t * int
   | Pop of Loc.t * int

src/lib/structures/parsed.mli

@@ -129,6 +129,9 @@ type decl =
   | Function_def of
       Loc.t * (string * string) *
       (Loc.t * string * ppure_type) list * ppure_type * lexpr
+  | MutRecDefs of
+      (Loc.t * (string * string) *
+       (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list
   | TypeDecl of type_decl list
   | Push of Loc.t * int
   | Pop of Loc.t * int

src/parsers/native_parser.mly

@@ -105,7 +105,7 @@ decl:
     { mk_abstract_type_decl ($startpos, $endpos) ty_vars ty }
 
 | TYPE ty_vars = type_vars ty = ident EQUAL enum = list1_constructors_sep_bar
-   others = and_recursive_opt
+   others = and_recursive_ty_opt
     {
       match others with
         | [] ->
@@ -132,14 +132,23 @@ decl:
 
 | FUNC app=named_ident LEFTPAR args=list0_logic_binder_sep_comma RIGHTPAR
    COLON ret_ty = primitive_type EQUAL body = lexpr
-   { mk_function_def ($startpos, $endpos) app args ret_ty body }
+   others = and_recursive_def_opt
+   { match others with
+     | [] -> mk_function_def ($startpos, $endpos) app args ret_ty body
+     | _ ->
+       mk_mut_rec_def
+         ((($startpos, $endpos), app, args, Some ret_ty, body) :: others)}
 
 | PRED app = named_ident EQUAL body = lexpr
    { mk_ground_predicate_def ($startpos, $endpos) app body }
 
 | PRED app = named_ident LEFTPAR args = list0_logic_binder_sep_comma RIGHTPAR
-   EQUAL body = lexpr
-   { mk_non_ground_predicate_def ($startpos, $endpos) app args body }
+   EQUAL body = lexpr others = and_recursive_def_opt
+   { match others with
+     | [] -> mk_non_ground_predicate_def ($startpos, $endpos) app args body
+     | _ ->
+       mk_mut_rec_def
+         ((($startpos, $endpos), app, args, None, body) :: others)}
 
 | AXIOM name = ident COLON body = lexpr
    { mk_generic_axiom ($startpos, $endpos) name body }
@@ -229,11 +238,21 @@ algebraic_args:
 | { [] }
 | OF record_type { $2 }
 
-and_recursive_opt:
+and_recursive_ty_opt:
   | { [] }
   | AND ty_vars = type_vars ty = ident EQUAL enum = list1_constructors_sep_bar
-others = and_recursive_opt
-    { (($startpos, $endpos), ty_vars, ty, enum) :: others}
+      others = and_recursive_ty_opt
+      { (($startpos, $endpos), ty_vars, ty, enum) :: others}
+
+and_recursive_def_opt:
+  | { [] }
+  | AND PRED app=named_ident LEFTPAR args=list0_logic_binder_sep_comma RIGHTPAR
+      EQUAL body = lexpr others = and_recursive_def_opt
+      { (($startpos, $endpos), app, args, None, body) :: others }
+  | AND FUNC app=named_ident LEFTPAR args=list0_logic_binder_sep_comma RIGHTPAR
+      COLON ret_ty = primitive_type EQUAL body = lexpr
+      others = and_recursive_def_opt
+      { (($startpos, $endpos), app, args, Some ret_ty, body) :: others }
 
 lexpr:
 

tests/typing/mutual-recursion001.ae

@@ -0,0 +1,19 @@
+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)

tests/typing/mutual-recursion001.expected

@@ -0,0 +1,2 @@
+
+unsat