st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: fixes, first (empty) synthesizer test

Browse source
This commit is contained in:
ProgramSnail 2026-05-06 16:57:14 +00:00
parent 781fdbafd2
commit a130ffe819
3 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
model_with_structures/synthesizer.ml
View file

@ -167,7 +167,7 @@ struct
[%%ocanren_inject [%%ocanren_inject
type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type ground = ((Nat.ground List.ground * Stmt.ground) List.ground, Nat.ground, ground List.ground) t type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
] ]
end end
@ -814,8 +814,8 @@ struct
s == CallS (f, es) & s == CallS (f, es) &
pathvalo mem vals f v & pathvalo mem vals f v &
pathtypeo types f tp & pathtypeo types f tp &
types' == TypesEnv [] & types' == TypesEnv [] & (* TODO: FIXME add globals *)
vals' == ValsEnv [] & vals' == ValsEnv [] & (* TODO: FIXME add globals *)
v == FunV fstmts & v == FunV fstmts &
tp == FunT tps & tp == FunT tps &
st' == StEnv (mem, types', vals') & st' == StEnv (mem, types', vals') &
@ -867,9 +867,12 @@ struct
let prog_evalo prog st' = let prog_evalo prog st' =
let open Prg in let open Prg in
let open Stmt in
ocanren { ocanren {
fresh decls, s, init_st in fresh decls, s, init_st in
prog == Prg (decls, s) & prog == Prg (decls, s) &
decls == [] &
s == SkipS &
prog_inito prog init_st & prog_inito prog init_st &
stmt_evalo init_st s st' stmt_evalo init_st s st'
} }

2
model_with_structures/tests.ml
View file

@ -2,6 +2,8 @@ open Tests_f
open Synthesizer open Synthesizer
open Relational open Relational
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([]), ValsEnv ([]))] |}]
(* type tests *) (* type tests *)
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *) (* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)

12
model_with_structures/tests_f.ml
View file

@ -4,7 +4,17 @@ open GT
open OCanren open OCanren
open OCanren.Std open OCanren.Std
(* @type answer = St.ground GT.list with show *) @type answer = StEnv.ground GT.list with show
let prog_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Prg in
let open Stmt in
ocanren {
fresh prog in
prog == Prg ([], SkipS) &
prog_evalo prog q})
(fun q -> q#reify (StEnv.prj_exn))))
(* @type answerArgs = (Arg.ground List.ground) GT.list with show *) (* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
(* @type answerValue = Value.ground GT.list with show *) (* @type answerValue = Value.ground GT.list with show *)
(* @type answerNat = Nat.ground GT.list with show *) (* @type answerNat = Nat.ground GT.list with show *)