diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 4779c49b94..b3ff633952 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -312,7 +312,7 @@ let rec dhexp_of_uexp = switch (Id.Map.find_opt(Term.UPat.rep_id(p), m)) { | Some(InfoPat({ty, _})) => switch (ty) { - | Module(c) => c + | Module(c) => c.inner_ctx | _ => [] } | _ => [] diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index f0f377469b..a68498754c 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -103,17 +103,19 @@ module CastHelpers = { let grounded_List = NotGroundOrHole(List(Unknown(Internal))); let grounded_Module = (ctx: Ctx.t) => NotGroundOrHole( - Typ.Module( - List.map( - fun - | Ctx.VarEntry(var_entry) => - Ctx.VarEntry({...var_entry, typ: Unknown(Internal)}) - | Ctx.ConstructorEntry(var_entry) => - Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)}) - | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry), - ctx, - ), - ), + Typ.Module({ + inner_ctx: + List.map( + fun + | Ctx.VarEntry(var_entry) => + Ctx.VarEntry({...var_entry, typ: Unknown(Internal)}) + | Ctx.ConstructorEntry(var_entry) => + Ctx.ConstructorEntry({...var_entry, typ: Unknown(Internal)}) + | Ctx.TVarEntry(tvar_entry) => Ctx.TVarEntry(tvar_entry), + ctx, + ), + incomplete: false, + }), ); let rec ground_cases_of = (ty: Typ.t): ground_cases => { @@ -144,19 +146,8 @@ module CastHelpers = { } else { tys |> List.length |> grounded_Prod; } - | Module(ctx) => - if (List.for_all( - fun - | Ctx.VarEntry(var_entry) - | Ctx.ConstructorEntry(var_entry) => - var_entry.typ == Unknown(Internal) - | Ctx.TVarEntry(_) => true, - ctx, - )) { - Ground; - } else { - grounded_Module(ctx); - } + | Module({inner_ctx: [], incomplete: true}) => Ground + | Module(_) => NotGroundOrHole(Module({inner_ctx: [], incomplete: true})) | Sum(sm) => sm |> ConstructorMap.is_ground(is_ground_arg) ? Ground : grounded_Sum(sm) @@ -311,12 +302,12 @@ module Transition = (EV: EV_MODE) => { | (Cast(d3', Module(ctx), Module(ctx')), BoundVar(name)) | (Cast(d3', Module(ctx), Module(ctx')), Constructor(name)) => let ty = - switch (Ctx.lookup_var(ctx, name)) { + switch (Ctx.lookup_var(ctx.inner_ctx, name)) { | None => Typ.Unknown(Internal) | Some(var) => var.typ }; let ty' = - switch (Ctx.lookup_var(ctx', name)) { + switch (Ctx.lookup_var(ctx'.inner_ctx, name)) { | None => Typ.Unknown(Internal) | Some(var) => var.typ }; diff --git a/src/haz3lcore/statics/Module.re b/src/haz3lcore/statics/Module.re index 80f9bf3521..d986c16dfe 100644 --- a/src/haz3lcore/statics/Module.re +++ b/src/haz3lcore/statics/Module.re @@ -31,7 +31,7 @@ let rec get_module = | Constructor(tag_name) | Var(tag_name) => switch (Ctx.lookup_var(ctx, tag_name)) { - | Some({typ: Module(inner_ctx), _}) => + | Some({typ: Module({inner_ctx, _}), _}) => Some((name ++ tag_name ++ ".", Some(inner_ctx))) | _ => Some((name ++ tag_name ++ ".", None)) } @@ -41,7 +41,7 @@ let rec get_module = let inner_ctx = { let* ctx = ctx; switch (Ctx.lookup_var(ctx, tag_name)) { - | Some({typ: Module(inner_ctx), _}) => Some(inner_ctx) + | Some({typ: Module({inner_ctx, _}), _}) => Some(inner_ctx) | _ => None }; }; @@ -51,5 +51,8 @@ let rec get_module = }; }; let mk = (name: Var.t, id: Id.t) => { - Typ.Module([VarEntry({name, id, typ: Unknown(Internal)})]); + Typ.Module({ + inner_ctx: [VarEntry({name, id, typ: Unknown(Internal)})], + incomplete: true, + }); }; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 4e81e98e4d..b07ba5c7a0 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -524,7 +524,7 @@ and uexp_to_info_map = }; }; switch (ty) { - | Module(inner_ctx) => + | Module({inner_ctx, _}) => let (body, m) = go'(~ctx=inner_ctx, ~mode, e_mem, m); let m = e_mem.ids @@ -744,7 +744,7 @@ and upat_to_info_map = add the type alias to the current context */ let ctx = { switch (ctx_typ) { - | Module(inner_ctx) => + | Module({inner_ctx, _}) => switch (Ctx.lookup_tvar(inner_ctx, ctr)) { | Some({kind: Singleton(ty), _}) => /** Currently all type shadowing are disallowed. See TyAlias */ @@ -977,7 +977,7 @@ and uexp_to_module = m: Map.t, inner_ctx: Ctx.t, ) - : (Ctx.t, Info.exp, Map.t) => { + : (Typ.module_typ, Info.exp, Map.t) => { let mode = switch (mode) { | Ana(Unknown(SynSwitch)) => Mode.Syn @@ -1018,7 +1018,7 @@ and uexp_to_module = // Var like patterns are looked up in the module context. | Var(name) | Constructor(name) => - switch (Ctx.lookup_var(m, name)) { + switch (Ctx.lookup_var(m.inner_ctx, name)) { | Some(t) => Ana(t.typ) | None => Syn } @@ -1286,7 +1286,7 @@ and uexp_to_module = let expects: Info.typ_expects = switch (mode) { | Ana(Module(m)) => - switch (Ctx.lookup_alias(m, name)) { + switch (Ctx.lookup_alias(m.inner_ctx, name)) { | Some(ty) => /* This check is moved here because utyp_to_info_map does not handle recursion. */ @@ -1342,7 +1342,7 @@ and uexp_to_module = ( switch (mode) { | Ana(Module(m)) => m - | _ => inner_ctx + | _ => {inner_ctx, incomplete: false} }, info, m, diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 4be6cd1291..7e5b518bb4 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -247,12 +247,14 @@ module UTyp = { List.hd(ids); }; let rec upat_to_ctx = - ((outer_ctx: Ctx.t, inner_ctx: Ctx.t), upat: TermBase.UPat.t) => { + ( + (outer_ctx: Ctx.t, inner_ctx: Ctx.t, incomplete: bool), + upat: TermBase.UPat.t, + ) => { switch (upat.term) { | Invalid(_) | EmptyHole | MultiHole(_) - | Wild | Int(_) | Float(_) | Bool(_) @@ -261,7 +263,9 @@ module UTyp = { | ListLit(_) | Cons(_) | Tuple(_) - | Ap(_) => (outer_ctx, inner_ctx) + | Wild + | Ap(_) => (outer_ctx, inner_ctx, incomplete) + // | Wild => (outer_ctx, inner_ctx, true) // disabled due to casting issues. | TypeAnn(var, utyp1) => switch (var.term, utyp1.term) { | (Var(name), _) @@ -276,8 +280,9 @@ module UTyp = { }), ...inner_ctx, ], + incomplete, ) - | _ => (outer_ctx, inner_ctx) + | _ => (outer_ctx, inner_ctx, incomplete) } | Var(name) => ( outer_ctx, @@ -285,6 +290,7 @@ module UTyp = { VarEntry({name, id: rep_id_p(upat), typ: Unknown(TypeHole)}), ...inner_ctx, ], + incomplete, ) | Constructor(name) => ( outer_ctx, @@ -296,6 +302,7 @@ module UTyp = { }), ...inner_ctx, ], + incomplete, ) | TyAlias(typat, utyp) => switch (typat.term) { @@ -339,22 +346,23 @@ module UTyp = { | Some(sm) => ( Ctx.add_ctrs(ctx_body, name, rep_id(utyp), sm), Ctx.add_ctrs(new_inner, name, rep_id(utyp), sm), + incomplete, ) - | None => (ctx_body, new_inner) + | None => (ctx_body, new_inner, incomplete) }; - | _ => (outer_ctx, inner_ctx) + | _ => (outer_ctx, inner_ctx, incomplete) } - | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx), p) + | Parens(p) => upat_to_ctx((outer_ctx, inner_ctx, incomplete), p) }; }; let rec get_Tuple: TermBase.UPat.t => Typ.t = ( ut => switch (ut.term) { | Tuple(us) => - let (_, module_ctx) = - List.fold_left(upat_to_ctx, (ctx, []), us); - Module(module_ctx); + let (_, inner_ctx, incomplete) = + List.fold_left(upat_to_ctx, (ctx, [], false), us); + Module({inner_ctx, incomplete}); | Parens(p) => get_Tuple(p) | TypeAnn(_) | Var(_) @@ -372,8 +380,9 @@ module UTyp = { | ListLit(_) | Cons(_) | Ap(_) => - let (_, module_ctx) = upat_to_ctx((ctx, []), ut); - Module(module_ctx); + let (_, inner_ctx, incomplete) = + upat_to_ctx((ctx, [], false), ut); + Module({inner_ctx, incomplete}); } ); get_Tuple(u); diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 53221f2d16..d5ad13c0d3 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -19,6 +19,11 @@ module rec Typ: { | Free(TypVar.t) | Internal; + type module_typ = { + inner_ctx: Ctx.t, + incomplete: bool, + }; + /* TYP.T: Hazel types */ [@deriving (show({with_path: false}), sexp, yojson)] type t = @@ -32,7 +37,7 @@ module rec Typ: { | Arrow(t, t) | Sum(sum_map) | Prod(list(t)) - | Module(Ctx.t) + | Module(module_typ) | Member(Token.t, t) | Rec(TypVar.t, t) | Forall(TypVar.t, t) @@ -83,7 +88,13 @@ module rec Typ: { | Free(TypVar.t) | Internal; + [@deriving (show({with_path: false}), sexp, yojson)] + type module_typ = { + inner_ctx: Ctx.t, + incomplete: bool, + }; /* TYP.T: Hazel types */ + [@deriving (show({with_path: false}), sexp, yojson)] type t = | Unknown(type_provenance) @@ -96,7 +107,7 @@ module rec Typ: { | Arrow(t, t) | Sum(sum_map) | Prod(list(t)) - | Module(Ctx.t) + | Module(module_typ) | Member(Token.t, t) | Rec(TypVar.t, t) | Forall(TypVar.t, t) @@ -167,7 +178,7 @@ module rec Typ: { List.map(snd, sm), ) | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) - | Module(inner_ctx) => + | Module({inner_ctx, _}) => let ctx_entry_subst = (l: list(Token.t), e: Ctx.entry): list(Token.t) => { switch (e) { | VarEntry(t) @@ -210,7 +221,7 @@ module rec Typ: { | Forall(y, ty) => Forall(y, subst(s, x, ty)) | List(ty) => List(subst(s, x, ty)) | Var(y) => TypVar.eq(x, y) ? s : Var(y) - | Module(inner_ctx) => + | Module({inner_ctx, incomplete}) => let ctx_entry_subst = (e: Ctx.entry): Ctx.entry => { switch (e) { | VarEntry(t) => VarEntry({...t, typ: subst(s, x, t.typ)}) @@ -219,7 +230,7 @@ module rec Typ: { | TVarEntry(_) => e }; }; - Module(List.map(ctx_entry_subst, inner_ctx)); + Module({inner_ctx: List.map(ctx_entry_subst, inner_ctx), incomplete}); | Member(name, ty) => Member(name, subst(s, x, ty)) }; }; @@ -257,7 +268,8 @@ module rec Typ: { | _ => false }; }; - List.equal(entry_equal, ctx1, ctx2); + List.equal(entry_equal, ctx1.inner_ctx, ctx2.inner_ctx) + && ctx1.incomplete == ctx2.incomplete; | (Module(_), _) => false | (Rec(x1, t1), Rec(x2, t2)) | (Forall(x1, t1), Forall(x2, t2)) => @@ -399,24 +411,39 @@ module rec Typ: { List(ty); | (List(_), _) => None | (Module(ctx1), Module(ctx2)) => + /* Module types can join if and only if for every variable, + Either: it appears in both ctxs and the types can join, + Or: it appears only in one ctx and the other ctx is incomplete */ let join_entry = - (ctx2: Ctx.t, ctx_joined: option(Ctx.t), ctx1_entry: Ctx.entry) + ( + {inner_ctx, incomplete}: module_typ, + ctx_joined: option(Ctx.t), + ctx1_entry: Ctx.entry, + ) : option(Ctx.t) => { + let do_incomplete = (entry1: 'a, entry2: option('a)): option('a) => + if (incomplete && entry2 == None) { + Some(entry1); + } else { + entry2; + }; let* ctx_joined = ctx_joined; switch (ctx1_entry) { - | VarEntry({name, typ, id}) => - let* entry2 = Ctx.lookup_var(ctx2, name); + | VarEntry({name, typ, id} as entry1) => + let* entry2 = + Ctx.lookup_var(inner_ctx, name) |> do_incomplete(entry1); let+ typ_joined = join'(typ, entry2.typ); Ctx.extend(ctx_joined, VarEntry({name, typ: typ_joined, id})); - | ConstructorEntry({name, typ, id}) => - let* entry2 = Ctx.lookup_ctr(ctx2, name); + | ConstructorEntry({name, typ, id} as entry1) => + let* entry2 = + Ctx.lookup_ctr(inner_ctx, name) |> do_incomplete(entry1); let+ typ_joined = join'(typ, entry2.typ); Ctx.extend( ctx_joined, ConstructorEntry({name, typ: typ_joined, id}), ); | TVarEntry({name, kind, id}) => - let* entry2 = Ctx.lookup_tvar(ctx2, name); + let* entry2 = Ctx.lookup_tvar(inner_ctx, name); let+ kind_joined = switch (kind, entry2.kind) { | (Abstract, Abstract) => Some(Kind.Abstract) @@ -428,8 +455,15 @@ module rec Typ: { Ctx.extend(ctx_joined, TVarEntry({name, kind: kind_joined, id})); }; }; - let* ctx = List.fold_left(join_entry(ctx2), Some([]), ctx1); - Some(Module(ctx)); + let* ctx = List.fold_left(join_entry(ctx2), Some([]), ctx1.inner_ctx); + let* ctx = + List.fold_left(join_entry(ctx1), Some(ctx), ctx2.inner_ctx); + Some( + Module({ + inner_ctx: ctx |> Ctx.filter_duplicates, + incomplete: ctx1.incomplete && ctx2.incomplete, + }), + ); | (Module(_), _) => None }; } @@ -488,7 +522,7 @@ module rec Typ: { | Arrow(t1, t2) => Arrow(normalize(ctx, t1), normalize(ctx, t2)) | Prod(ts) => Prod(List.map(normalize(ctx), ts)) | Sum(ts) => Sum(ConstructorMap.map(Option.map(normalize(ctx)), ts)) - | Module(inner_ctx) => + | Module({inner_ctx, incomplete}) => let ctx_entry_subst = (e: Ctx.entry): Ctx.entry => { switch (e) { | VarEntry(t) => VarEntry({...t, typ: normalize(ctx, t.typ)}) @@ -497,7 +531,7 @@ module rec Typ: { | TVarEntry(_) => e }; }; - Module(List.map(ctx_entry_subst, inner_ctx)); + Module({inner_ctx: List.map(ctx_entry_subst, inner_ctx), incomplete}); | Member(name, ty) => Member(name, normalize(ctx, ty)) | Rec(name, ty) => /* NOTE: Dummy tvar added has fake id but shouldn't matter @@ -641,8 +675,9 @@ module rec Typ: { ts, ) ++ ")" - | Module([]) => "Module" - | Module([e, ...es]) => + | Module({inner_ctx: [], incomplete: false}) => "Module" + | Module({inner_ctx: [], incomplete: true}) => "Module{...}" + | Module({inner_ctx: [e, ...es], incomplete}) => let view_entry = (m: Ctx.entry): string => { switch (m) { | VarEntry({name: n0, typ: t0, _}) @@ -663,6 +698,7 @@ module rec Typ: { es, ) ++ view_entry(e) + ++ (incomplete ? ",..." : "") ++ "}"; | Member(name, _) => name | Rec(tv, t) => "rec " ++ tv ++ "->" ++ pretty_print(t) @@ -886,7 +922,7 @@ and Ctx: { | Var(n) => x == n ? Var(n) : Member(x ++ "." ++ n, Typ.weak_head_normalize(ctx, ty)) - | Module(inner_ctx) => + | Module({inner_ctx, incomplete}) => let ctx_entry_modulize = (e: entry): entry => { switch (e) { | VarEntry(t) => VarEntry({...t, typ: modulize_item(ctx, x, t.typ)}) @@ -895,28 +931,36 @@ and Ctx: { | TVarEntry(_) => e }; }; - Module(List.map(ctx_entry_modulize, inner_ctx)); + Module({ + inner_ctx: List.map(ctx_entry_modulize, inner_ctx), + incomplete, + }); | Forall(_, t) => modulize_item(ctx, x, t) }; }; let modulize = (ty: Typ.t, x: string): Typ.t => { switch (ty) { - | Module(ctx) => - Module( - List.map( - (e: entry): entry => { - switch (e) { - | VarEntry(t) => - VarEntry({...t, typ: modulize_item(ctx, x, t.typ)}) - | ConstructorEntry(t) => - ConstructorEntry({...t, typ: modulize_item(ctx, x, t.typ)}) - | TVarEntry(_) => e - } - }, - ctx, - ), - ) + | Module({inner_ctx, incomplete}) => + Module({ + inner_ctx: + List.map( + (e: entry): entry => { + switch (e) { + | VarEntry(t) => + VarEntry({...t, typ: modulize_item(inner_ctx, x, t.typ)}) + | ConstructorEntry(t) => + ConstructorEntry({ + ...t, + typ: modulize_item(inner_ctx, x, t.typ), + }) + | TVarEntry(_) => e + } + }, + inner_ctx, + ), + incomplete, + }) | _ => ty }; }; diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 1d75fecbc2..00a39466ec 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -153,7 +153,7 @@ let typ_ok_view = (cls: Term.Cls.t, ok: Info.ok_typ) => | Module(name, inner_ctx) => [ Type.view(Var(String.sub(name, 0, String.length(name) - 1))), text("is a module of type"), - Type.view(Module(inner_ctx)), + Type.view(Module({inner_ctx, incomplete: false})), ] | Variant(name, sum_ty) => [ Type.view(Var(name)), diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 3b80e8a334..bcc190ced5 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -84,8 +84,11 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => } ), ) - | Module([]) => div(~attr=clss(["typ-view", "Module"]), [text("Module")]) - | Module([e, ...es]) => + | Module({inner_ctx: [], incomplete: false}) => + div(~attr=clss(["typ-view", "Module"]), [text("Module")]) + | Module({inner_ctx: [], incomplete: true}) => + div(~attr=clss(["typ-view", "Module"]), [text("Module{...}")]) + | Module({inner_ctx: [e, ...es], incomplete}) => let view_entry = (m: Haz3lcore.TypBase.Ctx.entry): list(t) => { switch (m) { | VarEntry({name: n0, typ: t0, _}) @@ -122,7 +125,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => ) @ view_entry(e), ), - text("}"), + text((incomplete ? "..." : "") ++ "}"), ], ); | Sum(ts) => diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 7a1b3f8e09..ab1cd80cb1 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -130,8 +130,15 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { ]), parenthesize, ) - | Module([]) => (text("Module{}"), parenthesize) - | Module(entries) => + | Module({inner_ctx: [], incomplete: false}) => ( + text("Module{}"), + parenthesize, + ) + | Module({inner_ctx: [], incomplete: true}) => ( + text("Module{...}"), + parenthesize, + ) + | Module({inner_ctx, incomplete}) => let decomp_entry = (m: Haz3lcore.TypBase.Ctx.entry): list((string, Typ.t)) => { switch (m) { @@ -140,7 +147,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | TVarEntry(_) => [] }; }; - let ntpairs = List.map(decomp_entry, entries) |> List.flatten; + let ntpairs = List.map(decomp_entry, inner_ctx) |> List.flatten; let center = List.mapi( (i, (name, ty)) => @@ -160,7 +167,14 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { hcats([text(","), choices([linebreak(), space()])]), ) |> hcats; - (hcats([text("Module{"), center, text("}")]), parenthesize); + ( + hcats([ + text("Module{"), + center, + text((incomplete ? "..." : "") ++ "}"), + ]), + parenthesize, + ); | Member(name, _) => (text(name), parenthesize) | Sum(sum_map) => let center =