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:d4e7f7c02e0651fcedf1c85ea19e1198c367a41a
Branches Tags
st:main
..
compare: st:30f052b1b1e2a7a94ea625e97da768e225a06154
Branches Tags
st:main

No commits in common. "d4e7f7c02e0651fcedf1c85ea19e1198c367a41a" and "30f052b1b1e2a7a94ea625e97da768e225a06154" have entirely different histories.
d4e7f7c02e ... 30f052b1b1

5 changed files with 112 additions and 218 deletions
Download patch file Download diff file Expand all files Collapse all files

27
lib/dune
View file

@ -28,7 +28,7 @@
(:standard -rectypes)) (:standard -rectypes))
(libraries OCanren OCanren.tester) (libraries OCanren OCanren.tester)
(preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
; (inline_tests) (inline_tests)
(wrapped false) (wrapped false)
(preprocess (preprocess
(pps (pps
@ -52,7 +52,7 @@
(:standard -rectypes)) (:standard -rectypes))
(libraries OCanren OCanren.tester) (libraries OCanren OCanren.tester)
(preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe) (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
; (inline_tests) (inline_tests)
(wrapped false) (wrapped false)
(preprocess (preprocess
(pps (pps
@ -68,29 +68,6 @@
-pp -pp
lib/pp5+gt+plugins+ocanren+dump.exe))) lib/pp5+gt+plugins+ocanren+dump.exe)))
; (library
; (name test)
; (modules test)
; (flags
; (-dsource)
; (:standard -rectypes))
; (libraries OCanren OCanren.tester)
; (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
; (wrapped false)
; (preprocess
; (pps
; ppx_expect
; ppx_inline_test
; GT.ppx
; GT.ppx_all
; OCanren-ppx.ppx_repr
; OCanren-ppx.ppx_deriving_reify
; OCanren-ppx.ppx_fresh
; OCanren-ppx.ppx_distrib
; --
; -pp
; lib/pp5+gt+plugins+ocanren+dump.exe)))
(rule (rule
(targets pp5+gt+plugins+ocanren+dump.exe) (targets pp5+gt+plugins+ocanren+dump.exe)
(action (action

2
lib/relational_semantic_interpreter.ml
View file

@ -1,3 +1,5 @@
(* (,,) -< Pair.inj _ (Pair.inj _ _) *)
module Relational = module Relational =
struct struct
open GT open GT

268
lib/relational_semantic_interpreter_oc.ml
View file

@ -1,3 +1,5 @@
(* (,,) -< Pair.inj _ (Pair.inj _ _) *)
module Relational = module Relational =
struct struct
open GT open GT
@ -12,120 +14,107 @@ struct
module Tag = struct module Tag = 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"]
[%%ocanren_inject [%%distrib
type nonrec t = Ref | Value type nonrec t = Ref | Value
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t type nonrec ground = t
] ]
module Test = struct let ref = inj Ref
@type answer = logic GT.list with show let value = inj Value
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref})
(fun q -> q#reify reify)))
end
end end
module Stmt = struct module Stmt = 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"]
[%%ocanren_inject [%%distrib
type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd
[@@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
] ]
module Test = struct let call f args = inj (Call (f, args))
@type answer = Nat.ground List.ground GT.list with show let read id = inj (Read id)
@type answer' = ground GT.list with show let write id = inj (Write id)
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)})
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let _ = Printf.printf "%s\n" @@ show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
(fun q -> q#reify (prj_exn))))
end end
module Body = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%distrib
type nonrec ('stmt, 'l) t = T of ('stmt, 'l) List.t
[@@deriving gt ~options:{ show; gmap }]
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"]
[%%ocanren_inject [%%distrib
type nonrec ('l, 'b) t = FunDecl of 'l * 'b type nonrec ('l, 'b) t = T of 'l * 'b
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t type nonrec ground = (Tag.ground List.ground, Body.ground) t
] ]
module Test = struct let make args body = inj (T (args, body))
@type answer = ground GT.list with show
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Tag in
let open Stmt in
ocanren {FunDecl ([Ref; Value], [Call (1, [0]); Write 1]) == q})
(fun q -> q#reify (prj_exn))))
end
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"]
[%%ocanren_inject [%%distrib
type nonrec ('l, 'f) t = Prog of 'l * 'f type nonrec ('l, 'f) t = T of 'l * 'f
[@@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 List.ground, FunDecl.ground) t
] ]
module Test = struct let make decls main_decl = inj (T (decls, main_decl))
@type answer = ground GT.list with show
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open FunDecl in
let open Tag in
let open Stmt in
ocanren {Prog ([], FunDecl ([Value], [Write 0; Read 0])) == q})
(fun q -> q#reify (prj_exn))))
end
end end
module Arg = struct module Arg = 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"]
[%%ocanren_inject [%%distrib
type nonrec 'd t = RValue | LValue of 'd type nonrec 'd t = RValue | LValue of 'd
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = Nat.ground t type nonrec ground = Nat.ground t
] ]
module Test = struct let rvalue = inj RValue
@type answer = logic GT.list with show let lvalue x = inj (LValue x)
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3})
(fun q -> q#reify reify)))
end
end end
module Value = struct module Value = 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"]
[%%ocanren_inject [%%distrib
type nonrec t = Unit | Bot type nonrec t = Unit | Bot
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t type nonrec ground = t
] ]
module Test = struct let unit = inj Unit
@type answer = logic GT.list with show let bot = inj Bot
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit})
(fun q -> q#reify reify)))
end
end end
module St = struct (* module Envr = struct *)
(* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
(* [%%distrib *)
(* type nonrec ('d, 'l) t = T of ('d * 'd, 'l) List.t *)
(* [@@deriving gt ~options:{ show; gmap }] *)
(* type nonrec ground = (Nat.ground, Nat.ground List.ground) t *)
(* ] *)
(* let make elems = inj (T elems) *)
(* end *)
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"]
[%%ocanren_inject [%%distrib
type nonrec ('env, 'mem, 'last_mem, 'assignments) t = St of 'env * 'mem * 'last_mem * 'assignments type nonrec ('env, 'mem, 'last_mem, 'assignments) t = T 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 = (((Nat.ground, Nat.ground) Pair.ground) List.ground,
Value.ground List.ground, Nat.ground, Nat.ground List.ground) t Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
] ]
module Test = struct let make env mem last_mem assignments = inj (T (env, mem, last_mem, assignments))
@type answer = ground GT.list with show
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Value in
ocanren {St ([Std.pair 0 0], [Bot], 1, [0]) == q})
(fun q -> q#reify (prj_exn))))
end
end end
let rec list_replaceo xs id value ys = ocanren { let rec list_replaceo xs id value ys = ocanren {
@ -141,8 +130,7 @@ struct
list_replaceo xs' id' value ys' } list_replaceo xs' id' value ys' }
} }
let rec list_assoco a xs v' = let rec list_assoco a xs v' = ocanren {
ocanren {
fresh a', b', xs' in fresh a', b', xs' in
(Std.pair a' b') :: xs' == xs & (Std.pair a' b') :: xs' == xs &
{ a =/= a' & list_assoco a xs' v' | { a =/= a' & list_assoco a xs' v' |
@ -150,20 +138,16 @@ struct
} }
(* TODO: difference from List.assoco ?? *) (* TODO: difference from List.assoco ?? *)
let env_geto state id mem_id' = let env_geto state id mem_id' = ocanren {
let open St in
ocanren {
fresh env, mem, mem_len, assignments in fresh env, mem, mem_len, assignments in
state == St (env, mem, mem_len, assignments) & state == State.make env mem mem_len assignments &
list_assoco id env mem_id' list_assoco id env mem_id'
} }
let env_addo state id mem_id state' = let env_addo state id mem_id state' = ocanren {
let open St in
ocanren {
fresh env, env', mem, mem_len, assignments in fresh env, env', mem, mem_len, assignments in
state == St (env, mem, mem_len, assignments) & state == State.make env mem mem_len assignments &
state' == St (env', mem, mem_len, assignments) & state' == State.make env' mem mem_len assignments &
(Std.pair id mem_id) :: env == env' (Std.pair id mem_id) :: env == env'
} }
@ -188,43 +172,35 @@ struct
} }
(* TODO: use real holes *) (* TODO: use real holes *)
let mem_geto state id value' = let mem_geto state id value' = ocanren {
let open St in
ocanren {
fresh mem, mem_len, mem_id, mem_id_inv, _env, _assignments in fresh mem, mem_len, mem_id, mem_id_inv, _env, _assignments in
state == St (_env, mem, mem_len, _assignments) & state == State.make _env mem mem_len _assignments &
env_geto state id mem_id & env_geto state id mem_id &
inv_ido mem_len mem_id mem_id_inv & inv_ido mem_len mem_id mem_id_inv &
list_ntho mem mem_id_inv value' list_ntho mem mem_id_inv value'
} }
let mem_seto state id value state'= let mem_seto state id value state'= ocanren {
let open St in
ocanren {
fresh env, mem, mem_len, assignments, mem_id, inv_mem_id, mem', assignments' in fresh env, mem, mem_len, assignments, mem_id, inv_mem_id, mem', assignments' in
state == St (env, mem, mem_len, assignments) & state == State.make env mem mem_len assignments &
env_geto state id mem_id & env_geto state id mem_id &
inv_ido mem_len mem_id inv_mem_id & inv_ido mem_len mem_id inv_mem_id &
list_replaceo mem mem_id value mem' & list_replaceo mem mem_id value mem' &
assignments' == id :: assignments & assignments' == id :: assignments &
state' == St (env, mem', mem_len, assignments') state' == State.make env mem' mem_len assignments'
} }
let mem_addo state value state' = let mem_addo state value state' = ocanren {
let open St in
ocanren {
fresh env, mem, mem_len, mem_len', assignments, mem' in fresh env, mem, mem_len, mem_len', assignments, mem' in
state == St (env, mem, mem_len, assignments) & state == State.make env mem mem_len assignments &
mem' == value :: mem & mem' == value :: mem &
mem_len' == Nat.s mem_len & mem_len' == Nat.s mem_len &
state' == St (env, mem, mem_len', assignments) state' == State.make env mem mem_len' assignments
} }
let mem_checko state id state' = let mem_checko state id state' = ocanren {
let open Value in mem_geto state id Value.bot & state' == state |
ocanren { mem_geto state id Value.unit & state' == state
mem_geto state id Bot & state' == state |
mem_geto state id Unit & state' == state
} }
(* --- *) (* --- *)
@ -256,71 +232,56 @@ struct
f acc_upd x' y' acc' } f acc_upd x' y' acc' }
} }
let arg_to_valueo state arg value' = let arg_to_valueo state arg value' = ocanren {
let open Arg in arg == Arg.rvalue & value' == Value.unit |
let open Value in
ocanren {
arg == RValue & value' == Unit |
{ fresh id in { fresh id in
arg == LValue id & arg == Arg.lvalue id &
mem_geto state id value' } mem_geto state id value' }
} }
let arg_to_rvalueo _arg value' = let arg_to_rvalueo _arg value' = ocanren { value' == Arg.rvalue }
let open Arg in
ocanren { value' == RValue }
let st_mem_leno state mem_len' = let st_mem_leno state mem_len' = ocanren {
let open St in
ocanren {
fresh _env, _mem, _assignments in (* TODO: replace with real placeholder ? *) fresh _env, _mem, _assignments in (* TODO: replace with real placeholder ? *)
state == St (_env, _mem, mem_len', _assignments) state == State.make _env _mem mem_len' _assignments
} }
let st_add_argo state state_before id arg_tag arg state'' = let st_add_argo state state_before id arg_tag arg state'' = ocanren {
(* let open Nat in *)
let open Arg in
let open Tag in
ocanren {
(* arg_tag == Tag.ref & arg == Arg.rvalue & state'' == state | *) (* arg_tag == Tag.ref & arg == Arg.rvalue & state'' == state | *)
(* TODO: error, TODO: allow later ?? *) (* TODO: error, TODO: allow later ?? *)
{ fresh arg', value' in { fresh arg', value' in
arg_tag == Ref & arg_tag == Tag.ref &
arg == LValue arg' & arg == Arg.lvalue arg' &
env_geto state_before arg' value' & env_geto state_before arg' value' &
env_addo state id value' state'' } | env_addo state id value' state'' } |
{ fresh value', state', mem_len_dec' in { fresh value', state', mem_len_dec' in
arg_tag == Value & arg_tag == Tag.value &
arg_to_valueo state_before arg value' & arg_to_valueo state_before arg value' &
mem_addo state value' state' & mem_addo state value' state' &
st_mem_leno state (Nat.s mem_len_dec') & st_mem_leno state (Nat.s mem_len_dec') &
env_addo state' id mem_len_dec' state'' } env_addo state' id mem_len_dec' state'' }
} }
let st_spoil_foldero mem_len state mem id mem' = let st_spoil_foldero mem_len state mem id mem' = ocanren {
let open Value in
ocanren {
fresh mem_id', mem_id_inv' in fresh mem_id', mem_id_inv' in
env_geto state id mem_id' & env_geto state id mem_id' &
inv_ido mem_len mem_id' mem_id_inv' & inv_ido mem_len mem_id' mem_id_inv' &
list_replaceo mem mem_id_inv' Bot mem' list_replaceo mem mem_id_inv' Value.bot mem'
} }
let st_spoil_assignmentso state state' = let st_spoil_assignmentso state state' = ocanren {
let open St in
ocanren {
fresh env, mem, mem', mem_len, assignments, nil' in fresh env, mem, mem', mem_len, assignments, nil' in
state == St (env, mem, mem_len, assignments) & state == State.make env mem mem_len assignments &
list_foldlo (st_spoil_foldero mem_len state) mem assignments mem' & list_foldlo (st_spoil_foldero mem_len state) mem assignments mem' &
nil' == [] & nil' == [] &
state' == St (env, mem', mem_len, nil') state' == State.make env mem' mem_len nil'
} }
(* --- *) (* --- *)
let arg_to_lvalueo arg arg' = let arg_to_lvalueo arg arg' = ocanren {
let open Arg in arg' == Arg.lvalue arg
ocanren { arg' == LValue arg } }
let rec list_dropo n xs xs' = ocanren { let rec list_dropo n xs xs' = ocanren {
xs == [] & xs' == [] | xs == [] & xs' == [] |
@ -331,17 +292,14 @@ struct
list_dropo n' ys xs' } list_dropo n' ys xs' }
} }
let rec eval_stmto state prog stmt state' = let rec eval_stmto state prog stmt state' = ocanren {
let open Stmt in
let open Value in
ocanren {
{ fresh f_id, args, f, args' in { fresh f_id, args, f, args' in
stmt == Call (f_id, args) & stmt == Stmt.call f_id args &
list_ntho prog f_id f & list_ntho prog f_id f &
List.mapo arg_to_lvalueo args args' & List.mapo arg_to_lvalueo args args' &
eval_funo state prog f args' state' } | eval_funo state prog f args' state' } |
{ fresh id in stmt == Read id & mem_checko state id state' } | { fresh id in stmt == Stmt.read id & mem_checko state id state' } |
{ fresh id in stmt === Write id & mem_seto state id Unit state' } { fresh id in stmt === Stmt.write id & mem_seto state id Value.unit state' }
} }
and eval_body_foldero prog state stmt state' = and eval_body_foldero prog state stmt state' =
@ -352,19 +310,15 @@ struct
(* (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: other types on translation to ocanren ? *) (* TODO: other types on translation to ocanren ? *)
and add_arg_foldero state_before state_c arg_tag arg state_c' = and add_arg_foldero state_before state_c arg_tag arg state_c' = ocanren {
ocanren {
fresh state, id, state', id' in fresh state, id, state', id' in
state_c == Std.pair state id & state_c == (state, id) &
st_add_argo state state_before id arg_tag arg state' & st_add_argo state state_before id arg_tag arg state' &
id' == Nat.s id & id' == Nat.s id &
state_c' == Std.pair state' id' state_c' == (state', id')
} }
and eval_funo state prog decl args state' = and eval_funo state prog decl args state' = ocanren {
let open FunDecl in
let open St in
ocanren {
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,
@ -376,44 +330,38 @@ struct
nil_env, nil_assignments in nil_env, nil_assignments in
nil_env == [] & nil_env == [] &
nil_assignments == [] & nil_assignments == [] &
decl == FunDecl (arg_tags, body) & decl == FunDecl.make arg_tags body &
state == St (env_before, mem_before, len_before, assignments_before) & state == State.make env_before mem_before len_before assignments_before &
state_clean == St (nil_env, mem_before, len_before, nil_assignments) & state_clean == State.make nil_env mem_before len_before nil_assignments &
list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: replace with real placeholder *) list_foldl2o (add_arg_foldero state) (state, Nat.o) arg_tags args (state_with_vars, _counter) & (* TODO: replace with real placeholder *)
eval_bodyo state_with_vars prog body state_evaled & eval_bodyo state_with_vars prog body state_evaled &
st_spoil_assignmentso state_evaled state_spoiled & st_spoil_assignmentso state_evaled state_spoiled &
state_spoiled == St (_env, mem_spoiled, len, _assignments) & state_spoiled == State.make _env mem_spoiled len _assignments &
Nat.addo len_to_drop len_before len & Nat.addo len_to_drop len_before len &
list_dropo len_to_drop mem_spoiled mem_updated & list_dropo len_to_drop mem_spoiled mem_updated &
state' == St (env_before, mem_updated, len_before, assignments_before) state' == State.make env_before mem_updated len_before assignments_before
} }
and eval_fun_empty_argso state prog decl state' = and eval_fun_empty_argso state prog decl state' = ocanren {
let open FunDecl in fresh arg_tags, args, _hole in (* TODO: replace with real placeholder *)
ocanren { decl == FunDecl.make arg_tags _hole &
fresh arg_tags, args, _body in (* TODO: replace with real placeholder *)
decl == FunDecl (arg_tags, _body) &
List.mapo arg_to_rvalueo arg_tags args & List.mapo arg_to_rvalueo arg_tags args &
eval_funo state prog decl args state' eval_funo state prog decl args state'
} }
(* --- *) (* --- *)
let empty_stateo state = let empty_stateo state = ocanren {
let open St in
ocanren {
fresh nil_env, nil_mem, nil_assignments in fresh nil_env, nil_mem, nil_assignments in
nil_env == [] & nil_env == [] &
nil_assignments == [] & nil_assignments == [] &
nil_mem == [] & nil_mem == [] &
state == St (nil_env, nil_mem, Nat.o, nil_assignments) state == State.make nil_env nil_mem Nat.o nil_assignments
} }
let eval_progo all_prog state' = let eval_progo all_prog state' = ocanren {
let open Prog in
ocanren {
fresh prog, main_decl, state in fresh prog, main_decl, state in
all_prog == Prog (prog, main_decl) & all_prog == Prog.make prog main_decl &
empty_stateo state & empty_stateo state &
eval_fun_empty_argso state prog main_decl state' eval_fun_empty_argso state prog main_decl state'
} }
@ -428,20 +376,16 @@ struct
(* let empty_prog = Prog.T (List.Nil, FunDecl.T (List.Nil, Body.T List.Nil)) *) (* let empty_prog = Prog.T (List.Nil, FunDecl.T (List.Nil, Body.T List.Nil)) *)
(* let empty_prog'' = ocanren { T ([], T ([], T [])) } *) (* let empty_prog'' = ocanren { T ([], T ([], T [])) } *)
(* let empty_prog = *) (* let empty_prog = ocanren { Prog.make [] (FunDecl.make [] (Body.make [])) } *)
(* let open FunDecl in *)
(* let open Prog in *)
(* ocanren { Prog ([], FunDecl ([], [])) } *)
(* let empty_prog = Prog.make (Std.nil ()) (FunDecl.make (Std.nil ()) (Body.make (Std.nil ()))) *) (* let empty_prog = Prog.make (Std.nil ()) (FunDecl.make (Std.nil ()) (Body.make (Std.nil ()))) *)
let eval_test () = let eval_test =
Stream.hd @@ Stream.hd @@
run q (fun q -> ocanren { list_assoco 0 [(0, 0)] q }) run q (fun q -> ocanren { list_assoco 0 [(0, 0)] q })
(fun qs -> qs#reify Nat.prj_exn) (fun qs -> qs#reify Nat.prj_exn)
(* TODO: launch tests *)
let%expect_test "empty" = let%expect_test "empty" =
let x = eval_test () in let x = eval_test in
Printf.printf "done! %s" ((show (Nat.ground)) x); Printf.printf "done! %s" ((show (Nat.ground)) x);
[%expect {| done! 0 |}] [%expect {| done! 0 |}]

6
lib/semantic_interpreter.ml
View file

@ -1,3 +1,5 @@
(* (,,) -< Pair.inj _ (Pair.inj _ _) *)
module Functional = module Functional =
struct struct
@ -78,8 +80,6 @@ struct
(* TODO: use env var ids instead of mem_ids ?? *) (* TODO: use env var ids instead of mem_ids ?? *)
(env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, []) (env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, [])
let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
let rec eval_stmt state prog stmt = let rec eval_stmt state prog stmt =
match stmt with match stmt with
| Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args) | Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args)
@ -97,7 +97,7 @@ struct
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
match state with (_env, mem, len, _assignments) -> match state with (_env, mem, len, _assignments) ->
(env_before, list_drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *) (env_before, List.drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *)
and eval_fun_empty_args state prog decl = and eval_fun_empty_args state prog decl =
match decl with (arg_tags, _) -> match decl with (arg_tags, _) ->

29
lib/test.ml
View file

@ -1,29 +0,0 @@
open GT
open OCanren
module Tag = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
ocanren type tag = Ref | Value
module Test = struct
@type answer = logic GT.list with show
let _ =
Printf.printf "%s" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q === Ref})
(fun q -> q#reify reify)))
end
end
module Stmt = struct
ocanren type ('d, 'dl) stmt = Call of 'd * 'dl | Read of 'd | Write of 'd
module Test = struct
@type answer1 = Nat.ground List.ground GT.list with show
@type answer = (Nat.ground, Nat.ground List.ground) ground GT.list with show
let _ = Printf.printf "%s\n" @@ show(answer1) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) === Call (1, q)})
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) === q})
(fun q -> q#reify (prj_exn Nat.prj_exn (List.prj_exn Nat.prj_exn)))))
end
end