st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: correct glob context handling in synthesizer (fix ported from ananlyzer)

Browse source
This commit is contained in:
ProgramSnail 2026-05-06 17:17:36 +00:00
parent a130ffe819
commit ee8ff429cf
3 changed files with 83 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

2
model_with_structures/model.typ
View file

@ -15,6 +15,8 @@
*TODO: top-level value copy mode ??* // TODO: FIXME *TODO: top-level value copy mode ??* // TODO: FIXME
*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
#h(10pt) #h(10pt)
#let rf = $\& #h(3pt)$ #let rf = $\& #h(3pt)$

118
model_with_structures/synthesizer.ml
View file

@ -185,7 +185,7 @@ struct
module TypesEnv = struct module TypesEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec 'dtl t = TypesEnv of 'dtl type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Type.ground) List.ground) t type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
] ]
@ -194,7 +194,7 @@ struct
module ValsEnv = struct module ValsEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec 'ddl t = ValsEnv of 'ddl type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
] ]
@ -211,6 +211,58 @@ struct
(* --- *) (* --- *)
(* - state utils *)
let types_assoco id types tp =
let open TypesEnv in
ocanren {
fresh _glob_tps, tps in
types == TypesEnv (_glob_tps, tps) &
List.assoco id tps tp
}
let vals_assoco id vals v =
let open ValsEnv in
ocanren {
fresh _glob_vs, vs in
vals == ValsEnv (_glob_vs, vs) &
List.assoco id vs v
}
let types_glob_addo types x tp types' =
let open TypesEnv in
ocanren {
fresh glob_tps, tps in
types == TypesEnv (glob_tps, tps) &
types' == TypesEnv ((Std.pair x tp) :: glob_tps,
(Std.pair x tp) :: tps)
}
let types_addo types x tp types' =
let open TypesEnv in
ocanren {
fresh glob_tps, tps in
types == TypesEnv (glob_tps, tps) &
types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
}
let vals_glob_addo vals x v vals' =
let open ValsEnv in
ocanren {
fresh glob_vs, vs in
vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv ((Std.pair x v) :: glob_vs,
(Std.pair x v) :: vs)
}
let vals_addo vals x v vals' =
let open ValsEnv in
ocanren {
fresh glob_vs, vs in
vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
}
(* - utils *) (* - utils *)
let rec list_replaceo xs id value ys = ocanren { let rec list_replaceo xs id value ys = ocanren {
@ -357,22 +409,6 @@ struct
{ fresh p', _id in p == AccessP (p', _id) & 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 rec pathtypeo types p tp =
let open Path in let open Path in
let open Type in let open Type in
@ -572,24 +608,23 @@ struct
let add_declo st x d st' = let add_declo st x d st' =
let open StEnv in let open StEnv in
let open Decl in let open Decl in
let open TypesEnv in
let open ValsEnv in
ocanren { ocanren {
fresh mem, types, vals in fresh mem, types, vals in
st == StEnv (mem, TypesEnv types, ValsEnv vals) & st == StEnv (mem, types, vals) &
{ {
{ fresh tp, e, v, { fresh tp, e, v,
mem_with_v_cp, mem_cp, v_cp, mem_with_v_cp, mem_cp, v_cp,
mem_with_id_add, mem_add, id_add in mem_with_id_add, mem_add, id_add,
types', vals' in
d == VarD (tp, e) & d == VarD (tp, e) &
exprvalo mem (ValsEnv vals) e v & exprvalo mem vals e v &
valcopyo mem v tp mem_with_v_cp & valcopyo mem v tp mem_with_v_cp &
Pair.pair mem_cp v_cp == mem_with_v_cp & Pair.pair mem_cp v_cp == mem_with_v_cp &
mem_addo mem_cp v_cp mem_with_id_add & mem_addo mem_cp v_cp mem_with_id_add &
Pair.pair mem_add id_add == mem_with_id_add & Pair.pair mem_add id_add == mem_with_id_add &
st' == StEnv (mem_add, types_glob_addo types x tp types' &
TypesEnv ((Pair.pair x tp) :: types), vals_glob_addo vals x id_add vals' &
ValsEnv ((Pair.pair x id_add) :: vals)) st' == StEnv (mem_add, types', vals')
} }
} }
} }
@ -605,7 +640,7 @@ struct
ocanren { ocanren {
fresh m in fresh m in
empty_memo m & empty_memo m &
st == StEnv (m, TypesEnv [], ValsEnv []) st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []))
} }
(* TODO: better way ??? *) (* TODO: better way ??? *)
@ -759,17 +794,18 @@ struct
let addargo st oldvals x tp e st' = let addargo st oldvals x tp e st' =
let open StEnv in let open StEnv in
let open TypesEnv in
let open ValsEnv in
ocanren { ocanren {
fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in fresh mem, types, vals, v,
st == StEnv (mem, TypesEnv types, ValsEnv vals) & mem_cp, v_cp,
mem_add, id_add,
types', vals' in
st == StEnv (mem, types, vals) &
exprvalo mem oldvals e v & exprvalo mem oldvals e v &
valcopyo mem v tp (Std.pair mem_cp v_cp) & valcopyo mem v tp (Std.pair mem_cp v_cp) &
mem_addo mem_cp v_cp (Std.pair mem_add id_add) & mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
st' == StEnv (mem_add, types_addo types x tp types' &
TypesEnv ((Std.pair x tp) :: types), vals_addo vals x id_add vals' &
ValsEnv ((Std.pair x id_add) :: vals)) st' == StEnv (mem_add, types', vals')
} }
(* - function evaluation *) (* - function evaluation *)
@ -806,16 +842,20 @@ struct
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals) &
{ {
{ s == SkipS & st == st' } | { s == SkipS & st == st' } |
{ fresh f, es, v, tp, types', vals', { fresh f, es, v, tp,
glob_tps, _tps,
glob_vs, _vs,
types', vals',
fstmts, tps, st', fstmts, tps, st',
state_with_args, _arg_id, state_with_args, _arg_id,
_states_evaled, _states_evaled, mem_spoiled in
mem_spoiled in
s == CallS (f, es) & s == CallS (f, es) &
pathvalo mem vals f v & pathvalo mem vals f v &
pathtypeo types f tp & pathtypeo types f tp &
types' == TypesEnv [] & (* TODO: FIXME add globals *) types == TypesEnv (glob_tps, _tps) &
vals' == ValsEnv [] & (* TODO: FIXME add globals *) vals == ValsEnv (glob_vs, _vs) &
types' == TypesEnv (glob_tps, glob_tps) &
vals' == ValsEnv (glob_vs, glob_vs) &
v == FunV fstmts & v == FunV fstmts &
tp == FunT tps & tp == FunT tps &
st' == StEnv (mem, types', vals') & st' == StEnv (mem, types', vals') &

3
model_with_structures/tests.ml
View file

@ -2,7 +2,8 @@ open Tests_f
open Synthesizer open Synthesizer
open Relational open Relational
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([]), ValsEnv ([]))] |}] let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ());
[%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}]
(* type tests *) (* type tests *)
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)