st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-03-12 02:57:09 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:f15613d1924ac1bc267747eca9a82ccae5585ec7
Branches Tags
st:main
..
compare: st:22901cdc22d736fa07bd06e6fb555caa5d9ffab7
Branches Tags
st:main

No commits in common. "f15613d1924ac1bc267747eca9a82ccae5585ec7" and "22901cdc22d736fa07bd06e6fb555caa5d9ffab7" have entirely different histories.
f15613d192 ... 22901cdc22

1 changed files with 59 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

156
lib/relational_semantic_interpreter.ml
View file

@ -19,9 +19,6 @@ struct
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t type nonrec ground = t
] ]
let ref = inj Ref
let value = inj Value
end end
module Stmt = struct module Stmt = struct
@ -31,43 +28,33 @@ struct
[@@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
] ]
let call f args = inj (Call (f, args))
let read id = inj (Read id)
let write id = inj (Write id)
end end
module Body = struct module Body = 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"]
[%%distrib [%%distrib
type nonrec ('stmt, 'l) t = T of ('stmt, 'l) List.t type nonrec ('stmt, 'l) t = Body of ('stmt, 'l) List.t
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Stmt.ground, Stmt.ground List.ground) t type nonrec ground = (Stmt.ground, Stmt.ground List.ground) t
] ]
let make stmts = inj (T stmts)
end end
module FunDecl = struct module FunDecl = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%distrib [%%distrib
type nonrec ('l, 'b) t = T of 'l * 'b type nonrec ('tag, 'lt, 'stmt, 'ls) t = FunDecl of ('tag, 'lt) List.t * ('stmt, 'ls) Body.t
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Tag.ground List.ground, Body.ground) t type nonrec ground = (Tag.ground, Tag.ground List.ground, Stmt.ground, Stmt.ground List.ground) t
] ]
let make args body = inj (T (args, body))
end end
module Prog = struct module Prog = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%distrib [%%distrib
type nonrec ('l, 'f) t = T of 'l * 'f type nonrec ('fd, 'lf, 'tag, 'lt, 'stmt, 'ls) t = Prog of ('fd, 'lf) List.t * ('tag, 'lt, 'stmt, 'ls) FunDecl.t
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t type nonrec ground = (FunDecl.ground, FunDecl.ground List.ground, Tag.ground, Tag.ground List.ground, Stmt.ground, Stmt.ground List.ground) t
] ]
let make decls main_decl = inj (T (decls, main_decl))
end end
module Arg = struct module Arg = struct
@ -77,9 +64,6 @@ struct
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = Nat.ground t type nonrec ground = Nat.ground t
] ]
let rvalue = inj RValue
let lvalue x = inj (LValue x)
end end
module Value = struct module Value = struct
@ -89,32 +73,24 @@ struct
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t type nonrec ground = t
] ]
let unit = inj Unit
let bot = inj Bot
end end
(* module Envr = struct *) module Envr = 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"]
(* [%%distrib *) [%%distrib
(* type nonrec ('d, 'l) t = T of ('d * 'd, 'l) List.t *) type nonrec ('d, 'l) t = Envr of ('d * 'd, 'l) List.t
(* [@@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
(* ] *) ]
end
(* let make elems = inj (T elems) *)
(* end *)
module State = struct module State = 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"]
[%%distrib [%%distrib
type nonrec ('env, 'mem, 'last_mem, 'assignments) t = T of 'env * 'mem * 'last_mem * 'assignments type nonrec ('env, 'mem, 'last_mem, 'assignments) t = State of 'env * 'mem * 'last_mem * 'assignments
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (((Nat.ground, Nat.ground) Pair.ground) List.ground, type nonrec ground = (Envr.ground, Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
] ]
let make env mem last_mem assignments = inj (T (env, mem, last_mem, assignments))
end end
let rec list_replace xs id value ys = let rec list_replace xs id value ys =
@ -140,14 +116,14 @@ struct
let env_get state id mem_id' = let env_get state id mem_id' =
fresh (env mem mem_len assignments) fresh (env mem mem_len assignments)
(state === State.make env mem mem_len assignments) (state === inj (env, mem, mem_len, assignments))
(list_assoc id env mem_id') (list_assoc id env mem_id')
(* (List.assoco id env mem_id') *) (* (List.assoco id env mem_id') *)
let env_add state id mem_id state' = let env_add state id mem_id state' =
fresh (env env' mem mem_len assignments) fresh (env env' mem mem_len assignments)
(state === State.make env mem mem_len assignments) (state === inj (env, mem, mem_len, assignments))
(state' === State.make env' mem mem_len assignments) (state' === inj (env', mem, mem_len, assignments))
(env' === List.cons (id, mem_id) env) (env' === List.cons (id, mem_id) env)
let inv_id mem_len id id' = let inv_id mem_len id id' =
@ -166,32 +142,30 @@ struct
(* TODO: use real holes *) (* TODO: use real holes *)
let mem_get state id value' = let mem_get state id value' =
fresh (mem mem_len mem_id mem_id_inv _env _assignments) fresh (mem mem_len mem_id mem_id_inv env_ assignments_)
(state === inj (State.T (_env, mem, mem_len, _assignments))) (state === inj (env_, mem, mem_len, assignments_))
(env_get state id mem_id) (env_get state id mem_id)
(inv_id mem_len mem_id mem_id_inv) (inv_id mem_len mem_id mem_id_inv)
(list_nth mem mem_id_inv value') (list_nth mem mem_id_inv value')
let mem_set state id value state'= let mem_set state id value state'=
fresh (env mem mem_len assignments mem_id inv_mem_id mem' assignments') fresh (env mem mem_len assignments mem_id inv_mem_id mem')
(state === State.make env mem mem_len assignments) (state === inj (env, mem, mem_len, assignments))
(env_get state id mem_id) (env_get state id mem_id)
(inv_id mem_len mem_id inv_mem_id) (inv_id mem_len mem_id inv_mem_id)
(list_replace mem mem_id value mem') (list_replace mem mem_id value mem')
(assignments' === List.cons id assignments) (state' === inj (env, mem', mem_len, List.cons id assignments))
(state' === State.make env mem' mem_len assignments')
let mem_add state value state' = let mem_add state value state' =
fresh (env mem mem_len mem_len' assignments mem') fresh (env mem mem_len assignments mem')
(state === State.make env mem mem_len assignments) (state === inj (env, mem, mem_len, assignments))
(mem' === List.cons value mem) (mem' === List.cons value mem)
(mem_len' === Nat.s mem_len) (state' === inj (env, mem, Nat.s mem_len, assignments))
(state' === State.make env mem mem_len' assignments)
let mem_check state id state' = let mem_check state id state' =
conde conde
[ (mem_get state id Value.bot) &&& (state' === state) [ (mem_get state id (inj Value.Bot)) &&& (state' === state) (* TODO: error *)
; (mem_get state id Value.unit) &&& (state' === state) ; (mem_get state id (inj Value.Unit)) &&& (state' === state)
] ]
(* --- *) (* --- *)
@ -228,27 +202,27 @@ struct
let arg_to_value state arg value' = let arg_to_value state arg value' =
conde conde
[ (arg === Arg.rvalue) &&& (value' === Value.unit) [ (arg === inj Arg.RValue) &&& (value' === inj Value.Unit)
; fresh (id) (arg === Arg.lvalue id) (mem_get state id value') ; fresh (id) (arg === inj (Arg.LValue id)) (mem_get state id value')
] ]
let arg_to_rvalue _arg value' = (value' === inj Arg.RValue) let arg_to_rvalue _arg value' = (value' === inj Arg.RValue)
let st_mem_len state mem_len' = let st_mem_len state mem_len' =
fresh (_env _mem _assignments) (* TODO: replace with real placeholder ? *) fresh (env_ mem_ assignments_) (* TODO: replace with real placeholder ? *)
(state === State.make _env _mem mem_len' _assignments) (state === inj (env_, mem_, mem_len', assignments_))
let st_add_arg state state_before id arg_tag arg state'' = let st_add_arg state state_before id arg_tag arg state'' =
conde conde
[ (arg_tag === Tag.ref) &&& (arg === Arg.rvalue) &&& (state'' === state) [ (arg_tag === inj Tag.Ref) &&& (arg === inj Arg.RValue) &&& (state'' === state)
(* TODO: error, TODO: allow later ?? *) (* TODO: error, TODO: allow later ?? *)
; fresh (arg' value') ; fresh (arg' value')
(arg_tag === Tag.ref) (arg_tag === inj Tag.Ref)
(arg === Arg.lvalue arg') (arg === inj (Arg.LValue arg'))
(env_get state_before arg' value') (env_get state_before arg' value')
(env_add state id value' state'') (env_add state id value' state'')
; fresh (value' state' mem_len_dec') ; fresh (value' state' mem_len_dec')
(arg_tag === Tag.value) (arg_tag === inj Tag.Value)
(arg_to_value state_before arg value') (arg_to_value state_before arg value')
(mem_add state value' state') (mem_add state value' state')
(st_mem_len state (Nat.s mem_len_dec')) (st_mem_len state (Nat.s mem_len_dec'))
@ -262,12 +236,11 @@ struct
(list_replace mem mem_id_inv' (inj Value.Bot) mem') (list_replace mem mem_id_inv' (inj Value.Bot) mem')
let st_spoil_assignments state state' = let st_spoil_assignments state state' =
fresh (env mem mem' mem_len assignments nil') fresh (env mem mem' mem_len assignments)
(state === State.make env mem mem_len assignments) (state === inj (env, mem, mem_len, assignments))
(list_foldl (st_spoil_folder mem_len state) mem assignments mem') (list_foldl (st_spoil_folder mem_len state) mem assignments mem')
(* (List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments mem') *) (* (List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments mem') *)
(nil' === Std.nil ()) (state' === inj (env, mem', mem_len, Std.nil ()))
(state' === State.make env mem' mem_len nil')
(* --- *) (* --- *)
@ -283,12 +256,12 @@ struct
let rec eval_stmt state prog stmt state' = let rec eval_stmt state prog stmt state' =
conde conde
[ fresh (f_id args f args') [ fresh (f_id args f args')
(stmt === Stmt.call f_id args) (stmt === inj (Stmt.Call (f_id, args)))
(list_nth prog f_id f) (list_nth prog f_id f)
(List.mapo arg_to_lvalue args args') (List.mapo arg_to_lvalue args args')
(eval_fun state prog f args' state') (eval_fun state prog f args' state')
; fresh (id) (stmt === Stmt.read id) (mem_check state id state') ; fresh (id) (stmt === inj (Stmt.Read id)) (mem_check state id state')
; fresh (id) (stmt === Stmt.write id) (mem_set state id Value.unit state') ; fresh (id) (stmt === inj (Stmt.Write id)) (mem_set state id (inj Value.Unit) state')
] ]
and eval_body_folder prog state stmt state' = eval_stmt state prog stmt state' and eval_body_folder prog state stmt state' = eval_stmt state prog stmt state'
@ -308,55 +281,44 @@ struct
fresh (arg_tags body fresh (arg_tags body
env_before mem_before len_before assignments_before env_before mem_before len_before assignments_before
state_clean state_clean
state_with_vars _counter state_with_vars counter_
state_evaled state_evaled
state_spoiled state_spoiled
_env mem_spoiled len _assignments env_ mem_spoiled len assignments_
mem_updated len_to_drop mem_updated len_to_drop)
nil_env nil_assignments) (decl === inj (arg_tags, body))
(nil_env === Std.nil ()) (state === inj (env_before, mem_before, len_before, assignments_before))
(nil_assignments === Std.nil ()) (state_clean === inj (Std.nil (), mem_before, len_before, Std.nil ()))
(decl === FunDecl.make arg_tags body) (list_foldl2 (add_arg_folder state) (inj (state, Nat.o)) arg_tags args (inj (state_with_vars, counter_))) (* TODO: replace with real placeholder *)
(state === State.make env_before mem_before len_before assignments_before)
(state_clean === State.make nil_env mem_before len_before nil_assignments)
(list_foldl2 (add_arg_folder state) (inj (state, Nat.o)) arg_tags args (inj (state_with_vars, _counter))) (* TODO: replace with real placeholder *)
(eval_body state_with_vars prog body state_evaled) (eval_body state_with_vars prog body state_evaled)
(st_spoil_assignments state_evaled state_spoiled) (st_spoil_assignments state_evaled state_spoiled)
(state_spoiled === State.make _env mem_spoiled len _assignments) (state_spoiled === inj (env_, mem_spoiled, len, assignments_))
(Nat.addo len_to_drop len_before len) (Nat.addo len_to_drop len_before len)
(list_drop len_to_drop mem_spoiled mem_updated) (list_drop len_to_drop mem_spoiled mem_updated)
(state' === State.make env_before mem_updated len_before assignments_before) (state' === inj (env_before, mem_updated, len_before, assignments_before))
and eval_fun_empty_args state prog decl state' = and eval_fun_empty_args state prog decl state' =
fresh (arg_tags args _hole) (* TODO: replace with real placeholder *) fresh (arg_tags args hole_) (* TODO: replace with real placeholder *)
(decl === FunDecl.make arg_tags _hole) (decl === inj (arg_tags, hole_))
(List.mapo arg_to_rvalue arg_tags args) (List.mapo arg_to_rvalue arg_tags args)
(eval_fun state prog decl args state') (eval_fun state prog decl args state')
(* --- *) (* --- *)
let empty_state state = let empty_state state = (state === inj (Std.nil (), Std.nil (), Nat.o, Std.nil ()))
fresh (nil_env nil_mem nil_assignments)
(nil_env === Std.nil ())
(nil_assignments === Std.nil ())
(nil_mem === Std.nil ())
(state === State.make nil_env nil_mem Nat.o nil_assignments)
let eval_prog all_prog state' = let eval_prog all_prog state' =
fresh (prog main_decl state) fresh (prog main_decl state)
(all_prog === Prog.make prog main_decl) (all_prog === inj (prog, main_decl))
(empty_state state) (empty_state state)
(eval_fun_empty_args state prog main_decl state') (eval_fun_empty_args state prog main_decl state')
(* TODO: fix *) (* let eval_prog_fwd all_prog = *)
let eval_prog_fwd all_prog = (* run q (fun q -> eval_prog (inj_state all_prog) q) *)
Stream.hd @@ (* (fun _ -> ()) *)
run q (fun q -> eval_prog (inj all_prog) q)
(fun qs -> qs#reify prj_exn)
(* TODO: fix *)
(* let%expect_test "empty" = *) (* let%expect_test "empty" = *)
(* eval_prog_fwd (Prog.T ([], FunDecl.T ([], []))); *) (* eval_prog_fwd ([], ([], [])); *)
(* Printf.printf "done!"; *) (* Printf.printf "done!"; *)
(* [%expect {| done! |}] *) (* [%expect {| done! |}] *)