From 1bacb6dfd77072ae74c1eb4fe7d05996c9d1e818 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 29 Apr 2026 15:12:45 +0000 Subject: [PATCH] structures: analyzer prog eval, some trivial tests --- model_with_structures/analyzer.ml | 49 ++++++++++++++-- model_with_structures/dune | 94 +++++++++++++++---------------- model_with_structures/model.typ | 20 ++++++- 3 files changed, 108 insertions(+), 55 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 548ceb5..006a42a 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -30,7 +30,8 @@ struct (* | RefE *) | TupleE of expr list - type stmt = CallS of path * expr list + type stmt = SkipS + | CallS of path * expr list | WriteS of path | ReadS of path | SeqS of stmt * stmt @@ -207,20 +208,27 @@ struct (* - context initialization *) + (* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with *) + + (* TODO: check new in vars *) let add_decl (state : state) (x : data) (d : decl) : state = match state with (mem, types, vals) -> match d with | VarD (t, e) -> let v = exprval mem vals e in - let (mem', id) = mem_add mem v in - (mem', (x, t) :: types, (x, id) :: vals) + let (mem', v') = valcopy mem v t in + let (mem'', id) = mem_add mem' v' in + (mem'', (x, t) :: types, (x, id) :: vals) | FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in (mem', (x, FunT ts) :: types, (x, id) :: vals) let empty_state : state = (([], 0), [], []) + (* TODO: better way ??? *) + let globals_min_id : data = 1000 + let prog_init (prog : prog) : state = match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *) (fun (st, x) d -> (add_decl st x d, x + 1)) - (empty_state, 0) + (empty_state, globals_min_id) decls (* - call values spoil *) @@ -301,6 +309,7 @@ struct let rec stmt_eval (state : state) (s : stmt) : state = match state with (mem, types, vals) -> match s with (* TODO: FIXME: Add memoisation *) + | SkipS -> state | CallS (f, es) -> let v = pathval mem vals f in let t = pathtype types f in let types' : types = [] in @@ -340,9 +349,39 @@ struct then raise @@ Eval_error "choice" else (memcomb meml memr, typesl, valsl) + (* --- program execution --- *) + + let prog_eval (prog : prog) : state = + match prog with (decls, s) -> + let init_state = prog_init prog in + stmt_eval init_state s + + let prog_eval_noret (prog : prog) : unit = + ignore @@ prog_eval prog + + (* --- tests --- *) + + (* - tests without functions *) + + let%expect_test "empty" = + prog_eval_noret ([], SkipS); + Printf.printf "done!"; + [%expect {| done! |}] + + let%expect_test "simple var" = + prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id)); + Printf.printf "done!"; + [%expect {| done! |}] + + let%expect_test "simple var, no read" = + try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id)); + [%expect.unreachable]); + with Eval_error msg -> Printf.printf "%s" msg; + [%expect {| read |}] + (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) - (* tests *) + (* --- tests --- *) (* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *) (* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *) diff --git a/model_with_structures/dune b/model_with_structures/dune index eae17b8..489258f 100644 --- a/model_with_structures/dune +++ b/model_with_structures/dune @@ -13,52 +13,52 @@ (preprocess (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test))) -(library - (name tests_st) - (modules tests) - (flags (-rectypes)) - (libraries synthesizer_st tests_f_st) - (inline_tests) - (wrapped false) - (preprocess - (pps ppx_expect ppx_inline_test))) +; (library +; (name tests_st) +; (modules tests) +; (flags (-rectypes)) +; (libraries synthesizer_st tests_f_st) +; (inline_tests) +; (wrapped false) +; (preprocess +; (pps ppx_expect ppx_inline_test))) -(library - (name tests_f_st) - (modules tests_f) - (flags (-rectypes)) - (libraries OCanren OCanren.tester synthesizer_st) - (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) - (wrapped false) - (preprocess - (pps - OCanren-ppx.ppx_repr - OCanren-ppx.ppx_deriving_reify - OCanren-ppx.ppx_fresh - GT.ppx - GT.ppx_all - OCanren-ppx.ppx_distrib - -- - -pp - camlp5/pp5+gt+plugins+ocanren+dump.exe))) +; (library +; (name tests_f_st) +; (modules tests_f) +; (flags (-rectypes)) +; (libraries OCanren OCanren.tester synthesizer_st) +; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) +; (wrapped false) +; (preprocess +; (pps +; OCanren-ppx.ppx_repr +; OCanren-ppx.ppx_deriving_reify +; OCanren-ppx.ppx_fresh +; GT.ppx +; GT.ppx_all +; OCanren-ppx.ppx_distrib +; -- +; -pp +; camlp5/pp5+gt+plugins+ocanren+dump.exe))) -(library - (name synthesizer_st) - (modules synthesizer) - (flags - ; (-dsource) - (:standard -rectypes)) - (libraries OCanren OCanren.tester) - (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) - (wrapped false) - (preprocess - (pps - OCanren-ppx.ppx_repr - OCanren-ppx.ppx_deriving_reify - OCanren-ppx.ppx_fresh - GT.ppx - GT.ppx_all - OCanren-ppx.ppx_distrib - -- - -pp - camlp5/pp5+gt+plugins+ocanren+dump.exe))) +; (library +; (name synthesizer_st) +; (modules synthesizer) +; (flags +; ; (-dsource) +; (:standard -rectypes)) +; (libraries OCanren OCanren.tester) +; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) +; (wrapped false) +; (preprocess +; (pps +; OCanren-ppx.ppx_repr +; OCanren-ppx.ppx_deriving_reify +; OCanren-ppx.ppx_fresh +; GT.ppx +; GT.ppx_all +; OCanren-ppx.ppx_distrib +; -- +; -pp +; camlp5/pp5+gt+plugins+ocanren+dump.exe))) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 76b2442..3742b24 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -120,6 +120,7 @@ Prod( `stmt`, { + Or[`SKIP`][do nothing] Or[`CALL` $path expr+$][call function] Or[`WRITE` $path$][write to variable] Or[`READ` $path$][read from variable] @@ -756,10 +757,10 @@ $s in stmt, f in X, x in X, a in X$ // expect well typed program $vals, mu texpre e eqmu v$, - // $types texprt e : t'$, - $mu xarrowSquiggly(v)_#[add] cl l, mu' cr$, + $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?) + $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, - $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu' cr$ + $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ ) )) @@ -994,6 +995,19 @@ $s in stmt, f in X, x in X, a in X$ === Statement Evaluation +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ SKIP], + + $cl types, vals, mu cr + xarrow("SKIP") + cl types, vals, mu cr$, + ) +)) + +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule(