[Seq] Added builtins

colibri2/theories/array/array.ml

@@ -141,23 +141,24 @@ module Builtin = struct
         (Dolmen_type.Base.term_app2
            (module Dolmen_loop.Typer.T)
            env s
-           (fun a b ->
-             assert (Expr.Term.ty a == Expr.Term.ty b);
-             Expr.Term.apply_cst f [] [ a; b ]))
+           (fun a b -> apply_cst f [] [ a; b ]))
     in
     Expr.add_builtins (fun env s ->
         match s with
-        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "array_diff" } ->
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_array_diff" } ->
             app2 env s array_diff
-        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "array_const" } ->
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_array_const" } ->
             app1 env s array_const
         | Dolmen_loop.Typer.T.Id
-            { ns = Term; name = Simple "array_default_index" } ->
+            { ns = Term; name = Simple "colibri2_array_default_index" } ->
             app1 env s array_default_index
         | Dolmen_loop.Typer.T.Id
-            { ns = Term; name = Simple "array_default_value" } ->
+            { ns = Term; name = Simple "colibri2_array_default_value" } ->
             app1 env s array_default_value
-        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "array_map" } ->
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_array_map" } ->
             `Term
               (Dolmen_type.Base.term_app_list
                  (module Dolmen_loop.Typer.T)

colibri2/theories/array/dune

 (library
  (name colibri2_theories_array)
  (public_name colibri2.theories.array)
- (synopsis "theory array for colibri2")
+ (synopsis "The array theory for colibri2")
  (libraries
   containers
   ocamlgraph

colibri2/theories/nseq/dune

+(library
+ (name colibri2_theories_nseq)
+ (public_name colibri2.theories.nseq)
+ (synopsis "The theory of n-sequences for colibri2")
+ (libraries
+  containers
+  ocamlgraph
+  colibri2.stdlib
+  colibri2.popop_lib
+  colibri2.core
+  colibri2.theories.quantifiers)
+ (preprocess
+  (pps ppx_deriving.std ppx_hash))
+ (flags
+  :standard
+  -w
+  +a-4-42-44-48-50-58-32-60-40-9@8
+  -color
+  always
+  -open
+  Colibri2_stdlib
+  -open
+  Std
+  -open
+  Colibri2_core
+  -open
+  Colibri2_theories_bool)
+ (ocamlopt_flags
+  :standard
+  -O3
+  -bin-annot
+  -unbox-closures
+  -unbox-closures-factor
+  20))

colibri2/theories/nseq/nseq.ml

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)
+
+(* Builtins *)
+module Builtin = struct
+  type _ Expr.t +=
+    | NSeq
+    | NSeq_first
+    | NSeq_last
+    | NSeq_length
+    | NSeq_get
+    | NSeq_set
+    | NSeq_eq
+    | NSeq_const
+    | NSeq_empty
+    | NSeq_concat
+    | NSeq_relocate
+    | NSeq_slice
+
+  let nseq_ty_const : Expr.Term.ty_const =
+    Expr.Id.mk ~builtin:NSeq
+      (Dolmen_std.Path.global "nseq")
+      Expr.{ arity = 1; alias = No_alias }
+
+  let int_ty = Expr.Ty.int
+  let nseq_ty ty = Expr.Ty.apply nseq_ty_const [ ty ]
+  let val_ty_var = Expr.Ty.Var.mk "val_ty"
+  let val_ty = Expr.Ty.of_var val_ty_var
+  let val_nseq_ty = nseq_ty val_ty
+
+  let nseq_first : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_first" ~builtin:NSeq_first
+      (Dolmen_std.Path.global "colibri2_nseq_first")
+      (Expr.Ty.arrow [ val_nseq_ty ] int_ty)
+
+  let nseq_last : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_last" ~builtin:NSeq_last
+      (Dolmen_std.Path.global "colibri2_nseq_last")
+      (Expr.Ty.arrow [ val_nseq_ty ] int_ty)
+
+  let nseq_length : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_length" ~builtin:NSeq_length
+      (Dolmen_std.Path.global "colibri2_nseq_length")
+      (Expr.Ty.arrow [ val_nseq_ty ] int_ty)
+
+  let nseq_get : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_get" ~builtin:NSeq_get
+      (Dolmen_std.Path.global "colibri2_nseq_get")
+      (Expr.Ty.arrow [ val_nseq_ty; int_ty ] val_ty)
+
+  let nseq_set : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_set" ~builtin:NSeq_set
+      (Dolmen_std.Path.global "colibri2_nseq_set")
+      (Expr.Ty.arrow [ val_nseq_ty; int_ty; val_ty ] val_nseq_ty)
+
+  let nseq_eq : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_eq" ~builtin:NSeq_eq
+      (Dolmen_std.Path.global "colibri2_nseq_eq")
+      (Expr.Ty.arrow [ val_nseq_ty; val_nseq_ty ] Expr.Ty.bool)
+
+  let nseq_const : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_const" ~builtin:NSeq_const
+      (Dolmen_std.Path.global "colibri2_nseq_const")
+      (Expr.Ty.arrow [ int_ty; int_ty; val_ty ] val_nseq_ty)
+
+  let nseq_empty : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_empty" ~builtin:NSeq_empty
+      (Dolmen_std.Path.global "colibri2_nseq_empty")
+      (Expr.Ty.arrow [ int_ty; int_ty ] val_nseq_ty)
+
+  let nseq_concat : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_concat" ~builtin:NSeq_concat
+      (Dolmen_std.Path.global "colibri2_nseq_concat")
+      (Expr.Ty.arrow [ val_nseq_ty; val_nseq_ty ] val_nseq_ty)
+
+  let nseq_relocate : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_relocate" ~builtin:NSeq_relocate
+      (Dolmen_std.Path.global "colibri2_nseq_relocate")
+      (Expr.Ty.arrow [ val_nseq_ty; int_ty ] val_nseq_ty)
+
+  let nseq_slice : Dolmen_std.Expr.term_cst =
+    Expr.Id.mk ~name:"colibri2_nseq_slice" ~builtin:NSeq_slice
+      (Dolmen_std.Path.global "colibri2_nseq_slice")
+      (Expr.Ty.arrow [ val_nseq_ty; int_ty; int_ty ] val_nseq_ty)
+
+  let () =
+    let app1 env s f =
+      `Term
+        (Dolmen_type.Base.term_app1
+           (module Dolmen_loop.Typer.T)
+           env s
+           (fun a -> Expr.Term.apply_cst f [] [ a ]))
+    in
+    let app2 env s f =
+      `Term
+        (Dolmen_type.Base.term_app2
+           (module Dolmen_loop.Typer.T)
+           env s
+           (fun a b -> Expr.Term.apply_cst f [] [ a; b ]))
+    in
+    let app3 env s f =
+      `Term
+        (Dolmen_type.Base.term_app2
+           (module Dolmen_loop.Typer.T)
+           env s
+           (fun a b -> Expr.Term.apply_cst f [] [ a; b ]))
+    in
+    Expr.add_builtins (fun env s ->
+        match s with
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_first" } ->
+            app1 env s nseq_first
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_last" } ->
+            app1 env s nseq_last
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_length" } ->
+            app1 env s nseq_length
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_get" } ->
+            app2 env s nseq_get
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_set" } ->
+            app3 env s nseq_set
+        | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri2_nseq_eq" }
+          ->
+            app2 env s nseq_get
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_const" } ->
+            app3 env s nseq_const
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_empty" } ->
+            app2 env s nseq_empty
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_concat" } ->
+            app2 env s nseq_concat
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_relocate" } ->
+            app2 env s nseq_relocate
+        | Dolmen_loop.Typer.T.Id
+            { ns = Term; name = Simple "colibri2_nseq_slice" } ->
+            app3 env s nseq_slice
+        | _ -> `Not_found)
+end

colibri2/theories/nseq/nseq.mli

+(*************************************************************************)
+(*  This file is part of Colibri2.                                       *)
+(*                                                                       *)
+(*  Copyright (C) 2014-2021                                              *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
+(*           alternatives)                                               *)
+(*    OCamlPro                                                           *)
+(*                                                                       *)
+(*  you can redistribute it and/or modify it under the terms of the GNU  *)
+(*  Lesser General Public License as published by the Free Software      *)
+(*  Foundation, version 2.1.                                             *)
+(*                                                                       *)
+(*  It is distributed in the hope that it will be useful,                *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
+(*  GNU Lesser General Public License for more details.                  *)
+(*                                                                       *)
+(*  See the GNU Lesser General Public License version 2.1                *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
+(*************************************************************************)