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:22901cdc22d736fa07bd06e6fb555caa5d9ffab7
Branches Tags
st:main
..
compare: st:f8b89966fb4752c9bb47622f49bb08a152a7f7f0
Branches Tags
st:main

No commits in common. "22901cdc22d736fa07bd06e6fb555caa5d9ffab7" and "f8b89966fb4752c9bb47622f49bb08a152a7f7f0" have entirely different histories.
22901cdc22 ... f8b89966fb

2 changed files with 53 additions and 106 deletions
Download patch file Download diff file Expand all files Collapse all files

9
lib/dune
View file

@ -30,18 +30,17 @@
(inline_tests) (inline_tests)
(wrapped false) (wrapped false)
(preprocess (preprocess
(pps (pps
OCanren-ppx.ppx_repr OCanren-ppx.ppx_repr
OCanren-ppx.ppx_distrib
OCanren-ppx.ppx_deriving_reify OCanren-ppx.ppx_deriving_reify
OCanren-ppx.ppx_fresh OCanren-ppx.ppx_fresh
ppx_expect ppx_expect
ppx_inline_test ppx_inline_test
GT.ppx
GT.ppx_all
OCanren-ppx.ppx_distrib
-- --
-pp -pp
lib/pp5+gt+plugins+ocanren+dump.exe))) lib/pp5+gt+plugins+ocanren+dump.exe)
))
(rule (rule
(targets pp5+gt+plugins+ocanren+dump.exe) (targets pp5+gt+plugins+ocanren+dump.exe)

150
lib/relational_semantic_interpreter.ml
View file

@ -6,92 +6,50 @@ struct
open OCanren open OCanren
open OCanren.Std open OCanren.Std
type data_ground = Nat.ground (* with show, gmap *) @type data_ground = Nat.ground with show, gmap
[@@deriving gt ~options:{ show; gmap }] @type data_logic = Nat.logic with show, gmap
type data_logic = Nat.logic
[@@deriving gt ~options:{ show; gmap }]
type data_injected = Nat.injected type data_injected = Nat.injected
module Tag = struct @type tag_ground = Ref | Value with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type tag_logic = tag_ground logic with show, gmap
[%%distrib type tag_injected = tag_ground ilogic
type nonrec t = Ref | Value
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module Stmt = struct @type ('d, 'dl) stmt_abs = Call of 'd * 'dl | Read of 'd | Write of 'd with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type stmt_ground = (data_ground, data_ground List.ground) stmt_abs with show, gmap
[%%distrib @type stmt_logic = (data_logic, data_logic List.logic) stmt_abs logic with show, gmap
type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd type stmt_injected = (data_injected, data_injected List.injected) stmt_abs ilogic
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Nat.ground, Nat.ground List.ground) t
]
end
module Body = struct @type body_ground = stmt_ground List.ground with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type body_logic = stmt_logic List.logic with show, gmap
[%%distrib type body_injected = stmt_injected List.injected
type nonrec ('stmt, 'l) t = Body of ('stmt, 'l) List.t
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Stmt.ground, Stmt.ground List.ground) t
]
end
module FunDecl = struct @type fun_decl_ground = tag_ground List.ground * body_ground with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type fun_decl_logic = (tag_logic List.logic * body_logic) logic with show, gmap
[%%distrib type fun_decl_injected = (tag_injected List.injected * body_injected) ilogic
type nonrec ('tag, 'lt, 'stmt, 'ls) t = FunDecl of ('tag, 'lt) List.t * ('stmt, 'ls) Body.t
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Tag.ground, Tag.ground List.ground, Stmt.ground, Stmt.ground List.ground) t
]
end
module Prog = struct @type prog_ground = fun_decl_ground List.ground * fun_decl_ground with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type prog_logic = (fun_decl_logic List.logic * fun_decl_logic) logic with show, gmap
[%%distrib type prog_injected = (fun_decl_injected List.injected * fun_decl_injected) ilogic
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 }]
type nonrec ground = (FunDecl.ground, FunDecl.ground List.ground, Tag.ground, Tag.ground List.ground, Stmt.ground, Stmt.ground List.ground) t
]
end
module Arg = struct @type 'd arg_abs = RValue | LValue of 'd with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type arg_ground = data_ground arg_abs with show, gmap
[%%distrib @type arg_logic = data_logic arg_abs logic with show, gmap
type nonrec 'd t = RValue | LValue of 'd type arg_injected = data_injected arg_abs ilogic
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = Nat.ground t
]
end
module Value = struct @type value_ground = UnitV | BotV with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type value_logic = value_ground logic with show, gmap
[%%distrib type value_injected = value_ground ilogic
type nonrec t = Unit | Bot
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module Envr = struct @type env_ground = (data_ground * data_ground) List.ground with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type env_logic = (data_logic * data_logic) List.logic with show, gmap
[%%distrib type env_injected = (data_injected * data_injected) List.injected ilogic
type nonrec ('d, 'l) t = Envr of ('d * 'd, 'l) List.t
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Nat.ground, Nat.ground List.ground) t
]
end
module State = struct @type ('env, 'mem, 'last_mem, 'assignments) state_abs = 'env * 'mem * 'last_mem * 'assignments with show, gmap
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] @type state_ground = (env_ground, value_ground List.ground, data_ground, data_ground List.ground) state_abs with show, gmap
[%%distrib @type state_logic = (env_logic, value_logic List.logic, data_logic, data_logic List.logic) state_abs logic with show, gmap
type nonrec ('env, 'mem, 'last_mem, 'assignments) t = State of 'env * 'mem * 'last_mem * 'assignments type state_injected = (env_injected, value_injected List.injected, data_injected, data_injected List.injected) state_abs ilogic
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Envr.ground, Value.ground List.ground, Nat.ground, Nat.ground List.ground) t (* ocanren type 'a lst = Nil | Cons of 'a * 'a lst *)
]
end
let rec list_replace xs id value ys = let rec list_replace xs id value ys =
conde conde
@ -112,7 +70,7 @@ struct
(a === a') (a === a')
(v' === b') (v' === b')
] ]
(* TODO: difference from List.assoco ?? *) (* TODO: dofference from List.assoco ?? *)
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)
@ -164,8 +122,8 @@ struct
let mem_check state id state' = let mem_check state id state' =
conde conde
[ (mem_get state id (inj Value.Bot)) &&& (state' === state) (* TODO: error *) [ (mem_get state id (inj BotV)) &&& (state' === state) (* TODO: error *)
; (mem_get state id (inj Value.Unit)) &&& (state' === state) ; (mem_get state id (inj UnitV)) &&& (state' === state)
] ]
(* --- *) (* --- *)
@ -202,11 +160,11 @@ struct
let arg_to_value state arg value' = let arg_to_value state arg value' =
conde conde
[ (arg === inj Arg.RValue) &&& (value' === inj Value.Unit) [ (arg === inj RValue) &&& (value' === inj UnitV)
; fresh (id) (arg === inj (Arg.LValue id)) (mem_get state id value') ; fresh (id) (arg === inj (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 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 ? *)
@ -214,15 +172,15 @@ struct
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 Tag.Ref) &&& (arg === inj Arg.RValue) &&& (state'' === state) [ (arg_tag === inj Ref) &&& (arg === inj RValue) &&& (state'' === state)
(* TODO: error, TODO: allow later ?? *) (* TODO: error, TODO: allow later ?? *)
; fresh (arg' value') ; fresh (arg' value')
(arg_tag === inj Tag.Ref) (arg_tag === inj Ref)
(arg === inj (Arg.LValue arg')) (arg === inj (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 === inj Tag.Value) (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')) (st_mem_len state (Nat.s mem_len_dec'))
@ -233,7 +191,7 @@ struct
fresh (mem_id' mem_id_inv') 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_id_inv')
(list_replace mem mem_id_inv' (inj Value.Bot) mem') (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)
@ -244,7 +202,7 @@ struct
(* --- *) (* --- *)
let arg_to_lvalue arg arg' = (arg' === inj (Arg.LValue arg)) let arg_to_lvalue arg arg' = (arg' === inj (LValue arg))
let rec list_drop n xs xs' = let rec list_drop n xs xs' =
conde conde
@ -256,12 +214,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 === inj (Stmt.Call (f_id, args))) (stmt === inj (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 === inj (Stmt.Read id)) (mem_check state id state') ; fresh (id) (stmt === inj (Read id)) (mem_check state id state')
; fresh (id) (stmt === inj (Stmt.Write id)) (mem_set state id (inj Value.Unit) state') ; fresh (id) (stmt === inj (Write id)) (mem_set state id (inj UnitV) 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'
@ -312,14 +270,4 @@ struct
(all_prog === inj (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')
(* let eval_prog_fwd all_prog = *)
(* run q (fun q -> eval_prog (inj_state all_prog) q) *)
(* (fun _ -> ()) *)
(* let%expect_test "empty" = *)
(* eval_prog_fwd ([], ([], [])); *)
(* Printf.printf "done!"; *)
(* [%expect {| done! |}] *)
end end