From 77e92cc70f09434fd0779cd10f8528e7f1609bab Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 22 Nov 2022 23:37:13 +0100
Subject: [PATCH] [Seq] Added builtins
---
colibri2/theories/array/array.ml | 17 +--
colibri2/theories/array/dune | 2 +-
colibri2/theories/nseq/.ocamlformat | 0
colibri2/theories/nseq/dune | 34 ++++++
colibri2/theories/nseq/nseq.ml | 162 ++++++++++++++++++++++++++++
colibri2/theories/nseq/nseq.mli | 20 ++++
6 files changed, 226 insertions(+), 9 deletions(-)
create mode 100644 colibri2/theories/nseq/.ocamlformat
create mode 100644 colibri2/theories/nseq/dune
create mode 100644 colibri2/theories/nseq/nseq.ml
create mode 100644 colibri2/theories/nseq/nseq.mli
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 41c232ae6..f318eb324 100644
--- a/colibri2/theories/array/array.ml
+++ b/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)
diff --git a/colibri2/theories/array/dune b/colibri2/theories/array/dune
index 928124146..fee0822d2 100644
--- a/colibri2/theories/array/dune
+++ b/colibri2/theories/array/dune
@@ -1,7 +1,7 @@
(library
(name colibri2_theories_array)
(public_name colibri2.theories.array)
- (synopsis "theory array for colibri2")
+ (synopsis "The array theory for colibri2")
(libraries
containers
ocamlgraph
diff --git a/colibri2/theories/nseq/.ocamlformat b/colibri2/theories/nseq/.ocamlformat
new file mode 100644
index 000000000..e69de29bb
diff --git a/colibri2/theories/nseq/dune b/colibri2/theories/nseq/dune
new file mode 100644
index 000000000..148b27614
--- /dev/null
+++ b/colibri2/theories/nseq/dune
@@ -0,0 +1,34 @@
+(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))
diff --git a/colibri2/theories/nseq/nseq.ml b/colibri2/theories/nseq/nseq.ml
new file mode 100644
index 000000000..929357d5c
--- /dev/null
+++ b/colibri2/theories/nseq/nseq.ml
@@ -0,0 +1,162 @@
+(*************************************************************************)
+(* 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
diff --git a/colibri2/theories/nseq/nseq.mli b/colibri2/theories/nseq/nseq.mli
new file mode 100644
index 000000000..4bf15b085
--- /dev/null
+++ b/colibri2/theories/nseq/nseq.mli
@@ -0,0 +1,20 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
--
GitLab