struct: init synthesizer rewrite

model_with_structures/analyzer.ml

@@ -27,7 +27,8 @@ struct
 
   type expr = UnitE
             | PathE of path
-            (* | RefE *)
+            (* TODO: extend to include arbitrary path *)
+            | RefE of data
             | TupleE of expr list
 
   type stmt = SkipS
@@ -96,11 +97,11 @@ struct
     (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
   (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
     (* ((id, v) :: fst mem, snd mem) *)
-  let mem_get (mem : mem) (id : memid) : value = List.nth (fst mem) id
+  let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *) List.nth (fst mem) (snd mem - id - 1)
   let mem_add (mem : mem) (v : value) : mem * memid =
     ((v :: fst mem, snd mem + 1), snd mem)
   let mem_set (mem : mem) (id : memid) (v : value) : mem =
-    (list_replace (fst mem) id v, snd mem)
+    (list_replace (fst mem) (snd mem - id - 1) v, snd mem)
 
   let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
     | ZeroV -> ZeroDV
@@ -130,7 +131,12 @@ struct
                            | _ -> raise @@ Typing_error "pathtype: access"
 
   let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
-    | VarP x -> mem_get mem @@ List.assoc x vals
+    | VarP x -> mem_get mem @@ ((* Printf.printf "%i: " x; (* FIXME TMP *)
+                                ignore @@ List.map (fun (x, _) -> Printf.printf "%i " x) vals;
+                                Printf.printf "mem size: %i, " (List.length (fst mem));
+                                Printf.printf "mem size stored: %i " (snd mem);
+                                Printf.printf "\n"; *)
+                                List.assoc x vals)
     | DerefP p -> (match pathval mem vals p with
                     | RefV id -> mem_get mem id
                     | _ -> raise @@ Typing_error "pathval: deref")
@@ -197,6 +203,7 @@ struct
   let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
     | UnitE -> ZeroV
     | PathE p -> pathval mem vals p
+    | RefE x -> RefV (List.assoc x vals)
     | TupleE es -> TupleV (List.map (exprval mem vals) es)
 
   (* - expression typing *)
@@ -204,6 +211,7 @@ struct
   let rec exprtype (types : types) (e : expr) : atype = match e with
     | UnitE -> UnitT (Rd, NeverWr)
     | PathE p -> pathtype types p
+    | RefE x -> RefT (Rf, List.assoc x types)
     | TupleE es -> TupleT (List.map (exprtype types) es)
 
   (* - context initialization *)
@@ -220,7 +228,8 @@ struct
     | 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), [], [])
+  let empty_mem : mem = ([], 0)
+  let empty_state : state = (empty_mem, [], [])
 
   (* TODO: better way ??? *)
   let globals_min_id : data = 1000
@@ -237,11 +246,18 @@ struct
   let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
                       (r' : read_cap) (w' : write_cap) (m : mode)
                       (c : copy_cap) : bool =
+    (* FIXME TMP
+    Printf.printf "%b %b %b %b %b\n"
+      (r != Rd || v == ZeroV)
+      (r != Rd || fst m == In)
+      (snd m != Out || w == AlwaysWr)
+      (((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
+      (is_trivial_v v); *)
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
     (* TODO: check *)
-    ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
+    ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
     is_trivial_v v
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
@@ -291,13 +307,13 @@ struct
 
   (* - funciton argument addition *)
 
-  let addarg (state : state) (x : data) (t : atype) (e : expr) : state =
+  let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
     match state with (mem, types, vals) ->
-    let v = exprval mem vals e in
+    let v = exprval mem oldvals e in
     (* let t' = pathtype types p in *)
     let (mem', v') = valcopy mem v t in
     let (mem'', id) = mem_add mem' v in
-    (mem', (x, t) :: types, (x, id) :: vals)
+    (mem'', (x, t) :: types, (x, id) :: vals)
 
   (* - function evaluation *)
 
@@ -310,23 +326,25 @@ struct
     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
+    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in
+                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in
                        let types' : types = [] in
                        let vals' : vals = [] in
                        (match v, t with
                           | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                             (* TODO: memoisation of the called functions *)
-                            let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *)
-                              (fun (st, x) (m, t) p -> (addarg st x t p, x + 1))
+                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *)
+                              (fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1))
                               ((mem, types', vals'), 0) ts es in
                             (* NOTE: same x's, so can use same args for all the statements *)
-                            let _states_evaled = List.map (stmt_eval state_with_args) fstmts in
-                            let mem_spoiled = List.fold_left2
+                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in
+                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2
                               (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
                               mem ts es in
                             (mem_spoiled, types, vals)
-                          | _, _ -> raise @@ Eval_error "call: function")
+                          | FunV _, _ -> raise @@ Eval_error "call: function type"
+                          | _, FunT _ -> raise @@ Eval_error "call: function val"
+                          | _, _ -> raise @@ Eval_error "call: function type & val")
     | WriteS p -> (match pathtype types p with
                      | UnitT (_, w) ->
                        if w == NeverWr
@@ -361,7 +379,59 @@ struct
 
   (* --- tests --- *)
 
-  (* - tests without functions *)
+  (* - shortcuts *)
+
+  let ( #. ) x y = SeqS (x, y)
+
+  let vx = VarP 0
+  let vy = VarP 1
+  let vz = VarP 2
+
+  let vgx = VarP (globals_min_id)
+  let vgy = VarP (globals_min_id + 1)
+  let vgz = VarP (globals_min_id + 2)
+
+  let drf p = DerefP p
+  let access p i = AccessP (p, i)
+
+  let wr x = ReadS x 
+  let rd x = WriteS x
+  let skp = SkipS
+
+  let uT_r_aw = UnitT (Rd, AlwaysWr)
+  let uT_r_mw = UnitT (Rd, MayWr)
+  let uT_aw = UnitT (NRd, AlwaysWr)
+  let uT_mw = UnitT (NRd, MayWr)
+  let uT_r = UnitT (Rd, NeverWr)
+  let uT = UnitT (NRd, NeverWr)
+
+  let rfT t = RefT (Rf, t)
+  let cpT t = RefT (Cp, t)
+
+  let moded t = ((In, NOut), t)
+
+  let defg t = VarD (t, UnitE)
+
+  (* - utils tests *)
+
+  let%expect_test "mem add / get / set" =
+    let mem = empty_mem in
+    let (mem, id1) = mem_add mem ZeroV in 
+    let (mem, id2) = mem_add mem SmthV in 
+    let (mem, id3) = mem_add mem BotV in 
+    Printf.printf "%i %i %i " id1 id2 id3;
+    Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
+                              (mem_get mem id2 == SmthV)
+                              (mem_get mem id3 == BotV);
+    let mem = mem_set mem id1 BotV in 
+    let mem = mem_set mem id2 ZeroV in 
+    let mem = mem_set mem id3 SmthV in 
+    Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
+                              (mem_get mem id2 == ZeroV)
+                              (mem_get mem id3 == SmthV);
+    [%expect {| 0 1 2 true true true true true true |}]
+
+  (* - basic var tests *)
 
   let%expect_test "empty" =
     prog_eval_noret ([], SkipS);
@@ -379,6 +449,49 @@ struct
     with Eval_error msg -> Printf.printf "%s" msg;
     [%expect {| read |}]
 
+  let%expect_test "simple vars, no read & read" =
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
+                      VarD (UnitT (Rd, MayWr), UnitE)],
+                     ReadS (VarP (globals_min_id + 1)));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple var, write" =
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple var, no write" =
+    try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id));
+         [%expect.unreachable]);
+    with Eval_error msg -> Printf.printf "%s" msg;
+    [%expect {| write: write tag |}]
+
+  let%expect_test "simple var, write & read" =
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id),
+                                                               ReadS (VarP globals_min_id)));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* - basic call tests *)
+
+  let%expect_test "simple call with read" =
+    prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
+                      FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
+                     CallS (VarP (globals_min_id + 1),
+                            [PathE (VarP globals_min_id)]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with write" =
+    prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
+                      VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
+                      FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
+                     CallS (VarP (globals_min_id + 2),
+                            [PathE (VarP (globals_min_id + 1))]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
   (* --- tests --- *)

model_with_structures/dune

@@ -42,23 +42,23 @@
 ;    -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)))

model_with_structures/model.typ

@@ -112,8 +112,9 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      // TODO: decide what is the result of ref expr eval
-      // Or[$rf expr$][reference expr] // `Ref`
+      // TODO FIXME: expand to support arbitrary paths (that do lead to lvalue)
+      // add relation to calc lvalue / rvalue for each element ?
+      Or[$rf X$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
   ),
@@ -652,7 +653,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value type],
+    name: [ unit expr value],
 
     $vals, mu texpre () eqmu 0$,
   )
@@ -661,32 +662,26 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ path type],
+    name: [ path expr value],
 
     $vals, mu tval p eqmu v$,
     $vals, mu texpre p eqmu v$,
   )
 ))
 
-// NOTE: tmp removed
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ unit value type],
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ ref expr value],
 
-//     $vals, mu texpre e : t$,
-
-//     [*TODO*],
-
-//     // TODO: reference to what ??
-//     $vals, mu texpre rf e eqmu rf ??$,
-//   )
-// ))
+    $vals, mu texpre rf x eqmu rf vals[x]$,
+  )
+))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value type],
+    name: [ tuple expr value],
 
     $vals, mu texpre e_1 eqmu v_1$,
     $...$,
@@ -704,7 +699,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value type],
+    name: [ unit value expr type],
 
     $types texprt () : cl Read, NotWrite cr$,
   )
@@ -713,29 +708,26 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ path type],
+    name: [ path expr type],
 
     $types ttype p : t$,
     $types texprt p : t$,
   )
 ))
 
-// NOTE: tmp removed
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ unit value type],
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ ref expr type],
 
-//     $types texprt e : t$,
-//     // TODO: why Ref mode ?? <- due to immutability ??
-//     $types texprt rf e : rf Ref t$,
-//   )
-// ))
+    $types texprt rf x : rf Ref types[x]$,
+  )
+))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value type],
+    name: [ tuple expr type],
 
     $types texprt e_1 : t_1$,
     $...$,
@@ -928,7 +920,21 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ full spoil for tuple expr],
 
-    $e = [e_1, ... e_n]$,
+    // NOTE: x as path
+    $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
+
+    // TODO:: is c important ?
+    $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ full spoil for tuple expr],
+
     $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
     $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,