module system

src/haz3lcore/dynamics/DH.re

@@ -18,6 +18,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))
     | TypFun(Term.UTPat.t, t, option(Var.t))
@@ -44,6 +46,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | ModuleVal(ClosureEnvironment.t, list(Var.t))
     | IfThenElse(if_consistency, t, t, t) // use bool tag to track if branches are consistent
   and case =
     | Case(t, list(rule), int)
@@ -79,6 +82,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))
     | TypFun(Term.UTPat.t, t, option(Var.t))
@@ -105,6 +110,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | ModuleVal(ClosureEnvironment.t, list(Var.t))
     | IfThenElse(if_consistency, t, t, t)
   and case =
     | Case(t, list(rule), int)
@@ -121,6 +127,8 @@ module rec DHExp: {
     | Sequence(_, _) => "Sequence"
     | Filter(_, _) => "Filter"
     | Let(_, _, _) => "Let"
+    | Module(_, _, _) => "Module"
+    | Dot(_, _) => "DotMember"
     | FixF(_, _, _) => "FixF"
     | Fun(_, _, _, _) => "Fun"
     | TypFun(_) => "TypFun"
@@ -149,6 +157,7 @@ module rec DHExp: {
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
     | InvalidOperation(_) => "InvalidOperation"
+    | ModuleVal(_) => "ModuleVal"
     | IfThenElse(_, _, _, _) => "IfThenElse"
     };
 
@@ -182,6 +191,8 @@ module rec DHExp: {
     | Sequence(a, b) => Sequence(strip_casts(a), strip_casts(b))
     | Filter(f, b) => Filter(DHFilter.strip_casts(f), 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)
     | TypFun(a, b, c) => TypFun(a, strip_casts(b), c)
@@ -214,6 +225,7 @@ module rec DHExp: {
     | FloatLit(_) as d
     | StringLit(_) as d
     | Constructor(_) as d
+    | ModuleVal(_) as d
     | InvalidOperation(_) as d => d
     | IfThenElse(consistent, c, d1, d2) =>
       IfThenElse(
@@ -244,6 +256,10 @@ module rec DHExp: {
       DHFilter.fast_equal(f1, f2) && fast_equal(d1, d2)
     | (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)) =>
@@ -280,6 +296,8 @@ module rec DHExp: {
       fast_equal(d1, d2) && reason1 == reason2
     | (ConsistentCase(case1), ConsistentCase(case2)) =>
       fast_equal_case(case1, case2)
+    | (ModuleVal(mv1, names1), ModuleVal(mv2, names2)) =>
+      mv1 == mv2 && names1 == names2
     | (IfThenElse(c1, d11, d12, d13), IfThenElse(c2, d21, d22, d23)) =>
       c1 == c2
       && fast_equal(d11, d21)
@@ -290,6 +308,8 @@ module rec DHExp: {
     | (Sequence(_), _)
     | (Filter(_), _)
     | (Let(_), _)
+    | (Module(_), _)
+    | (Dot(_), _)
     | (FixF(_), _)
     | (Fun(_), _)
     | (TypFun(_), _)
@@ -310,6 +330,7 @@ module rec DHExp: {
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)
+    | (ModuleVal(_), _)
     | (IfThenElse(_), _)
     | (ConsistentCase(_), _) => false
 
@@ -383,6 +404,8 @@ module rec DHExp: {
     | Closure(ce, t) => Closure(ce, re(t))
     | Sequence(t1, t2) => Sequence(re(t1), re(t2))
     | Let(dhpat, t1, t2) => Let(dhpat, re(t1), re(t2))
+    | Module(dhpat, t1, t2) => Module(dhpat, re(t1), re(t2))
+    | Dot(t1, t2) => Dot(re(t1), re(t2))
     | Ap(t1, t2) => Ap(re(t1), re(t2))
     | ApBuiltin(s, args) => ApBuiltin(s, re(args))
     | BinBoolOp(op, t1, t2) => BinBoolOp(op, re(t1), re(t2))
@@ -409,6 +432,7 @@ module rec DHExp: {
     | IntLit(_)
     | FloatLit(_)
     | StringLit(_)
+    | ModuleVal(_)
     | FailedCast(_, _, _) => exp
     };
   }

src/haz3lcore/dynamics/Elaborator.re

@@ -81,6 +81,8 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
       switch (ana_ty, self_ty) {
       | (Unknown(prov), Rec(_, Sum(_)))
       | (Unknown(prov), Sum(_)) => DHExp.cast(d, self_ty, Unknown(prov))
+      | (_, Module(_))
+      | (Module(_), _) => DHExp.cast(d, self_ty, ana_ty)
       | _ => d
       }
     /* Forms with special ana rules but no particular typing requirements */
@@ -89,6 +91,8 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | IfThenElse(_)
     | Sequence(_)
     | Let(_)
+    | Module(_)
+    | Dot(_)
     | FixF(_) => d
     /* Hole-like forms: Don't cast */
     | InvalidText(_)
@@ -103,6 +107,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | InvalidOperation(_) => d
     /* Normal cases: wrap */
     | BoundVar(_)
+    | ModuleVal(_)
     | Ap(_)
     | ApBuiltin(_)
     | BuiltinFun(_)
@@ -294,6 +299,60 @@ let rec dhexp_of_uexp =
             Let(dp, FixF(self_id, ty, substituted_def), dbody);
           };
         };
+      | Module(p, def, body) =>
+        let* dp = dhpat_of_upat(m, p);
+        let* ddef = dhexp_of_uexp(m, def);
+        let+ dbody = dhexp_of_uexp(m, body);
+        /* if get module type, apply alias(Let).*/
+        let is_alias =
+          switch (Id.Map.find_opt(Term.UExp.rep_id(def), m)) {
+          | Some(InfoExp({self, _})) =>
+            switch (self) {
+            | Common(Just(Module(_))) => true
+            | _ => false
+            }
+          | _ => false
+          };
+        let signiture =
+          switch (Id.Map.find_opt(Term.UPat.rep_id(p), m)) {
+          | Some(InfoPat({ty, _})) =>
+            switch (ty) {
+            | Module(c) => c.inner_ctx
+            | _ => []
+            }
+          | _ => []
+          };
+        let (closure, names) =
+          List.fold_left(
+            ((closure, names): (ClosureEnvironment.t, list(Var.t))) =>
+              fun
+              | Ctx.VarEntry({name, id, _}) => (
+                  Environment.extend(
+                    closure |> ClosureEnvironment.map_of,
+                    (name, EmptyHole(id, 0)),
+                  )
+                  |> ClosureEnvironment.wrap(
+                       ClosureEnvironment.id_of(closure),
+                     ),
+                  [name, ...names],
+                )
+              | Ctx.TVarEntry(_)
+              | Ctx.ConstructorEntry(_) => (closure, names),
+            (ClosureEnvironment.empty, []),
+            signiture,
+          );
+        let rec body_modulize: DHExp.t => DHExp.t = (
+          fun
+          | Let(dp, d1, d2) => Let(dp, d1, body_modulize(d2))
+          | Module(dp, d1, d2) => Module(dp, d1, body_modulize(d2))
+          | _ as d => is_alias ? d : ModuleVal(closure, names)
+        );
+        let ddef = ddef |> body_modulize;
+        DHExp.Module(dp, ddef, 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)
       | Pipeline(arg, fn) =>
         let* c_fn = dhexp_of_uexp(m, fn);
@@ -456,6 +515,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(_) | Secondary(_))
   | None => None

src/haz3lcore/dynamics/EvalCtx.re

@@ -11,6 +11,11 @@ type cls =
   | Sequence2
   | Let1
   | Let2
+  | Module1
+  | Module2
+  | ModuleVal
+  | Dot1
+  | Dot2
   | TypAp
   | Ap1
   | Ap2
@@ -57,6 +62,10 @@ type t =
   | Sequence2(DHExp.t, t)
   | Let1(DHPat.t, t, DHExp.t)
   | Let2(DHPat.t, DHExp.t, t)
+  | Module1(DHPat.t, t, DHExp.t)
+  | Module2(DHPat.t, DHExp.t, t)
+  | Dot1(t, DHExp.t)
+  | Dot2(DHExp.t, t)
   | Fun(DHPat.t, Typ.t, t, option(Var.t))
   | FixF(Var.t, Typ.t, t)
   | TypAp(t, Typ.t)
@@ -126,6 +135,10 @@ let rec fuzzy_mark =
   | Sequence2(_)
   | Let1(_)
   | Let2(_)
+  | Module1(_)
+  | Module2(_)
+  | Dot1(_)
+  | Dot2(_)
   | Fun(_)
   | FixF(_)
   | TypAp(_)
@@ -173,6 +186,10 @@ let rec unwrap = (ctx: t, sel: cls): option(t) => {
   | (Sequence2, Sequence2(_, c))
   | (Let1, Let1(_, c, _))
   | (Let2, Let2(_, _, c))
+  | (Module1, Module1(_, c, _))
+  | (Module2, Module2(_, _, c))
+  | (Dot1, Dot1(c, _))
+  | (Dot2, Dot2(_, c))
   | (Fun, Fun(_, _, c, _))
   | (FixF, FixF(_, _, c))
   | (TypAp, TypAp(c, _))
@@ -228,6 +245,10 @@ let rec unwrap = (ctx: t, sel: cls): option(t) => {
   | (IfThenElse3, IfThenElse2(_))
   | (Let1, Let2(_))
   | (Let2, Let1(_))
+  | (Module1, Module2(_))
+  | (Module2, Module1(_))
+  | (Dot1, Dot2(_, _))
+  | (Dot2, Dot1(_, _))
   | (BinBoolOp1, BinBoolOp2(_))
   | (BinBoolOp2, BinBoolOp1(_))
   | (BinIntOp1, BinIntOp2(_))

src/haz3lcore/dynamics/EvaluatorError.re

@@ -9,6 +9,7 @@ type t =
   | CastBVHoleGround(DHExp.t)
   | InvalidBoxedTypFun(DHExp.t)
   | InvalidBoxedFun(DHExp.t)
+  | InvalidBoxedModule(DHExp.t)
   | InvalidBoxedBoolLit(DHExp.t)
   | InvalidBoxedIntLit(DHExp.t)
   | InvalidBoxedFloatLit(DHExp.t)

src/haz3lcore/dynamics/EvaluatorError.rei

@@ -7,6 +7,7 @@ type t =
   | CastBVHoleGround(DHExp.t)
   | InvalidBoxedTypFun(DHExp.t)
   | InvalidBoxedFun(DHExp.t)
+  | InvalidBoxedModule(DHExp.t)
   | InvalidBoxedBoolLit(DHExp.t)
   | InvalidBoxedIntLit(DHExp.t)
   | InvalidBoxedFloatLit(DHExp.t)

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -46,6 +46,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | IntLit(_)
   | FloatLit(_)
   | StringLit(_)
+  | ModuleVal(_)
   | Constructor(_) => d |> return
 
   | Sequence(d1, d2) =>
@@ -62,6 +63,10 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     Ap(d1', d2') |> return;
 
+  | Dot(d1, d2) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    Dot(d1', d2') |> return;
   | TypAp(d1, ty) =>
     let* d1' = pp_eval(d1);
     TypAp(d1', ty) |> return;
@@ -153,6 +158,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   /* These expression forms should not exist outside closure in evaluated result */
   | BoundVar(_)
   | Let(_)
+  | Module(_)
   | ConsistentCase(_)
   | Fun(_)
   | TypFun(_)
@@ -190,6 +196,12 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
       let* d2 = pp_uneval(env, d2);
       Let(dp, d1, d2) |> return;
 
+    | Module(dp, d1, d2) =>
+      /* d1 should already be evaluated, d2 is not */
+      let* d1 = pp_eval(d1);
+      let* d2 = pp_uneval(env, d2);
+      Let(dp, d1, d2) |> return;
+
     | ConsistentCase(Case(scrut, rules, i)) =>
       /* scrut should already be evaluated, rule bodies are not */
       let* scrut =
@@ -278,6 +290,7 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
   | IntLit(_)
   | FloatLit(_)
   | StringLit(_)
+  | ModuleVal(_)
   | Constructor(_) => d |> return
 
   | Test(id, d1) =>
@@ -297,6 +310,16 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     Let(dp, d1', d2') |> return;
 
+  | Module(dp, d1, d2) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    Module(dp, d1', d2') |> return;
+
+  | Dot(d1, d2) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    Dot(d1', d2') |> return;
+
   | FixF(f, ty, d1) =>
     let* d1' = pp_uneval(env, d1);
     FixF(f, ty, d1') |> return;
@@ -470,6 +493,7 @@ let rec track_children_of_hole =
   | IntLit(_)
   | FloatLit(_)
   | StringLit(_)
+  | ModuleVal(_)
   | BuiltinFun(_)
   | BoundVar(_) => hii
   | Test(_, d)
@@ -483,11 +507,13 @@ let rec track_children_of_hole =
   | InvalidOperation(d, _) => track_children_of_hole(hii, parent, d)
   | Sequence(d1, d2)
   | Let(_, d1, d2)
+  | Module(_, d1, d2)
   | Ap(d1, d2)
   | BinBoolOp(_, d1, d2)
   | BinIntOp(_, d1, d2)
   | BinFloatOp(_, d1, d2)
   | BinStringOp(_, d1, d2)
+  | Dot(d1, d2)
   | Cons(d1, d2) =>
     let hii = track_children_of_hole(hii, parent, d1);
     track_children_of_hole(hii, parent, d2);