Begin testing statics using anntoations to represent inferred types

src/haz3lcore/lang/term/Annotated.re

@@ -2,7 +2,7 @@
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t('term, 'a) = {
-  [@show.opaque]
+  // [@show.opaque]
   annotation: 'a,
   term: 'term,
 };
@@ -36,3 +36,9 @@ let new_ids =
     copied,
   },
 };
+
+let map_annotation = (f, {term, annotation}: t('term, 'a)) => {
+  {term, annotation: f(annotation)};
+};
+
+let unannotated = term => {term, annotation: ()};

src/haz3lcore/statics/TermBase.re

@@ -179,6 +179,8 @@ and Exp: {
     | Cast(t('a), Typ.t('a), Typ.t('a)) // first Typ.t field is only meaningful in dynamic expressions
   and t('a) = Annotated.t(term('a), 'a);
 
+  let map_annotation: ('b => 'c, t('b)) => t('c);
+
   let map_term:
     (
       ~f_exp: (Exp.t('a) => Exp.t('a), Exp.t('a)) => Exp.t('a)=?,
@@ -246,6 +248,20 @@ and Exp: {
     | Cast(t('a), Typ.t('a), Typ.t('a)) // first Typ.t field is only meaningful in dynamic expressions
   and t('a) = Annotated.t(term('a), 'a);
 
+  let map_annotation: 'a 'b. ('a => 'b, t('a)) => t('b) =
+    (f, {term, annotation}) => {
+      {
+        term:
+          switch (term) {
+          | Invalid(str) => Invalid(str)
+          | EmptyHole => EmptyHole
+          | Int(i) => Int(i)
+          | Bool(b) => Bool(b)
+          | _ => raise(NotYetImplemented("Exp"))
+          },
+        annotation: f(annotation),
+      };
+    };
   let map_term =
       (
         ~f_exp=continue,
@@ -471,7 +487,7 @@ and Pat: {
     | Ap(t('a), t('a))
     | Cast(t('a), Typ.t('a), Typ.t('a)) // The second Typ.t field is only meaningful in dynamic patterns
   and t('a) = Annotated.t(term('a), 'a);
-
+  let map_annotation: ('b => 'c, t('b)) => t('c);
   let map_term:
     (
       ~f_exp: (Exp.t('a) => Exp.t('a), Exp.t('a)) => Exp.t('a)=?,
@@ -505,6 +521,24 @@ and Pat: {
     | Ap(t('a), t('a))
     | Cast(t('a), Typ.t('a), Typ.t('a)) // The second one is hidden from the user
   and t('a) = Annotated.t(term('a), 'a);
+  let map_annotation: 'a 'b. ('a => 'b, t('a)) => t('b) =
+    (f, {term, annotation}) => {
+      {
+        term:
+          switch (term) {
+          | Invalid(s) => Invalid(s)
+          | EmptyHole => EmptyHole
+          | Wild => Wild
+          | Int(i) => Int(i)
+          | Float(f) => Float(f)
+          | Bool(b) => Bool(b)
+          | String(s) => String(s)
+          | Var(v) => Var(v)
+          | _ => raise(NotYetImplemented("Pat"))
+          },
+        annotation: f(annotation),
+      };
+    };
 
   let map_term =
       (
@@ -627,7 +661,7 @@ and Typ: {
   and t('a) = Annotated.t(term('a), 'a);
 
   type sum_map('a) = ConstructorMap.t(t('a));
-
+  let map_annotation: ('b => 'c, t('b)) => t('c);
   let map_term:
     (
       ~f_exp: (Exp.t('a) => Exp.t('a), Exp.t('a)) => Exp.t('a)=?,
@@ -679,7 +713,20 @@ and Typ: {
   and t('a) = Annotated.t(term('a), 'a);
 
   type sum_map('a) = ConstructorMap.t(t('a));
-
+  let map_annotation: 'b 'c. ('b => 'c, t('b)) => t('c) =
+    (f, {term, annotation}) => {
+      {
+        term:
+          switch (term) {
+          | Int => Int
+          | Float => Float
+          | Bool => Bool
+          | String => String
+          | _ => raise(NotYetImplemented("Typ"))
+          },
+        annotation: f(annotation),
+      };
+    };
   let map_term =
       (
         ~f_exp=continue,

src/util/Util.re

@@ -23,3 +23,4 @@ module Point = Point;
 // Used by [@deriving sexp, yojson)]
 include Sexplib.Std;
 include Ppx_yojson_conv_lib.Yojson_conv.Primitives;
+exception NotYetImplemented(string);

test/Test_Statics.re

@@ -0,0 +1,94 @@
+open Alcotest;
+open Haz3lcore;
+
+// /*Create a testable type for dhexp which requires
+//   an equal function (dhexp_eq) and a print function (dhexp_print) */
+let statics_map =
+  testable(
+    Fmt.using([%derive.show: UExp.t(Typ.t(unit))], Fmt.string),
+    (==),
+  );
+
+let ids = List.init(12, _ => Id.mk());
+let id_at = x => x |> List.nth(ids);
+
+let typ = (typ: Typ.term(unit)): Typ.t(unit) => {
+  term: typ,
+  annotation: (),
+};
+
+let get_statics = exp =>
+  Statics.uexp_to_info_map(~ctx=[], ~ancestors=[], exp, Id.Map.empty) |> snd;
+
+let sample_int: Exp.t(IdTag.t) = {
+  term: Int(9),
+  annotation: {
+    ids: [id_at(0)],
+    copied: false,
+  },
+};
+// Take the statics map and the expression tagged with id and interleave statics throughout the annotations
+let run_statics = exp => {
+  let static_map = get_statics(exp);
+  let traverse = (exp: UExp.t(IdTag.t)): Exp.t(Typ.t(unit)) => {
+    let baz: Exp.t(Typ.t(unit)) =
+      Exp.map_annotation(
+        (idtag: IdTag.t) => {
+          let bar = List.hd(idtag.ids);
+          let foo = Id.Map.find(bar, static_map);
+          switch (foo) {
+          | InfoExp(e) => Typ.map_annotation((_: IdTag.t) => (), e.ty)
+          | _ => raise(Util.NotYetImplemented("Extract type from info"))
+          };
+        },
+        exp,
+      );
+    baz;
+  };
+  traverse(exp);
+};
+
+let single_integer = () => {
+  let expected: UExp.t(Typ.t(unit)) = {
+    term: Int(9),
+    annotation: {
+      term: Int,
+      annotation: (),
+    },
+  };
+  let actual =
+    run_statics({
+      term: Int(9),
+      annotation: {
+        ids: [id_at(0)],
+        copied: false,
+      },
+    });
+  Alcotest.check(statics_map, "foo", expected, actual);
+};
+let boolean = () => {
+  let expected: UExp.t(Typ.t(unit)) = {
+    term: Bool(false),
+    annotation: {
+      term: Bool,
+      annotation: (),
+    },
+  };
+  let actual =
+    run_statics({
+      term: Bool(false),
+      annotation: {
+        ids: [id_at(0)],
+        copied: false,
+      },
+    });
+  Alcotest.check(statics_map, "ascribed with boolean", expected, actual);
+};
+
+let tests = (
+  "Statics",
+  [
+    test_case("Single integer", `Quick, single_integer),
+    test_case("Boolean", `Quick, boolean),
+  ],
+);

test/haz3ltest.re

@@ -4,6 +4,9 @@ let (suite, _) =
   run_and_report(
     ~and_exit=false,
     "Dynamics",
-    [("Elaboration", Test_Elaboration.elaboration_tests)],
+    [
+      ("Elaboration", Test_Elaboration.elaboration_tests),
+      Test_Statics.tests,
+    ],
   );
 Junit.to_file(Junit.make([suite]), "junit_tests.xml");