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

Compare commits

base: st:f8b89966fb4752c9bb47622f49bb08a152a7f7f0
Branches Tags
st:main
..
compare: st:5f7b25be8116086047c87304a56d7fd4ad5e5afc
Branches Tags
st:main

No commits in common. "f8b89966fb4752c9bb47622f49bb08a152a7f7f0" and "5f7b25be8116086047c87304a56d7fd4ad5e5afc" have entirely different histories.
f8b89966fb ... 5f7b25be81

2 changed files with 86 additions and 160 deletions
Download patch file Download diff file Expand all files Collapse all files

10
lib/dune
View file

@ -1,7 +1,7 @@
; (env (env
; (_ (_
; (flags (flags
; (:standard -warn-error +5)))) (:standard -warn-error +5))))
(library (library
(name semantic_interpreter) (name semantic_interpreter)
@ -26,7 +26,7 @@
(flags (flags
(:standard -rectypes)) (:standard -rectypes))
(libraries OCanren OCanren.tester) (libraries OCanren OCanren.tester)
(preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) (preprocessor_deps %{project_root}/lib/pp5+gt+plugins+ocanren+dump.exe)
(inline_tests) (inline_tests)
(wrapped false) (wrapped false)
(preprocess (preprocess

236
lib/relational_semantic_interpreter.ml
View file

@ -45,229 +45,155 @@ struct
type env_injected = (data_injected * data_injected) List.injected ilogic type env_injected = (data_injected * data_injected) List.injected ilogic
@type ('env, 'mem, 'last_mem, 'assignments) state_abs = 'env * 'mem * 'last_mem * 'assignments with show, gmap @type ('env, 'mem, 'last_mem, 'assignments) state_abs = 'env * 'mem * 'last_mem * 'assignments with show, gmap
@type state_ground = (env_ground, value_ground List.ground, data_ground, data_ground List.ground) state_abs with show, gmap @type state_ground = (list_map_ground, value_ground List.ground, data_ground, data_ground List.ground) state_abs with show, gmap
@type state_logic = (env_logic, value_logic List.logic, data_logic, data_logic List.logic) state_abs logic with show, gmap @type state_logic = (list_map_logic, value_logic List.logic, data_logic, data_logic List.logic) state_abs logic with show, gmap
type state_injected = (env_injected, value_injected List.injected, data_injected, data_injected List.injected) state_abs ilogic type state_injected = (env_injected, value_injected List.injected, data_injected, data_injected List.injected) state_abs ilogic
(* ocanren type 'a lst = Nil | Cons of 'a * 'a lst *) (* ocanren type 'a lst = Nil | Cons of 'a * 'a lst *)
let rec list_replace xs id value ys = let rec list_replace xs id value ys =
conde conde
[ (xs === Std.nil ()) &&& (ys === Std.nil ()) (* TODO: error *) [ (xs === List.nil) (ys === List.nil) (* TODO: error *)
; fresh (x xs') (xs === List.cons x xs') (id === Nat.o) (ys === List.cons value xs) ; fresh (x xs') (xs === List.cons x xs') (id === 0) (ys === List.cons value xs)
; fresh (x xs' id' ys') (xs === List. cons x xs') (id === Nat.s id') (ys === List.cons x ys') ; fresh (x xs' id' ys') (xs ===List. cons x xs') (id === Nat.succ id') (ys === List.cons x ys')
(list_replace xs' id' value ys') (list_replace xs' id' value ys')
] ]
let rec list_assoc a xs v' = let env_get state id state' =
conde fresh (env env' mem mem_len assignments)
[ fresh (a' b' xs') (state === (env, mem, mem_len, assignments))
(xs === List.cons (a', b') xs') (state' === (env', mem, mem_len, assignments))
(a =/= a') (List.assoco id env env')
(list_assoc a xs' v')
; fresh (a' b' xs')
(xs === List.cons (a', b') xs')
(a === a')
(v' === b')
]
(* TODO: dofference from List.assoco ?? *)
let env_get state id mem_id' =
fresh (env mem mem_len assignments)
(state === inj (env, mem, mem_len, assignments))
(list_assoc 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 === inj (env, mem, mem_len, assignments)) (state === (env, mem, mem_len, assignments))
(state' === inj (env', mem, mem_len, assignments)) (state' === (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' =
fresh (inv_id_inc) (fresh inv_id_inc)
(Nat.addo inv_id_inc id mem_len) (Nat.addo inv_id_inc id mem_len)
(Nat.addo id' (Nat.s Nat.o) inv_id_inc) (Nat.addo id' 1 inv_id_inc)
(* --- *) (* --- *)
let rec list_nth xs id x' = let list_nth xs id x' =
conde conde
[ (xs === Std.nil ()) (* TODO: error *) [ (xs === List.nil) (* TODO: error *)
; fresh (y' xs') (id === Nat.o) (List.cons y' xs' === xs) (x' === y') ; (fresh y' xs') (id === 0) (List.cons y' xs' === xs) (x' === y')
; fresh (id' y' xs') (Nat.s id' === id) (List.cons y' xs' === xs) (list_nth xs' id' x') ; (fresh id' y' xs') (Nat.succ id' === id) (List.cons y' xs' === xs) (list_nth xs' id' x')
] ]
(* 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)
(state === inj (env_, mem, mem_len, assignments_)) (state === (_, mem, mem_len, _))
(fresh mem_id mem_id_inv)
(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_len_inv)
(list_nth mem mem_id_inv value') (list_nth mem mem_id 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') (fresh env mem mem_len assignments)
(state === inj (env, mem, mem_len, assignments)) (state === (env, mem, mem_len, assignments))
(env_get state id mem_id) (fresh mem_id) (env_get state id mem_id)
(inv_id mem_len mem_id inv_mem_id) (fresh inv_mem_id) (inv_id mem_len mem_id inv_mem_id)
(list_replace mem mem_id value mem') (fresh mem') (list_replace mem mem_id value mem')
(state' === inj (env, mem', mem_len, List.cons id assignments)) (state' === (env, mem', mem_len, List.cons id assignments))
let mem_add state value state' = let mem_add state value state' =
fresh (env mem mem_len assignments mem') (fresh env mem mem_len assignments)
(state === inj (env, mem, mem_len, assignments)) (state === (env, mem, mem_len, assignments))
(mem' === List.cons value mem) (fresh mem') (mem' === List.cons value mem)
(state' === inj (env, mem, Nat.s mem_len, assignments)) (state' === (env, mem, Nat.succ mem_len, assignments))
let mem_check state id state' = let mem_check state id state' =
conde conde
[ (mem_get state id (inj BotV)) &&& (state' === state) (* TODO: error *) [ (mem_get state id BotV) (state' === state) (* TODO: error *)
; (mem_get state id (inj UnitV)) &&& (state' === state) ; (mem_get state id UnitV) (state' === state)
] ]
(* --- *) (* --- *)
let rec list_foldl f acc xs acc' =
conde
[ (xs === Std.nil ()) &&& (acc' === acc)
; fresh (x' xs' acc_upd)
(xs === List.cons x' xs')
(list_foldl f acc xs' acc_upd)
(f acc_upd x' acc')
]
let rec list_foldr2 f acc xs ys acc' =
conde
[ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc)
; fresh (x' xs' y' ys' acc_upd)
(xs === List.cons x' xs')
(ys === List.cons y' ys')
(f acc x' y' acc_upd)
(list_foldr2 f acc_upd xs' ys' acc')
]
let rec list_foldl2 f acc xs ys acc' =
conde
[ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc)
; fresh (x' xs' y' ys' acc_upd)
(xs === List.cons x' xs')
(ys === List.cons y' ys')
(list_foldl2 f acc xs' ys' acc_upd)
(f acc_upd x' y' acc')
]
let arg_to_value state arg value' = let arg_to_value state arg value' =
conde conde
[ (arg === inj RValue) &&& (value' === inj UnitV) [ (arg === RValue) (value' === UnitV)
; fresh (id) (arg === inj (LValue id)) (mem_get state id value') ; (fresh id) (arg === LValue id) (mem_get state id value')
] ]
let arg_to_rvalue _arg value' = (value' === inj RValue) let st_mem_len state mem_len' = (state === (_, _, mem_len, _))
let st_mem_len state mem_len' =
fresh (env_ mem_ assignments_) (* TODO: replace with real placeholder ? *)
(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 === inj Ref) &&& (arg === inj RValue) &&& (state'' === state) [ (arg_tag === Ref) (arg === RValue) (state'' === state) (* TODO: error *) (* TODO: allow later ?? *)
(* TODO: error, TODO: allow later ?? *) ; (fresh arg') (arg_tag === Ref) (arg === LValue arg')
; fresh (arg' value') (fresh value') (env_get state_before arg value')
(arg_tag === inj Ref) (env_add state id value' state'')
(arg === inj (LValue arg')) ; (arg_tag === Value)
(env_get state_before arg' value') (fresh value' state' mem_len_dec')
(env_add state id value' state'')
; fresh (value' state' mem_len_dec')
(arg_tag === inj 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')) (Nat.succ mem_len_dec' === st_mem_len state)
(env_add state' id mem_len_dec' state'') (env_add state' id mem_len_dec' state'')
] ]
let st_spoil_folder mem_len state mem id mem' =
fresh (mem_id' mem_id_inv')
(env_get state id mem_id')
(inv_id mem_len mem_id' mem_id_inv')
(list_replace mem mem_id_inv' (inj BotV) mem')
let st_spoil_assignments state state' = let st_spoil_assignments state state' =
fresh (env mem mem' mem_len assignments) (fresh env mem mem' mem_len assignments)
(state === inj (env, mem, mem_len, assignments)) (state === (env, mem, mem_len, assignments))
(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') *) (* TODO: replace with foldlo (or foldro ?) *)
(state' === inj (env, mem', mem_len, Std.nil ())) (state') === (env, mem', mem_len, [])
(* --- *) (* --- *)
let arg_to_lvalue arg arg' = (arg' === inj (LValue arg)) let arg_to_lvalue arg arg' = (arg' === LValue arg)
let rec list_drop n xs xs' =
conde
[ (xs === Std.nil ()) &&& (xs' === Std.nil ())
; n === Nat.o &&& (xs === xs')
; fresh (n' y ys) (Nat.s n' === n) (xs === List.cons y ys) (list_drop n' ys xs')
]
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)
(stmt === inj (Call (f_id, args))) (stmt === Call (f_id, args))
(fresh f 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')
; fresh (id) (stmt === inj (Read id)) (mem_check state id state') ; (fresh id) (stmt === Read id) (mem_check state id state')
; fresh (id) (stmt === inj (Write id)) (mem_set state id (inj UnitV) state') ; (fresh id) (stmt === Write id) (mem_set state it UnitV state')
] ]
and eval_body_folder prog state stmt state' = eval_stmt state prog stmt state'
and eval_body state prog body state' = and eval_body state prog body state' =
list_foldl (eval_body_folder prog) state body state' (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body)
(* (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body) *) (* TODO: replace with foldlo (or foldro ?) *)
and add_arg_folder state_before state_c arg_tag arg state_c' =
fresh (state id state' id')
(state_c === inj (state, id))
(st_add_arg state state_before id arg_tag arg state')
(id' === Nat.s id)
(state_c' === inj (state', id'))
and eval_fun state prog decl args state' = and eval_fun state prog decl args state' =
fresh (arg_tags body (fresh arg_tags body)
env_before mem_before len_before assignments_before (fresh env_before mem_before len_before assignments_before)
state_clean (fresh state_clean)
state_with_vars counter_ (state_clean === ([], mem_before, len_before, []))
state_evaled (fresh state_with_vars)
state_spoiled (state_with_vars === List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state id arg_tag arg, id + 1)) (state, 0) arg_tags args)
env_ mem_spoiled len assignments_ (* TODO how, rewrite from scratch ??? *)
mem_updated len_to_drop) (* TODO: replace with foldlo (or foldro ?) ?? *)
(decl === inj (arg_tags, body)) (fresh state_evaled)
(state === inj (env_before, mem_before, len_before, assignments_before)) (eval_body state prog body state_evaled)
(state_clean === inj (Std.nil (), mem_before, len_before, Std.nil ())) (fresh state_spoiled)
(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)
(st_spoil_assignments state_evaled state_spoiled) (st_spoil_assignments state_evaled state_spoiled)
(state_spoiled === inj (env_, mem_spoiled, len, assignments_)) (fresh mem_updated len_to_drop)
(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 mem_updated)
(state' === inj (env_before, mem_updated, len_before, assignments_before)) (state' === (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)
(decl === inj (arg_tags, hole_)) (decl === (arg_tags, _))
(List.mapo arg_to_rvalue arg_tags args) (List.mapo arg_to_rvalue arg_tags args) (* TODO how, rewrite from scratch ??? *)
(eval_fun state prog decl args state') (eval_fun state prog decl args state')
(* --- *) (* --- *)
let empty_state state = (state === inj (Std.nil (), Std.nil (), Nat.o, Std.nil ())) let empty_state state = (state === ([], [], 0, []))
let eval_prog all_prog state' = let eval_prog all_prog state' =
fresh (prog main_decl state) (fresh prog main_decl)
(all_prog === inj (prog, main_decl)) (all_prog == (prog, main_decl))
(empty_state state) (eval_fun_empty_args empty_state prog main_decl state')
(eval_fun_empty_args state prog main_decl state')
end end