Also add statement extensions to psmt2 (following #190)

src/classes/logic.ml

@@ -110,7 +110,7 @@ module Make
     Smtlib2 `V2_6, ".smt2",
     (module Dolmen_smtlib2.Script.V2_6.Make(L)(I)(T)(S)(E.Smtlib2) : S);
     Smtlib2 `Poly, ".psmt2",
-    (module Dolmen_smtlib2.Script.Poly.Make(L)(I)(T)(S) : S);
+    (module Dolmen_smtlib2.Script.Poly.Make(L)(I)(T)(S)(E.Smtlib2) : S);
 
     (* TPTP *)
     Tptp `Latest, ".p",

src/languages/smtlib2/poly/ast.ml

@@ -8,6 +8,23 @@
     in an interactive loop (so it includes directive for getting and setting options,
     getting information about the solver's internal model, etc...) *)
 
+module type Extension = sig
+
+  type location
+  (** The type of locations. *)
+
+  type term
+  (** The type of terms *)
+
+  type statement
+  (** The type of statements *)
+
+  val statement : string -> (?loc:location -> term list -> statement) option
+  (** Called on statements of the form `(<id> <term>)` where `<id>` is
+      not the name of a statement in the official smtlib specification. *)
+
+end
+
 module type Id = sig
 
   type t

src/languages/smtlib2/poly/dolmen_smtlib2_poly.ml

@@ -4,16 +4,18 @@
 module type Id = Ast.Id
 module type Term = Ast.Term
 module type Statement = Ast.Statement
+module type Extension = Ast.Extension
 
 module Make
     (L : Dolmen_intf.Location.S)
     (I : Id)
     (T : Term with type location := L.t and type id := I.t)
-    (S : Statement with type location := L.t and type id := I.t and type term := T.t) =
+    (S : Statement with type location := L.t and type id := I.t and type term := T.t)
+    (E : Extension with type location := L.t and type term := T.t and type statement := S.t) =
   Dolmen_std.Transformer.Make(L)(struct
     type token = Tokens.token
     type statement = S.t
     let env = []
     let incremental = true
     let error s = Syntax_messages.message s
-  end)(Lexer)(Parser.Make(L)(I)(T)(S))
+  end)(Lexer)(Parser.Make(L)(I)(T)(S)(E))

src/languages/smtlib2/poly/dolmen_smtlib2_poly.mli

@@ -6,12 +6,14 @@
 module type Id = Ast.Id
 module type Term = Ast.Term
 module type Statement = Ast.Statement
+module type Extension = Ast.Extension
 (** Implementation requirement for the Smtlib format. *)
 
 module Make
     (L : Dolmen_intf.Location.S)
     (I : Id)
     (T : Term with type location := L.t and type id := I.t)
-    (S : Statement with type location := L.t and type id := I.t and type term := T.t) :
+    (S : Statement with type location := L.t and type id := I.t and type term := T.t)
+    (E : Extension with type location := L.t and type term := T.t and type statement := S.t) :
   Dolmen_intf.Language.S with type statement = S.t and type file := L.file
 (** Functor to generate a parser for the Smtlib format. *)

src/languages/smtlib2/poly/parser.mly

@@ -5,6 +5,7 @@
 %parameter <I : Ast.Id>
 %parameter <T : Ast.Term with type location := L.t and type id := I.t>
 %parameter <S : Ast.Statement with type location := L.t and type id := I.t and type term := T.t>
+%parameter <E : Ast.Extension with type location := L.t and type term := T.t and type statement := S.t>
 
 %start <T.t> term
 %start <S.t list> file
@@ -471,6 +472,23 @@ command:
     { let loc = L.mk_pos $startpos $endpos in S.set_logic ~loc s }
   | OPEN SET_OPTION c=command_option CLOSE
     { let loc = L.mk_pos $startpos $endpos in S.set_option ~loc c }
+
+  | OPEN e=extension_statement l=s_expr* CLOSE
+    { let loc = Some (L.mk_pos $startpos $endpos) in
+      e ?loc l }
+;
+
+extension_statement:
+  | s=SYMBOL
+    { match E.statement s with
+      | Some mk_ext -> mk_ext
+      | None ->
+        let loc = L.mk_pos $startpos $endpos in
+        raise (L.Syntax_error (loc, `Advanced ("115",
+          Format.dprintf "a command",
+          Format.dprintf "the symbol '%s'" s,
+          Format.dprintf "a command name")))
+    }
 ;
 
 file: