From 3e61eb32047dd91615e3cf51c2b9884791e0aecd Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 5 May 2026 14:35:35 +0000 Subject: [PATCH 1/3] struct: part sythesizer functions + some minor (mostly stylistic) analyzer corrections --- model_with_structures/analyzer.ml | 56 ++-- model_with_structures/synthesizer.ml | 477 +++++++++++++++++++++++++-- 2 files changed, 480 insertions(+), 53 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 31613ee..9bc39d6 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -91,6 +91,14 @@ struct | x :: xs, _ -> x :: list_replace xs (id - 1) y | [], _ -> raise Not_found + (* TODO: FIXME: check if this foldl or foldr *) + let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with + | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs + | [], [], [] -> acc + | _, _, _ -> raise Cant_fold3_error + + (* --- *) + (* NOTE: old variant with assoc array *) (* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *) (* let mem_add (mem : mem) (v : value) : mem * memid = *) @@ -147,31 +155,32 @@ struct (* --- eval rules --- *) - (* TODO: FIXME: check if this foldl or foldr *) - let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with - | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs - | [], [], [] -> acc - | _, _, _ -> raise Cant_fold3_error - (* - value construction *) - let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with - | UnitT (Rd, w), ZeroV -> (mem, v) - | UnitT (Rd, w), SmthV -> (mem, v) - | UnitT (Rd, w), BotV -> (mem, v) - | UnitT (NRd, w), ZeroV -> (mem, BotV) - | UnitT (NRd, w), SmthV -> (mem, BotV) - | UnitT (NRd, w), BotV -> (mem, BotV) + let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = + if is_trivial_v v + then match t with + | UnitT (Rd, _) -> (mem, v) + | UnitT (NRd, _) -> (mem, BotV) + | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type" + else match t, v with + (* NOTE: replaced with if | best choice ?? *) + (* | UnitT (Rd, w), ZeroV -> (mem, v) *) + (* | UnitT (Rd, w), SmthV -> (mem, v) *) + (* | UnitT (Rd, w), BotV -> (mem, v) *) + (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *) + (* | UnitT (NRd, w), SmthV -> (mem, BotV) *) + (* | UnitT (NRd, w), BotV -> (mem, BotV) *) | FunT _, FunV _ -> (mem, v) | RefT (Rf, _), RefV _ -> (mem, v) | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in let (mem'', id'') = mem_add mem' v' in (mem'', RefV id'') | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in - mem, v' :: vs' in + (mem, v' :: vs') in let mem', vs' = List.fold_left2 folder (mem, []) vs ts in (mem', TupleV vs') - | _, _ -> raise @@ Typing_error "valcopy" + | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" (* - value update *) @@ -189,7 +198,7 @@ struct if is_trivial_v u && is_trivial_v v then (if u == v then u else BotV) else match u, v with - | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) + | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref" | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs) | _, _ -> raise @@ Typing_error "valcomb" @@ -317,7 +326,6 @@ struct (mem'', (x, t) :: types, (x, id) :: vals) (* - function evaluation *) - (* NOTE: not needed due to performed optimization in stmt_eval *) (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *) @@ -368,15 +376,15 @@ struct then raise @@ Eval_error "choice" else (memcomb meml memr, typesl, valsl) - (* --- program execution --- *) + (* --- program execution --- *) - let prog_eval (prog : prog) : state = - match prog with (decls, s) -> - let init_state = prog_init prog in - stmt_eval init_state s + let prog_eval (prog : prog) : state = + match prog with (decls, s) -> + let init_state = prog_init prog in + stmt_eval init_state s - let prog_eval_noret (prog : prog) : unit = - ignore @@ prog_eval prog + let prog_eval_noret (prog : prog) : unit = + ignore @@ prog_eval prog (* --- tests --- *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index a277f4d..f23acc2 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -145,16 +145,16 @@ struct 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 + 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 + 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 + module Prg = 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 + type nonrec ('dl, 's) t = Prg of 'dl * 's [@@deriving gt ~options:{ show; gmap }] type nonrec ground = (Decl.ground List.ground, Stmt.ground) t ] @@ -173,39 +173,39 @@ struct (* --- *) - module Mem = struct + module MemEnv = 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 + type nonrec ('vl, 'd) t = MemEnv of 'vl * 'd [@@deriving gt ~options:{ show; gmap }] type nonrec ground = (Value.ground List.ground, Nat.ground) t ] end - module Types = struct + module TypesEnv = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec 'dtl t = Types of 'dtl + type nonrec 'dtl t = TypesEnv of 'dtl [@@deriving gt ~options:{ show; gmap }] type nonrec ground = ((Nat.ground * Type.ground) List.ground) t ] end - module Vals = struct + module ValsEnv = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec 'ddl t = Vals of 'ddl + type nonrec 'ddl t = ValsEnv of 'ddl [@@deriving gt ~options:{ show; gmap }] type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t ] end - module St = struct + module StEnv = 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 + type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t + type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t ] end @@ -238,30 +238,449 @@ struct 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 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 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 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 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' + + 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_foldr3o f acc xs ys zs acc' = ocanren { + xs == [] & ys == [] & zs == [] & acc' == acc | + { fresh x', xs', y', ys', z', zs', acc_upd in + xs == x' :: xs' & + ys == y' :: ys' & + zs == z' :: zs' & + f acc x' y' z' acc_upd & + list_foldr3o f acc_upd xs' ys' zs' acc' } + } + + let rec list_foldl3o f acc xs ys zs acc' = ocanren { + xs == [] & ys == [] & zs == [] & acc' == acc | + { fresh x', xs', y', ys', z', zs', acc_upd in + xs == x' :: xs' & + ys == y' :: ys' & + zs == z' :: zs' & + list_foldl3o f acc xs' ys' zs' acc_upd & + f acc_upd x' y' z' acc' } + } + + 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 mem_geto mem id v = + let open MemEnv in + ocanren { + fresh mem_data, mem_len, rev_id in + MemEnv (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' = + let open MemEnv in + ocanren { + fresh mem_data, mem_len, mem' in + MemEnv (mem_data, mem_len) == mem & + mem' == MemEnv (v :: mem_data, Nat.s mem_len) & + Std.pair mem' mem_len == mem_with_id' + } + + let mem_seto mem id v mem' = + let open MemEnv in + ocanren { + fresh mem_data, mem_len, rev_id, mem_data' in + MemEnv (mem_data, mem_len) == mem & + Nat.addo (Nat.s rev_id) id mem_len & + list_replaceo mem_data rev_id v mem_data' & + MemEnv (mem_data', mem_len) == mem' + } + + let is_trivial_vo v = + let open Value in + ocanren { + v == ZeroV | v == SmthV | v == BotV + } + + let rec pathvaro p x = + let open Path in + ocanren { + p == VarP x | + { fresh p' in p == DerefP p' & pathvaro p' x } | + { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x } + } + + let types_assoco id types tp = + let open TypesEnv in + ocanren { + fresh tps in + types == TypesEnv tps & + List.assoco id tps tp + } + + let vals_assoco id vals v = + let open ValsEnv in + ocanren { + fresh vs in + vals == ValsEnv vs & + List.assoco id vs v + } + + let rec pathtypeo types p tp = + let open Path in + let open Type in + ocanren { + { fresh x in + p == VarP x & + types_assoco x types tp } | + { fresh p', tp', _c in + p == DerefP p' & + pathtypeo types p' tp' & + tp' == RefT (_c, tp) } | + { fresh p', id', tp', tps in + p == AccessP (p', id') & + pathtypeo types p' tp' & + tp' == TupleT tps & + list_ntho tps id' tp } + } + + let rec pathvalo mem vals p v = + let open Path in + let open Value in + ocanren { + { fresh x, id in + p == VarP x & + vals_assoco x vals id & + mem_geto mem id v } | + { fresh p', v', id in + p == DerefP p' & + pathvalo mem vals p' v' & + v' == RefV id & + mem_geto mem id v } | + { fresh p', id, v', vs in + p == AccessP (p', id) & + pathvalo mem vals p' v' & + v' == TupleV vs & + list_ntho vs id v } + } + + (* --- eval rules --- *) + + (* - value construction *) + + let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = + ocanren { + fresh mem, vs, mem', v', mem_with_v', vs' in + Std.pair mem vs == mem_with_vs & + valcopyo mem v tp mem_with_v' & + Std.pair mem' v' == mem_with_v' & + vs' == v' :: vs & + mem_with_vs' == Std.pair mem vs' + } + + and valcopyo mem v tp mem_with_id' = + let open Type in + let open Value in + let open ReadCap in + let open CopyCap in + ocanren { + { fresh r, w in + is_trivial_vo v & + tp == UnitT (r, w) & + { { r == Rd & mem_with_id' == Std.pair mem v } | + { r == NRd & mem_with_id' == Std.pair mem BotV } } } | + { fresh stmts, ts in + v == FunV stmts & + tp == FunT ts & + mem_with_id' == Std.pair mem v } | + { fresh c, tp', id in + v == RefV id & + tp == RefT (c, tp') & + { { c == Rf & mem_with_id' == Std.pair mem v } | + { fresh v, mem_cp, v_cp, mem_with_v_cp, + mem_add, id_add, mem_with_id_add in + c == Cp & + mem_geto mem id v & + valcopyo mem v tp mem_with_v_cp & + Std.pair mem v_cp == mem_with_v_cp & + mem_addo mem_cp v_cp mem_with_id_add & + Std.pair mem_add id_add == mem_with_id_add & + mem_with_id' == (mem_add, RefV id_add) } } } | + { fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in + v == TupleV vs & + tp == TupleT tps & + init_mem_with_vs == Std.pair mem [] & + list_foldl2o valcopy_foldero init_mem_with_vs vs tps mem_with_vs' & + Std.pair mem' vs' == mem_with_vs' & + mem_with_id' == Std.pair mem' (TupleV vs') } + } + + (* - value update *) + + let rec valupdo mem v p b mem_with_v' = + let open Path in + let open Value in + ocanren { + { fresh x in + p == VarP x & + mem_with_v' == Std.pair mem b } | + { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in + p == DerefP p' & + v == RefV id & + mem_geto mem id v' & + valupdo mem v' p' b mem_with_v_upd & + Std.pair mem_upd v_upd == mem_with_v_upd & + mem_seto mem_upd id v_upd mem_st & + mem_with_v' == Std.pair mem_st (RefV id) } | + { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in + p == AccessP (p', id) & + v == TupleV vs' & + list_ntho vs' id v' & + valupdo mem v' p' b mem_with_v_upd & + Std.pair mem_upd v_upd == mem_with_v_upd & + list_replaceo vs' id v_upd vs_upd & + mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } + } + + (* - value combination *) + + let rec valcombo u v u' = + let open Value in + ocanren { + { is_trivial_vo u & + is_trivial_vo v & + (* TODO: do not use disequality constraint ? *) + { { u == v & u' == u } | { u =/= v & u' == BotV } } } | + { fresh ustmts, vstmts, ustmts' in + u == FunV ustmts & + v == FunV vstmts & + (* TODO: swap stmts order o efficiency ? *) + List.appendo ustmts vstmts ustmts' & + u' == FunV ustmts' } | + { fresh a, b in + u == RefV a & + v == RefV b & + a == b } | + { fresh us, vs, us' in + u == TupleV us & + v == TupleV vs & + list_zip_witho valcombo us vs us' & + u' == TupleV us' } + } + + let memcombo m n m' = ocanren { + fresh mm, ml, nm, nl, mm' in + Pair.pair mm ml == m & + Pair.pair nm nl == n & + list_zip_witho valcombo mm nm mm' & + m' == Pair.pair mm' ml + } + + (* - expression evaluation *) + + let rec exprvalo mem vals e v' = + let open Expr in + let open Value in + ocanren { + { e == UnitE & v' == ZeroV } | + { fresh p in + e == PathE p & + pathvalo mem vals p v' } | + { fresh x, v in + e == RefE x & + vals_assoco x vals v & + v' == RefV v } | + { fresh es, vs' in + e == TupleE es & + List.mapo (exprvalo mem vals) es vs' & + v' == TupleV vs' } + } + + (* - expression typing *) + + let rec exprtypeo types e tp' = + let open Expr in + let open Type in + let open ReadCap in + let open WriteCap in + let open CopyCap in + ocanren { + { e == UnitE & tp' == UnitT (Rd, NeverWr) } | + { fresh p in + e == PathE p & + pathtypeo types p tp' } | + { fresh x, tp in + e == RefE x & + types_assoco x types tp & + tp' == RefT (Rf, tp) } | + { fresh es, tps' in + e == TupleE es & + List.mapo (exprtypeo types) es tps' & + tp' == TupleT tps' } + } + + (* - context initialization *) + + let add_declo st x d st' = + let open StEnv in + let open Decl in + let open TypesEnv in + let open ValsEnv in + ocanren { + fresh mem, types, vals in + st == StEnv (mem, TypesEnv types, ValsEnv vals) & + { + { fresh tp, e, v, + mem_with_v_cp, mem_cp, v_cp, + mem_with_id_add, mem_add, id_add in + d == VarD (tp, e) & + exprvalo mem (ValsEnv vals) e v & + valcopyo mem v tp mem_with_v_cp & + Pair.pair mem_cp v_cp == mem_with_v_cp & + mem_addo mem_cp v_cp mem_with_id_add & + Pair.pair mem_add id_add == mem_with_id_add & + st' == StEnv (mem_add, + TypesEnv ((Pair.pair x tp) :: types), + ValsEnv ((Pair.pair x id_add) :: vals)) + } + } + } + + let empty_memo m = + let open MemEnv in + ocanren { m == MemEnv ([], 0) } + + let empty_stateo st = + let open StEnv in + let open TypesEnv in + let open ValsEnv in + ocanren { + fresh m in + empty_memo m & + st == StEnv (m, TypesEnv [], ValsEnv []) + } + + (* TODO: better way ??? *) + let globals_min_ido x = ocanren { x == 1000 } + + let prog_init_foldero st_with_id d st_with_id' = + ocanren { + fresh st, x, st' in + Std.pair st x == st_with_id & + add_declo st x d st' & + st_with_id' == Std.pair st' (Nat.s x) + } + + let prog_inito prog st' = + let open Prg in + ocanren { + fresh decls, s, st_init, min_id, st_with_id', _id' in + prog == Prg (decls, s) & + empty_stateo st_init & + globals_min_ido min_id & + list_foldlo prog_init_foldero (Std.pair st_init min_id) decls st_with_id' & + Std.pair st' _id' == st_with_id' + } + + (* - call values spoil *) + + (* TODO: check that negation is interpreted correctly *) + let is_correct_args v r w _r' w' m c = + let open Value in + let open ReadCap in + let open WriteCap in + let open Mode in + let open CopyCap in + ocanren { + { r == NRd | v == ZeroV } & + { r == NRd | is_ino m } & + { is_not_outo m | w == AlwaysWr } & + { w == NeverWr | + { is_not_outo m & c == Cp } | + w' == AlwaysWr } & + is_trivial_vo v + } + + (* TODO *) + + (* full spoil *) + (* TODO *) + + (* - funciton argument addition *) + (* TODO *) + + (* - function evaluation *) + (* NOTE: not needed due to performed optimization in stmt_eval ? *) + + (* - statement evaluation *) + (* TODO *) + + (* --- program execution --- *) + + (* let prog_evalo prog st' = *) + (* let open Prog in *) + (* ocanren { *) + (* fresh decls, s, init_st, *) + (* prog == Prog (decls, s) & *) + (* prog_inito prog init_st & *) + (* stmt_evalo init_st s st' *) + (* } *) + (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) + (* --- tests --- *) + (* TODO *) + + (* - shortcuts *) + (* TODO *) + (* --- *) (* let rec list_zip_witho f xs ys zs = ocanren { *) From 99a18feee9e0d47f74890ba8e32083a552914ada Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 5 May 2026 16:52:43 +0000 Subject: [PATCH 2/3] struct: synt: valspoil --- model_with_structures/synthesizer.ml | 59 +++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 2 deletions(-) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index f23acc2..8386ddf 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -424,7 +424,6 @@ struct vs' == v' :: vs & mem_with_vs' == Std.pair mem vs' } - and valcopyo mem v tp mem_with_id' = let open Type in let open Value in @@ -632,7 +631,7 @@ struct (* - call values spoil *) (* TODO: check that negation is interpreted correctly *) - let is_correct_args v r w _r' w' m c = + let is_correct_tagso v r w _r' w' m c = let open Value in let open ReadCap in let open WriteCap in @@ -650,7 +649,63 @@ struct (* TODO *) + let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren { + fresh mem, vs, mem', v' in + Std.pair mem vs == mem_with_vs & + valspoilo mem v tp u m c (Std.pair mem' v') & + mem_with_vs' == Std.pair mem' (v' :: vs) + } + and valspoilo mem v tp u m c mem_with_v' = + let open Type in + let open Value in + let open Mode in + let open WriteCap in + let open CopyCap in + ocanren { + { fresh r, w, r', w' in + tp == UnitT (r, w) & + u == UnitT (r', w') & + is_trivial_vo v & + is_correct_tagso v r w r' w' m c & + { + { is_not_outo m & + c == Rf & + { w == AlwaysWr | w == MayWr } & + mem_with_v' == Std.pair mem BotV } | + { is_outo m & + w == AlwaysWr & + mem_with_v' == Std.pair mem ZeroV } | + { { is_outo m | c == Cp | w == NeverWr } & + { is_not_outo m | w == MayWr | w == NeverWr } & + mem_with_v' == Std.pair mem v } + } } | + { fresh ts, us, _stmts in + tp == FunT ts & + u == FunT us & + v == FunV _stmts & + ts == us & + mem_with_v' == Std.pair mem v } | + { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in + tp == RefT (ctp', tp') & + u == RefT (cu', u') & + v == RefV id' & + mem_geto mem id' v' & + valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) & + mem_seto mem_sp id' v_sp mem_set & + mem_with_v' == Std.pair mem_set (RefV id') } | + { fresh tps, us, vs, mem_sp,vs_sp in + tp == TupleT tps & + u == TupleT us & + v == TupleV vs & + list_foldl3o (valspoil_foldero m c) + (Std.pair mem []) tps us vs + (Std.pair mem_sp vs_sp) & + mem_with_v' == Std.pair mem_sp (TupleV vs_sp) + } + } + (* full spoil *) + (* TODO *) (* - funciton argument addition *) From ddde0e95416f84d431de3bcfd6b371042839e3e2 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 5 May 2026 18:14:58 +0000 Subject: [PATCH 3/3] struct: fixes, full untested version of synt (without memoization, strightforward rewrite without testing) --- model_with_structures/analyzer.ml | 25 ++-- model_with_structures/model.typ | 32 ++--- model_with_structures/synthesizer.ml | 179 ++++++++++++++++++++++++--- 3 files changed, 195 insertions(+), 41 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 9bc39d6..10b74d7 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -296,7 +296,7 @@ struct (* full spoil *) - let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = + let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = match state with (mem, types, vals) -> let x = pathvar p in let id = List.assoc x vals in @@ -310,6 +310,8 @@ struct match state with (mem, types, vals) -> match e, t with | UnitE, UnitT _ -> mem | PathE p, t -> argsspoilp state m t p + | RefE x, t -> argsspoilp state m t (VarP x) + (* TODO: FIXME: check RefE case ? *) | TupleE es, TupleT ts -> List.fold_left2 (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e') mem ts es @@ -322,7 +324,7 @@ struct 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 + let (mem'', id) = mem_add mem' v' in (mem'', (x, t) :: types, (x, id) :: vals) (* - function evaluation *) @@ -333,21 +335,26 @@ struct let rec stmt_eval (state : state) (s : stmt) : state = match state with (mem, types, vals) -> match s with - (* TODO: FIXME: Add memoisation *) + (* TODO: FIXME: Add memoization *) | SkipS -> state - | 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 + | 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, _) = (* 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)) + 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) e -> (addarg st vals x t e, 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 = (* 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 + 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) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 8ca0dc1..76424e1 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -926,7 +926,7 @@ $s in stmt, f in X, x in X, a in X$ $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$, // TODO:: is c important ? - $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$, + $mu stretch(=>)^(m space rf c space t space rf x)_(cl vals, types cr) mu'$, ) )) @@ -1042,21 +1042,6 @@ $s in stmt, f in X, x in X, a in X$ #h(10pt) -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ READ $p$], - - $vals, mu tval p eqmu 0$, - - $cl types, vals, mu cr - xarrow("READ" p) - cl types, vals, mu cr$, - ) -)) - -#h(10pt) - #align(center, prooftree( vertical-spacing: 4pt, rule( @@ -1074,6 +1059,21 @@ $s in stmt, f in X, x in X, a in X$ ) )) +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ READ $p$], + + $vals, mu tval p eqmu 0$, + + $cl types, vals, mu cr + xarrow("READ" p) + cl types, vals, mu cr$, + ) +)) + +#h(10pt) + #h(10pt) #align(center, prooftree( diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 8386ddf..759730a 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -514,12 +514,14 @@ struct u' == TupleV us' } } - let memcombo m n m' = ocanren { + let memcombo m n m' = + let open MemEnv in + ocanren { fresh mm, ml, nm, nl, mm' in - Pair.pair mm ml == m & - Pair.pair nm nl == n & + MemEnv (mm, ml) == m & + MemEnv (nm, nl) == n & list_zip_witho valcombo mm nm mm' & - m' == Pair.pair mm' ml + m' == MemEnv (mm', ml) } (* - expression evaluation *) @@ -647,8 +649,6 @@ struct is_trivial_vo v } - (* TODO *) - let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren { fresh mem, vs, mem', v' in Std.pair mem vs == mem_with_vs & @@ -706,10 +706,71 @@ struct (* full spoil *) - (* TODO *) + let argspoilpo st m tp p mem' = + let open StEnv in + let open CopyCap in + ocanren { + fresh mem, types, vals, x, id, b, tp', + mem_sp, b_sp, v_sp, mem_upd, v_upd in + st == StEnv (mem, types, vals) & + pathvaro p x & + vals_assoco x vals id & + pathvalo mem vals p b & + pathtypeo types p tp' & + valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) & + mem_geto mem_sp id v_sp & + valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) & + mem_seto mem_upd id v_upd mem' + } + + let rec argspoile_foldero types vals m mem tp e mem' = + let open StEnv in + ocanren { + fresh st in + st == StEnv (mem, types, vals) & + argspoileo st m tp e mem' + } + and argspoileo st m tp e mem' = + let open StEnv in + let open Expr in + let open Type in + let open Path in + ocanren { + fresh _r, _w, mem, types, vals in + st == StEnv (mem, types, vals) & + { + { e == UnitE & + tp == UnitT (_r, _w) & + mem' == mem } | + { fresh p in + e == PathE p & + argspoilpo st m tp p mem' } | + { fresh x in + e == RefE x & + argspoilpo st m tp (VarP x) mem' } | + { fresh es, tps in + e == TupleE es & + tp == TupleT tps & + list_foldl2o (argspoile_foldero types vals m) mem tps es mem'} + } + } (* - funciton argument addition *) - (* TODO *) + + let addargo st oldvals x tp e st' = + let open StEnv in + let open TypesEnv in + let open ValsEnv in + ocanren { + fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in + st == StEnv (mem, TypesEnv types, ValsEnv vals) & + exprvalo mem oldvals e v & + valcopyo mem v tp (Std.pair mem_cp v_cp) & + mem_addo mem_cp v_cp (Std.pair mem_add id_add) & + st' == StEnv (mem_add, + TypesEnv ((Std.pair x tp) :: types), + ValsEnv ((Std.pair x id_add) :: vals)) + } (* - function evaluation *) (* NOTE: not needed due to performed optimization in stmt_eval ? *) @@ -717,16 +778,102 @@ struct (* - statement evaluation *) (* TODO *) + let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren { + fresh st, x, m, tp, st' in + Std.pair st x == st_with_id & + Std.pair m tp == mtp & + addargo st vals x tp e st' & + st_with_id' == Std.pair st' (Nat.s x) + } + and stmt_eval_spoil_foldero types vals mem mtp e mem' = + let open StEnv in + ocanren { + fresh m, tp, st in + Std.pair m tp == mtp & + st == StEnv (mem, types, vals) & + argspoileo st m tp e mem' + } + and stmt_evalo st s st' = + let open StEnv in + let open Stmt in + let open Value in + let open Type in + let open WriteCap in + let open TypesEnv in + let open ValsEnv in + ocanren { + fresh mem, types, vals in + st == StEnv (mem, types, vals) & + { + { s == SkipS & st == st' } | + { fresh f, es, v, tp, types', vals', + fstmts, tps, st', + state_with_args, _arg_id, + _states_evaled, + mem_spoiled in + s == CallS (f, es) & + pathvalo mem vals f v & + pathtypeo types f tp & + types' == TypesEnv [] & + vals' == ValsEnv [] & + v == FunV fstmts & + tp == FunT tps & + st' == StEnv (mem, types', vals') & + (* TODO: type error, fix required *) + list_foldl2o (stmt_addarg_foldero vals) + (Std.pair st' 0) tps es + (Std.pair state_with_args _arg_id) & + List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & + (* TODO: FIXME check left or right order *) + list_foldl2o (stmt_eval_spoil_foldero types vals) + mem tps es mem_spoiled & + st' == StEnv (mem_spoiled, types, vals) } | + { fresh p, tp, _r, w, x, id, v, + mem_upd, v_upd, mem_set in + s == WriteS p & + pathtypeo types p tp & + tp == UnitT (_r, w) & + { w == AlwaysWr | w == MayWr } & + pathvaro p x & + vals_assoco x vals id & + mem_geto mem id v & + valupdo mem v p ZeroV (Std.pair mem_upd v_upd) & + mem_seto mem_upd id v_upd mem_set & + st' == StEnv (mem_set, types, vals) } | + { fresh p in + s == ReadS p & + pathvalo mem vals p ZeroV & + st == st' } | + { fresh sl, sr, stl in + s == SeqS (sl, sr) & + stmt_evalo st sl stl & + stmt_evalo stl sr st' } | + { fresh sl, sr, stl, str, + meml, typesl, valsl, + memr, typesr, valsr, + mem' in + s == ChoiceS (sl, sr) & + stmt_evalo st sl stl & + stmt_evalo st sr str & + str == StEnv (memr, typesr, valsr) & + stl == StEnv (meml, typesl, valsl) & + typesl == typesr & + valsl == valsr & + memcombo meml memr mem' & + st' == StEnv (mem', typesl, valsl) } + } + } + (* --- program execution --- *) - (* let prog_evalo prog st' = *) - (* let open Prog in *) - (* ocanren { *) - (* fresh decls, s, init_st, *) - (* prog == Prog (decls, s) & *) - (* prog_inito prog init_st & *) - (* stmt_evalo init_st s st' *) - (* } *) + let prog_evalo prog st' = + let open Prg in + ocanren { + fresh decls, s, init_st in + prog == Prg (decls, s) & + prog_inito prog init_st & + stmt_evalo init_st s st' + } (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)