mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-03-12 02:57:09 +00:00
ocanren type syntax test file, migration to 4.14.2 (with pinned ocanren from repo)
This commit is contained in:
parent
30f052b1b1
commit
e2dcf6c2a1
3 changed files with 44 additions and 3 deletions
27
lib/dune
27
lib/dune
|
|
@ -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,6 +68,29 @@
|
||||||
-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
|
||||||
|
|
|
||||||
|
|
@ -80,6 +80,8 @@ 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 +99,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, _) ->
|
||||||
|
|
|
||||||
16
lib/test.ml
Normal file
16
lib/test.ml
Normal file
|
|
@ -0,0 +1,16 @@
|
||||||
|
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
|
||||||
Loading…
Add table
Add a link
Reference in a new issue