module system

src/haz3lcore/dynamics/DH.re

@@ -13,6 +13,8 @@ module rec DHExp: {
     | BoundVar(Var.t)
     | Sequence(t, t)
     | Let(DHPat.t, t, t)
+    | Module(DHPat.t, t, t)
+    | Dot(t, t)
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
@@ -36,6 +38,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | ModuleVal(Environment.t)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -67,6 +70,8 @@ module rec DHExp: {
     | BoundVar(Var.t)
     | Sequence(t, t)
     | Let(DHPat.t, t, t)
+    | Module(DHPat.t, t, t)
+    | Dot(t, t)
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
@@ -90,6 +95,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | ModuleVal(Environment.t)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -105,6 +111,8 @@ module rec DHExp: {
     | BoundVar(_) => "BoundVar"
     | Sequence(_, _) => "Sequence"
     | Let(_, _, _) => "Let"
+    | Module(_, _, _) => "Module"
+    | Dot(_, _) => "DotMember"
     | FixF(_, _, _) => "FixF"
     | Fun(_, _, _, _) => "Fun"
     | Closure(_, _) => "Closure"
@@ -130,6 +138,7 @@ module rec DHExp: {
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
     | InvalidOperation(_) => "InvalidOperation"
+    | ModuleVal(_) => "ModuleVal"
     };
 
   let mk_tuple: list(t) => t =
@@ -161,6 +170,8 @@ module rec DHExp: {
     | NonEmptyHole(err, u, i, d) => NonEmptyHole(err, u, i, strip_casts(d))
     | Sequence(a, b) => Sequence(strip_casts(a), strip_casts(b))
     | Let(dp, b, c) => Let(dp, strip_casts(b), strip_casts(c))
+    | Module(dp, b, c) => Module(dp, strip_casts(b), strip_casts(c))
+    | Dot(a, b) => Dot(strip_casts(a), strip_casts(b))
     | FixF(a, b, c) => FixF(a, b, strip_casts(c))
     | Fun(a, b, c, d) => Fun(a, b, strip_casts(c), d)
     | Ap(a, b) => Ap(strip_casts(a), strip_casts(b))
@@ -191,6 +202,7 @@ module rec DHExp: {
     | FloatLit(_) as d
     | StringLit(_) as d
     | Constructor(_) as d
+    | ModuleVal(_) as d
     | InvalidOperation(_) as d => d
   and strip_casts_rule = (Rule(a, d)) => Rule(a, strip_casts(d));
 
@@ -212,6 +224,10 @@ module rec DHExp: {
       fast_equal(d11, d12) && fast_equal(d21, d22)
     | (Let(dp1, d11, d21), Let(dp2, d12, d22)) =>
       dp1 == dp2 && fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (Module(dp1, d11, d21), Module(dp2, d12, d22)) =>
+      dp1 == dp2 && fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (Dot(d11, d21), Dot(d12, d22)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22)
     | (FixF(f1, ty1, d1), FixF(f2, ty2, d2)) =>
       f1 == f2 && ty1 == ty2 && fast_equal(d1, d2)
     | (Fun(dp1, ty1, d1, s1), Fun(dp2, ty2, d2, s2)) =>
@@ -244,10 +260,13 @@ module rec DHExp: {
       fast_equal(d1, d2) && reason1 == reason2
     | (ConsistentCase(case1), ConsistentCase(case2)) =>
       fast_equal_case(case1, case2)
+    | (ModuleVal(mv1), ModuleVal(mv2)) => mv1 == mv2
     /* We can group these all into a `_ => false` clause; separating
        these so that we get exhaustiveness checking. */
     | (Sequence(_), _)
     | (Let(_), _)
+    | (Module(_), _)
+    | (Dot(_), _)
     | (FixF(_), _)
     | (Fun(_), _)
     | (Ap(_), _)
@@ -264,7 +283,8 @@ module rec DHExp: {
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)
-    | (ConsistentCase(_), _) => false
+    | (ConsistentCase(_), _)
+    | (ModuleVal(_), _) => false
 
     /* Hole forms: when checking environments, only check that
        environment ID's are equal, don't check structural equality.

src/haz3lcore/dynamics/Elaborator.re

@@ -72,6 +72,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | InconsistentBranches(_)
     | Sequence(_)
     | Let(_)
+    | Module(_)
     | FixF(_) => d
     /* Hole-like forms: Don't cast */
     | InvalidText(_)
@@ -86,6 +87,8 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | InvalidOperation(_) => d
     /* Normal cases: wrap */
     | BoundVar(_)
+    | Dot(_)
+    | ModuleVal(_)
     | Ap(_)
     | ApBuiltin(_)
     | Prj(_)
@@ -237,6 +240,51 @@ let rec dhexp_of_uexp =
                );
           Let(dp, FixF(self_id, ty_body, substituted_def), dbody);
         };
+      | Module(p, def, body) =>
+        let add_name: (option(string), DHExp.t) => DHExp.t = (
+          name =>
+            fun
+            | Fun(p, ty, e, _) => DHExp.Fun(p, ty, e, name)
+            | d => d
+        );
+        let* dp = dhpat_of_upat(m, p);
+        let* ddef = dhexp_of_uexp(m, def);
+        let* dbody = dhexp_of_uexp(m, body);
+        let+ ty_body = fixed_exp_typ(m, body);
+        switch (Term.UPat.get_recursive_bindings(p)) {
+        | None =>
+          /* not recursive */
+          DHExp.Module(dp, ddef, dbody)
+        | Some([f]) =>
+          /* simple recursion */
+          Module(dp, FixF(f, ty_body, add_name(Some(f), ddef)), dbody)
+        | Some(fs) =>
+          /* mutual recursion */
+          let ddef =
+            switch (ddef) {
+            | Tuple(a) =>
+              DHExp.Tuple(List.map2(s => add_name(Some(s)), fs, a))
+            | _ => ddef
+            };
+          let uniq_id = List.nth(def.ids, 0);
+          let self_id = "__mutual__" ++ string_of_int(uniq_id);
+          let self_var = DHExp.BoundVar(self_id);
+          let (_, substituted_def) =
+            fs
+            |> List.fold_left(
+                 ((i, ddef), f) => {
+                   let ddef =
+                     Substitution.subst_var(DHExp.Prj(self_var, i), f, ddef);
+                   (i + 1, ddef);
+                 },
+                 (0, ddef),
+               );
+          Module(dp, FixF(self_id, ty_body, substituted_def), dbody);
+        };
+      | Dot(e_mod, e_mem) =>
+        let* e_mod = dhexp_of_uexp(m, e_mod);
+        let+ e_mem = dhexp_of_uexp(m, e_mem);
+        DHExp.Dot(e_mod, e_mem);
       | Ap(fn, arg) =>
         let* c_fn = dhexp_of_uexp(m, fn);
         let+ c_arg = dhexp_of_uexp(m, arg);
@@ -331,6 +379,7 @@ and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
     | TypeAnn(p, _ty) =>
       let* dp = dhpat_of_upat(m, p);
       wrap(dp);
+    | TyAlias(_, _) => Some(DHPat.InvalidText(u, 0, ""))
     };
   | Some(InfoExp(_) | InfoTyp(_) | InfoTPat(_))
   | None => None

src/haz3lcore/dynamics/Evaluator.re

@@ -43,6 +43,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
+  | Module(_)
   | Var(_)
   | Rec(_)
   | Arrow(Unknown(_), Unknown(_))
@@ -62,6 +63,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
     sm |> ConstructorMap.is_ground(is_ground_arg) ? Ground : grounded_Sum(sm)
   | Arrow(_, _) => grounded_Arrow
   | List(_) => grounded_List
+  | Member(_, ty) => ground_cases_of(ty)
   };
 };
 
@@ -94,6 +96,10 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result =>
   | (Wild, _) => Matches(Environment.empty)
   | (ExpandingKeyword(_), _) => DoesNotMatch
   | (InvalidText(_), _) => IndetMatch
+  | (Var(_), ModuleVal(_)) => DoesNotMatch
+  | (Constructor(x), ModuleVal(_)) =>
+    let env = Environment.extend(Environment.empty, (x, d));
+    Matches(env);
   | (BadConstructor(_), _) => IndetMatch
   | (Var(x), _) =>
     let env = Environment.extend(Environment.empty, (x, d));
@@ -297,6 +303,7 @@ and matches_cast_Sum =
   | ExpandingKeyword(_)
   | InvalidText(_)
   | Let(_)
+  | Module(_)
   | Ap(_)
   | ApBuiltin(_)
   | BinBoolOp(_)
@@ -310,6 +317,8 @@ and matches_cast_Sum =
   | InvalidOperation(_) => IndetMatch
   | Cast(_)
   | BoundVar(_)
+  | Dot(_)
+  | ModuleVal(_)
   | FixF(_)
   | Fun(_)
   | BoolLit(_)
@@ -387,6 +396,8 @@ and matches_cast_Tuple =
   | InvalidText(_) => IndetMatch
   | ExpandingKeyword(_) => IndetMatch
   | Let(_, _, _) => IndetMatch
+  | Module(_, _, _) => IndetMatch
+  | Dot(_, _) => IndetMatch
   | FixF(_, _, _) => DoesNotMatch
   | Fun(_, _, _, _) => DoesNotMatch
   | Closure(_, Fun(_)) => DoesNotMatch
@@ -399,6 +410,7 @@ and matches_cast_Tuple =
   | BinStringOp(_)
   | BoolLit(_) => DoesNotMatch
   | IntLit(_) => DoesNotMatch
+  | ModuleVal(_) => DoesNotMatch
   | Sequence(_)
   | TestLit(_) => DoesNotMatch
   | FloatLit(_) => DoesNotMatch
@@ -524,6 +536,8 @@ and matches_cast_Cons =
   | InvalidText(_) => IndetMatch
   | ExpandingKeyword(_) => IndetMatch
   | Let(_, _, _) => IndetMatch
+  | Module(_, _, _) => IndetMatch
+  | Dot(_, _) => IndetMatch
   | FixF(_, _, _) => DoesNotMatch
   | Fun(_, _, _, _) => DoesNotMatch
   | Closure(_, d') => matches_cast_Cons(dp, d', elt_casts)
@@ -536,6 +550,7 @@ and matches_cast_Cons =
   | ListConcat(_)
   | BoolLit(_) => DoesNotMatch
   | IntLit(_) => DoesNotMatch
+  | ModuleVal(_) => DoesNotMatch
   | Sequence(_)
   | TestLit(_) => DoesNotMatch
   | FloatLit(_) => DoesNotMatch
@@ -624,7 +639,6 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
   (env, d) => {
     /* Increment number of evaluation steps (calls to `evaluate`). */
     let* () = take_step;
-
     switch (d) {
     | BoundVar(x) =>
       let d =
@@ -667,6 +681,42 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
         }
       };
 
+    | Module(dp, d1, d2) =>
+      let empty_env = Environment.empty;
+      let* r1 = module_evaluate(env, empty_env, d1);
+      switch (r1) {
+      | BoxedValue(d1)
+      | Indet(d1) =>
+        switch (matches(dp, d1)) {
+        | IndetMatch
+        | DoesNotMatch => Indet(Closure(env, Module(dp, d1, d2))) |> return
+        | Matches(env') =>
+          let* env = evaluate_extend_env(env', env);
+          evaluate(env, d2);
+        }
+      };
+
+    | Dot(d1, d2) =>
+      let* r1 = evaluate(env, d1);
+      switch (r1) {
+      | BoxedValue(ModuleVal(inner_env)) =>
+        let* inner_env =
+          inner_env |> ClosureEnvironment.of_environment |> with_eig;
+        let* r2 = evaluate(inner_env, d2);
+        switch (r2) {
+        | BoxedValue(_) => r2 |> return
+        | Indet(d2') => Indet(Dot(d1, d2')) |> return
+        };
+      | BoxedValue(d1') =>
+        print_endline("InvalidModule");
+        raise(EvaluatorError.Exception(InvalidBoxedFun(d1')));
+      | Indet(d1') =>
+        let* r2 = evaluate(env, d2);
+        switch (r2) {
+        | BoxedValue(d2')
+        | Indet(d2') => Indet(Dot(d1', d2')) |> return
+        };
+      };
     | FixF(f, _, d') =>
       let* env' = evaluate_extend_env(Environment.singleton((f, d)), env);
       evaluate(env', d');
@@ -677,7 +727,9 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
       let* r1 = evaluate(env, d1);
       switch (r1) {
       | BoxedValue(TestLit(id)) => evaluate_test(env, id, d2)
-      | BoxedValue(Constructor(_)) =>
+      // Now Constructors are also introduced by accessing from a module.
+      // So I'm using the evaluated result as d1 in final result.
+      | BoxedValue(Constructor(_) as d1) =>
         let* r2 = evaluate(env, d2);
         switch (r2) {
         | BoxedValue(d2) => BoxedValue(Ap(d1, d2)) |> return
@@ -725,7 +777,12 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
     | IntLit(_)
     | FloatLit(_)
     | StringLit(_)
-    | Constructor(_) => BoxedValue(d) |> return
+    | ModuleVal(_) => BoxedValue(d) |> return
+    | Constructor(x) =>
+      switch (ClosureEnvironment.lookup(env, x)) {
+      | None => return(BoxedValue(d))
+      | Some(d) => evaluate(env, d)
+      }
 
     | BinBoolOp(op, d1, d2) =>
       let* r1 = evaluate(env, d1);
@@ -1270,7 +1327,51 @@ and evaluate_test_eq =
   let* arg_result = evaluate(env, arg_show);
 
   (arg_show, arg_result) |> return;
-};
+}
+and module_evaluate:
+  (ClosureEnvironment.t, Environment.t, DHExp.t) => m(EvaluatorResult.t) =
+  (env, env_in, d) => {
+    switch (d) {
+    | Let(dp, d1, d2) =>
+      let* r1 = evaluate(env, d1);
+      switch (r1) {
+      | BoxedValue(d1)
+      | Indet(d1) =>
+        switch (matches(dp, d1)) {
+        | IndetMatch
+        | DoesNotMatch => Indet(Closure(env, Let(dp, d1, d2))) |> return
+        | Matches(env') =>
+          let* env = evaluate_extend_env(env', env);
+          let* env_in =
+            Environment.union(env', env_in)
+            |> ClosureEnvironment.of_environment
+            |> with_eig;
+          let env_in = ClosureEnvironment.map_of(env_in);
+          module_evaluate(env, env_in, d2);
+        }
+      };
+    | Module(dp, d1, d2) =>
+      let empty_env = Environment.empty;
+      let* r1 = module_evaluate(env, empty_env, d1);
+      switch (r1) {
+      | BoxedValue(d1)
+      | Indet(d1) =>
+        switch (matches(dp, d1)) {
+        | IndetMatch
+        | DoesNotMatch => Indet(Closure(env, Module(dp, d1, d2))) |> return
+        | Matches(env') =>
+          let* env = evaluate_extend_env(env', env);
+          let* env_in =
+            Environment.union(env', env_in)
+            |> ClosureEnvironment.of_environment
+            |> with_eig;
+          let env_in = ClosureEnvironment.map_of(env_in);
+          module_evaluate(env, env_in, d2);
+        }
+      };
+    | _ => BoxedValue(ModuleVal(env_in)) |> return
+    };
+  };
 
 let evaluate = (env, d) => {
   let es = EvaluatorState.init;