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:909dad66940e9cf94a8dbca6adf12a472d96287d
Branches Tags
st:main
..
compare: st:b8ea97d537c3e700df3ef63eb231064e64ddd83f
Branches Tags
st:main

No commits in common. "909dad66940e9cf94a8dbca6adf12a472d96287d" and "b8ea97d537c3e700df3ef63eb231064e64ddd83f" have entirely different histories.
909dad6694 ... b8ea97d537

2 changed files with 6 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

9
lib/relational_semantic_interpreter.ml
View file

@ -40,14 +40,5 @@ struct
@type value_logic = value_ground logic with show, gmap @type value_logic = value_ground logic with show, gmap
type value_injected = value_ground ilogic type value_injected = value_ground ilogic
@type list_map_ground = (data_ground * data_ground) List.ground with show, gmap
@type list_map_logic = (data_logic * data_logic) List.logic with show, gmap
type list_map_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 state_ground = (list_map_ground, value_ground List.ground, data_ground, data_ground List.ground) state_abs 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 = (list_map_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 *)
end end

12
lib/semantic_interpreter.ml
View file

@ -23,7 +23,7 @@ struct
(* --- static interpreter (no rec) --- *) (* --- static interpreter (no rec) --- *)
type env = (int * data) list module M = Map.Make (Int);;
(* TODO: allow data (rvalue) in calls ?? *) (* TODO: allow data (rvalue) in calls ?? *)
type arg = RValue | LValue of data type arg = RValue | LValue of data
@ -31,7 +31,7 @@ struct
(* TODO: replace env map with pairs *) (* TODO: replace env map with pairs *)
(* env * memory * last unused memory * assignments *) (* env * memory * last unused memory * assignments *)
type state = env * value list * int * data list type state = data M.t * value list * int * data list
(* TODO: replace with pairs *) (* TODO: replace with pairs *)
let rec list_replace xs id value = match (xs, id) with let rec list_replace xs id value = match (xs, id) with
@ -41,10 +41,10 @@ struct
let env_get state id = match state with let env_get state id = match state with
(env, _mem, _mem_len, _assignments) -> List.assoc id env (env, _mem, _mem_len, _assignments) -> M.find id env
let env_add state id mem_id = match state with let env_add state id mem_id = match state with
(env, mem, mem_len, assignments) -> let env = (id, mem_id) :: env in (env, mem, mem_len, assignments) -> let env = M.add id mem_id env in
(env, mem, mem_len, assignments) (env, mem, mem_len, assignments)
let inv_id mem_len id = mem_len - id - 1 let inv_id mem_len id = mem_len - id - 1
@ -93,7 +93,7 @@ struct
and eval_fun state prog decl args = and eval_fun state prog decl args =
match decl with (arg_tags, body) -> match decl with (arg_tags, body) ->
match state with (env_before, mem_before, len_before, assignments_before) as state_before -> match state with (env_before, mem_before, len_before, assignments_before) as state_before ->
let state = ([], mem_before, len_before, []) in let state = (M.empty, mem_before, len_before, []) in
let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1)) (state, 0) arg_tags args in let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1)) (state, 0) arg_tags args in
let state = eval_body state prog body in let state = eval_body state prog body in
let state = st_spoil_assignments state in let state = st_spoil_assignments state in
@ -105,7 +105,7 @@ struct
let args = List.map (fun _ -> RValue) arg_tags in let args = List.map (fun _ -> RValue) arg_tags in
eval_fun state prog decl args eval_fun state prog decl args
let empty_state = ([], [], 0, []) let empty_state = (M.empty, [], 0, [])
let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl