[NSeq] updated builtins

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

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

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