From fc62d09029ef4626fd742cfc2ffdc3d73e4008c4 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Thu, 1 Dec 2022 16:44:04 +0100
Subject: [PATCH] [NSeq] updated builtins
---
colibri2/bin/dune | 3 +-
colibri2/theories/array/array.ml | 2 +-
colibri2/theories/nseq/nseq.ml | 128 +++++++++++++++++--------------
3 files changed, 73 insertions(+), 60 deletions(-)
diff --git a/colibri2/bin/dune b/colibri2/bin/dune
index b4abf839c..2eae1ca6d 100644
--- a/colibri2/bin/dune
+++ b/colibri2/bin/dune
@@ -22,7 +22,8 @@
colibri2.theories.quantifiers
colibri2.theories.fp
colibri2.theories.adt
- colibri2.theories.array)
+ colibri2.theories.array
+ colibri2.theories.nseq)
(modules main options))
; Colibri2 stage0
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 5147e8313..71c3be7db 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -705,7 +705,7 @@ module Theory = struct
let mapf_s = Ground.sem mapf_t in
let f_arity = IArray.length mapf_s.args - 1 in
NM.find new_map_db env f_arity
- Node.equal
+
(** gets a list of all the inhabitants of a given finite type *)
let get_gty_inhabitants (gty : Ground.Ty.t) =
match gty with
diff --git a/colibri2/theories/nseq/nseq.ml b/colibri2/theories/nseq/nseq.ml
index 929357d5c..07bfdc6b2 100644
--- a/colibri2/theories/nseq/nseq.ml
+++ b/colibri2/theories/nseq/nseq.ml
@@ -47,116 +47,128 @@ module Builtin = struct
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)
+ Expr.Id.mk ~name:"nseq_first" ~builtin:NSeq_first
+ (Dolmen_std.Path.global "nseq_first")
+ (Expr.Ty.pi [ val_ty_var ] (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)
+ Expr.Id.mk ~name:"nseq_last" ~builtin:NSeq_last
+ (Dolmen_std.Path.global "nseq_last")
+ (Expr.Ty.pi [ val_ty_var ] (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)
+ Expr.Id.mk ~name:"nseq_length" ~builtin:NSeq_length
+ (Dolmen_std.Path.global "nseq_length")
+ (Expr.Ty.pi [ val_ty_var ] (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)
+ Expr.Id.mk ~name:"nseq_get" ~builtin:NSeq_get
+ (Dolmen_std.Path.global "nseq_get")
+ (Expr.Ty.pi [ val_ty_var ] (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)
+ Expr.Id.mk ~name:"nseq_set" ~builtin:NSeq_set
+ (Dolmen_std.Path.global "nseq_set")
+ (Expr.Ty.pi [ val_ty_var ]
+ (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)
+ Expr.Id.mk ~name:"nseq_eq" ~builtin:NSeq_eq
+ (Dolmen_std.Path.global "nseq_eq")
+ (Expr.Ty.pi [ val_ty_var ]
+ (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)
+ Expr.Id.mk ~name:"nseq_const" ~builtin:NSeq_const
+ (Dolmen_std.Path.global "nseq_const")
+ (Expr.Ty.pi [ val_ty_var ]
+ (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)
+ Expr.Id.mk ~name:"nseq_empty" ~builtin:NSeq_empty
+ (Dolmen_std.Path.global "nseq_empty")
+ (Expr.Ty.pi [ val_ty_var ] (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)
+ Expr.Id.mk ~name:"nseq_concat" ~builtin:NSeq_concat
+ (Dolmen_std.Path.global "nseq_concat")
+ (Expr.Ty.pi [ val_ty_var ]
+ (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)
+ Expr.Id.mk ~name:"nseq_relocate" ~builtin:NSeq_relocate
+ (Dolmen_std.Path.global "nseq_relocate")
+ (Expr.Ty.pi [ val_ty_var ]
+ (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)
+ Expr.Id.mk ~name:"nseq_slice" ~builtin:NSeq_slice
+ (Dolmen_std.Path.global "nseq_slice")
+ (Expr.Ty.pi [ val_ty_var ]
+ (Expr.Ty.arrow [ val_nseq_ty; int_ty; int_ty ] val_nseq_ty))
+
+ let get_nseq_val : Expr.ty -> Expr.ty = function
+ | { ty_descr = TyApp ({ builtin = NSeq; _ }, [ val_ty ]); _ } -> val_ty
+ | ty ->
+ failwith (Format.asprintf "'%a' is not an nseq type!" Expr.Ty.print ty)
let () =
+ let ty_app1 env s f =
+ `Ty
+ (Dolmen_type.Base.ty_app1
+ (module Dolmen_loop.Typer.T)
+ env s
+ (fun ty -> Expr.Ty.apply f [ ty ]))
+ in
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 ]))
+ (fun a ->
+ Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ 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 ]))
+ (fun a b ->
+ Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ 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 ]))
+ (fun a b ->
+ Expr.Term.apply_cst f [ get_nseq_val a.Expr.term_ty ] [ a; b ]))
in
Expr.add_builtins (fun env s ->
match s with
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_first" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "seq" } ->
+ ty_app1 env s nseq_ty_const
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_first" } ->
app1 env s nseq_first
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_last" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_last" } ->
app1 env s nseq_last
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_length" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_length" } ->
app1 env s nseq_length
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_get" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_get" } ->
app2 env s nseq_get
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_set" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_set" } ->
app3 env s nseq_set
- | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri2_nseq_eq" }
- ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_eq" } ->
app2 env s nseq_get
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_const" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_const" } ->
app3 env s nseq_const
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_empty" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_empty" } ->
app2 env s nseq_empty
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_concat" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_concat" } ->
app2 env s nseq_concat
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_relocate" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_relocate" } ->
app2 env s nseq_relocate
- | Dolmen_loop.Typer.T.Id
- { ns = Term; name = Simple "colibri2_nseq_slice" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_slice" } ->
app3 env s nseq_slice
| _ -> `Not_found)
end
--
GitLab