mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
No commits in common. "b31415cf8ebdf9c7a0b9fcc3ef039a7b8c85bada" and "66ea0e53da2fdc4867f0fd110491cc7b343736c1" have entirely different histories.
b31415cf8e
...
66ea0e53da
3 changed files with 213 additions and 187 deletions
|
|
@ -97,8 +97,7 @@ struct
|
||||||
(* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
|
(* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
|
||||||
(* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
|
(* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
|
||||||
(* ((id, v) :: fst mem, snd mem) *)
|
(* ((id, v) :: fst mem, snd mem) *)
|
||||||
let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *)
|
let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *) List.nth (fst mem) (snd mem - id - 1)
|
||||||
List.nth (fst mem) (snd mem - id - 1)
|
|
||||||
let mem_add (mem : mem) (v : value) : mem * memid =
|
let mem_add (mem : mem) (v : value) : mem * memid =
|
||||||
((v :: fst mem, snd mem + 1), snd mem)
|
((v :: fst mem, snd mem + 1), snd mem)
|
||||||
let mem_set (mem : mem) (id : memid) (v : value) : mem =
|
let mem_set (mem : mem) (id : memid) (v : value) : mem =
|
||||||
|
|
|
||||||
|
|
@ -13,8 +13,6 @@
|
||||||
|
|
||||||
== Syntax
|
== Syntax
|
||||||
|
|
||||||
*TODO: top-level value copy mode ??* // TODO: FIXME
|
|
||||||
|
|
||||||
#h(10pt)
|
#h(10pt)
|
||||||
|
|
||||||
#let rf = $\& #h(3pt)$
|
#let rf = $\& #h(3pt)$
|
||||||
|
|
@ -100,7 +98,7 @@
|
||||||
|
|
||||||
// NOTE: do not use names in type
|
// NOTE: do not use names in type
|
||||||
// Or[$lambda_((x type)+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
|
// Or[$lambda_((x type)+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
|
||||||
Or[$lambda (modedType+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
|
Or[$lambda (modedType)+$][type of lambda or function pointer, defined by function declaration] // `Fun`
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
Prod(
|
Prod(
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
module Relational =
|
module Relational =
|
||||||
struct
|
struct
|
||||||
open GT
|
open GT
|
||||||
open OCanren
|
(* open OCanren *)
|
||||||
open OCanren.Std
|
open OCanren.Std
|
||||||
|
|
||||||
type data_ground = Nat.ground (* with show, gmap *)
|
type data_ground = Nat.ground (* with show, gmap *)
|
||||||
|
|
@ -56,211 +56,240 @@ struct
|
||||||
]
|
]
|
||||||
end
|
end
|
||||||
|
|
||||||
module Mode = struct
|
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
|
||||||
[%%ocanren_inject
|
|
||||||
type nonrec ('i, 'o) t = Mode of 'i * 'o
|
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
|
||||||
type nonrec ground = (InCap.ground, OutCap.ground) t
|
|
||||||
]
|
|
||||||
|
|
||||||
(* constructors *)
|
(* module Tag = struct *)
|
||||||
let n_val = let open InCap in
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
let open OutCap in
|
(* [%%ocanren_inject *)
|
||||||
ocanren { Mode (NIn, NOut) }
|
(* type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o *)
|
||||||
let i_val = let open InCap in
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
let open OutCap in
|
(* type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t *)
|
||||||
ocanren { Mode (In, NOut) }
|
(* ] *)
|
||||||
let o_val = let open InCap in
|
|
||||||
let open OutCap in
|
(* TODO: less repeats *)
|
||||||
ocanren { Mode (NIn, Out) }
|
(* common constructors *)
|
||||||
let io_val = let open InCap in
|
(* let rwi_val = let open ReadCap in *)
|
||||||
let open OutCap in
|
(* let open WriteCap in *)
|
||||||
ocanren { Mode (In, Out) }
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (Rd, AlwaysWr, Val, In, NOut) } *)
|
||||||
|
(* let ri_val = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (Rd, NeverWr, Val, In, NOut) } *)
|
||||||
|
(* let wi_val = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (NRd, AlwaysWr, Val, In, NOut) } *)
|
||||||
|
(* let i_val = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (NRd, NeverWr, Val, In, NOut) } *)
|
||||||
|
(* let rwi_ref = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (Rd, AlwaysWr, Ref, In, NOut) } *)
|
||||||
|
(* let ri_ref = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (Rd, NeverWr, Ref, In, NOut) } *)
|
||||||
|
(* let wi_ref = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (NRd, AlwaysWr, Ref, In, NOut) } *)
|
||||||
|
(* let i_ref = let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { Tag (NRd, NeverWr, Ref, In, NOut) } *)
|
||||||
|
|
||||||
|
(* constraints *)
|
||||||
|
(* let x_any tag = let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { fresh r, w, c in *)
|
||||||
|
(* tag == Tag (r, w, c, NIn, NOut) } *)
|
||||||
|
(* let i_any tag = let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { fresh r, w, c in *)
|
||||||
|
(* tag == Tag (r, w, c, In, NOut) } *)
|
||||||
|
(* let o_any tag = let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { fresh r, w, c in *)
|
||||||
|
(* tag == Tag (r, w, c, NIn, Out) } *)
|
||||||
|
(* let io_any tag = let open InCap in *)
|
||||||
|
(* let open OutCap in *)
|
||||||
|
(* ocanren { fresh r, w, c in *)
|
||||||
|
(* tag == Tag (r, w, c, In, Out) } *)
|
||||||
|
|
||||||
(* accessors *)
|
(* accessors *)
|
||||||
let is_ino m = let open InCap in ocanren {
|
(* let is_reado tag = let open ReadCap in ocanren { *)
|
||||||
fresh o_ in
|
(* fresh w_, c_, i_, o_ in *)
|
||||||
m == Mode (In, o_) }
|
(* tag == Tag (Rd, w_, c_, i_, o_) } *)
|
||||||
let is_not_ino m = let open InCap in ocanren {
|
(* let is_not_reado tag = let open ReadCap in ocanren { *)
|
||||||
fresh o_ in
|
(* fresh w_, c_, i_, o_ in *)
|
||||||
m == Mode (NIn, o_) }
|
(* tag == Tag (NRd, w_, c_, i_, o_) } *)
|
||||||
let is_outo m = let open OutCap in ocanren {
|
(* let is_always_writeo tag = let open WriteCap in ocanren { *)
|
||||||
fresh i_ in
|
(* fresh r_, c_, i_, o_ in *)
|
||||||
m == Mode (i_, Out) }
|
(* tag == Tag (r_, AlwaysWr, c_, i_, o_) } *)
|
||||||
let is_not_outo m = let open OutCap in ocanren {
|
(* let is_may_writeo tag = let open WriteCap in ocanren { *)
|
||||||
fresh i_ in
|
(* fresh r_, c_, i_, o_ in *)
|
||||||
m == Mode (i_, NOut) }
|
(* { tag == Tag (r_, AlwaysWr, c_, i_, o_) | *)
|
||||||
|
(* tag == Tag (r_, MayWr, c_, i_, o_) } } *)
|
||||||
|
(* let is_never_writeo tag = let open WriteCap in ocanren { *)
|
||||||
|
(* fresh r_, c_, i_, o_ in *)
|
||||||
|
(* tag == Tag (r_, NeverWr, c_, i_, o_) } *)
|
||||||
|
(* let is_refo tag = let open CopyCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, i_, o_ in *)
|
||||||
|
(* tag == Tag (r_, w_, Ref, i_, o_) } *)
|
||||||
|
(* let is_valueo tag = let open CopyCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, i_, o_ in *)
|
||||||
|
(* tag == Tag (r_, w_, Val, i_, o_) } *)
|
||||||
|
(* let is_ino tag = let open InCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, c_, o_ in *)
|
||||||
|
(* tag == Tag (r_, w_, c_, In, o_) } *)
|
||||||
|
(* let is_not_ino tag = let open InCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, c_, o_ in *)
|
||||||
|
(* tag == Tag (r_, w_, c_, NIn, o_) } *)
|
||||||
|
(* let is_outo tag = let open OutCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, c_, i_ in *)
|
||||||
|
(* tag == Tag (r_, w_, c_, i_, Out) } *)
|
||||||
|
(* let is_not_outo tag = let open OutCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, c_, i_ in *)
|
||||||
|
(* tag == Tag (r_, w_, c_, i_, NOut) } *)
|
||||||
|
|
||||||
|
(* let eq_copyo tag cp = let open CopyCap in ocanren { *)
|
||||||
|
(* fresh r_, w_, i_, o_ in *)
|
||||||
|
(* tag == Tag (r_, w_, cp, i_, o_) } *)
|
||||||
|
|
||||||
(* module Test = struct *)
|
(* module Test = struct *)
|
||||||
(* @type answer = logic GT.list with show *)
|
(* @type answer = logic GT.list with show *)
|
||||||
|
|
||||||
(* let test _ = show(answer) (Stream.take (run q (fun q -> let open InCap in *)
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> let open ReadCap in *)
|
||||||
|
(* let open WriteCap in *)
|
||||||
|
(* let open CopyCap in *)
|
||||||
|
(* let open InCap in *)
|
||||||
(* let open OutCap in *)
|
(* let open OutCap in *)
|
||||||
(* ocanren {q == Mode (In, NOut)}) *)
|
(* ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)}) *)
|
||||||
(* (fun q -> q#reify reify))) *)
|
(* (fun q -> q#reify reify))) *)
|
||||||
(* end *)
|
(* end *)
|
||||||
end
|
(* end *)
|
||||||
|
|
||||||
(* TODO: access: data or int ? *)
|
(* module Stmt = struct *)
|
||||||
module Path = struct
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [%%ocanren_inject *)
|
||||||
[%%ocanren_inject
|
(* type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl *)
|
||||||
type nonrec ('d, 'p) t = VarP of 'd | DerefP of 'p | AccessP of 'p * 'd
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t *)
|
||||||
type ground = (Nat.ground, ground) t
|
(* ] *)
|
||||||
]
|
|
||||||
end
|
|
||||||
|
|
||||||
module Type = struct
|
(* module Test = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* @type answer = Nat.ground List.ground GT.list with show *)
|
||||||
[%%ocanren_inject
|
(* @type answer' = ground GT.list with show *)
|
||||||
type nonrec ('r, 'w, 'c, 't, 'tl, 'mtl) t = UnitT of 'r * 'w | RefT of 'c * 't | TupleT of 'tl | FunT of 'mtl
|
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
|
||||||
type ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, ground, ground List.ground, (Mode.ground * ground) List.ground) t
|
|
||||||
]
|
|
||||||
end
|
|
||||||
|
|
||||||
(* moded type - no separated type ? *)
|
(* let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)}) *)
|
||||||
|
(* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
|
||||||
|
|
||||||
module Expr = struct
|
(* let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q}) *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* (fun q -> q#reify (prj_exn)))) *)
|
||||||
[%%ocanren_inject
|
(* end *)
|
||||||
type nonrec ('d, 'p, 'el) t = UnitE | PathE of 'p | RefE of 'd | TupleE of 'el
|
(* end *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
|
||||||
type ground = (Nat.ground, Path.ground, ground List.ground) t
|
|
||||||
]
|
|
||||||
end
|
|
||||||
|
|
||||||
module Stmt = struct
|
(* module FunDecl = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[%%ocanren_inject
|
(* [%%ocanren_inject *)
|
||||||
type nonrec ('p, 'el, 's) t = SkipS | CallS of 'p * 'el | WriteS of 'p | ReadS of 'p | SeqS of 's * 's | ChoiceS of 's * 's
|
(* type nonrec ('l, 'b) t = FunDecl of 'l * 'b *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
type ground = (Path.ground, Expr.ground List.ground, ground) t
|
(* type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t *)
|
||||||
]
|
(* ] *)
|
||||||
end
|
|
||||||
|
|
||||||
(* TODO: list of 3 is not impelmented ?, replaced with two lists for now *)
|
(* module Test = struct *)
|
||||||
module Decl = struct
|
(* @type answer = ground GT.list with show *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in *)
|
||||||
[%%ocanren_inject
|
(* let open Stmt in *)
|
||||||
type nonrec ('d, 't, 'e, 'dl, 'mtl, 's) t = VarD of 'd * 't * 'e | FunD of 'd * 'dl * 'mtl * 's
|
(* ocanren {FunDecl ([rwi_ref; rwi_val], [Call (1, [0]); Write 1]) == q}) *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* (fun q -> q#reify (prj_exn)))) *)
|
||||||
type ground = (Nat.ground, Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
|
(* end *)
|
||||||
]
|
(* end *)
|
||||||
end
|
|
||||||
|
|
||||||
module Prog = struct
|
(* module Prog = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[%%ocanren_inject
|
(* [%%ocanren_inject *)
|
||||||
type nonrec ('dl, 's) t = Prog of 'dl * 's
|
(* type nonrec ('l, 'f) t = Prog of 'l * 'f *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
type nonrec ground = (Decl.ground List.ground, Stmt.ground) t
|
(* type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t *)
|
||||||
]
|
(* ] *)
|
||||||
end
|
|
||||||
|
|
||||||
(* NOTE: deepvalue - not used (?) *)
|
(* module Test = struct *)
|
||||||
|
(* @type answer = ground GT.list with show *)
|
||||||
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in *)
|
||||||
|
(* let open Tag in *)
|
||||||
|
(* let open Stmt in *)
|
||||||
|
(* ocanren {Prog ([], FunDecl ([ri_val], [Write 0; Read 0])) == q}) *)
|
||||||
|
(* (fun q -> q#reify (prj_exn)))) *)
|
||||||
|
(* end *)
|
||||||
|
(* end *)
|
||||||
|
|
||||||
module Value = struct
|
(* module Arg = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[%%ocanren_inject
|
(* [%%ocanren_inject *)
|
||||||
type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
|
(* type nonrec 'd t = RValue | LValue of 'd *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
type ground = ((Nat.ground List.ground * Stmt.ground) List.ground, Nat.ground, ground List.ground) t
|
(* type nonrec ground = Nat.ground t *)
|
||||||
]
|
(* ] *)
|
||||||
end
|
|
||||||
|
|
||||||
(* --- *)
|
(* module Test = struct *)
|
||||||
|
(* @type answer = logic GT.list with show *)
|
||||||
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3}) *)
|
||||||
|
(* (fun q -> q#reify reify))) *)
|
||||||
|
(* end *)
|
||||||
|
(* end *)
|
||||||
|
|
||||||
module Mem = struct
|
(* module Value = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[%%ocanren_inject
|
(* [%%ocanren_inject *)
|
||||||
type nonrec ('vl, 'd) t = Mem of 'vl * 'd
|
(* type nonrec t = Unit | Undef | Bot *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
type nonrec ground = (Value.ground List.ground, Nat.ground) t
|
(* type nonrec ground = t *)
|
||||||
]
|
(* ] *)
|
||||||
end
|
|
||||||
|
|
||||||
module Types = struct
|
(* module Test = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* @type answer = logic GT.list with show *)
|
||||||
[%%ocanren_inject
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit}) *)
|
||||||
type nonrec 'dtl t = Types of 'dtl
|
(* (fun q -> q#reify reify))) *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* end *)
|
||||||
type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
|
(* end *)
|
||||||
]
|
|
||||||
end
|
|
||||||
|
|
||||||
module Vals = struct
|
(* module St = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
|
||||||
[%%ocanren_inject
|
(* [%%ocanren_inject *)
|
||||||
type nonrec 'ddl t = Vals of 'ddl
|
(* type nonrec ('env, 'mem, 'last_mem, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* [@@deriving gt ~options:{ show; gmap }] *)
|
||||||
type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
|
(* type nonrec ground = (((Nat.ground, ((Tag.ground, Nat.ground) Pair.ground)) Pair.ground) List.ground, *)
|
||||||
]
|
(* Value.ground List.ground, Nat.ground, Nat.ground List.ground) t *)
|
||||||
end
|
(* ] *)
|
||||||
|
|
||||||
module St = struct
|
(* module Test = struct *)
|
||||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
(* @type answer = ground GT.list with show *)
|
||||||
[%%ocanren_inject
|
(* let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in *)
|
||||||
type nonrec ('mem, 'types, 'vals) t = St of 'mem * 'types * 'vals
|
(* let open Tag in *)
|
||||||
[@@deriving gt ~options:{ show; gmap }]
|
(* ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q}) *)
|
||||||
type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t
|
(* (fun q -> q#reify (prj_exn)))) *)
|
||||||
]
|
(* end *)
|
||||||
end
|
(* end *)
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
(* - utils *)
|
|
||||||
|
|
||||||
let rec list_replaceo xs id value ys = ocanren {
|
|
||||||
(* xs == [] & ys == [] | (* NOTE: error *) *)
|
|
||||||
{ fresh x, xs' in
|
|
||||||
xs == x :: xs' &
|
|
||||||
id == Nat.o &
|
|
||||||
ys == value :: xs' } |
|
|
||||||
{ fresh x, xs', id', ys' in
|
|
||||||
xs == x :: xs' &
|
|
||||||
id == Nat.s id' &
|
|
||||||
ys == x :: ys' &
|
|
||||||
list_replaceo xs' id' value ys' }
|
|
||||||
}
|
|
||||||
|
|
||||||
let rec list_ntho xs id x' = ocanren {
|
|
||||||
(* xs == [] | (* NOTE: error *) *)
|
|
||||||
{ fresh y', xs' in
|
|
||||||
id == Nat.o &
|
|
||||||
y' :: xs' == xs &
|
|
||||||
x' == y' } |
|
|
||||||
{ fresh id', y', xs' in
|
|
||||||
Nat.s id' == id &
|
|
||||||
y' :: xs' == xs &
|
|
||||||
list_ntho xs' id' x' }
|
|
||||||
}
|
|
||||||
|
|
||||||
let mem_geto mem id v = ocanren {
|
|
||||||
fresh mem_data, mem_len, rev_id in
|
|
||||||
Std.pair mem_data mem_len == mem &
|
|
||||||
Nat.addo (Nat.s rev_id) id mem_len &
|
|
||||||
list_ntho mem_data rev_id v
|
|
||||||
}
|
|
||||||
|
|
||||||
let mem_addo mem v mem_with_id' = ocanren {
|
|
||||||
fresh mem_data, mem_len, mem' in
|
|
||||||
Std.pair mem_data mem_len == mem &
|
|
||||||
mem' == Std.pair (v :: mem_data) (Nat.s mem_len) &
|
|
||||||
Std.pair mem' mem_len == mem_with_id'
|
|
||||||
}
|
|
||||||
|
|
||||||
let mem_seto mem id v mem' = ocanren {
|
|
||||||
fresh mem_data, mem_len, rev_id, mem_data' in
|
|
||||||
Std.pair mem_data mem_len == mem &
|
|
||||||
Nat.addo (Nat.s rev_id) id mem_len &
|
|
||||||
list_replaceo mem_data rev_id v mem_data' &
|
|
||||||
Std.pair mem_data' mem_len == mem'
|
|
||||||
}
|
|
||||||
|
|
||||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
|
||||||
|
|
||||||
(* --- *)
|
(* --- *)
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue