diff --git a/lib/dune b/lib/dune index a4e98e3..7791c5e 100644 --- a/lib/dune +++ b/lib/dune @@ -1,7 +1,7 @@ -; (env -; (_ -; (flags -; (:standard -warn-error +5)))) +(env + (_ + (flags + (:standard -warn-error +5)))) (library (name semantic_interpreter) @@ -26,7 +26,7 @@ (flags (:standard -rectypes)) (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) (wrapped false) (preprocess diff --git a/lib/relational_semantic_interpreter.ml b/lib/relational_semantic_interpreter.ml index a1e5cd6..1163292 100644 --- a/lib/relational_semantic_interpreter.ml +++ b/lib/relational_semantic_interpreter.ml @@ -45,229 +45,155 @@ struct 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 state_ground = (env_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_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 = (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 *) let rec list_replace xs id value ys = conde - [ (xs === Std.nil ()) &&& (ys === Std.nil ()) (* TODO: error *) - ; fresh (x xs') (xs === List.cons x xs') (id === Nat.o) (ys === List.cons value xs) - ; fresh (x xs' id' ys') (xs === List. cons x xs') (id === Nat.s id') (ys === List.cons x ys') + [ (xs === List.nil) (ys === List.nil) (* TODO: error *) + ; 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.succ id') (ys === List.cons x ys') (list_replace xs' id' value ys') ] - let rec list_assoc a xs v' = - conde - [ fresh (a' b' xs') - (xs === List.cons (a', b') xs') - (a =/= a') - (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_get state id state' = + fresh (env env' mem mem_len assignments) + (state === (env, mem, mem_len, assignments)) + (state' === (env', mem, mem_len, assignments)) + (List.assoco id env env') let env_add state id mem_id state' = fresh (env env' mem mem_len assignments) - (state === inj (env, mem, mem_len, assignments)) - (state' === inj (env', mem, mem_len, assignments)) - (env' === List.cons (id, mem_id) env) + (state === (env, mem, mem_len, assignments)) + (state' === (env', mem, mem_len, assignments)) + (env' == List.cons (id, mem_id) env) 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 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 - [ (xs === Std.nil ()) (* TODO: error *) - ; fresh (y' xs') (id === Nat.o) (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') + [ (xs === List.nil) (* TODO: error *) + ; (fresh y' xs') (id === 0) (List.cons y' xs' === xs) (x' === y') + ; (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' = - fresh (mem mem_len mem_id mem_id_inv env_ assignments_) - (state === inj (env_, mem, mem_len, assignments_)) + (fresh mem mem_len) + (state === (_, mem, mem_len, _)) + (fresh mem_id mem_id_inv) (env_get state id mem_id) - (inv_id mem_len mem_id mem_id_inv) - (list_nth mem mem_id_inv value') + (inv_id mem_len mem_id mem_len_inv) + (list_nth mem mem_id value') let mem_set state id value state'= - fresh (env mem mem_len assignments mem_id inv_mem_id mem') - (state === inj (env, mem, mem_len, assignments)) - (env_get state id mem_id) - (inv_id mem_len mem_id inv_mem_id) - (list_replace mem mem_id value mem') - (state' === inj (env, mem', mem_len, List.cons id assignments)) + (fresh env mem mem_len assignments) + (state === (env, mem, mem_len, assignments)) + (fresh mem_id) (env_get state id mem_id) + (fresh inv_mem_id) (inv_id mem_len mem_id inv_mem_id) + (fresh mem') (list_replace mem mem_id value mem') + (state' === (env, mem', mem_len, List.cons id assignments)) let mem_add state value state' = - fresh (env mem mem_len assignments mem') - (state === inj (env, mem, mem_len, assignments)) - (mem' === List.cons value mem) - (state' === inj (env, mem, Nat.s mem_len, assignments)) + (fresh env mem mem_len assignments) + (state === (env, mem, mem_len, assignments)) + (fresh mem') (mem' === List.cons value mem) + (state' === (env, mem, Nat.succ mem_len, assignments)) let mem_check state id state' = conde - [ (mem_get state id (inj BotV)) &&& (state' === state) (* TODO: error *) - ; (mem_get state id (inj UnitV)) &&& (state' === state) + [ (mem_get state id BotV) (state' === state) (* TODO: error *) + ; (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' = conde - [ (arg === inj RValue) &&& (value' === inj UnitV) - ; fresh (id) (arg === inj (LValue id)) (mem_get state id value') + [ (arg === RValue) (value' === UnitV) + ; (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' = - fresh (env_ mem_ assignments_) (* TODO: replace with real placeholder ? *) - (state === inj (env_, mem_, mem_len', assignments_)) + let st_mem_len state mem_len' = (state === (_, _, mem_len, _)) let st_add_arg state state_before id arg_tag arg state'' = conde - [ (arg_tag === inj Ref) &&& (arg === inj RValue) &&& (state'' === state) - (* TODO: error, TODO: allow later ?? *) - ; fresh (arg' value') - (arg_tag === inj Ref) - (arg === inj (LValue arg')) - (env_get state_before arg' value') - (env_add state id value' state'') - ; fresh (value' state' mem_len_dec') - (arg_tag === inj Value) + [ (arg_tag === Ref) (arg === RValue) (state'' === state) (* TODO: error *) (* TODO: allow later ?? *) + ; (fresh arg') (arg_tag === Ref) (arg === LValue arg') + (fresh value') (env_get state_before arg value') + (env_add state id value' state'') + ; (arg_tag === Value) + (fresh value' state' mem_len_dec') (arg_to_value state_before arg value') (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'') ] - 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' = - fresh (env mem mem' mem_len assignments) - (state === inj (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') *) - (state' === inj (env, mem', mem_len, Std.nil ())) + (fresh env mem mem' mem_len assignments) + (state === (env, mem, mem_len, assignments)) + (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') === (env, mem', mem_len, []) (* --- *) - let arg_to_lvalue arg arg' = (arg' === inj (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 arg_to_lvalue arg arg' = (arg' === LValue arg) let rec eval_stmt state prog stmt state' = conde - [ fresh (f_id args f args') - (stmt === inj (Call (f_id, args))) + [ (fresh f_id args) + (stmt === Call (f_id, args)) + (fresh f args') (list_nth prog f_id f) (List.mapo arg_to_lvalue args args') - (eval_fun state prog f args' state') - ; fresh (id) (stmt === inj (Read id)) (mem_check state id state') - ; fresh (id) (stmt === inj (Write id)) (mem_set state id (inj UnitV) state') + (eval_fun state prog f args') + ; (fresh id) (stmt === Read id) (mem_check state id 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' = - list_foldl (eval_body_folder prog) state body state' - (* (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body) *) - - 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')) + (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body) + (* TODO: replace with foldlo (or foldro ?) *) and eval_fun state prog decl args state' = - fresh (arg_tags body - env_before mem_before len_before assignments_before - state_clean - state_with_vars counter_ - state_evaled - state_spoiled - env_ mem_spoiled len assignments_ - mem_updated len_to_drop) - (decl === inj (arg_tags, body)) - (state === inj (env_before, mem_before, len_before, assignments_before)) - (state_clean === inj (Std.nil (), mem_before, len_before, Std.nil ())) - (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) + (fresh arg_tags body) + (fresh env_before mem_before len_before assignments_before) + (fresh state_clean) + (state_clean === ([], mem_before, len_before, [])) + (fresh state_with_vars) + (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) + (* TODO how, rewrite from scratch ??? *) + (* TODO: replace with foldlo (or foldro ?) ?? *) + (fresh state_evaled) + (eval_body state prog body state_evaled) + (fresh 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) - (list_drop len_to_drop mem_spoiled mem_updated) - (state' === inj (env_before, mem_updated, len_before, assignments_before)) + (List.drop len_to_drop mem mem_updated) + (state' === (env_before, mem_updated, len_before, assignments_before)) and eval_fun_empty_args state prog decl state' = - fresh (arg_tags args hole_) (* TODO: replace with real placeholder *) - (decl === inj (arg_tags, hole_)) - (List.mapo arg_to_rvalue arg_tags args) + (fresh arg_tags) + (decl === (arg_tags, _)) + (List.mapo arg_to_rvalue arg_tags args) (* TODO how, rewrite from scratch ??? *) (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' = - fresh (prog main_decl state) - (all_prog === inj (prog, main_decl)) - (empty_state state) - (eval_fun_empty_args state prog main_decl state') + (fresh prog main_decl) + (all_prog == (prog, main_decl)) + (eval_fun_empty_args empty_state prog main_decl state') end