From 80ac511c7a8be2b01089963243d4e4d5e9ee012b Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 1 May 2026 13:40:56 +0000 Subject: [PATCH 1/2] structures: ref expr (semantics & impl, only for var refs for now), simple tests & constructor abbriviations for future --- model_with_structures/analyzer.ml | 147 ++++++++++++++++++++++++++---- model_with_structures/model.typ | 70 +++++++------- 2 files changed, 168 insertions(+), 49 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 006a42a..3e8ec19 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -27,7 +27,8 @@ struct type expr = UnitE | PathE of path - (* | RefE *) + (* TODO: extend to include arbitrary path *) + | RefE of data | TupleE of expr list type stmt = SkipS @@ -96,11 +97,11 @@ 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 = List.nth (fst mem) id + 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 = - (list_replace (fst mem) id v, snd mem) + (list_replace (fst mem) (snd mem - id - 1) v, snd mem) let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with | ZeroV -> ZeroDV @@ -130,7 +131,12 @@ struct | _ -> raise @@ Typing_error "pathtype: access" let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with - | VarP x -> mem_get mem @@ List.assoc x vals + | VarP x -> mem_get mem @@ ((* Printf.printf "%i: " x; (* FIXME TMP *) + ignore @@ List.map (fun (x, _) -> Printf.printf "%i " x) vals; + Printf.printf "mem size: %i, " (List.length (fst mem)); + Printf.printf "mem size stored: %i " (snd mem); + Printf.printf "\n"; *) + List.assoc x vals) | DerefP p -> (match pathval mem vals p with | RefV id -> mem_get mem id | _ -> raise @@ Typing_error "pathval: deref") @@ -197,6 +203,7 @@ struct let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with | UnitE -> ZeroV | PathE p -> pathval mem vals p + | RefE x -> RefV (List.assoc x vals) | TupleE es -> TupleV (List.map (exprval mem vals) es) (* - expression typing *) @@ -204,6 +211,7 @@ struct let rec exprtype (types : types) (e : expr) : atype = match e with | UnitE -> UnitT (Rd, NeverWr) | PathE p -> pathtype types p + | RefE x -> RefT (Rf, List.assoc x types) | TupleE es -> TupleT (List.map (exprtype types) es) (* - context initialization *) @@ -220,7 +228,8 @@ struct | FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in (mem', (x, FunT ts) :: types, (x, id) :: vals) - let empty_state : state = (([], 0), [], []) + let empty_mem : mem = ([], 0) + let empty_state : state = (empty_mem, [], []) (* TODO: better way ??? *) let globals_min_id : data = 1000 @@ -237,11 +246,18 @@ struct let is_correct_tags (v : value) (r : read_cap) (w : write_cap) (r' : read_cap) (w' : write_cap) (m : mode) (c : copy_cap) : bool = + (* FIXME TMP + Printf.printf "%b %b %b %b %b\n" + (r != Rd || v == ZeroV) + (r != Rd || fst m == In) + (snd m != Out || w == AlwaysWr) + (((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr)) + (is_trivial_v v); *) (r != Rd || v == ZeroV) && (r != Rd || fst m == In) && (snd m != Out || w == AlwaysWr) && (* TODO: check *) - ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) && + ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) && is_trivial_v v let rec valspoil (mem : mem) (v : value) (t : atype) @@ -291,13 +307,13 @@ struct (* - funciton argument addition *) - let addarg (state : state) (x : data) (t : atype) (e : expr) : state = + let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state = match state with (mem, types, vals) -> - let v = exprval mem vals e in + let v = exprval mem oldvals e in (* let t' = pathtype types p in *) let (mem', v') = valcopy mem v t in let (mem'', id) = mem_add mem' v in - (mem', (x, t) :: types, (x, id) :: vals) + (mem'', (x, t) :: types, (x, id) :: vals) (* - function evaluation *) @@ -310,23 +326,25 @@ struct match state with (mem, types, vals) -> match s with (* TODO: FIXME: Add memoisation *) | SkipS -> state - | CallS (f, es) -> let v = pathval mem vals f in - let t = pathtype types f in + | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in + let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in let types' : types = [] in let vals' : vals = [] in (match v, t with | FunV (* xs, *) fstmts (* ) *), FunT ts -> (* TODO: memoisation of the called functions *) - let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *) - (fun (st, x) (m, t) p -> (addarg st x t p, x + 1)) + let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *) + (fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1)) ((mem, types', vals'), 0) ts es in (* NOTE: same x's, so can use same args for all the statements *) - let _states_evaled = List.map (stmt_eval state_with_args) fstmts in - let mem_spoiled = List.fold_left2 + let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in + let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2 (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e) mem ts es in (mem_spoiled, types, vals) - | _, _ -> raise @@ Eval_error "call: function") + | FunV _, _ -> raise @@ Eval_error "call: function type" + | _, FunT _ -> raise @@ Eval_error "call: function val" + | _, _ -> raise @@ Eval_error "call: function type & val") | WriteS p -> (match pathtype types p with | UnitT (_, w) -> if w == NeverWr @@ -361,7 +379,59 @@ struct (* --- tests --- *) - (* - tests without functions *) + (* - shortcuts *) + + let ( #. ) x y = SeqS (x, y) + + let vx = VarP 0 + let vy = VarP 1 + let vz = VarP 2 + + let vgx = VarP (globals_min_id) + let vgy = VarP (globals_min_id + 1) + let vgz = VarP (globals_min_id + 2) + + let drf p = DerefP p + let access p i = AccessP (p, i) + + let wr x = ReadS x + let rd x = WriteS x + let skp = SkipS + + let uT_r_aw = UnitT (Rd, AlwaysWr) + let uT_r_mw = UnitT (Rd, MayWr) + let uT_aw = UnitT (NRd, AlwaysWr) + let uT_mw = UnitT (NRd, MayWr) + let uT_r = UnitT (Rd, NeverWr) + let uT = UnitT (NRd, NeverWr) + + let rfT t = RefT (Rf, t) + let cpT t = RefT (Cp, t) + + let moded t = ((In, NOut), t) + + let defg t = VarD (t, UnitE) + + (* - utils tests *) + + let%expect_test "mem add / get / set" = + let mem = empty_mem in + let (mem, id1) = mem_add mem ZeroV in + let (mem, id2) = mem_add mem SmthV in + let (mem, id3) = mem_add mem BotV in + Printf.printf "%i %i %i " id1 id2 id3; + Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV) + (mem_get mem id2 == SmthV) + (mem_get mem id3 == BotV); + let mem = mem_set mem id1 BotV in + let mem = mem_set mem id2 ZeroV in + let mem = mem_set mem id3 SmthV in + Printf.printf "%b %b %b" (mem_get mem id1 == BotV) + (mem_get mem id2 == ZeroV) + (mem_get mem id3 == SmthV); + [%expect {| 0 1 2 true true true true true true |}] + + (* - basic var tests *) let%expect_test "empty" = prog_eval_noret ([], SkipS); @@ -379,6 +449,49 @@ struct with Eval_error msg -> Printf.printf "%s" msg; [%expect {| read |}] + let%expect_test "simple vars, no read & read" = + prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE); + VarD (UnitT (Rd, MayWr), UnitE)], + ReadS (VarP (globals_min_id + 1))); + Printf.printf "done!"; + [%expect {| done! |}] + + let%expect_test "simple var, write" = + prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id)); + Printf.printf "done!"; + [%expect {| done! |}] + + let%expect_test "simple var, no write" = + try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id)); + [%expect.unreachable]); + with Eval_error msg -> Printf.printf "%s" msg; + [%expect {| write: write tag |}] + + let%expect_test "simple var, write & read" = + prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id), + ReadS (VarP globals_min_id))); + Printf.printf "done!"; + [%expect {| done! |}] + + (* - basic call tests *) + + let%expect_test "simple call with read" = + prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); + FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], + CallS (VarP (globals_min_id + 1), + [PathE (VarP globals_min_id)])); + Printf.printf "done!"; + [%expect {| done! |}] + + let%expect_test "simple call with write" = + prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); + VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); + FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], + CallS (VarP (globals_min_id + 2), + [PathE (VarP (globals_min_id + 1))])); + Printf.printf "done!"; + [%expect {| done! |}] + (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) (* --- tests --- *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 3742b24..5e8cccf 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -112,8 +112,9 @@ { Or[$()$][value of simple type] // `Unit` Or[$path$][value from variable] // `Path` - // TODO: decide what is the result of ref expr eval - // Or[$rf expr$][reference expr] // `Ref` + // TODO FIXME: expand to support arbitrary paths (that do lead to lvalue) + // add relation to calc lvalue / rvalue for each element ? + Or[$rf X$][reference expr] // `Ref` Or[$[expr+]$][tuple expr] // `Prod` } ), @@ -652,7 +653,7 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ unit expr value], $vals, mu texpre () eqmu 0$, ) @@ -661,32 +662,26 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ path type], + name: [ path expr value], $vals, mu tval p eqmu v$, $vals, mu texpre p eqmu v$, ) )) -// NOTE: tmp removed -// #align(center, prooftree( -// vertical-spacing: 4pt, -// rule( -// name: [ unit value type], +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ ref expr value], -// $vals, mu texpre e : t$, - -// [*TODO*], - -// // TODO: reference to what ?? -// $vals, mu texpre rf e eqmu rf ??$, -// ) -// )) + $vals, mu texpre rf x eqmu rf vals[x]$, + ) +)) #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ tuple expr value], $vals, mu texpre e_1 eqmu v_1$, $...$, @@ -704,7 +699,7 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ unit value expr type], $types texprt () : cl Read, NotWrite cr$, ) @@ -713,29 +708,26 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ path type], + name: [ path expr type], $types ttype p : t$, $types texprt p : t$, ) )) -// NOTE: tmp removed -// #align(center, prooftree( -// vertical-spacing: 4pt, -// rule( -// name: [ unit value type], +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ ref expr type], -// $types texprt e : t$, -// // TODO: why Ref mode ?? <- due to immutability ?? -// $types texprt rf e : rf Ref t$, -// ) -// )) + $types texprt rf x : rf Ref types[x]$, + ) +)) #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ tuple expr type], $types texprt e_1 : t_1$, $...$, @@ -928,7 +920,21 @@ $s in stmt, f in X, x in X, a in X$ rule( name: [ full spoil for tuple expr], - $e = [e_1, ... e_n]$, + // NOTE: x as path + $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$, + + // TODO: FIXME: is c important ? + $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ full spoil for tuple expr], + $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$, $...$, $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$, From 66ea0e53da2fdc4867f0fd110491cc7b343736c1 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 1 May 2026 13:45:09 +0000 Subject: [PATCH 2/2] struct: init synthesizer rewrite --- model_with_structures/dune | 40 +- model_with_structures/model.typ | 2 +- model_with_structures/synthesizer.ml | 1105 +++++++++++++------------- 3 files changed, 574 insertions(+), 573 deletions(-) diff --git a/model_with_structures/dune b/model_with_structures/dune index 489258f..54383e4 100644 --- a/model_with_structures/dune +++ b/model_with_structures/dune @@ -42,23 +42,23 @@ ; -pp ; camlp5/pp5+gt+plugins+ocanren+dump.exe))) -; (library -; (name synthesizer_st) -; (modules synthesizer) -; (flags -; ; (-dsource) -; (:standard -rectypes)) -; (libraries OCanren OCanren.tester) -; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) -; (wrapped false) -; (preprocess -; (pps -; OCanren-ppx.ppx_repr -; OCanren-ppx.ppx_deriving_reify -; OCanren-ppx.ppx_fresh -; GT.ppx -; GT.ppx_all -; OCanren-ppx.ppx_distrib -; -- -; -pp -; camlp5/pp5+gt+plugins+ocanren+dump.exe))) +(library + (name synthesizer_st) + (modules synthesizer) + (flags + ; (-dsource) + (:standard -rectypes)) + (libraries OCanren OCanren.tester) + (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) + (wrapped false) + (preprocess + (pps + OCanren-ppx.ppx_repr + OCanren-ppx.ppx_deriving_reify + OCanren-ppx.ppx_fresh + GT.ppx + GT.ppx_all + OCanren-ppx.ppx_distrib + -- + -pp + camlp5/pp5+gt+plugins+ocanren+dump.exe))) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 5e8cccf..6b4cf41 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -923,7 +923,7 @@ $s in stmt, f in X, x in X, a in X$ // NOTE: x as path $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$, - // TODO: FIXME: is c important ? + // TODO:: is c important ? $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$, ) )) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 02d5250..696722b 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 *) @@ -28,11 +28,10 @@ struct ] end - (* NOTE: rename names ?? *) module CopyCap = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec t = Ref | Val + type nonrec t = Rf | Cp [@@deriving gt ~options:{ show; gmap }] type nonrec ground = t ] @@ -57,493 +56,495 @@ struct ] end - 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 - ] + (* --- 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) } + (* 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) } + (* 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 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_) } + (* 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 + (* 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 + (* 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 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 + (* 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 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 + (* 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 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 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 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 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 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 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 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 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 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 + (* 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 { - { fresh x, xs', y, ys', z, zs' in - xs == x :: xs' & - ys == y :: ys' & - zs == z :: zs' & - f x y z & - list_zip_witho f xs' ys' zs' } | - { fresh x, xs' in - xs == x :: xs' & - ys == [] & - zs == [] } | - { fresh y, ys' in - xs == [] & - ys == y :: ys' & - zs == [] } | - { xs == [] & ys == [] & zs == [] } - } + (* let rec list_zip_witho f xs ys zs = ocanren { *) + (* { fresh x, xs', y, ys', z, zs' in *) + (* xs == x :: xs' & *) + (* ys == y :: ys' & *) + (* zs == z :: zs' & *) + (* f x y z & *) + (* list_zip_witho f xs' ys' zs' } | *) + (* { fresh x, xs' in *) + (* xs == x :: xs' & *) + (* ys == [] & *) + (* zs == [] } | *) + (* { fresh y, ys' in *) + (* xs == [] & *) + (* ys == y :: ys' & *) + (* zs == [] } | *) + (* { xs == [] & ys == [] & zs == [] } *) + (* } *) (* --- *) - let value_combineo left right res = let open Value in ocanren { - { left == Unit & right == Unit & res == Unit } | - { left == Bot & right == Bot & res == Bot } | - { left == Unit & right == Bot & res == Undef } | - { left == Bot & right == Unit & res == Undef } - } + (* let value_combineo left right res = let open Value in ocanren { *) + (* { left == Unit & right == Unit & res == Unit } | *) + (* { left == Bot & right == Bot & res == Bot } | *) + (* { left == Unit & right == Bot & res == Undef } | *) + (* { left == Bot & right == Unit & res == Undef } *) + (* } *) - let memory_combineo left right res = ocanren { - list_zip_witho value_combineo left right res - } + (* let memory_combineo left right res = ocanren { *) + (* list_zip_witho value_combineo left right res *) + (* } *) - let state_combineo left right res = let open St in ocanren { - fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in - left == St (lenv, lmem, lmem_len, lvisited) & - right == St (renv, rmem, rmem_len, rvisited) & - lenv == renv & lmem_len == rmem_len & - memory_combineo lmem rmem res_mem & - res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) + (* let state_combineo left right res = let open St in ocanren { *) + (* fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in *) + (* left == St (lenv, lmem, lmem_len, lvisited) & *) + (* right == St (renv, rmem, rmem_len, rvisited) & *) + (* lenv == renv & lmem_len == rmem_len & *) + (* memory_combineo lmem rmem res_mem & *) + (* res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) *) (* TODO: union visited lists instead ? *) - } + (* } *) (* --- *) - let rec list_replaceo xs id value ys = ocanren { + (* 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' } - } + (* { 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 env_geto state id tag' mem_id' = - let open St in - ocanren { - fresh env, _mem, _mem_len, _visited, elem in - state == St (env, _mem, _mem_len, _visited) & - List.assoco id env elem & - Std.pair tag' mem_id' == elem - } + (* let env_geto state id tag' mem_id' = *) + (* let open St in *) + (* ocanren { *) + (* fresh env, _mem, _mem_len, _visited, elem in *) + (* state == St (env, _mem, _mem_len, _visited) & *) + (* List.assoco id env elem & *) + (* Std.pair tag' mem_id' == elem *) + (* } *) - let env_addo state id tg mem_id state' = - let open St in - ocanren { - fresh env, env', mem, mem_len, visited, elem in - state == St (env, mem, mem_len, visited) & - Std.pair tg mem_id == elem & - (Std.pair id elem) :: env == env' & - state' == St (env', mem, mem_len, visited) - } + (* let env_addo state id tg mem_id state' = *) + (* let open St in *) + (* ocanren { *) + (* fresh env, env', mem, mem_len, visited, elem in *) + (* state == St (env, mem, mem_len, visited) & *) + (* Std.pair tg mem_id == elem & *) + (* (Std.pair id elem) :: env == env' & *) + (* state' == St (env', mem, mem_len, visited) *) + (* } *) - let inv_ido mem_len id id' = ocanren { - fresh inv_id_inc in - Nat.addo inv_id_inc id mem_len & - Nat.addo id' 1 inv_id_inc - } + (* let inv_ido mem_len id id' = ocanren { *) + (* fresh inv_id_inc in *) + (* Nat.addo inv_id_inc id mem_len & *) + (* Nat.addo id' 1 inv_id_inc *) + (* } *) (* --- *) - let rec list_ntho xs id x' = ocanren { + (* 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' } - } + (* { 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 state id value' = - let open St in - ocanren { - fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in - state == St (_env, mem, mem_len, _visited) & - env_geto state id _tag mem_id & - inv_ido mem_len mem_id mem_id_inv & - list_ntho mem mem_id_inv value' - } + (* let mem_geto state id value' = *) + (* let open St in *) + (* ocanren { *) + (* fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in *) + (* state == St (_env, mem, mem_len, _visited) & *) + (* env_geto state id _tag mem_id & *) + (* inv_ido mem_len mem_id mem_id_inv & *) + (* list_ntho mem mem_id_inv value' *) + (* } *) - let mem_seto state id value state'= - let open St in - ocanren { - fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in - state == St (env, mem, mem_len, visited) & - env_geto state id _tag mem_id & - inv_ido mem_len mem_id inv_mem_id & - list_replaceo mem inv_mem_id value mem' & - state' == St (env, mem', mem_len, visited) - } + (* let mem_seto state id value state'= *) + (* let open St in *) + (* ocanren { *) + (* fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in *) + (* state == St (env, mem, mem_len, visited) & *) + (* env_geto state id _tag mem_id & *) + (* inv_ido mem_len mem_id inv_mem_id & *) + (* list_replaceo mem inv_mem_id value mem' & *) + (* state' == St (env, mem', mem_len, visited) *) + (* } *) - let mem_addo state value state' = - let open St in - ocanren { - fresh env, mem, mem_len, mem_len', visited, mem' in - state == St (env, mem, mem_len, visited) & - mem' == value :: mem & - mem_len' == Nat.s mem_len & - state' == St (env, mem', mem_len', visited) - } + (* let mem_addo state value state' = *) + (* let open St in *) + (* ocanren { *) + (* fresh env, mem, mem_len, mem_len', visited, mem' in *) + (* state == St (env, mem, mem_len, visited) & *) + (* mem' == value :: mem & *) + (* mem_len' == Nat.s mem_len & *) + (* state' == St (env, mem', mem_len', visited) *) + (* } *) - let mem_checko state id = - let open Value in - ocanren { - mem_geto state id Unit - } + (* let mem_checko state id = *) + (* let open Value in *) + (* ocanren { *) + (* mem_geto state id Unit *) + (* } *) (* --- *) - let rec list_foldlo f acc xs acc' = ocanren { - xs == [] & acc' == acc | - { fresh x', xs', acc_upd in - xs == x' :: xs' & - list_foldlo f acc xs' acc_upd & - f acc_upd x' acc' } - } + (* let rec list_foldlo f acc xs acc' = ocanren { *) + (* xs == [] & acc' == acc | *) + (* { fresh x', xs', acc_upd in *) + (* xs == x' :: xs' & *) + (* list_foldlo f acc xs' acc_upd & *) + (* f acc_upd x' acc' } *) + (* } *) - let rec list_foldro f acc xs acc' = ocanren { - xs == [] & acc' == acc | - { fresh x', xs', acc_upd in - xs == x' :: xs' & - f acc x' acc_upd & - list_foldro f acc_upd xs' acc' } + (* let rec list_foldro f acc xs acc' = ocanren { *) + (* xs == [] & acc' == acc | *) + (* { fresh x', xs', acc_upd in *) + (* xs == x' :: xs' & *) + (* f acc x' acc_upd & *) + (* list_foldro f acc_upd xs' acc' } *) (* TODO: inf search on swap, investigate *) - } + (* } *) - let rec list_foldr2o f acc xs ys acc' = ocanren { - xs == [] & ys == [] & acc' == acc | - { fresh x', xs', y', ys', acc_upd in - xs == x' :: xs' & - ys == y' :: ys' & - f acc x' y' acc_upd & - list_foldr2o f acc_upd xs' ys' acc' } - } + (* let rec list_foldr2o f acc xs ys acc' = ocanren { *) + (* xs == [] & ys == [] & acc' == acc | *) + (* { fresh x', xs', y', ys', acc_upd in *) + (* xs == x' :: xs' & *) + (* ys == y' :: ys' & *) + (* f acc x' y' acc_upd & *) + (* list_foldr2o f acc_upd xs' ys' acc' } *) + (* } *) - let rec list_foldl2o f acc xs ys acc' = ocanren { - xs == [] & ys == [] & acc' == acc | - { fresh x', xs', y', ys', acc_upd in - xs == x' :: xs' & - ys == y' :: ys' & - list_foldl2o f acc xs' ys' acc_upd & - f acc_upd x' y' acc' } - } + (* let rec list_foldl2o f acc xs ys acc' = ocanren { *) + (* xs == [] & ys == [] & acc' == acc | *) + (* { fresh x', xs', y', ys', acc_upd in *) + (* xs == x' :: xs' & *) + (* ys == y' :: ys' & *) + (* list_foldl2o f acc xs' ys' acc_upd & *) + (* f acc_upd x' y' acc' } *) + (* } *) - let arg_to_valueo state arg value' = - let open Arg in - let open Value in - ocanren { - arg == RValue & value' == Unit | - { fresh id in - arg == LValue id & - mem_geto state id value' } - } + (* let arg_to_valueo state arg value' = *) + (* let open Arg in *) + (* let open Value in *) + (* ocanren { *) + (* arg == RValue & value' == Unit | *) + (* { fresh id in *) + (* arg == LValue id & *) + (* mem_geto state id value' } *) + (* } *) - let arg_to_rvalueo arg value' = - let open Arg in - let open Tag in - ocanren { is_valueo arg & value' == RValue } + (* let arg_to_rvalueo arg value' = *) + (* let open Arg in *) + (* let open Tag in *) + (* ocanren { is_valueo arg & value' == RValue } *) - let st_mem_leno state mem_len' = - let open St in - ocanren { - fresh _env, _mem, _visited in - state == St (_env, _mem, mem_len', _visited) - } + (* let st_mem_leno state mem_len' = *) + (* let open St in *) + (* ocanren { *) + (* fresh _env, _mem, _visited in *) + (* state == St (_env, _mem, mem_len', _visited) *) + (* } *) - let tag_correcto tg = - let open Tag in - ocanren { - {is_not_outo tg | { is_outo tg & is_always_writeo tg } } & - {is_not_reado tg | { is_reado tg & is_ino tg } } - } + (* let tag_correcto tg = *) + (* let open Tag in *) + (* ocanren { *) + (* {is_not_outo tg | { is_outo tg & is_always_writeo tg } } & *) + (* {is_not_reado tg | { is_reado tg & is_ino tg } } *) + (* } *) - let st_add_argo state state_before id arg_tag arg state'' = + (* let st_add_argo state state_before id arg_tag arg state'' = *) (* let open Nat in *) - let open Value in - let open Arg in - let open Tag in - ocanren { - tag_correcto arg_tag & { - { fresh value', state', mem_len_prev' in - is_valueo arg_tag & - arg_to_valueo state_before arg value' & - mem_addo state value' state' & - st_mem_leno state mem_len_prev' & - env_addo state' id arg_tag mem_len_prev' state'' } | - { fresh arg', parent_tag, mem_id, state' in - is_refo arg_tag & + (* let open Value in *) + (* let open Arg in *) + (* let open Tag in *) + (* ocanren { *) + (* tag_correcto arg_tag & { *) + (* { fresh value', state', mem_len_prev' in *) + (* is_valueo arg_tag & *) + (* arg_to_valueo state_before arg value' & *) + (* mem_addo state value' state' & *) + (* st_mem_leno state mem_len_prev' & *) + (* env_addo state' id arg_tag mem_len_prev' state'' } | *) + (* { fresh arg', parent_tag, mem_id, state' in *) + (* is_refo arg_tag & *) (* { arg == RValue } *) (* NOTE: not allowed for now *) - arg == LValue arg' & - env_geto state_before id parent_tag mem_id & - env_addo state id arg_tag mem_id state' & - { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } & - { - { is_reado arg_tag & state' == state'' } | - { is_not_reado arg_tag & mem_seto state' id Bot state'' } - } - } - } - } + (* arg == LValue arg' & *) + (* env_geto state_before id parent_tag mem_id & *) + (* env_addo state id arg_tag mem_id state' & *) + (* { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } & *) + (* { *) + (* { is_reado arg_tag & state' == state'' } | *) + (* { is_not_reado arg_tag & mem_seto state' id Bot state'' } *) + (* } *) + (* } *) + (* } *) + (* } *) - let st_spoil_foldero state_before state tg id state' = - let open Value in - let open Tag in - let open St in - ocanren { - fresh env, mem, mem_len, _visited, parent_tg, _mem_id in - state == St (env, mem, mem_len, _visited) & - env_geto state id parent_tg _mem_id & - { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & - { { is_never_writeo tg & state == state'} | - { is_always_writeo tg & - is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } | - { is_may_writeo tg & { - { is_not_outo tg & is_valueo tg & state == state' } | - { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' } - } } - } - } + (* let st_spoil_foldero state_before state tg id state' = *) + (* let open Value in *) + (* let open Tag in *) + (* let open St in *) + (* ocanren { *) + (* fresh env, mem, mem_len, _visited, parent_tg, _mem_id in *) + (* state == St (env, mem, mem_len, _visited) & *) + (* env_geto state id parent_tg _mem_id & *) + (* { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & *) + (* { { is_never_writeo tg & state == state'} | *) + (* { is_always_writeo tg & *) + (* is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } | *) + (* { is_may_writeo tg & { *) + (* { is_not_outo tg & is_valueo tg & state == state' } | *) + (* { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' } *) + (* } } *) + (* } *) + (* } *) - let st_spoil_by_argso state arg_tags args state' = - ocanren { - fresh state_before in - state == state_before & (* TODO: required ? *) - list_foldl2o (st_spoil_foldero state_before) state arg_tags args state' - } + (* let st_spoil_by_argso state arg_tags args state' = *) + (* ocanren { *) + (* fresh state_before in *) + (* state == state_before & (* TODO: required ? *) *) + (* list_foldl2o (st_spoil_foldero state_before) state arg_tags args state' *) + (* } *) (* let st_spoil_assignmentso state state' = *) (* let open St in *) @@ -555,150 +556,150 @@ struct (* --- *) - let arg_to_lvalueo arg arg' = - let open Arg in - ocanren { arg' == LValue arg } + (* let arg_to_lvalueo arg arg' = *) + (* let open Arg in *) + (* ocanren { arg' == LValue arg } *) - let rec list_dropo n xs xs' = ocanren { - xs == [] & xs' == [] | - n == Nat.o & xs == xs' & xs =/= [] | - { fresh n', _y, ys in - Nat.s n' == n & - xs == _y :: ys & - list_dropo n' ys xs' } - } + (* let rec list_dropo n xs xs' = ocanren { *) + (* xs == [] & xs' == [] | *) + (* n == Nat.o & xs == xs' & xs =/= [] | *) + (* { fresh n', _y, ys in *) + (* Nat.s n' == n & *) + (* xs == _y :: ys & *) + (* list_dropo n' ys xs' } *) + (* } *) - let rec list_not_membero xs x = ocanren { - xs == [] | - { fresh x', xs' in - xs == x' :: xs' & - x' =/= x & - list_not_membero xs' x } - } + (* let rec list_not_membero xs x = ocanren { *) + (* xs == [] | *) + (* { fresh x', xs' in *) + (* xs == x' :: xs' & *) + (* x' =/= x & *) + (* list_not_membero xs' x } *) + (* } *) - let visited_checko state f_id = - let open St in - ocanren { - fresh _env, _mem, _mem_len, visited in - state == St (_env, _mem, _mem_len, visited) & - List.membero visited f_id - } + (* let visited_checko state f_id = *) + (* let open St in *) + (* ocanren { *) + (* fresh _env, _mem, _mem_len, visited in *) + (* state == St (_env, _mem, _mem_len, visited) & *) + (* List.membero visited f_id *) + (* } *) - let not_visited_checko state f_id = - let open St in - ocanren { - fresh _env, _mem, _mem_len, visited in - state == St (_env, _mem, _mem_len, visited) & - list_not_membero visited f_id - } + (* let not_visited_checko state f_id = *) + (* let open St in *) + (* ocanren { *) + (* fresh _env, _mem, _mem_len, visited in *) + (* state == St (_env, _mem, _mem_len, visited) & *) + (* list_not_membero visited f_id *) + (* } *) - let visited_addo state f_id state' = - let open St in - ocanren { - fresh env, mem, mem_len, visited, visited' in - state == St (env, mem, mem_len, visited) & - visited' == f_id :: visited & - state' == St (env,mem, mem_len, visited') - } + (* let visited_addo state f_id state' = *) + (* let open St in *) + (* ocanren { *) + (* fresh env, mem, mem_len, visited, visited' in *) + (* state == St (env, mem, mem_len, visited) & *) + (* visited' == f_id :: visited & *) + (* state' == St (env,mem, mem_len, visited') *) + (* } *) - let rec eval_stmto state prog stmt state' = - let open Stmt in - let open Value in - let open FunDecl in - let open Tag in - ocanren { - { fresh f_id, args, f, args', state_after_call, arg_tags, _body in - stmt == Call (f_id, args) & - list_ntho prog f_id f & - FunDecl (arg_tags, _body) == f & - List.mapo arg_to_lvalueo args args' & + (* let rec eval_stmto state prog stmt state' = *) + (* let open Stmt in *) + (* let open Value in *) + (* let open FunDecl in *) + (* let open Tag in *) + (* ocanren { *) + (* { fresh f_id, args, f, args', state_after_call, arg_tags, _body in *) + (* stmt == Call (f_id, args) & *) + (* list_ntho prog f_id f & *) + (* FunDecl (arg_tags, _body) == f & *) + (* List.mapo arg_to_lvalueo args args' & *) (* TODO: FIXME: memoisation, do not do calls on check successfull *) (* NOTE: tmp simplification for less branching (TODO?) *) - { { fresh state_with_visited in - not_visited_checko state f_id & - visited_addo state f_id state_with_visited & - eval_funo state_with_visited prog f args' state_after_call } | - { visited_checko state f_id & - state_after_call == state } } & - st_spoil_by_argso state_after_call arg_tags args state' } | - { fresh id in stmt == Read id & mem_checko state id & state == state' } | - { fresh id, tag, _mem_id in - stmt == Write id & - env_geto state id tag _mem_id & - is_may_writeo tag & - mem_seto state id Unit state' } | - { fresh xs, ys in - stmt == Choice (xs, ys) } + (* { { fresh state_with_visited in *) + (* not_visited_checko state f_id & *) + (* visited_addo state f_id state_with_visited & *) + (* eval_funo state_with_visited prog f args' state_after_call } | *) + (* { visited_checko state f_id & *) + (* state_after_call == state } } & *) + (* st_spoil_by_argso state_after_call arg_tags args state' } | *) + (* { fresh id in stmt == Read id & mem_checko state id & state == state' } | *) + (* { fresh id, tag, _mem_id in *) + (* stmt == Write id & *) + (* env_geto state id tag _mem_id & *) + (* is_may_writeo tag & *) + (* mem_seto state id Unit state' } | *) + (* { fresh xs, ys in *) + (* stmt == Choice (xs, ys) } *) (* TODO: FIXME: choice actions *) - } + (* } *) - and eval_body_foldero prog state stmt state' = - eval_stmto state prog stmt state' + (* and eval_body_foldero prog state stmt state' = *) + (* eval_stmto state prog stmt state' *) - and eval_bodyo state prog body state' = - list_foldro (eval_body_foldero prog) state body state' + (* and eval_bodyo state prog body state' = *) + (* list_foldro (eval_body_foldero prog) state body state' *) - and add_arg_foldero state_before state_c arg_tag arg state_c' = - ocanren { - fresh state, id, state', id' in - state_c == Std.pair state id & - st_add_argo state state_before id arg_tag arg state' & - id' == Nat.s id & - state_c' == Std.pair state' id' - } + (* and add_arg_foldero state_before state_c arg_tag arg state_c' = *) + (* ocanren { *) + (* fresh state, id, state', id' in *) + (* state_c == Std.pair state id & *) + (* st_add_argo state state_before id arg_tag arg state' & *) + (* id' == Nat.s id & *) + (* state_c' == Std.pair state' id' *) + (* } *) - and eval_funo state prog decl args state' = - let open FunDecl in - let open St in - ocanren { - fresh arg_tags, body, - env_before, mem_before, len_before, visited_before, - state_clean, - state_with_vars, _counter, - state_evaled, - _env, _mem, _len, visited, - nil_env, nil_visited in - nil_env == [] & - nil_visited == [] & - decl == FunDecl (arg_tags, body) & - state == St (env_before, mem_before, len_before, visited_before) & - state_clean == St (nil_env, mem_before, len_before, nil_visited) & - list_foldr2o (add_arg_foldero state) - (Std.pair state Nat.o) arg_tags args - (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *) - eval_bodyo state_with_vars prog body state_evaled & - state_evaled == St (_env,_mem, _len, visited) & - state' == St (env_before, mem_before, len_before, visited) - } + (* and eval_funo state prog decl args state' = *) + (* let open FunDecl in *) + (* let open St in *) + (* ocanren { *) + (* fresh arg_tags, body, *) + (* env_before, mem_before, len_before, visited_before, *) + (* state_clean, *) + (* state_with_vars, _counter, *) + (* state_evaled, *) + (* _env, _mem, _len, visited, *) + (* nil_env, nil_visited in *) + (* nil_env == [] & *) + (* nil_visited == [] & *) + (* decl == FunDecl (arg_tags, body) & *) + (* state == St (env_before, mem_before, len_before, visited_before) & *) + (* state_clean == St (nil_env, mem_before, len_before, nil_visited) & *) + (* list_foldr2o (add_arg_foldero state) *) + (* (Std.pair state Nat.o) arg_tags args *) + (* (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *) *) + (* eval_bodyo state_with_vars prog body state_evaled & *) + (* state_evaled == St (_env,_mem, _len, visited) & *) + (* state' == St (env_before, mem_before, len_before, visited) *) + (* } *) - and eval_fun_empty_argso state prog decl state' = - let open FunDecl in - ocanren { - fresh arg_tags, args, _body in - decl == FunDecl (arg_tags, _body) & - List.mapo arg_to_rvalueo arg_tags args & - eval_funo state prog decl args state' - } + (* and eval_fun_empty_argso state prog decl state' = *) + (* let open FunDecl in *) + (* ocanren { *) + (* fresh arg_tags, args, _body in *) + (* decl == FunDecl (arg_tags, _body) & *) + (* List.mapo arg_to_rvalueo arg_tags args & *) + (* eval_funo state prog decl args state' *) + (* } *) (* --- *) - let empty_stateo state = - let open St in - ocanren { - fresh nil_env, nil_mem, nil_visited in - nil_env == [] & - nil_visited == [] & - nil_mem == [] & - state == St (nil_env, nil_mem, Nat.o, nil_visited) - } + (* let empty_stateo state = *) + (* let open St in *) + (* ocanren { *) + (* fresh nil_env, nil_mem, nil_visited in *) + (* nil_env == [] & *) + (* nil_visited == [] & *) + (* nil_mem == [] & *) + (* state == St (nil_env, nil_mem, Nat.o, nil_visited) *) + (* } *) - let eval_progo all_prog state' = - let open Prog in - ocanren { - fresh prog, main_decl, state in - all_prog == Prog (prog, main_decl) & - empty_stateo state & - eval_fun_empty_argso state prog main_decl state' - } + (* let eval_progo all_prog state' = *) + (* let open Prog in *) + (* ocanren { *) + (* fresh prog, main_decl, state in *) + (* all_prog == Prog (prog, main_decl) & *) + (* empty_stateo state & *) + (* eval_fun_empty_argso state prog main_decl state' *) + (* } *) end