Add polymorphism of smt v3 in smt v2.6

src/interface/stmt.ml

@@ -135,17 +135,17 @@ module type Logic = sig
   (** Inductive type definitions.
       TODO: some more documentation. *)
 
-  val fun_decl    : ?loc:location -> id -> term list -> term -> t
-  (** Symbol declaration. [fun_decl f args ret] defines [f] as a function
+  val fun_decl    : ?loc:location -> id -> term list -> term list -> term -> t
+  (** Symbol declaration. [fun_decl f vars args ret] defines [f] as a function
       which takes arguments of type as described in [args] and which returns
       a value of type [ret]. *)
 
-  val fun_def     : ?loc:location -> id -> term list -> term -> term -> t
-  (** Symbol definition. [fun_def f args ret body] means that "f(args) = (body : ret)",
+  val fun_def     : ?loc:location -> id -> term list -> term list -> term -> term -> t
+  (** Symbol definition. [fun_def f vars args ret body] means that "f(args) = (body : ret)",
       i.e f is a function symbol with arguments [args], and which returns the value
       [body] which is of type [ret]. *)
 
-  val funs_def_rec : ?loc:location -> (id * term list * term * term) list -> t
+  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
       definition as in [fun_def] *)
 

src/languages/ae/ast_ae.ml

@@ -194,7 +194,7 @@ module type Statement = sig
   val record_type : ?loc:location -> id -> term list -> (id * term) list -> t
   (** Record type definition. *)
 
-  val fun_def : ?loc:location -> id -> term list -> term -> term -> t
+  val fun_def : ?loc:location -> id -> term list -> term list -> term -> term -> t
   (** Function definition. *)
 
   val abstract_type : ?loc:location -> id -> term list -> t

src/languages/ae/parseAe.mly

@@ -538,18 +538,18 @@ decl:
     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 }
+      S.fun_def ~loc f [] args ret_ty body }
 
   | PRED p=raw_named_ident EQUAL body=lexpr
     { let loc = L.mk_pos $startpos $endpos in
       let ret_ty = T.prop ~loc () in
-      S.fun_def ~loc p [] ret_ty body }
+      S.fun_def ~loc p [] [] ret_ty 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
       let ret_ty = T.prop ~loc () in
-      S.fun_def ~loc p args ret_ty body }
+      S.fun_def ~loc p [] args ret_ty body }
 
   | AXIOM name=decl_ident COLON body=lexpr
     { let loc = L.mk_pos $startpos $endpos in

src/languages/smtlib2/v2.6/ast_smtlib.ml

@@ -73,6 +73,9 @@ module type Term = sig
   val exists  : ?loc:location -> t list -> t -> t
   (** Existencial quantification. *)
 
+  val pi     : ?loc:location -> t list -> t -> t
+  (** Type quantification. *)
+
   val match_ : ?loc:location -> t -> (t * t) list -> t
   (** Pattern matching. The first term is the term to match,
       and each tuple in the list is a match case, which is a pair
@@ -86,6 +89,18 @@ module type Term = sig
       in the smtlib manual, "Term attributes have no logical meaning --
       semantically, [attr t l] is equivalent to [t]" *)
 
+  val tType     : ?loc:location -> unit -> t
+  (** The type of types, defined as specific token by the Zipperposition format;
+      in other languages, will be represented as a constant (the "$tType" constant
+      in tptp for instance). Used to define new types, or quantify type variables
+      in languages that support polymorphism. *)
+
+  val trigger : ?loc:location -> t list -> t
+  (** Create a (multi) trigger. *)
+
+  val triggers : ?loc:location -> t -> t list -> t
+  (** Annotate a term (generally a quantified formula), with a list of triggers. *)
+
 end
 (** Implementation requirements for Smtlib terms. *)
 
@@ -144,17 +159,17 @@ module type Statement = sig
   val datatypes : ?loc:location -> (id * term list * (id * term list) list) list -> t
   (** Inductive type definitions. *)
 
-  val fun_decl  : ?loc:location -> id -> term list -> term -> t
-  (** Declares a new term symbol, and its type. [fun_decl f args ret]
+  val fun_decl  : ?loc:location -> id -> term list -> term list -> term -> t
+  (** Declares a new term symbol, and its type. [fun_decl f ty_args args ret]
       declares [f] as a new function symbol which takes arguments of types
       described in [args], and with return type [ret]. *)
 
-  val fun_def   : ?loc:location -> id -> term list -> term -> term -> t
-  (** Defines a new function. [fun_def f args ret body] is such that
+  val fun_def   : ?loc:location -> id -> term list -> term list -> term -> term -> t
+  (** Defines a new function. [fun_def f ty_args args ret body] is such that
       applications of [f] are equal to [body] (module substitution of the arguments),
       which should be of type [ret]. *)
 
-  val funs_def_rec : ?loc:location -> (id * term list * term * term) list -> t
+  val funs_def_rec : ?loc:location -> (id * term list * term list * term * term) list -> t
   (** Declare a list of mutually recursive functions. *)
 
 

src/languages/smtlib2/v2.6/parseSmtlib.mly

@@ -248,11 +248,16 @@ datatype_dec:
 
 function_dec:
   | OPEN s=SYMBOL OPEN args=sorted_var* CLOSE ret=sort CLOSE
-    { I.(mk term s), args, ret }
+    { I.(mk term s), [], args, ret }
+  | OPEN s=SYMBOL PAR OPEN vars=datatype_symbol+ CLOSE OPEN args=sorted_var* CLOSE ret=sort CLOSE CLOSE
+    { I.(mk term s), vars, args, ret }
 
 function_def:
   | s=SYMBOL OPEN args=sorted_var* CLOSE ret=sort body=term
-    { I.(mk term s), args, ret, body }
+    { I.(mk term s), [], args, ret, body }
+  | s=SYMBOL OPEN PAR OPEN vars=datatype_symbol+ CLOSE OPEN args=sorted_var* CLOSE ret=sort body=term CLOSE
+    { I.(mk term s), vars, args, ret, body }
+
 
 /* Additional rule for prop_literals symbols, to have lighter
    semantic actions in prop_literal reductions. */
@@ -280,12 +285,16 @@ prop_literal:
 command:
   | OPEN ASSERT t=term CLOSE
     { let loc = L.mk_pos $startpos $endpos in S.assert_ ~loc t }
+  | OPEN ASSERT OPEN PAR OPEN vars=datatype_symbol+ CLOSE t=term CLOSE CLOSE
+    { let loc = L.mk_pos $startpos $endpos in
+      let vars = List.map (fun v -> T.colon v (T.tType ~loc ())) vars in
+      S.assert_ ~loc (T.forall ~loc vars t) }
   | OPEN CHECK_SAT CLOSE
     { let loc = L.mk_pos $startpos $endpos in S.check_sat ~loc [] }
   | OPEN CHECK_SAT_ASSUMING OPEN l=prop_literal* CLOSE CLOSE
     { let loc = L.mk_pos $startpos $endpos in S.check_sat ~loc l }
   | OPEN DECLARE_CONST s=SYMBOL ty=sort CLOSE
-    { let loc = L.mk_pos $startpos $endpos in S.fun_decl ~loc I.(mk term s) [] ty }
+    { let loc = L.mk_pos $startpos $endpos in S.fun_decl ~loc I.(mk term s) [] [] ty }
   | OPEN DECLARE_DATATYPE s=SYMBOL d=datatype_dec CLOSE
     { let vars, constructors = d in
       let loc = L.mk_pos $startpos $endpos in
@@ -302,24 +311,28 @@ command:
   | OPEN DECLARE_FUN s=SYMBOL OPEN args=sort* CLOSE ty=sort CLOSE
     { let id = I.(mk term s) in
       let loc = L.mk_pos $startpos $endpos in
-      S.fun_decl ~loc id args ty }
+      S.fun_decl ~loc id [] args ty }
+  | OPEN DECLARE_FUN s=SYMBOL OPEN PAR OPEN vars=datatype_symbol+ CLOSE OPEN args=sort* CLOSE ty=sort CLOSE CLOSE
+    { let id = I.(mk term s) in
+      let loc = L.mk_pos $startpos $endpos in
+      S.fun_decl ~loc id vars args ty }
   | OPEN DECLARE_SORT s=SYMBOL n=NUM CLOSE
     { let id = I.(mk sort s) in
       let loc = L.mk_pos $startpos $endpos in
       S.type_decl ~loc id (int_of_string n) }
   | OPEN DEFINE_FUN f=function_def CLOSE
-    { let id, args, ret, body = f in
+    { let id, vars, args, ret, body = f in
       let loc = L.mk_pos $startpos $endpos in
-      S.fun_def ~loc id args ret body }
+      S.fun_def ~loc id vars args ret body }
   | OPEN DEFINE_FUN_REC f=function_def CLOSE
-    { let id, args, ret, body = f in
+    { let id, vars, args, ret, body = f in
       let loc = L.mk_pos $startpos $endpos in
-      S.funs_def_rec ~loc [id, args, ret, body] }
+      S.funs_def_rec ~loc [id, vars, args, ret, body] }
   /* The syntax technically defines this reduction as having l and l' be the same length,
       but that isn't easily expressible in menhir, so the check is delayed */
   | OPEN DEFINE_FUNS_REC OPEN l1=function_dec+ CLOSE OPEN l2=term+ CLOSE OPEN
     { let res =
-        try List.map2 (fun (id, args, ret) body -> id, args, ret, body) l1 l2
+        try List.map2 (fun (id, vars, args, ret) body -> id, vars, args, ret, body) l1 l2
         with Invalid_argument _ -> assert false
       in
       let loc = L.mk_pos $startpos $endpos in

src/standard/statement.ml

@@ -457,8 +457,11 @@ let type_decl ?loc id n =
   let ty = Term.fun_ty ?loc (Misc.replicate n @@ Term.tType ()) @@ Term.tType () in
   mk_decls ?loc ~recursive:false [abstract ?loc id ty]
 
-let fun_decl ?loc id l t' =
+let fun_decl ?loc id vars l t' =
   let ty = Term.fun_ty ?loc l t' in
+  let ty = match vars with
+    | [] -> ty
+    | vars -> Term.pi ?loc vars ty  in
   mk_decls ?loc ~recursive:false [abstract ?loc id ty]
 
 let type_def ?loc id args body =
@@ -473,18 +476,25 @@ let datatypes ?loc l =
     ) l in
   mk_decls ?loc ~recursive:true l'
 
-let fun_def_aux id args ty_ret body =
+let fun_def_aux ?loc id vars args ty_ret body =
   let ty = Term.fun_ty (List.map extract_type args) ty_ret in
+  let ty = match vars with
+    | [] -> ty
+    | vars -> Term.pi ?loc vars ty  in
   let t = Term.lambda args (Term.colon body ty_ret) in
+  let t = match vars with
+    | [] -> t
+    | vars ->
+      Term.lambda (List.map (fun e -> Term.colon e (Term.tType ?loc ())) vars) t in
   id, ty, t
 
-let fun_def ?loc id args ty_ret body =
-  let id, ty, body = fun_def_aux id args ty_ret body in
+let fun_def ?loc id vars args ty_ret body =
+  let id, ty, body = fun_def_aux ?loc id vars args ty_ret body in
   mk_defs ?loc ~recursive:false [def ?loc id ty body]
 
 let funs_def_rec ?loc l =
-  let contents = List.map (fun (id, args, ty_ret, body) ->
-      let id, ty, body = fun_def_aux id args ty_ret body in
+  let contents = List.map (fun (id, vars, args, ty_ret, body) ->
+      let id, ty, body = fun_def_aux ?loc id vars args ty_ret body in
       def ?loc id ty body
     ) l in
   mk_defs ?loc ~recursive:true contents