From b99aa58db08e7283b3e371bec30b52566d50a188 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Mon, 4 May 2026 13:00:32 +0000 Subject: [PATCH 1/2] struct: synthesizer basic types (relational, without tests) --- model_with_structures/model.typ | 2 +- model_with_structures/synthesizer.ml | 115 +++++++++++++++++++++++++++ 2 files changed, 116 insertions(+), 1 deletion(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 6b4cf41..38b901b 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -98,7 +98,7 @@ // NOTE: do not use names in type // 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( diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 696722b..63c3871 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -56,6 +56,121 @@ struct ] end + module Mode = struct + [@@@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 *) + let n_val = let open InCap in + let open OutCap in + ocanren { Mode (NIn, NOut) } + let i_val = let open InCap in + let open OutCap in + ocanren { Mode (In, NOut) } + let o_val = let open InCap in + let open OutCap in + ocanren { Mode (NIn, Out) } + let io_val = let open InCap in + let open OutCap in + ocanren { Mode (In, Out) } + + (* accessors *) + let is_ino m = let open InCap in ocanren { + fresh o_ in + m == Mode (In, o_) } + let is_not_ino m = let open InCap in ocanren { + fresh o_ in + m == Mode (NIn, o_) } + let is_outo m = let open OutCap in ocanren { + fresh i_ in + m == Mode (i_, Out) } + let is_not_outo m = let open OutCap in ocanren { + fresh i_ in + m == Mode (i_, NOut) } + + (* module Test = struct *) + (* @type answer = logic GT.list with show *) + + (* let test _ = show(answer) (Stream.take (run q (fun q -> let open InCap in *) + (* let open OutCap in *) + (* ocanren {q == Mode (In, NOut)}) *) + (* (fun q -> q#reify reify))) *) + (* end *) + end + + (* TODO: access: data or int ? *) + module Path = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('d, 'p) t = VarP of 'd | DerefP of 'p | AccessP of 'p * 'd + [@@deriving gt ~options:{ show; gmap }] + type ground = (Nat.ground, ground) t + ] + end + + module Type = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + 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 ? *) + + module Expr = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('d, 'p, 'el) t = UnitE | PathE of 'p | RefE of 'd | TupleE of 'el + [@@deriving gt ~options:{ show; gmap }] + type ground = (Nat.ground, Path.ground, ground List.ground) t + ] + end + + module Stmt = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%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 + [@@deriving gt ~options:{ show; gmap }] + type ground = (Path.ground, Expr.ground List.ground, ground) t + ] + end + + (* TODO: list of 3 is not impelmented ?, replaced with two lists for now *) + module Decl = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('d, 't, 'e, 'dl, 'mtl, 's) t = VarD of 'd * 't * 'e | FunD of 'd * 'dl * 'mtl * 's + [@@deriving gt ~options:{ show; gmap }] + type ground = (Nat.ground, Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t + ] + end + + module Prog = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('dl, 's) t = Prog of 'dl * 's + [@@deriving gt ~options:{ show; gmap }] + type nonrec ground = (Decl.ground List.ground, Stmt.ground) t + ] + end + + (* NOTE: deepvalue - not used (?) *) + + module Value = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl + [@@deriving gt ~options:{ show; gmap }] + type ground = ((Nat.ground List.ground * Stmt.ground) List.ground, Nat.ground, ground List.ground) t + ] + end + (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) (* module Tag = struct *) From b31415cf8ebdf9c7a0b9fcc3ef039a7b8c85bada Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Mon, 4 May 2026 13:42:53 +0000 Subject: [PATCH 2/2] struct: sythesizer util functions --- model_with_structures/analyzer.ml | 3 +- model_with_structures/model.typ | 2 + model_with_structures/synthesizer.ml | 324 ++++++++------------------- 3 files changed, 94 insertions(+), 235 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 3e8ec19..31613ee 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -97,7 +97,8 @@ struct (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *) (* let mem_set (mem : mem) (id : memid) (v : value) : 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); *) List.nth (fst mem) (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) let mem_add (mem : mem) (v : value) : mem * memid = ((v :: fst mem, snd mem + 1), snd mem) let mem_set (mem : mem) (id : memid) (v : value) : mem = diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 38b901b..8ca0dc1 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -13,6 +13,8 @@ == Syntax +*TODO: top-level value copy mode ??* // TODO: FIXME + #h(10pt) #let rf = $\& #h(3pt)$ diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 63c3871..a277f4d 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -1,7 +1,7 @@ module Relational = struct open GT - (* open OCanren *) + open OCanren open OCanren.Std type data_ground = Nat.ground (* with show, gmap *) @@ -171,241 +171,97 @@ struct ] end + (* --- *) + + module Mem = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('vl, 'd) t = Mem of 'vl * 'd + [@@deriving gt ~options:{ show; gmap }] + type nonrec ground = (Value.ground List.ground, Nat.ground) t + ] + end + + module Types = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec 'dtl t = Types of 'dtl + [@@deriving gt ~options:{ show; gmap }] + type nonrec ground = ((Nat.ground * Type.ground) List.ground) t + ] + end + + module Vals = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec 'ddl t = Vals of 'ddl + [@@deriving gt ~options:{ show; gmap }] + type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t + ] + end + + module St = struct + [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + [%%ocanren_inject + type nonrec ('mem, 'types, 'vals) t = St of 'mem * 'types * 'vals + [@@deriving gt ~options:{ show; gmap }] + type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t + ] + 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 --- *) - (* module Tag = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t *) - (* ] *) - - (* TODO: less repeats *) - (* common constructors *) - (* let rwi_val = let open ReadCap in *) - (* let open WriteCap in *) - (* 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 *) - (* let is_reado tag = let open ReadCap in ocanren { *) - (* fresh w_, c_, i_, o_ in *) - (* tag == Tag (Rd, w_, c_, i_, o_) } *) - (* let is_not_reado tag = let open ReadCap in ocanren { *) - (* fresh w_, c_, i_, o_ in *) - (* tag == Tag (NRd, w_, c_, i_, o_) } *) - (* let is_always_writeo tag = let open WriteCap in ocanren { *) - (* fresh r_, c_, i_, o_ in *) - (* tag == Tag (r_, AlwaysWr, c_, i_, o_) } *) - (* let is_may_writeo tag = let open WriteCap in ocanren { *) - (* fresh r_, c_, i_, o_ in *) - (* { 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 *) - (* @type answer = logic GT.list with show *) - - (* 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 *) - (* ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)}) *) - (* (fun q -> q#reify reify))) *) - (* end *) - (* end *) - - (* module Stmt = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t *) - (* ] *) - - (* module Test = struct *) - (* @type answer = Nat.ground List.ground GT.list with show *) - (* @type answer' = ground GT.list with show *) - - (* 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)))) *) - - (* let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q}) *) - (* (fun q -> q#reify (prj_exn)))) *) - (* end *) - (* end *) - - (* module FunDecl = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec ('l, 'b) t = FunDecl of 'l * 'b *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t *) - (* ] *) - - (* module Test = struct *) - (* @type answer = ground GT.list with show *) - (* let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in *) - (* let open Stmt in *) - (* ocanren {FunDecl ([rwi_ref; rwi_val], [Call (1, [0]); Write 1]) == q}) *) - (* (fun q -> q#reify (prj_exn)))) *) - (* end *) - (* end *) - - (* module Prog = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec ('l, 'f) t = Prog of 'l * 'f *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t *) - (* ] *) - - (* 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 Arg = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec 'd t = RValue | LValue of 'd *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = Nat.ground t *) - (* ] *) - - (* 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 Value = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec t = Unit | Undef | Bot *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* type nonrec ground = t *) - (* ] *) - - (* module Test = struct *) - (* @type answer = logic GT.list with show *) - (* let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit}) *) - (* (fun q -> q#reify reify))) *) - (* end *) - (* end *) - - (* module St = struct *) - (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *) - (* [%%ocanren_inject *) - (* type nonrec ('env, 'mem, 'last_mem, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited *) - (* [@@deriving gt ~options:{ show; gmap }] *) - (* 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 *) - (* ] *) - - (* module Test = struct *) - (* @type answer = ground GT.list with show *) - (* let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in *) - (* let open Tag in *) - (* ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q}) *) - (* (fun q -> q#reify (prj_exn)))) *) - (* end *) - (* end *) - (* --- *) (* let rec list_zip_witho f xs ys zs = ocanren { *)