From 2606648e00c6f8dc89cc1530431fa43219795931 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Fri, 18 Aug 2023 16:54:58 -0400 Subject: [PATCH 01/14] Add: mold and forms of parameterized type --- src/haz3lcore/lang/Form.re | 2 ++ src/haz3lcore/statics/Info.re | 18 ++++++++-- src/haz3lcore/statics/MakeTerm.re | 50 ++++++++++++++++++++-------- src/haz3lcore/statics/Statics.re | 55 +++++++++++++++++++++++++++++++ src/haz3lcore/statics/Term.re | 11 ++++--- src/haz3lcore/statics/TermBase.re | 2 ++ src/haz3lcore/statics/TypBase.re | 28 +++++++++++++--- src/haz3lweb/view/CtxInspector.re | 3 +- src/haz3lweb/view/Kind.re | 2 ++ src/haz3lweb/view/LangDoc.re | 1 + 10 files changed, 146 insertions(+), 26 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index f115522c3c..080137dd2d 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -91,6 +91,7 @@ let is_reserved = str => is_bool(str); let is_var = str => !is_reserved(str) && regexp("^[a-z][A-Za-z0-9_]*$", str); let is_capitalized_name = regexp("^[A-Z][A-Za-z0-9_]*$"); let is_ctr = is_capitalized_name; +let is_type_input = regexp("^[a-z]*$"); let base_typs = ["String", "Int", "Float", "Bool"]; let is_base_typ = regexp("^(" ++ String.concat("|", base_typs) ++ ")$"); let is_typ_var = is_capitalized_name; @@ -258,6 +259,7 @@ let forms: list((string, t)) = [ ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))), ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))), ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))), + ("ap_tpat", mk(ii, ["(", ")"], mk_post(P.ap, TPat, [TPat]))), ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))), ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), ( diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 69d3871db6..9c24e3bd79 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -337,7 +337,11 @@ let status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp => free, and whether a ctr name is a dupe. */ let status_typ = (ctx: Ctx.t, expects: typ_expects, term: TermBase.UTyp.t, ty: Typ.t) - : status_typ => + : status_typ => { + //Printf.printf("status_ctx: %s\n", TermBase.UTyp.show(term)); + //Printf.printf("status_expects: %s\n", Typ.show(ty)); + //Printf.printf("status_term: %s\n", TermBase.UTyp.show(term)); + //Printf.printf("status_ty: %s\n", Typ.show(ty)); switch (term.term) { | Invalid(token) => InHole(BadToken(token)) | EmptyHole => NotInHole(Type(ty)) @@ -375,7 +379,7 @@ let status_typ = | VariantExpected(_) => InHole(WantConstructorFoundType(ty)) } }; - +}; let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat => switch (utpat.term) { | EmptyHole => NotInHole(Empty) @@ -385,6 +389,16 @@ let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat => | Var(name) => NotInHole(Var(name)) | Invalid(_) => InHole(NotAVar(NotCapitalized)) | MultiHole(_) => InHole(NotAVar(Other)) + | Ap(t, _) => + switch (t.term) { + | Var(name) => + if (Form.is_base_typ(name) || Ctx.lookup_alias(ctx, name) != None) { + InHole(ShadowsType(name)); + } else { + NotInHole(Var(name)); + } + | _ => InHole(NotAVar(Other)) + } }; /* Determines whether any term is in an error hole. */ diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 1c170c63ee..cdf21a754f 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -228,7 +228,12 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => - TyAlias(tpat, def, r) + Printf.printf( + "tpat: %s, def: %s\n", + UTPat.show(tpat), + UTyp.show(def), + ); + TyAlias(tpat, def, r); | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => If(cond, conseq, r) | _ => hole(tm) @@ -297,10 +302,10 @@ and pat = unsorted => { let ids = ids(unsorted) @ inner_ids; return(p => Pat(p), ids, {ids, term}); } -and pat_term: unsorted => (UPat.term, list(Id.t)) = { +and pat_term = (unsorted: unsorted): (UPat.term, list(Id.t)) => { let ret = (term: UPat.term) => (term, []); let hole = unsorted => Term.UPat.hole(kids_of_unsorted(unsorted)); - fun + switch (unsorted) { | Op(tiles) as tm => switch (tiles) { | ([(_id, tile)], []) => @@ -356,17 +361,19 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | _ => ret(hole(tm)) } } - | tm => ret(hole(tm)); + | tm => ret(hole(tm)) + }; } and typ = unsorted => { let (term, inner_ids) = typ_term(unsorted); let ids = ids(unsorted) @ inner_ids; return(ty => Typ(ty), ids, {ids, term}); } -and typ_term: unsorted => (UTyp.term, list(Id.t)) = { +and typ_term = (unsorted: unsorted): (UTyp.term, list(Id.t)) => { let ret = (term: UTyp.term) => (term, []); let hole = unsorted => Term.UTyp.hole(kids_of_unsorted(unsorted)); - fun + //Printf.printf("typ_term: %s\n", show_unsorted(unsorted)); + switch (unsorted) { | Op(tiles) as tm => switch (tiles) { | ([(_id, tile)], []) => @@ -378,6 +385,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { | (["Float"], []) => Float | (["String"], []) => String | ([t], []) when Form.is_typ_var(t) => Var(t) + | ([t], []) when Form.is_type_input(t) => Var(t) | (["(", ")"], [Typ(body)]) => Parens(body) | (["[", "]"], [Typ(body)]) => List(body) | ([t], []) when t != " " => Invalid(t) @@ -417,17 +425,18 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { | _ => ret(hole(tm)) } } - | tm => ret(hole(tm)); + | tm => ret(hole(tm)) + }; } and tpat = unsorted => { let term = tpat_term(unsorted); let ids = ids(unsorted); return(ty => TPat(ty), ids, {ids, term}); } -and tpat_term: unsorted => UTPat.term = { +and tpat_term = (unsorted: unsorted): UTPat.term => { let ret = (term: UTPat.term) => term; let hole = unsorted => Term.UTPat.hole(kids_of_unsorted(unsorted)); - fun + switch (unsorted) { | Op(tiles) as tm => switch (tiles) { | ([(_id, tile)], []) => @@ -440,10 +449,26 @@ and tpat_term: unsorted => UTPat.term = { ) | _ => ret(hole(tm)) } - | (Pre(_) | Post(_)) as tm => ret(hole(tm)) - | tm => ret(hole(tm)); + | Post(TPat(l), tiles) as tm => + switch (tiles) { + | ([(_id, tile)], []) => + ret( + switch (tile) { + | (["(", ")"], [TPat(arg)]) => + switch (arg.term) { + | Invalid(s) when Form.is_type_input(s) => + Ap(l, {ids: arg.ids, term: Var(s)}) + | _ => ret(hole(tm)) + } + | _ => hole(tm) + }, + ) + | _ => ret(hole(tm)) + } + | Pre(_) as tm => ret(hole(tm)) + | tm => ret(hole(tm)) + }; } - // and rul = unsorted => { // let term = rul_term(unsorted); // let ids = ids(unsorted); @@ -468,7 +493,6 @@ and rul = (unsorted: unsorted): URul.t => { | e => {ids: [], term: Rules(e, [])} }; } - and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => { let tile_kids = (p: Piece.t): list(any) => switch (p) { diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 1fb4d040c5..46b3d92794 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -326,6 +326,60 @@ and uexp_to_info_map = let ty_escape = Typ.subst(ty_def, name, ty_body); let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd; add(~self=Just(ty_escape), ~co_ctx, m); + | Ap(t1, _) => + let constructor = + switch (t1.term) { + | Var(s) => s + | _ => "" + }; + //let arg = + // switch (t2.term) { + // | Var(s) => s + // | _ => "" + // }; + Printf.printf( + "typat: %s, utyp: %s, body:%s \n", + UTPat.show(typat), + UTyp.show(utyp), + UExp.show(body), + ); + let (ty_def, ctx_def, ctx_body) = { + let ty_pre = + UTyp.to_typ(Ctx.extend_dummy_tvar(ctx, constructor), utyp); + switch (utyp.term) { + | Sum(_) when List.mem(constructor, Typ.free_vars(ty_pre)) => + let ty_rec = + Typ.Rec("α", Typ.subst(Var("α"), constructor, ty_pre)); + let ctx_def = + Ctx.extend_alias(ctx, constructor, UTPat.rep_id(typat), ty_rec); + (ty_rec, ctx_def, ctx_def); + | _ => + let ty = UTyp.to_typ(ctx, utyp); + ( + ty, + ctx, + Ctx.extend_alias(ctx, constructor, UTPat.rep_id(typat), ty), + ); + }; + }; + //Printf.printf( + // "ty_def: %s, ctx_def: %s, ctx_body: %s \n", + // Typ.show(ty_def), + // Ctx.show(ctx_def), + // Ctx.show(ctx_body), + //); + let ctx_body = + switch (Typ.get_sum_constructors(ctx, ty_def)) { + | Some(sm) => + Ctx.add_ctrs(ctx_body, constructor, UTyp.rep_id(utyp), sm) + | None => ctx_body + }; + let ({co_ctx, ty: ty_body, _}: Info.exp, m) = + go'(~ctx=ctx_body, ~mode, body, m); + /* Make sure types don't escape their scope */ + let ty_escape = Typ.subst(ty_def, constructor, ty_body); + let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd; + add(~self=Just(ty_escape), ~co_ctx, m); | Var(_) | Invalid(_) | EmptyHole @@ -488,6 +542,7 @@ and utpat_to_info_map = let (_, m) = multi(~ctx, ~ancestors, m, tms); add(m); | Invalid(_) + | Ap(_) | EmptyHole | Var(_) => add(m) }; diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index f62a502e8c..e297f47942 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -155,8 +155,8 @@ module UTPat = { | Invalid | EmptyHole | MultiHole - | Var; - + | Var + | Ap; include TermBase.UTPat; let rep_id = ({ids, _}) => { @@ -175,14 +175,15 @@ module UTPat = { | Invalid(_) => Invalid | EmptyHole => EmptyHole | MultiHole(_) => MultiHole - | Var(_) => Var; - + | Var(_) => Var + | Ap(_) => Ap; let show_cls: cls => string = fun | Invalid => "Invalid type alias" | MultiHole => "Broken type alias" | EmptyHole => "Empty type alias hole" - | Var => "Type alias"; + | Var => "Type alias" + | Ap => "Type Application"; }; module UPat = { diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index ee0280b17c..585c331842 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -379,6 +379,7 @@ and UTPat: { | EmptyHole | MultiHole(list(Any.t)) | Var(TypVar.t) + | Ap(t, t) and t = { ids: list(Id.t), term, @@ -390,6 +391,7 @@ and UTPat: { | EmptyHole | MultiHole(list(Any.t)) | Var(TypVar.t) + | Ap(t, t) and t = { ids: list(Id.t), term, diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 3ad0570301..ab368d6161 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -432,7 +432,8 @@ and Ctx: { type entry = | VarEntry(var_entry) | ConstructorEntry(var_entry) - | TVarEntry(tvar_entry); + | TVarEntry(tvar_entry) + | TConstructorEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); @@ -471,7 +472,8 @@ and Ctx: { type entry = | VarEntry(var_entry) | ConstructorEntry(var_entry) - | TVarEntry(tvar_entry); + | TVarEntry(tvar_entry) + | TConstructorEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); @@ -480,10 +482,14 @@ and Ctx: { let extend_tvar = (ctx: t, tvar_entry: tvar_entry): t => extend(ctx, TVarEntry(tvar_entry)); + //let extend_tConstructor = (ctx: t, tvar_entry: tvar_entry): t => + // extend(ctx, TConstructorEntry(tvar_entry)); + //let extend_ctr = + // (ctx: t, name: TypVar.t, id: Id.t, ty1: Typ.t, ty2: Typ.t): t => + // extend_tConstructor(ctx, {name, id, kind: Arrow(ty1, ty2)}); let extend_alias = (ctx: t, name: TypVar.t, id: Id.t, ty: Typ.t): t => extend_tvar(ctx, {name, id, kind: Singleton(ty)}); - let extend_dummy_tvar = (ctx: t, name: TypVar.t) => extend_tvar(ctx, {kind: Abstract, name, id: Id.invalid}); @@ -494,9 +500,17 @@ and Ctx: { | _ => None, ctx, ); + //let lookup_tctr = (ctx: t, name: TypVar.t): option(tvar_entry) => + // List.find_map( + // fun + // | TConstructorEntry(v) when v.name == name => Some(v) + // | _ => None, + // ctx, + // ); let lookup_alias = (ctx: t, t: TypVar.t): option(Typ.t) => switch (lookup_tvar(ctx, t)) { + | Some({kind: Arrow(ty_in, ty_out), _}) => Some(Arrow(ty_in, ty_out)) | Some({kind: Singleton(ty), _}) => Some(ty) | Some({kind: Abstract, _}) | None => None @@ -506,7 +520,8 @@ and Ctx: { fun | VarEntry({id, _}) | ConstructorEntry({id, _}) - | TVarEntry({id, _}) => id; + | TVarEntry({id, _}) => id + | TConstructorEntry({id, _}) => id; let lookup_var = (ctx: t, name: string): option(var_entry) => List.find_map( @@ -583,7 +598,8 @@ and Ctx: { VarSet.mem(name, term_set) ? (ctx, term_set, typ_set) : ([entry, ...ctx], VarSet.add(name, term_set), typ_set) - | TVarEntry({name, _}) => + | TVarEntry({name, _}) + | TConstructorEntry({name, _}) => VarSet.mem(name, typ_set) ? (ctx, term_set, typ_set) : ([entry, ...ctx], term_set, VarSet.add(name, typ_set)) @@ -599,11 +615,13 @@ and Ctx: { and Kind: { [@deriving (show({with_path: false}), sexp, yojson)] type t = + | Arrow(Typ.t, Typ.t) | Singleton(Typ.t) | Abstract; } = { [@deriving (show({with_path: false}), sexp, yojson)] type t = + | Arrow(Typ.t, Typ.t) | Singleton(Typ.t) | Abstract; }; diff --git a/src/haz3lweb/view/CtxInspector.re b/src/haz3lweb/view/CtxInspector.re index a148f149cc..9ac4b1b828 100644 --- a/src/haz3lweb/view/CtxInspector.re +++ b/src/haz3lweb/view/CtxInspector.re @@ -25,7 +25,8 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { Type.view(typ), ], ) - | TVarEntry({name, kind, _}) => + | TVarEntry({name, kind, _}) + | TConstructorEntry({name, kind, _}) => div_c( "context-entry", [ diff --git a/src/haz3lweb/view/Kind.re b/src/haz3lweb/view/Kind.re index f84672515c..416427a9d1 100644 --- a/src/haz3lweb/view/Kind.re +++ b/src/haz3lweb/view/Kind.re @@ -4,6 +4,8 @@ open Util.Web; let view = (kind: Haz3lcore.Kind.t): Node.t => switch (kind) { + | Arrow(ty1, ty2) => + div_c("kind-view", [Type.view(ty1), text(" -> "), Type.view(ty2)]) | Singleton(ty) => div_c("kind-view", [Type.view(ty)]) | Abstract => div_c("kind-view", [text("Type")]) }; diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index b0eedb8869..bc8cfeeeb9 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2817,6 +2817,7 @@ let get_doc = ), [], ); + | _ => default } | None => default }; From fe2761462c97effd4ac47993e277e5dcf07fb749 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Sun, 20 Aug 2023 23:51:13 -0400 Subject: [PATCH 02/14] Fix: the type in let works --- src/haz3lcore/dynamics/Builtins.re | 2 +- src/haz3lcore/dynamics/Evaluator.re | 1 + src/haz3lcore/statics/Info.re | 31 +++++--- src/haz3lcore/statics/MakeTerm.re | 8 +- src/haz3lcore/statics/Statics.re | 62 +++++++++------- src/haz3lcore/statics/Term.re | 21 +++++- src/haz3lcore/statics/TypBase.re | 85 +++++++++++++++------- src/haz3lweb/view/CtxInspector.re | 3 +- src/haz3lweb/view/Type.re | 5 ++ src/haz3lweb/view/dhcode/layout/HTypDoc.re | 1 + 10 files changed, 142 insertions(+), 77 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 85bda5dbe1..466a090039 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -279,7 +279,7 @@ module Pervasives = { let ctx_init: Ctx.t = List.map( ((name, Builtin.{typ, _})) => - Ctx.VarEntry({name, typ, id: Id.invalid}), + Ctx.VarEntry({name, parameter: "", typ, id: Id.invalid}), Pervasives.builtins, ); diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 529ca04260..b945c73cb3 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -45,6 +45,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | String | Var(_) | Rec(_) + | TypeConstructorAp(_, _) | Arrow(Unknown(_), Unknown(_)) | List(Unknown(_)) => Ground | Prod(tys) => diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 9c24e3bd79..1ef074e068 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -338,10 +338,6 @@ let status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp => let status_typ = (ctx: Ctx.t, expects: typ_expects, term: TermBase.UTyp.t, ty: Typ.t) : status_typ => { - //Printf.printf("status_ctx: %s\n", TermBase.UTyp.show(term)); - //Printf.printf("status_expects: %s\n", Typ.show(ty)); - //Printf.printf("status_term: %s\n", TermBase.UTyp.show(term)); - //Printf.printf("status_ty: %s\n", Typ.show(ty)); switch (term.term) { | Invalid(token) => InHole(BadToken(token)) | EmptyHole => NotInHole(Type(ty)) @@ -370,7 +366,17 @@ let status_typ = | _ => NotInHole(VariantIncomplete(Arrow(ty_in, ty_variant))) }; | ConstructorExpected(_) => InHole(WantConstructorFoundAp) - | TypeExpected => InHole(WantTypeFoundAp) + | TypeExpected => + let constructor = + switch (t1.term) { + | Var(s) => s + | _ => "" + }; + switch (Ctx.is_alias(ctx, constructor)) { + | false => InHole(FreeTypeVariable(constructor)) + | true => + NotInHole(TypeAlias(constructor, Typ.weak_head_normalize(ctx, ty))) + }; } | _ => switch (expects) { @@ -405,20 +411,23 @@ let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat => let is_error = (ci: t): bool => { switch (ci) { | InfoExp({mode, self, ctx, _}) => - switch (status_exp(ctx, mode, self)) { + let status = status_exp(ctx, mode, self); + switch (status) { | InHole(_) => true | NotInHole(_) => false - } + }; | InfoPat({mode, self, ctx, _}) => - switch (status_pat(ctx, mode, self)) { + let status = status_pat(ctx, mode, self); + switch (status) { | InHole(_) => true | NotInHole(_) => false - } + }; | InfoTyp({expects, ctx, term, ty, _}) => - switch (status_typ(ctx, expects, term, ty)) { + let status = status_typ(ctx, expects, term, ty); + switch (status) { | InHole(_) => true | NotInHole(_) => false - } + }; | InfoTPat({term, ctx, _}) => switch (status_tpat(ctx, term)) { | InHole(_) => true diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index cdf21a754f..dd7d7f788a 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -228,12 +228,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => - Printf.printf( - "tpat: %s, def: %s\n", - UTPat.show(tpat), - UTyp.show(def), - ); - TyAlias(tpat, def, r); + TyAlias(tpat, def, r) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => If(cond, conseq, r) | _ => hole(tm) @@ -372,7 +367,6 @@ and typ = unsorted => { and typ_term = (unsorted: unsorted): (UTyp.term, list(Id.t)) => { let ret = (term: UTyp.term) => (term, []); let hole = unsorted => Term.UTyp.hole(kids_of_unsorted(unsorted)); - //Printf.printf("typ_term: %s\n", show_unsorted(unsorted)); switch (unsorted) { | Op(tiles) as tm => switch (tiles) { diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 46b3d92794..65a0cc0f12 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -308,16 +308,20 @@ and uexp_to_info_map = | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) => let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre)); let ctx_def = - Ctx.extend_alias(ctx, name, UTPat.rep_id(typat), ty_rec); + Ctx.extend_alias(ctx, name, "", UTPat.rep_id(typat), ty_rec); (ty_rec, ctx_def, ctx_def); | _ => let ty = UTyp.to_typ(ctx, utyp); - (ty, ctx, Ctx.extend_alias(ctx, name, UTPat.rep_id(typat), ty)); + ( + ty, + ctx, + Ctx.extend_alias(ctx, name, "", UTPat.rep_id(typat), ty), + ); }; }; let ctx_body = switch (Typ.get_sum_constructors(ctx, ty_def)) { - | Some(sm) => Ctx.add_ctrs(ctx_body, name, UTyp.rep_id(utyp), sm) + | Some(sm) => Ctx.add_ctrs(ctx_body, name, "", UTyp.rep_id(utyp), sm) | None => ctx_body }; let ({co_ctx, ty: ty_body, _}: Info.exp, m) = @@ -326,52 +330,52 @@ and uexp_to_info_map = let ty_escape = Typ.subst(ty_def, name, ty_body); let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd; add(~self=Just(ty_escape), ~co_ctx, m); - | Ap(t1, _) => + | Ap(t1, t2) => let constructor = switch (t1.term) { | Var(s) => s | _ => "" }; - //let arg = - // switch (t2.term) { - // | Var(s) => s - // | _ => "" - // }; - Printf.printf( - "typat: %s, utyp: %s, body:%s \n", - UTPat.show(typat), - UTyp.show(utyp), - UExp.show(body), - ); + let arg = + switch (t2.term) { + | Var(s) => s + | _ => "" + }; let (ty_def, ctx_def, ctx_body) = { let ty_pre = - UTyp.to_typ(Ctx.extend_dummy_tvar(ctx, constructor), utyp); + UTyp.to_typ( + Ctx.extend_dummy_tvar( + Ctx.extend_dummy_tvar(ctx, constructor), + arg, + ), + utyp, + ); switch (utyp.term) { | Sum(_) when List.mem(constructor, Typ.free_vars(ty_pre)) => let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), constructor, ty_pre)); let ctx_def = - Ctx.extend_alias(ctx, constructor, UTPat.rep_id(typat), ty_rec); + Ctx.extend_alias( + ctx, + constructor, + arg, + UTPat.rep_id(typat), + ty_rec, + ); (ty_rec, ctx_def, ctx_def); | _ => let ty = UTyp.to_typ(ctx, utyp); ( ty, ctx, - Ctx.extend_alias(ctx, constructor, UTPat.rep_id(typat), ty), + Ctx.extend_alias(ctx, constructor, arg, UTPat.rep_id(typat), ty), ); }; }; - //Printf.printf( - // "ty_def: %s, ctx_def: %s, ctx_body: %s \n", - // Typ.show(ty_def), - // Ctx.show(ctx_def), - // Ctx.show(ctx_body), - //); let ctx_body = switch (Typ.get_sum_constructors(ctx, ty_def)) { | Some(sm) => - Ctx.add_ctrs(ctx_body, constructor, UTyp.rep_id(utyp), sm) + Ctx.add_ctrs(ctx_body, constructor, arg, UTyp.rep_id(utyp), sm) | None => ctx_body }; let ({co_ctx, ty: ty_body, _}: Info.exp, m) = @@ -445,7 +449,13 @@ and upat_to_info_map = Unknown(Internal) is used in this case */ let ctx_typ = Info.fixed_typ_pat(ctx, mode, Common(Just(Unknown(Internal)))); - let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); + let entry = + Ctx.VarEntry({ + name, + parameter: "", + id: UPat.rep_id(upat), + typ: ctx_typ, + }); add(~self=Just(unknown), ~ctx=Ctx.extend(ctx, entry), m); | Tuple(ps) => let modes = Mode.of_prod(ctx, mode, List.length(ps)); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index e297f47942..b762707d40 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -129,8 +129,25 @@ module UTyp = { | List(u) => List(to_typ(ctx, u)) | Parens(u) => to_typ(ctx, u) /* The below cases should occur only inside sums */ - | Constructor(_) - | Ap(_) => Unknown(Internal) + | Ap(t1, t2) => + let name = + switch (t1.term) { + | Var(s) => s + | _ => "" + }; + switch (Ctx.lookup_tvar(ctx, name)) { + | Some(ty) => + let arg = ty.parameter; + let res_ty = + switch (ty.kind) { + | Arrow(ty_in, ty_out) => Typ.Arrow(ty_in, ty_out) + | Singleton(ty) => ty + | Abstract => Unknown(Internal) + }; + Typ.subst(to_typ(ctx, t2), arg, res_ty); + | None => Unknown(Free(name)) + }; + | Constructor(_) => Unknown(Internal) } and to_variant: (Ctx.t, variant) => option(ConstructorMap.binding(option(Typ.t))) = diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index ab368d6161..9c0f134164 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -33,6 +33,8 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) + | TypeConstructorAp(TypVar.t, t) + and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -91,6 +93,7 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) + | TypeConstructorAp(TypVar.t, t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -157,6 +160,7 @@ module rec Typ: { | Var(_) | Rec(_) | Sum(_) => precedence_Sum + | TypeConstructorAp(_, _) | List(_) => precedence_Const | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow @@ -176,6 +180,7 @@ module rec Typ: { | Rec(y, ty) => Rec(y, subst(s, x, ty)) | List(ty) => List(subst(s, x, ty)) | Var(y) => TypVar.eq(x, y) ? s : Var(y) + | TypeConstructorAp(y, ty) => TypeConstructorAp(y, subst(s, x, ty)) }; }; @@ -212,6 +217,9 @@ module rec Typ: { | (Sum(_), _) => false | (Var(n1), Var(n2)) => n1 == n2 | (Var(_), _) => false + | (TypeConstructorAp(n1, t1), TypeConstructorAp(n2, t2)) => + n1 == n2 && eq(t1, t2) + | (TypeConstructorAp(_), _) => false }; }; @@ -234,6 +242,7 @@ module rec Typ: { ) | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) | Rec(x, ty) => free_vars(~bound=[x, ...bound], ty) + | TypeConstructorAp(_, ty) => free_vars(~bound, ty) }; /* Lattice join on types. This is a LUB join in the hazel2 @@ -319,6 +328,14 @@ module rec Typ: { let+ ty = join'(ty1, ty2); List(ty); | (List(_), _) => None + | (TypeConstructorAp(name1, ty1), TypeConstructorAp(name2, ty2)) => + if (name1 == name2) { + let+ ty = join'(ty1, ty2); + TypeConstructorAp(name1, ty); + } else { + None; + } + | (TypeConstructorAp(_), _) => None }; } and join_sum_entries = @@ -381,6 +398,8 @@ module rec Typ: { as in current implementation Recs do not occur in the surface syntax, so we won't try to jump to them. */ Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) + | TypeConstructorAp(name, ty) => + TypeConstructorAp(name, normalize(ctx, ty)) }; }; @@ -417,6 +436,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, + parameter: Var.t, id: Id.t, typ: Typ.t, }; @@ -424,6 +444,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type tvar_entry = { name: TypVar.t, + parameter: TypVar.t, id: Id.t, kind: Kind.t, }; @@ -432,15 +453,14 @@ and Ctx: { type entry = | VarEntry(var_entry) | ConstructorEntry(var_entry) - | TVarEntry(tvar_entry) - | TConstructorEntry(tvar_entry); + | TVarEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); let extend: (t, entry) => t; let extend_tvar: (t, tvar_entry) => t; - let extend_alias: (t, TypVar.t, Id.t, Typ.t) => t; + let extend_alias: (t, TypVar.t, TypVar.t, Id.t, Typ.t) => t; let extend_dummy_tvar: (t, TypVar.t) => t; let lookup_tvar: (t, TypVar.t) => option(tvar_entry); let lookup_alias: (t, TypVar.t) => option(Typ.t); @@ -448,7 +468,7 @@ and Ctx: { let lookup_var: (t, string) => option(var_entry); let lookup_ctr: (t, string) => option(var_entry); let is_alias: (t, TypVar.t) => bool; - let add_ctrs: (t, TypVar.t, Id.t, Typ.sum_map) => t; + let add_ctrs: (t, TypVar.t, TypVar.t, Id.t, Typ.sum_map) => t; let subtract_prefix: (t, t) => option(t); let added_bindings: (t, t) => t; let filter_duplicates: t => t; @@ -457,6 +477,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, + parameter: Var.t, id: Id.t, typ: Typ.t, }; @@ -464,6 +485,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type tvar_entry = { name: TypVar.t, + parameter: TypVar.t, id: Id.t, kind: Kind.t, }; @@ -472,9 +494,7 @@ and Ctx: { type entry = | VarEntry(var_entry) | ConstructorEntry(var_entry) - | TVarEntry(tvar_entry) - | TConstructorEntry(tvar_entry); - + | TVarEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); @@ -482,16 +502,25 @@ and Ctx: { let extend_tvar = (ctx: t, tvar_entry: tvar_entry): t => extend(ctx, TVarEntry(tvar_entry)); - //let extend_tConstructor = (ctx: t, tvar_entry: tvar_entry): t => - // extend(ctx, TConstructorEntry(tvar_entry)); - //let extend_ctr = - // (ctx: t, name: TypVar.t, id: Id.t, ty1: Typ.t, ty2: Typ.t): t => - // extend_tConstructor(ctx, {name, id, kind: Arrow(ty1, ty2)}); - - let extend_alias = (ctx: t, name: TypVar.t, id: Id.t, ty: Typ.t): t => - extend_tvar(ctx, {name, id, kind: Singleton(ty)}); + let extend_alias = + (ctx: t, name: TypVar.t, parameter: TypVar.t, id: Id.t, ty: Typ.t): t => { + let ctx = extend_tvar(ctx, {name, parameter, id, kind: Singleton(ty)}); + if (parameter != "") { + extend_tvar( + ctx, + { + name: parameter, + parameter: "", + id, + kind: Singleton(Unknown(TypeHole)), + }, + ); + } else { + ctx; + }; + }; let extend_dummy_tvar = (ctx: t, name: TypVar.t) => - extend_tvar(ctx, {kind: Abstract, name, id: Id.invalid}); + extend_tvar(ctx, {kind: Abstract, name, parameter: "", id: Id.invalid}); let lookup_tvar = (ctx: t, name: TypVar.t): option(tvar_entry) => List.find_map( @@ -500,13 +529,6 @@ and Ctx: { | _ => None, ctx, ); - //let lookup_tctr = (ctx: t, name: TypVar.t): option(tvar_entry) => - // List.find_map( - // fun - // | TConstructorEntry(v) when v.name == name => Some(v) - // | _ => None, - // ctx, - // ); let lookup_alias = (ctx: t, t: TypVar.t): option(Typ.t) => switch (lookup_tvar(ctx, t)) { @@ -520,8 +542,7 @@ and Ctx: { fun | VarEntry({id, _}) | ConstructorEntry({id, _}) - | TVarEntry({id, _}) => id - | TConstructorEntry({id, _}) => id; + | TVarEntry({id, _}) => id; let lookup_var = (ctx: t, name: string): option(var_entry) => List.find_map( @@ -545,11 +566,20 @@ and Ctx: { | None => false }; - let add_ctrs = (ctx: t, name: TypVar.t, id: Id.t, ctrs: Typ.sum_map): t => + let add_ctrs = + ( + ctx: t, + name: TypVar.t, + parameter: TypVar.t, + id: Id.t, + ctrs: Typ.sum_map, + ) + : t => List.map( ((ctr, typ)) => ConstructorEntry({ name: ctr, + parameter, id, typ: switch (typ) { @@ -598,8 +628,7 @@ and Ctx: { VarSet.mem(name, term_set) ? (ctx, term_set, typ_set) : ([entry, ...ctx], VarSet.add(name, term_set), typ_set) - | TVarEntry({name, _}) - | TConstructorEntry({name, _}) => + | TVarEntry({name, _}) => VarSet.mem(name, typ_set) ? (ctx, term_set, typ_set) : ([entry, ...ctx], term_set, VarSet.add(name, typ_set)) diff --git a/src/haz3lweb/view/CtxInspector.re b/src/haz3lweb/view/CtxInspector.re index 9ac4b1b828..a148f149cc 100644 --- a/src/haz3lweb/view/CtxInspector.re +++ b/src/haz3lweb/view/CtxInspector.re @@ -25,8 +25,7 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { Type.view(typ), ], ) - | TVarEntry({name, kind, _}) - | TConstructorEntry({name, kind, _}) => + | TVarEntry({name, kind, _}) => div_c( "context-entry", [ diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index ae88419f0e..80ba3cbe41 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -65,6 +65,11 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => text(")"), ], ) + | TypeConstructorAp(t, ts) => + div( + ~attr=clss(["typ-view", "TypeConstructorAp"]), + [text(t), text("("), view_ty(ts), text(")")], + ) | Sum(ts) => div( ~attr=clss(["typ-view", "Sum"]), diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 8acbc0455f..3a7972f330 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -51,6 +51,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | Bool => (text("Bool"), parenthesize) | String => (text("String"), parenthesize) | Var(name) => (text(name), parenthesize) + | TypeConstructorAp(name, _) => (text(name), parenthesize) | List(ty) => ( hcats([ mk_delim("["), From e08f671bec6faee4a5818f0e1da9c2ac66fd3b11 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Mon, 21 Aug 2023 23:20:19 -0400 Subject: [PATCH 03/14] Fix: typeHole ann bug --- src/haz3lcore/dynamics/Builtins.re | 2 +- src/haz3lcore/dynamics/Evaluator.re | 1 - src/haz3lcore/prog/Interface.re | 4 +- src/haz3lcore/statics/Self.re | 4 +- src/haz3lcore/statics/Statics.re | 85 ++++++++--- src/haz3lcore/statics/Term.re | 126 ++++++++++----- src/haz3lcore/statics/TypBase.re | 170 +++++++++++++-------- src/haz3lweb/view/CtxInspector.re | 4 +- src/haz3lweb/view/Type.re | 5 - src/haz3lweb/view/dhcode/layout/HTypDoc.re | 1 - 10 files changed, 263 insertions(+), 139 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 466a090039..85bda5dbe1 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -279,7 +279,7 @@ module Pervasives = { let ctx_init: Ctx.t = List.map( ((name, Builtin.{typ, _})) => - Ctx.VarEntry({name, parameter: "", typ, id: Id.invalid}), + Ctx.VarEntry({name, typ, id: Id.invalid}), Pervasives.builtins, ); diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index b945c73cb3..529ca04260 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -45,7 +45,6 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | String | Var(_) | Rec(_) - | TypeConstructorAp(_, _) | Arrow(Unknown(_), Unknown(_)) | List(Unknown(_)) => Ground | Prod(tys) => diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index 77106704c8..04c9493bb5 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -1,5 +1,5 @@ exception DoesNotElaborate; -let elaborate = (map, term): DHExp.t => +let elaborate = (map, term): DHExp.t => { switch (Elaborator.uexp_elab(map, term)) { | DoesNotElaborate => let error = "Internal error: Elaboration returns None"; @@ -7,7 +7,7 @@ let elaborate = (map, term): DHExp.t => InvalidText(-666, -666, error); | Elaborates(d, _, _) => d }; - +}; exception EvalError(EvaluatorError.t); exception PostprocessError(EvaluatorPost.error); let evaluate = diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index f30c1e2e13..358cf46080 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -80,8 +80,10 @@ let of_ctr = (ctx: Ctx.t, name: Constructor.t): t => name, syn_ty: switch (Ctx.lookup_ctr(ctx, name)) { + | Some({kind: Abstract, _}) | None => None - | Some({typ, _}) => Some(typ) + | Some({kind: Singleton(typ), _}) => Some(typ) + | Some({kind: Arrow(_, t2), _}) => Some(t2) }, }); diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 65a0cc0f12..039d86303b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -248,10 +248,49 @@ and uexp_to_info_map = | Let(p, def, body) => let (p_syn, _m) = go_pat(~is_synswitch=true, ~mode=Syn, p, m); let def_ctx = extend_let_def_ctx(ctx, p, p_syn.ctx, def); + let def_ctx = + switch (def.term) { + | Ap(fn, arg) => + switch (fn.term) { + | Constructor(ctr) => + switch (Ctx.lookup_higher_alias(def_ctx, ctr)) { + | Some((name_in, ty_in1)) => + let (ty_in2, _) = go(~mode=Syn, arg, m); + let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); + let ctx' = Ctx.revise_tvar(def_ctx, name_in, ty); + ctx'; + | None => def_ctx + } + | _ => def_ctx + } + | _ => def_ctx + }; let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m); /* Analyze pattern to incorporate def type into ctx */ let (p_ana, m) = go_pat(~is_synswitch=false, ~mode=Ana(def.ty), p, m); - let (body, m) = go'(~ctx=p_ana.ctx, ~mode, body, m); + let (body, m) = + go'( + ~ctx= + switch (def.term.term) { + | Ap(fn, arg) => + switch (fn.term) { + | Constructor(ctr) => + switch (Ctx.lookup_higher_alias(p_ana.ctx, ctr)) { + | Some((name_in, ty_in1)) => + let (ty_in2, _) = go(~mode=Syn, arg, m); + let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); + let ctx' = Ctx.revise_tvar(p_ana.ctx, name_in, ty); + ctx'; + | None => p_ana.ctx + } + | _ => p_ana.ctx + } + | _ => p_ana.ctx + }, + ~mode, + body, + m, + ); add( ~self=Just(body.ty), ~co_ctx= @@ -308,20 +347,16 @@ and uexp_to_info_map = | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) => let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre)); let ctx_def = - Ctx.extend_alias(ctx, name, "", UTPat.rep_id(typat), ty_rec); + Ctx.extend_alias(ctx, name, UTPat.rep_id(typat), ty_rec); (ty_rec, ctx_def, ctx_def); | _ => let ty = UTyp.to_typ(ctx, utyp); - ( - ty, - ctx, - Ctx.extend_alias(ctx, name, "", UTPat.rep_id(typat), ty), - ); + (ty, ctx, Ctx.extend_alias(ctx, name, UTPat.rep_id(typat), ty)); }; }; let ctx_body = switch (Typ.get_sum_constructors(ctx, ty_def)) { - | Some(sm) => Ctx.add_ctrs(ctx_body, name, "", UTyp.rep_id(utyp), sm) + | Some(sm) => Ctx.add_ctrs(ctx_body, name, UTyp.rep_id(utyp), sm) | None => ctx_body }; let ({co_ctx, ty: ty_body, _}: Info.exp, m) = @@ -341,6 +376,7 @@ and uexp_to_info_map = | Var(s) => s | _ => "" }; + let utyp = UTyp.remove_ap_in_def(constructor, arg, utyp); let (ty_def, ctx_def, ctx_body) = { let ty_pre = UTyp.to_typ( @@ -355,7 +391,7 @@ and uexp_to_info_map = let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), constructor, ty_pre)); let ctx_def = - Ctx.extend_alias( + Ctx.extend_higher_alias( ctx, constructor, arg, @@ -364,18 +400,27 @@ and uexp_to_info_map = ); (ty_rec, ctx_def, ctx_def); | _ => - let ty = UTyp.to_typ(ctx, utyp); - ( - ty, - ctx, - Ctx.extend_alias(ctx, constructor, arg, UTPat.rep_id(typat), ty), - ); + let ctx_def = + Ctx.extend_higher_alias( + ctx, + constructor, + arg, + UTPat.rep_id(typat), + ty_pre, + ); + (ty_pre, ctx_def, ctx_def); }; }; let ctx_body = switch (Typ.get_sum_constructors(ctx, ty_def)) { | Some(sm) => - Ctx.add_ctrs(ctx_body, constructor, arg, UTyp.rep_id(utyp), sm) + Ctx.add_higher_ctrs( + ctx_body, + constructor, + arg, + UTyp.rep_id(utyp), + sm, + ) | None => ctx_body }; let ({co_ctx, ty: ty_body, _}: Info.exp, m) = @@ -449,13 +494,7 @@ and upat_to_info_map = Unknown(Internal) is used in this case */ let ctx_typ = Info.fixed_typ_pat(ctx, mode, Common(Just(Unknown(Internal)))); - let entry = - Ctx.VarEntry({ - name, - parameter: "", - id: UPat.rep_id(upat), - typ: ctx_typ, - }); + let entry = Ctx.VarEntry({name, id: UPat.rep_id(upat), typ: ctx_typ}); add(~self=Just(unknown), ~ctx=Ctx.extend(ctx, entry), m); | Tuple(ps) => let modes = Mode.of_prod(ctx, mode, List.length(ps)); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index b762707d40..3609e0d0c5 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -109,46 +109,50 @@ module UTyp = { /* Converts a syntactic type into a semantic type */ let rec to_typ: (Ctx.t, t) => Typ.t = - (ctx, utyp) => - switch (utyp.term) { - | Invalid(_) - | MultiHole(_) => Unknown(Internal) - | EmptyHole => Unknown(TypeHole) - | Bool => Bool - | Int => Int - | Float => Float - | String => String - | Var(name) => - switch (Ctx.lookup_tvar(ctx, name)) { - | Some(_) => Var(name) - | None => Unknown(Free(name)) - } - | Arrow(u1, u2) => Arrow(to_typ(ctx, u1), to_typ(ctx, u2)) - | Tuple(us) => Prod(List.map(to_typ(ctx), us)) - | Sum(uts) => Sum(to_ctr_map(ctx, uts)) - | List(u) => List(to_typ(ctx, u)) - | Parens(u) => to_typ(ctx, u) - /* The below cases should occur only inside sums */ - | Ap(t1, t2) => - let name = - switch (t1.term) { - | Var(s) => s - | _ => "" - }; - switch (Ctx.lookup_tvar(ctx, name)) { - | Some(ty) => - let arg = ty.parameter; - let res_ty = + (ctx, utyp) => { + let res: Typ.t = + switch (utyp.term) { + | Invalid(_) + | MultiHole(_) => Unknown(Internal) + | EmptyHole => Unknown(TypeHole) + | Bool => Bool + | Int => Int + | Float => Float + | String => String + | Var(name) => + switch (Ctx.lookup_tvar(ctx, name)) { + | Some(_) => Var(name) + | None => Unknown(Free(name)) + } + | Arrow(u1, u2) => Arrow(to_typ(ctx, u1), to_typ(ctx, u2)) + | Tuple(us) => Prod(List.map(to_typ(ctx), us)) + | Sum(uts) => Sum(to_ctr_map(ctx, uts)) + | List(u) => List(to_typ(ctx, u)) + | Parens(u) => to_typ(ctx, u) + /* The below cases should occur only inside sums */ + | Ap(t1, t2) => + let name = + switch (t1.term) { + | Var(s) => s + | _ => "" + }; + switch (Ctx.lookup_tvar(ctx, name)) { + | Some(ty) => switch (ty.kind) { - | Arrow(ty_in, ty_out) => Typ.Arrow(ty_in, ty_out) - | Singleton(ty) => ty + | Arrow(ty_in, ty_out) => + switch (ty_in) { + | Var(arg) => Typ.subst(to_typ(ctx, t2), arg, ty_out) + | _ => Unknown(Internal) + } + | Singleton(_) | Abstract => Unknown(Internal) - }; - Typ.subst(to_typ(ctx, t2), arg, res_ty); - | None => Unknown(Free(name)) + } + | None => Unknown(Free(name)) + }; + | Constructor(_) => Unknown(Internal) }; - | Constructor(_) => Unknown(Internal) - } + res; + } and to_variant: (Ctx.t, variant) => option(ConstructorMap.binding(option(Typ.t))) = ctx => @@ -164,6 +168,54 @@ module UTyp = { List.filter_map(to_variant(ctx), uts), ); }; + let rec remove_ap_in_def = (ctr: string, arg: string, ty: t): t => { + let res: term = + switch (ty.term) { + | Invalid(s) => Invalid(s) + | EmptyHole => EmptyHole + | MultiHole(l) => MultiHole(l) + | Int => Int + | Float => Float + | Bool => Bool + | String => String + | List(t) => List(remove_ap_in_def(ctr, arg, t)) + | Var(string) => Var(string) + | Constructor(string) => Constructor(string) + | Arrow(t1, t2) => + Arrow( + remove_ap_in_def(ctr, arg, t1), + remove_ap_in_def(ctr, arg, t2), + ) + | Tuple(lst) => Tuple(List.map(remove_ap_in_def(ctr, arg), lst)) + | Parens(t) => Parens(remove_ap_in_def(ctr, arg, t)) + | Ap(ctr2, arg2) => + let name = + switch (ctr2.term) { + | Var(s) => s + | _ => "" + }; + if (name == ctr) { + Var(ctr); + } else { + Ap( + remove_ap_in_def(ctr, arg, ctr2), + remove_ap_in_def(ctr, arg, arg2), + ); + }; + | Sum(lst) => + let lst = + List.map( + fun + | Variant(a, b, Some(t)) => + Variant(a, b, Some(remove_ap_in_def(ctr, arg, t))) + | Variant(a, b, None) => Variant(a, b, None) + | BadEntry(t) => BadEntry(remove_ap_in_def(ctr, arg, t)), + lst, + ); + Sum(lst); + }; + {term: res, ids: ty.ids}; + }; }; module UTPat = { diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 9c0f134164..e513e0e849 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -33,8 +33,6 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) - | TypeConstructorAp(TypVar.t, t) - and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -93,7 +91,6 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) - | TypeConstructorAp(TypVar.t, t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -160,7 +157,6 @@ module rec Typ: { | Var(_) | Rec(_) | Sum(_) => precedence_Sum - | TypeConstructorAp(_, _) | List(_) => precedence_Const | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow @@ -180,7 +176,6 @@ module rec Typ: { | Rec(y, ty) => Rec(y, subst(s, x, ty)) | List(ty) => List(subst(s, x, ty)) | Var(y) => TypVar.eq(x, y) ? s : Var(y) - | TypeConstructorAp(y, ty) => TypeConstructorAp(y, subst(s, x, ty)) }; }; @@ -217,9 +212,6 @@ module rec Typ: { | (Sum(_), _) => false | (Var(n1), Var(n2)) => n1 == n2 | (Var(_), _) => false - | (TypeConstructorAp(n1, t1), TypeConstructorAp(n2, t2)) => - n1 == n2 && eq(t1, t2) - | (TypeConstructorAp(_), _) => false }; }; @@ -242,7 +234,6 @@ module rec Typ: { ) | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) | Rec(x, ty) => free_vars(~bound=[x, ...bound], ty) - | TypeConstructorAp(_, ty) => free_vars(~bound, ty) }; /* Lattice join on types. This is a LUB join in the hazel2 @@ -328,14 +319,6 @@ module rec Typ: { let+ ty = join'(ty1, ty2); List(ty); | (List(_), _) => None - | (TypeConstructorAp(name1, ty1), TypeConstructorAp(name2, ty2)) => - if (name1 == name2) { - let+ ty = join'(ty1, ty2); - TypeConstructorAp(name1, ty); - } else { - None; - } - | (TypeConstructorAp(_), _) => None }; } and join_sum_entries = @@ -398,8 +381,6 @@ module rec Typ: { as in current implementation Recs do not occur in the surface syntax, so we won't try to jump to them. */ Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) - | TypeConstructorAp(name, ty) => - TypeConstructorAp(name, normalize(ctx, ty)) }; }; @@ -436,7 +417,6 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, - parameter: Var.t, id: Id.t, typ: Typ.t, }; @@ -444,7 +424,6 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type tvar_entry = { name: TypVar.t, - parameter: TypVar.t, id: Id.t, kind: Kind.t, }; @@ -452,7 +431,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type entry = | VarEntry(var_entry) - | ConstructorEntry(var_entry) + | ConstructorEntry(tvar_entry) | TVarEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] @@ -460,24 +439,28 @@ and Ctx: { let extend: (t, entry) => t; let extend_tvar: (t, tvar_entry) => t; - let extend_alias: (t, TypVar.t, TypVar.t, Id.t, Typ.t) => t; + let extend_alias: (t, TypVar.t, Id.t, Typ.t) => t; + let extend_higher_alias: (t, TypVar.t, TypVar.t, Id.t, Typ.t) => t; let extend_dummy_tvar: (t, TypVar.t) => t; let lookup_tvar: (t, TypVar.t) => option(tvar_entry); let lookup_alias: (t, TypVar.t) => option(Typ.t); + let lookup_higher_alias: (t, TypVar.t) => option((TypVar.t, Typ.t)); + let revise_tvar: (t, TypVar.t, Typ.t) => t; let get_id: entry => int; let lookup_var: (t, string) => option(var_entry); - let lookup_ctr: (t, string) => option(var_entry); + let lookup_ctr: (t, string) => option(tvar_entry); let is_alias: (t, TypVar.t) => bool; - let add_ctrs: (t, TypVar.t, TypVar.t, Id.t, Typ.sum_map) => t; + let add_ctrs: (t, TypVar.t, Id.t, Typ.sum_map) => t; + let add_higher_ctrs: (t, TypVar.t, TypVar.t, Id.t, Typ.sum_map) => t; let subtract_prefix: (t, t) => option(t); let added_bindings: (t, t) => t; let filter_duplicates: t => t; let shadows_typ: (t, TypVar.t) => bool; + let find_parameter_type: (TypVar.t, Typ.t, Typ.t) => Typ.t; } = { [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, - parameter: Var.t, id: Id.t, typ: Typ.t, }; @@ -485,7 +468,6 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type tvar_entry = { name: TypVar.t, - parameter: TypVar.t, id: Id.t, kind: Kind.t, }; @@ -493,35 +475,79 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type entry = | VarEntry(var_entry) - | ConstructorEntry(var_entry) + | ConstructorEntry(tvar_entry) | TVarEntry(tvar_entry); + [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); - + let rec find_parameter_type = (name: TypVar.t, t1: Typ.t, t2: Typ.t): Typ.t => { + switch (t1, t2) { + | (Var(n1), ty) when n1 == name => ty + | (Rec(x1, t1), Rec(x2, t2)) => + find_parameter_type(name, t1, Typ.subst(Var(x1), x2, t2)) + | (Rec(_), _) => Unknown(Internal) + | (Int, _) => Unknown(Internal) + | (Float, _) => Unknown(Internal) + | (Bool, _) => Unknown(Internal) + | (String, _) => Unknown(Internal) + | (Unknown(_), _) => Unknown(Internal) + | (Arrow(t1, t2), Arrow(t1', t2')) => + switch (find_parameter_type(name, t1, t1')) { + | Unknown(Internal) => find_parameter_type(name, t2, t2') + | _ => find_parameter_type(name, t1, t1') + } + | (Arrow(_), _) => Unknown(Internal) + | (Prod(tys1), Prod(tys2)) => + switch (ListUtil.map2_opt(find_parameter_type(name), tys1, tys2)) { + | Some(tys) => + List.fold_left( + (a, b) => + if (a == Typ.Unknown(Internal)) { + b; + } else { + a; + }, + Unknown(Internal), + tys, + ) + | _ => Unknown(Internal) + } + | (Prod(_), _) => Unknown(Internal) + | (List(t1), List(t2)) => find_parameter_type(name, t1, t2) + | (List(_), _) => Unknown(Internal) + //| (Sum(sm1), Sum(sm2)) => + | (Sum(_), _) => Unknown(Internal) + | (Var(_), _) => Unknown(Internal) + }; + }; let extend = (ctx, entry) => List.cons(entry, ctx); let extend_tvar = (ctx: t, tvar_entry: tvar_entry): t => extend(ctx, TVarEntry(tvar_entry)); - let extend_alias = - (ctx: t, name: TypVar.t, parameter: TypVar.t, id: Id.t, ty: Typ.t): t => { - let ctx = extend_tvar(ctx, {name, parameter, id, kind: Singleton(ty)}); - if (parameter != "") { - extend_tvar( - ctx, - { - name: parameter, - parameter: "", - id, - kind: Singleton(Unknown(TypeHole)), - }, - ); - } else { - ctx; - }; + + let extend_alias = (ctx: t, name: TypVar.t, id: Id.t, ty: Typ.t): t => + extend_tvar(ctx, {name, id, kind: Singleton(ty)}); + let extend_higher_alias = + (ctx: t, name: TypVar.t, arg: TypVar.t, id: Id.t, ty: Typ.t): t => { + let ctx = extend_tvar(ctx, {name, id, kind: Arrow(Var(arg), ty)}); + extend_tvar(ctx, {name: arg, id, kind: Singleton(Unknown(SynSwitch))}); }; let extend_dummy_tvar = (ctx: t, name: TypVar.t) => - extend_tvar(ctx, {kind: Abstract, name, parameter: "", id: Id.invalid}); - + extend_tvar(ctx, {kind: Abstract, name, id: Id.invalid}); + let revise_tvar = (ctx: t, name: TypVar.t, typ: Typ.t): t => + List.map( + fun + | TVarEntry({name: name', id, _}) when TypVar.eq(name, name') => + TVarEntry({ + name, + id, + kind: { + Singleton(typ); + }, + }) + | entry => entry, + ctx, + ); let lookup_tvar = (ctx: t, name: TypVar.t): option(tvar_entry) => List.find_map( fun @@ -529,11 +555,11 @@ and Ctx: { | _ => None, ctx, ); - let lookup_alias = (ctx: t, t: TypVar.t): option(Typ.t) => switch (lookup_tvar(ctx, t)) { - | Some({kind: Arrow(ty_in, ty_out), _}) => Some(Arrow(ty_in, ty_out)) + | Some({kind: Arrow(_, ty), _}) | Some({kind: Singleton(ty), _}) => Some(ty) + | Some({kind: Abstract, _}) | None => None }; @@ -552,7 +578,7 @@ and Ctx: { ctx, ); - let lookup_ctr = (ctx: t, name: string): option(var_entry) => + let lookup_ctr = (ctx: t, name: string): option(tvar_entry) => List.find_map( fun | ConstructorEntry(t) when t.name == name => Some(t) @@ -565,32 +591,44 @@ and Ctx: { | Some(_) => true | None => false }; + let lookup_higher_alias = (ctx: t, t: TypVar.t): option((TypVar.t, Typ.t)) => + switch (lookup_ctr(ctx, t)) { + | Some({kind: Arrow(Var(arg), Arrow(typ, Var(_))), _}) => + Some((arg, typ)) + | _ => None + }; - let add_ctrs = - ( - ctx: t, - name: TypVar.t, - parameter: TypVar.t, - id: Id.t, - ctrs: Typ.sum_map, - ) - : t => + let add_ctrs = (ctx: t, name: TypVar.t, id: Id.t, ctrs: Typ.sum_map): t => List.map( ((ctr, typ)) => ConstructorEntry({ name: ctr, - parameter, id, - typ: + kind: switch (typ) { - | None => Var(name) - | Some(typ) => Arrow(typ, Var(name)) + | None => Singleton(Var(name)) + | Some(typ) => Singleton(Arrow(typ, Var(name))) + }, + }), + ctrs, + ) + @ ctx; + let add_higher_ctrs = + (ctx: t, name: TypVar.t, arg: TypVar.t, id: Id.t, ctrs: Typ.sum_map): t => + List.map( + ((ctr, typ)) => + ConstructorEntry({ + name: ctr, + id, + kind: + switch (typ) { + | None => Arrow(Var(arg), Var(name)) + | Some(typ) => Arrow(Var(arg), Arrow(typ, Var(name))) }, }), ctrs, ) @ ctx; - let subtract_prefix = (ctx: t, prefix_ctx: t): option(t) => { // NOTE: does not check that the prefix is an actual prefix let prefix_length = List.length(prefix_ctx); @@ -644,13 +682,13 @@ and Ctx: { and Kind: { [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Arrow(Typ.t, Typ.t) | Singleton(Typ.t) + | Arrow(Typ.t, Typ.t) | Abstract; } = { [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Arrow(Typ.t, Typ.t) | Singleton(Typ.t) + | Arrow(Typ.t, Typ.t) | Abstract; }; diff --git a/src/haz3lweb/view/CtxInspector.re b/src/haz3lweb/view/CtxInspector.re index a148f149cc..98d0ea6b40 100644 --- a/src/haz3lweb/view/CtxInspector.re +++ b/src/haz3lweb/view/CtxInspector.re @@ -15,8 +15,7 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { ]), ); switch (entry) { - | VarEntry({name, typ, _}) - | ConstructorEntry({name, typ, _}) => + | VarEntry({name, typ, _}) => div_c( "context-entry", [ @@ -25,6 +24,7 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { Type.view(typ), ], ) + | ConstructorEntry({name, kind, _}) | TVarEntry({name, kind, _}) => div_c( "context-entry", diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 80ba3cbe41..ae88419f0e 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -65,11 +65,6 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => text(")"), ], ) - | TypeConstructorAp(t, ts) => - div( - ~attr=clss(["typ-view", "TypeConstructorAp"]), - [text(t), text("("), view_ty(ts), text(")")], - ) | Sum(ts) => div( ~attr=clss(["typ-view", "Sum"]), diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 3a7972f330..8acbc0455f 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -51,7 +51,6 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | Bool => (text("Bool"), parenthesize) | String => (text("String"), parenthesize) | Var(name) => (text(name), parenthesize) - | TypeConstructorAp(name, _) => (text(name), parenthesize) | List(ty) => ( hcats([ mk_delim("["), From 13a0d20274fa209d964d41a7db7f9bace3bde2a5 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Tue, 22 Aug 2023 14:11:19 -0400 Subject: [PATCH 04/14] Fix: castfailed bug --- src/haz3lcore/dynamics/Evaluator.re | 1 + src/haz3lcore/statics/Statics.re | 68 +++++++++++----------- src/haz3lcore/statics/TypBase.re | 13 ++++- src/haz3lweb/view/Type.re | 1 + src/haz3lweb/view/dhcode/layout/HTypDoc.re | 1 + 5 files changed, 49 insertions(+), 35 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 529ca04260..29f1827111 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -46,6 +46,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Var(_) | Rec(_) | Arrow(Unknown(_), Unknown(_)) + | Parameter(_) => Hole | List(Unknown(_)) => Ground | Prod(tys) => if (List.for_all( diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 039d86303b..7284955ede 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -248,45 +248,45 @@ and uexp_to_info_map = | Let(p, def, body) => let (p_syn, _m) = go_pat(~is_synswitch=true, ~mode=Syn, p, m); let def_ctx = extend_let_def_ctx(ctx, p, p_syn.ctx, def); - let def_ctx = - switch (def.term) { - | Ap(fn, arg) => - switch (fn.term) { - | Constructor(ctr) => - switch (Ctx.lookup_higher_alias(def_ctx, ctr)) { - | Some((name_in, ty_in1)) => - let (ty_in2, _) = go(~mode=Syn, arg, m); - let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); - let ctx' = Ctx.revise_tvar(def_ctx, name_in, ty); - ctx'; - | None => def_ctx - } - | _ => def_ctx - } - | _ => def_ctx - }; + //let def_ctx = + // switch (def.term) { + // | Ap(fn, arg) => + // switch (fn.term) { + // | Constructor(ctr) => + // switch (Ctx.lookup_higher_alias(def_ctx, ctr)) { + // | Some((name_in, ty_in1)) => + // let (ty_in2, _) = go(~mode=Syn, arg, m); + // let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); + // let ctx' = Ctx.revise_tvar(def_ctx, name_in, ty); + // ctx'; + // | None => def_ctx + // } + // | _ => def_ctx + // } + // | _ => def_ctx + // }; let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m); /* Analyze pattern to incorporate def type into ctx */ let (p_ana, m) = go_pat(~is_synswitch=false, ~mode=Ana(def.ty), p, m); let (body, m) = go'( - ~ctx= - switch (def.term.term) { - | Ap(fn, arg) => - switch (fn.term) { - | Constructor(ctr) => - switch (Ctx.lookup_higher_alias(p_ana.ctx, ctr)) { - | Some((name_in, ty_in1)) => - let (ty_in2, _) = go(~mode=Syn, arg, m); - let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); - let ctx' = Ctx.revise_tvar(p_ana.ctx, name_in, ty); - ctx'; - | None => p_ana.ctx - } - | _ => p_ana.ctx - } - | _ => p_ana.ctx - }, + ~ctx=p_ana.ctx, + //switch (def.term.term) { + //| Ap(fn, arg) => + // switch (fn.term) { + // | Constructor(ctr) => + // switch (Ctx.lookup_higher_alias(p_ana.ctx, ctr)) { + // | Some((name_in, ty_in1)) => + // let (ty_in2, _) = go(~mode=Syn, arg, m); + // let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); + // let ctx' = Ctx.revise_tvar(p_ana.ctx, name_in, ty); + // ctx'; + // | None => p_ana.ctx + // } + // | _ => p_ana.ctx + // } + //| _ => p_ana.ctx + //}, ~mode, body, m, diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index e513e0e849..9b04b0fdc2 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -33,6 +33,7 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) + | Parameter(TypVar.t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -91,6 +92,7 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) + | Parameter(TypVar.t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -157,6 +159,7 @@ module rec Typ: { | Var(_) | Rec(_) | Sum(_) => precedence_Sum + | Parameter(_) | List(_) => precedence_Const | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow @@ -176,6 +179,7 @@ module rec Typ: { | Rec(y, ty) => Rec(y, subst(s, x, ty)) | List(ty) => List(subst(s, x, ty)) | Var(y) => TypVar.eq(x, y) ? s : Var(y) + | Parameter(y) => Parameter(y) }; }; @@ -189,6 +193,8 @@ module rec Typ: { but this will change when polymorphic types are implemented */ let rec eq = (t1: t, t2: t): bool => { switch (t1, t2) { + | (_, Parameter(_)) + | (Parameter(_), _) => true | (Rec(x1, t1), Rec(x2, t2)) => eq(t1, subst(Var(x1), x2, t2)) | (Rec(_), _) => false | (Int, Int) => true @@ -234,6 +240,7 @@ module rec Typ: { ) | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) | Rec(x, ty) => free_vars(~bound=[x, ...bound], ty) + | Parameter(v) => List.mem(v, bound) ? [] : [v] }; /* Lattice join on types. This is a LUB join in the hazel2 @@ -254,6 +261,8 @@ module rec Typ: { Some(Unknown(join_type_provenance(p1, p2))) | (Unknown(_), ty) | (ty, Unknown(Internal | SynSwitch)) => Some(ty) + | (Parameter(_), ty) => Some(ty) + | (ty, Parameter(_)) => Some(ty) | (Var(n1), Var(n2)) => if (n1 == n2) { Some(Var(n1)); @@ -381,6 +390,7 @@ module rec Typ: { as in current implementation Recs do not occur in the surface syntax, so we won't try to jump to them. */ Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) + | Parameter(_) => ty }; }; @@ -518,6 +528,7 @@ and Ctx: { //| (Sum(sm1), Sum(sm2)) => | (Sum(_), _) => Unknown(Internal) | (Var(_), _) => Unknown(Internal) + | (Parameter(_), _) => Unknown(Internal) }; }; let extend = (ctx, entry) => List.cons(entry, ctx); @@ -530,7 +541,7 @@ and Ctx: { let extend_higher_alias = (ctx: t, name: TypVar.t, arg: TypVar.t, id: Id.t, ty: Typ.t): t => { let ctx = extend_tvar(ctx, {name, id, kind: Arrow(Var(arg), ty)}); - extend_tvar(ctx, {name: arg, id, kind: Singleton(Unknown(SynSwitch))}); + extend_tvar(ctx, {name: arg, id, kind: Singleton(Parameter(arg))}); }; let extend_dummy_tvar = (ctx: t, name: TypVar.t) => extend_tvar(ctx, {kind: Abstract, name, id: Id.invalid}); diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index ae88419f0e..cc14fc3fd4 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -33,6 +33,7 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => | Float => ty_view("Float", "Float") | String => ty_view("String", "String") | Bool => ty_view("Bool", "Bool") + | Parameter(name) => ty_view("Parameter", name) | Var(name) => ty_view("Var", name) | Rec(x, t) => div( diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 8acbc0455f..7a525ed73f 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -50,6 +50,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | Float => (text("Float"), parenthesize) | Bool => (text("Bool"), parenthesize) | String => (text("String"), parenthesize) + | Parameter(name) | Var(name) => (text(name), parenthesize) | List(ty) => ( hcats([ From 609997d90583d455fe76608a9af6c9fe334c59d7 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Sun, 27 Aug 2023 11:16:29 -0400 Subject: [PATCH 05/14] merge typFun and typAp --- src/haz3lcore/dynamics/DH.re | 13 ++ src/haz3lcore/dynamics/Elaborator.re | 23 +++ src/haz3lcore/dynamics/Evaluator.re | 99 +++++++++++- src/haz3lcore/dynamics/EvaluatorPost.re | 19 ++- src/haz3lcore/dynamics/Substitution.re | 4 + src/haz3lcore/lang/Form.re | 4 + src/haz3lcore/statics/Info.re | 24 ++- src/haz3lcore/statics/Mode.re | 20 ++- src/haz3lcore/statics/Self.re | 4 +- src/haz3lcore/statics/TypBase.re | 161 ++++++++++--------- src/haz3lweb/view/CtxInspector.re | 2 +- src/haz3lweb/view/LangDoc.re | 29 ++++ src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 13 +- src/haz3lweb/view/dhcode/layout/HTypDoc.re | 14 +- 14 files changed, 328 insertions(+), 101 deletions(-) diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re index 61d7483930..0813e4c49a 100644 --- a/src/haz3lcore/dynamics/DH.re +++ b/src/haz3lcore/dynamics/DH.re @@ -16,6 +16,8 @@ module rec DHExp: { | FixF(Var.t, Typ.t, t) | Fun(DHPat.t, Typ.t, t, option(Var.t)) | Ap(t, t) + | TypFun(Term.UTPat.t, t) + | TypAp(t, Typ.t) | ApBuiltin(string, list(t)) | TestLit(KeywordID.t) | BoolLit(bool) @@ -70,6 +72,8 @@ module rec DHExp: { | FixF(Var.t, Typ.t, t) | Fun(DHPat.t, Typ.t, t, option(Var.t)) | Ap(t, t) + | TypFun(Term.UTPat.t, t) + | TypAp(t, Typ.t) | ApBuiltin(string, list(t)) | TestLit(KeywordID.t) | BoolLit(bool) @@ -109,6 +113,8 @@ module rec DHExp: { | Fun(_, _, _, _) => "Fun" | Closure(_, _) => "Closure" | Ap(_, _) => "Ap" + | TypFun(_, _) => "TypFun" + | TypAp(_) => "TypAp" | ApBuiltin(_, _) => "ApBuiltin" | TestLit(_) => "TestLit" | BoolLit(_) => "BoolLit" @@ -164,6 +170,8 @@ module rec DHExp: { | 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)) + | TypFun(a, b) => TypFun(a, strip_casts(b)) + | TypAp(a, b) => TypAp(strip_casts(a), b) | ApBuiltin(fn, args) => ApBuiltin(fn, List.map(strip_casts, args)) | BinBoolOp(a, b, c) => BinBoolOp(a, strip_casts(b), strip_casts(c)) | BinIntOp(a, b, c) => BinIntOp(a, strip_casts(b), strip_casts(c)) @@ -216,6 +224,9 @@ module rec DHExp: { f1 == f2 && ty1 == ty2 && fast_equal(d1, d2) | (Fun(dp1, ty1, d1, s1), Fun(dp2, ty2, d2, s2)) => dp1 == dp2 && ty1 == ty2 && fast_equal(d1, d2) && s1 == s2 + | (TypFun(ty1, d1), TypFun(ty2, d2)) => + ty1 == ty2 && fast_equal(d1, d2) + | (TypAp(d1, ty1), TypAp(d2, ty2)) => fast_equal(d1, d2) && ty1 == ty2 | (Ap(d11, d21), Ap(d12, d22)) | (Cons(d11, d21), Cons(d12, d22)) => fast_equal(d11, d12) && fast_equal(d21, d22) @@ -251,6 +262,8 @@ module rec DHExp: { | (FixF(_), _) | (Fun(_), _) | (Ap(_), _) + | (TypFun(_), _) + | (TypAp(_), _) | (ApBuiltin(_), _) | (Cons(_), _) | (ListConcat(_), _) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 9911b37710..ae0c5840ec 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -37,6 +37,14 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => | Arrow(_) => d | _ => failwith("Elaborator.wrap: SynFun non-arrow-type") } + | SynTypFun => + switch (self_ty) { + | Unknown(prov) => + /* ? |> forall _. ? */ + DHExp.cast(d, Unknown(prov), Forall("_", Unknown(prov))) + | Forall(_) => d + | _ => failwith("Elaborator.wrap: SynTypFun non-forall-type") + } | Ana(ana_ty) => let ana_ty = Typ.normalize(ctx, ana_ty); /* Forms with special ana rules get cast from their appropriate Matched types */ @@ -53,6 +61,12 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => let (_, ana_out) = Typ.matched_arrow(ana_ty); let (self_in, _) = Typ.matched_arrow(self_ty); DHExp.cast(d, Arrow(self_in, ana_out), ana_ty); + | TypFun(_) => + switch (ana_ty) { + | Unknown(prov) => + DHExp.cast(d, Forall("grounded_forall", Unknown(prov)), ana_ty) + | _ => d + } | Tuple(ds) => switch (ana_ty) { | Unknown(prov) => @@ -61,6 +75,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => | _ => d } | Ap(Constructor(_), _) + | TypAp(Constructor(_), _) | Constructor(_) => switch (ana_ty, self_ty) { | (Unknown(prov), Rec(_, Sum(_))) @@ -97,6 +112,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => | BinIntOp(_) | BinFloatOp(_) | BinStringOp(_) + | TypAp(_) | TestLit(_) => DHExp.cast(d, self_ty, ana_ty) }; }; @@ -145,6 +161,10 @@ let rec dhexp_of_uexp = let* d1 = dhexp_of_uexp(m, body); let+ ty = fixed_pat_typ(m, p); DHExp.Fun(dp, ty, d1, None); + | TypFun(tpat, body) => + // TODO (typfun) + let+ d1 = dhexp_of_uexp(m, body); + DHExp.TypFun(tpat, d1); | Tuple(es) => let+ ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence; DHExp.Tuple(ds); @@ -241,6 +261,9 @@ let rec dhexp_of_uexp = let* c_fn = dhexp_of_uexp(m, fn); let+ c_arg = dhexp_of_uexp(m, arg); DHExp.Ap(c_fn, c_arg); + | TypAp(fn, uty_arg) => + let+ d_fn = dhexp_of_uexp(m, fn); + DHExp.TypAp(d_fn, Term.UTyp.to_typ(ctx, uty_arg)); | If(scrut, e1, e2) => let* d_scrut = dhexp_of_uexp(m, scrut); let* d1 = dhexp_of_uexp(m, e1); diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 29f1827111..7f82fed3ad 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -30,7 +30,10 @@ let grounded_Sum = (sm: Typ.sum_map): ground_cases => { NotGroundOrHole(Sum(sm')); }; let grounded_List = NotGroundOrHole(List(Unknown(Internal))); - +let grounded_Forall = + NotGroundOrHole(Forall("grounded_forall", Unknown(Internal))); +let grounded_Ap = + NotGroundOrHole(Ap(Unknown(Internal), Unknown(Internal))); let rec ground_cases_of = (ty: Typ.t): ground_cases => { let is_ground_arg: option(Typ.t) => bool = fun @@ -46,7 +49,6 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Var(_) | Rec(_) | Arrow(Unknown(_), Unknown(_)) - | Parameter(_) => Hole | List(Unknown(_)) => Ground | Prod(tys) => if (List.for_all( @@ -63,6 +65,8 @@ 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 + | Forall(_) => grounded_Forall + | Ap(_) => grounded_Ap }; }; @@ -299,6 +303,7 @@ and matches_cast_Sum = | InvalidText(_) | Let(_) | Ap(_) + | TypAp(_) | ApBuiltin(_) | BinBoolOp(_) | BinIntOp(_) @@ -313,6 +318,7 @@ and matches_cast_Sum = | BoundVar(_) | FixF(_) | Fun(_) + | TypFun(_) | BoolLit(_) | IntLit(_) | FloatLit(_) @@ -390,7 +396,9 @@ and matches_cast_Tuple = | Let(_, _, _) => IndetMatch | FixF(_, _, _) => DoesNotMatch | Fun(_, _, _, _) => DoesNotMatch - | Closure(_, Fun(_)) => DoesNotMatch + | TypFun(_) => DoesNotMatch + | TypAp(_) => DoesNotMatch + | Closure(_, Fun(_) | TypFun(_)) => DoesNotMatch | Closure(_, _) => IndetMatch | Ap(_, _) => IndetMatch | ApBuiltin(_, _) => IndetMatch @@ -527,6 +535,8 @@ and matches_cast_Cons = | Let(_, _, _) => IndetMatch | FixF(_, _, _) => DoesNotMatch | Fun(_, _, _, _) => DoesNotMatch + | TypFun(_) => DoesNotMatch + | TypAp(_) => DoesNotMatch | Closure(_, d') => matches_cast_Cons(dp, d', elt_casts) | Ap(_, _) => IndetMatch | ApBuiltin(_, _) => IndetMatch @@ -621,6 +631,67 @@ let eval_bin_string_op = | Equals => BoolLit(s1 == s2) }; +let rec ty_subst = + (str, exp, targ) + : DHExp.t /* TODO: Maybe just keep error instead of recursing? */ => { + open DH.DHExp; + let re = e2 => ty_subst(str, e2, targ); + switch (exp) { + | Cast(t, t1, t2) => + Cast(re(t), Typ.subst(targ, str, t1), Typ.subst(targ, str, t2)) + | FixF(arg, ty, body) => FixF(arg, Typ.subst(targ, str, ty), re(body)) + | Fun(arg, ty, body, var) => + Fun(arg, Typ.subst(targ, str, ty), re(body), var) + | TypAp(tfun, ty) => TypAp(re(tfun), Typ.subst(targ, str, ty)) + | ListLit(mv, mvi, t, lst) => + ListLit(mv, mvi, Typ.subst(targ, str, t), List.map(re, lst)) + + | TypFun(utpat, body) => TypFun(utpat, ty_subst(str, body, targ)) + + | NonEmptyHole(errstat, mv, hid, t) => + NonEmptyHole(errstat, mv, hid, re(t)) + | InconsistentBranches(mv, hid, case) => + InconsistentBranches(mv, hid, ty_subst_case(str, case, targ)) + | 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)) + | Ap(t1, t2) => Ap(re(t1), re(t2)) + | ApBuiltin(s, args) => ApBuiltin(s, List.map(re, args)) + | BinBoolOp(op, t1, t2) => BinBoolOp(op, re(t1), re(t2)) + | BinIntOp(op, t1, t2) => BinIntOp(op, re(t1), re(t2)) + | BinFloatOp(op, t1, t2) => BinFloatOp(op, re(t1), re(t2)) + | BinStringOp(op, t1, t2) => BinStringOp(op, re(t1), re(t2)) + | Cons(t1, t2) => Cons(re(t1), re(t2)) + | Tuple(args) => Tuple(List.map(re, args)) + | Prj(t, n) => Prj(re(t), n) + | ConsistentCase(case) => ConsistentCase(ty_subst_case(str, case, targ)) + | InvalidOperation(t, err) => InvalidOperation(re(t), err) + | ListConcat(t1, t2) => ListConcat(re(t1), re(t2)) + | Constructor(_) + | EmptyHole(_) + | ExpandingKeyword(_, _, _) + | FreeVar(_, _, _) + | InvalidText(_, _, _) + | BoundVar(_) + | TestLit(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) + | FailedCast(_, _, _) => exp + }; +} //TODO: is this correct? +//TODO: Inconsistent cases: need to check again for inconsistency? + +and ty_subst_case = (str, Case(t, rules, n), targ) => + Case( + ty_subst(str, t, targ), + List.map( + (DHExp.Rule(dhpat, t)) => DHExp.Rule(dhpat, ty_subst(str, t, targ)), + rules, + ), + n, + ); let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = (env, d) => { /* Increment number of evaluation steps (calls to `evaluate`). */ @@ -673,7 +744,28 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = evaluate(env', d'); | Fun(_) => BoxedValue(Closure(env, d)) |> return + | TypFun(_) => BoxedValue(Closure(env, d)) |> return + | TypAp(d1, tau) => + let* r1 = evaluate(env, d1); + switch (r1) { + | BoxedValue(Closure(closure_env, TypFun({term: Var(name), _}, d2))) => + // TODO: Maybe additional cases to be done? + evaluate(closure_env, ty_subst(name, d2, tau)) + | BoxedValue(Constructor(name)) => evaluate(env, Constructor(name)) + | BoxedValue(Cast(d1', Forall("_", t), Forall("_", t'))) + | Indet(Cast(d1', Forall("_", t), Forall("_", t'))) => + evaluate( + env, + Cast( + TypAp(d1', tau), + Typ.subst(t, "_", tau), + Typ.subst(t', "_", tau), + ), + ) + | Indet(_) => r1 |> return + | _ => failwith("InvalidBoxedTypFun: " ++ show(r1)) + }; | Ap(d1, d2) => let* r1 = evaluate(env, d1); switch (r1) { @@ -980,6 +1072,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = | Closure(_, d') => switch (d') { | Fun(_) => BoxedValue(d) |> return + | TypFun(_) => BoxedValue(d) |> return | _ => Indet(d) |> return } diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re index 18d4ea2b44..2cfe38b7ce 100644 --- a/src/haz3lcore/dynamics/EvaluatorPost.re +++ b/src/haz3lcore/dynamics/EvaluatorPost.re @@ -69,7 +69,9 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) => let* d1' = pp_eval(d1); let* d2' = pp_eval(d2); Ap(d1', d2') |> return; - + | TypAp(d1, ty) => + let* d1' = pp_eval(d1); + TypAp(d1', ty) |> return; | ApBuiltin(f, args) => let* args' = args |> List.map(pp_eval) |> sequence; ApBuiltin(f, args') |> return; @@ -151,6 +153,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) => | Let(_) | ConsistentCase(_) | Fun(_) + | TypFun(_) | EmptyHole(_) | NonEmptyHole(_) | ExpandingKeyword(_) @@ -175,7 +178,9 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) => | Fun(dp, ty, d, s) => let* d = pp_uneval(env, d); Fun(dp, ty, d, s) |> return; - + | TypFun(tpat, d1) => + let* d1' = pp_uneval(env, d1); + TypFun(tpat, d1') |> return; | Let(dp, d1, d2) => /* d1 should already be evaluated, d2 is not */ let* d1 = pp_eval(d1); @@ -291,12 +296,16 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) => | Fun(dp, ty, d', s) => let* d'' = pp_uneval(env, d'); Fun(dp, ty, d'', s) |> return; - + | TypFun(tpat, d1) => + let* d1' = pp_uneval(env, d1); + TypFun(tpat, d1') |> return; | Ap(d1, d2) => let* d1' = pp_uneval(env, d1); let* d2' = pp_uneval(env, d2); Ap(d1', d2') |> return; - + | TypAp(d1, ty) => + let* d1' = pp_uneval(env, d1); + TypAp(d1', ty) |> return; | ApBuiltin(f, args) => let* args' = args |> List.map(pp_uneval(env)) |> sequence; ApBuiltin(f, args') |> return; @@ -449,6 +458,8 @@ let rec track_children_of_hole = | BoundVar(_) => hii | FixF(_, _, d) | Fun(_, _, d, _) + | TypFun(_, d) + | TypAp(d, _) | Prj(d, _) | Cast(d, _, _) | FailedCast(d, _, _) diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index 92f8cff0fe..4b1e4ae2fc 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -38,6 +38,8 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => let d3 = subst_var(d1, x, d3); Fun(dp, ty, d3, s); } + | TypFun(tpat, d3) => TypFun(tpat, subst_var(d1, x, d3)) + | Closure(env, d3) => /* Closure shouldn't appear during substitution (which only is called from elaboration currently) */ @@ -48,6 +50,8 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => let d3 = subst_var(d1, x, d3); let d4 = subst_var(d1, x, d4); Ap(d3, d4); + | TypAp(d3, ty) => TypAp(subst_var(d1, x, d3), ty) + | ApBuiltin(ident, args) => let args = List.map(subst_var(d1, x), args); ApBuiltin(ident, args); diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 9303fb4e17..3cf1699707 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -254,11 +254,15 @@ let forms: list((string, t)) = [ ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))), ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))), ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))), + ("typfun", mk(ds, ["typfun", "->"], mk_pre(P.fun_, Exp, [TPat]))), + ("forall", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [TPat]))), ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))), ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))), ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))), ("ap_tpat", mk(ii, ["(", ")"], mk_post(P.ap, TPat, [TPat]))), ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))), + ("ap_exp_typ", mk(ii, ["@<", ">"], mk_post(P.ap, Exp, [Typ]))), + ("at_sign", mk_nul_infix("@", P.eqs)), // HACK: SUBSTRING REQ ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), ( "type_alias", diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 1ef074e068..cd49f4529d 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -272,6 +272,13 @@ let rec status_common = | None => InHole(Inconsistent(WithArrow(syn))) | Some(_) => NotInHole(Syn(syn)) } + | (Just(ty), SynTypFun) => + /* Use ty first to preserve name if it exists. */ + switch (Typ.join_fix(ctx, ty, Forall("_", Unknown(Internal)))) { + | Some(_) => NotInHole(Syn(ty)) + | None => InHole(Inconsistent(WithArrow(ty))) + } + | (IsConstructor({name, syn_ty}), _) => /* If a ctr is being analyzed against (an arrow type returning) a sum type having that ctr as a variant, its self type is @@ -293,13 +300,13 @@ let rec status_common = Ana(InternallyInconsistent({ana, nojoin: Typ.of_source(tys)})), ) }; - | (NoJoin(_, tys), Syn | SynFun) => + | (NoJoin(_, tys), Syn | SynFun | SynTypFun) => InHole(Inconsistent(Internal(Typ.of_source(tys)))) }; -let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => +let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => { switch (mode, self) { - | (Syn | Ana(_), Common(self_pat)) + | (SynTypFun | Syn | Ana(_), Common(self_pat)) | (SynFun, Common(IsConstructor(_) as self_pat)) => /* Little bit of a hack. Anything other than a bound ctr will, in function position, have SynFun mode (see Typ.ap_mode). Since we @@ -313,7 +320,7 @@ let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => } | (SynFun, _) => InHole(ExpectedConstructor) }; - +}; /* Determines whether an expression or pattern is in an error hole, depending on the mode, which represents the expectations of the surrounding syntactic context, and the self which represents the @@ -352,7 +359,12 @@ let status_typ = InHole(DuplicateConstructor(name)) | TypeExpected => switch (Ctx.is_alias(ctx, name)) { - | false => InHole(FreeTypeVariable(name)) + | false => + switch (Ctx.is_tyVar(ctx, name)) { + | false => InHole(FreeTypeVariable(name)) + | true => + NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty))) + } | true => NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty))) } } @@ -372,7 +384,7 @@ let status_typ = | Var(s) => s | _ => "" }; - switch (Ctx.is_alias(ctx, constructor)) { + switch (Ctx.is_tyVar(ctx, constructor)) { | false => InHole(FreeTypeVariable(constructor)) | true => NotInHole(TypeAlias(constructor, Typ.weak_head_normalize(ctx, ty))) diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index 58594f928d..e75371b721 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -20,6 +20,7 @@ open OptUtil.Syntax; [@deriving (show({with_path: false}), sexp, yojson)] type t = | SynFun /* Used only in function position of applications */ + | SynTypFun | Syn | Ana(Typ.t); @@ -30,11 +31,13 @@ let ty_of: t => Typ.t = fun | Ana(ty) => ty | Syn => Unknown(SynSwitch) - | SynFun => Arrow(Unknown(SynSwitch), Unknown(SynSwitch)); + | SynFun + | SynTypFun => Arrow(Unknown(SynSwitch), Unknown(SynSwitch)); let of_arrow = (ctx: Ctx.t, mode: t): (t, t) => switch (mode) { | Syn + | SynTypFun | SynFun => (Syn, Syn) | Ana(ty) => ty @@ -42,10 +45,19 @@ let of_arrow = (ctx: Ctx.t, mode: t): (t, t) => |> Typ.matched_arrow |> TupleUtil.map2(ana) }; - +let of_forall: t => t = + fun + | SynFun + | SynTypFun + | Syn => Syn + | Ana(ty) => { + let (_, body) = Typ.matched_forall(ty); + Ana(body); + }; let of_prod = (ctx: Ctx.t, mode: t, length): list(t) => switch (mode) { | Syn + | SynTypFun | SynFun => List.init(length, _ => Syn) | Ana(ty) => ty @@ -60,6 +72,7 @@ let matched_list_normalize = (ctx: Ctx.t, ty: Typ.t): Typ.t => let of_cons_hd = (ctx: Ctx.t, mode: t): t => switch (mode) { | Syn + | SynTypFun | SynFun => Syn | Ana(ty) => Ana(matched_list_normalize(ctx, ty)) }; @@ -67,6 +80,7 @@ let of_cons_hd = (ctx: Ctx.t, mode: t): t => let of_cons_tl = (ctx: Ctx.t, mode: t, hd_ty: Typ.t): t => switch (mode) { | Syn + | SynTypFun | SynFun => Ana(List(hd_ty)) | Ana(ty) => Ana(List(matched_list_normalize(ctx, ty))) }; @@ -74,6 +88,7 @@ let of_cons_tl = (ctx: Ctx.t, mode: t, hd_ty: Typ.t): t => let of_list = (ctx: Ctx.t, mode: t): t => switch (mode) { | Syn + | SynTypFun | SynFun => Syn | Ana(ty) => Ana(matched_list_normalize(ctx, ty)) }; @@ -81,6 +96,7 @@ let of_list = (ctx: Ctx.t, mode: t): t => let of_list_concat = (mode: t): t => switch (mode) { | Syn + | SynTypFun | SynFun => Ana(List(Unknown(SynSwitch))) | Ana(ty) => Ana(List(Typ.matched_list(ty))) }; diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re index 358cf46080..f30c1e2e13 100644 --- a/src/haz3lcore/statics/Self.re +++ b/src/haz3lcore/statics/Self.re @@ -80,10 +80,8 @@ let of_ctr = (ctx: Ctx.t, name: Constructor.t): t => name, syn_ty: switch (Ctx.lookup_ctr(ctx, name)) { - | Some({kind: Abstract, _}) | None => None - | Some({kind: Singleton(typ), _}) => Some(typ) - | Some({kind: Arrow(_, t2), _}) => Some(t2) + | Some({typ, _}) => Some(typ) }, }); diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 9b04b0fdc2..197bfa6b65 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -33,7 +33,8 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) - | Parameter(TypVar.t) + | Forall(TypVar.t, t) + | Ap(t, t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -52,6 +53,7 @@ module rec Typ: { let of_source: list(source) => list(t); let join_type_provenance: (type_provenance, type_provenance) => type_provenance; + let matched_forall: t => (TypVar.t, t); let matched_arrow: t => (t, t); let matched_prod: (int, t) => list(t); let matched_cons: t => (t, t); @@ -92,7 +94,8 @@ module rec Typ: { | Sum(sum_map) | Prod(list(t)) | Rec(TypVar.t, t) - | Parameter(TypVar.t) + | Forall(TypVar.t, t) + | Ap(t, t) and sum_map = ConstructorMap.t(option(t)); [@deriving (show({with_path: false}), sexp, yojson)] @@ -123,7 +126,11 @@ module rec Typ: { | (_, Internal | Free(_)) => Internal | (SynSwitch, SynSwitch) => SynSwitch }; - + let matched_forall: t => (TypVar.t, t) = + fun + | Forall(name, ty) => (name, ty) + | Unknown(prov) => ("expected_forall", Unknown(prov)) + | _ => ("expected_forall", Unknown(Internal)); let matched_arrow: t => (t, t) = fun | Arrow(ty_in, ty_out) => (ty_in, ty_out) @@ -159,7 +166,8 @@ module rec Typ: { | Var(_) | Rec(_) | Sum(_) => precedence_Sum - | Parameter(_) + | Forall(_, _) + | Ap(_, _) | List(_) => precedence_Const | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow @@ -179,7 +187,9 @@ module rec Typ: { | Rec(y, ty) => Rec(y, subst(s, x, ty)) | List(ty) => List(subst(s, x, ty)) | Var(y) => TypVar.eq(x, y) ? s : Var(y) - | Parameter(y) => Parameter(y) + | Forall(y, ty) when TypVar.eq(x, y) => Forall(y, ty) + | Forall(y, ty) => Forall(y, subst(s, x, ty)) + | Ap(ty1, ty2) => Ap(subst(s, x, ty1), subst(s, x, ty2)) }; }; @@ -193,8 +203,6 @@ module rec Typ: { but this will change when polymorphic types are implemented */ let rec eq = (t1: t, t2: t): bool => { switch (t1, t2) { - | (_, Parameter(_)) - | (Parameter(_), _) => true | (Rec(x1, t1), Rec(x2, t2)) => eq(t1, subst(Var(x1), x2, t2)) | (Rec(_), _) => false | (Int, Int) => true @@ -218,6 +226,10 @@ module rec Typ: { | (Sum(_), _) => false | (Var(n1), Var(n2)) => n1 == n2 | (Var(_), _) => false + | (Forall(x1, t1), Forall(x2, t2)) => eq(t1, subst(Var(x1), x2, t2)) + | (Forall(_), _) => false + | (Ap(t1, t2), Ap(t1', t2')) => eq(t1, t1') && eq(t2, t2') + | (Ap(_), _) => false }; }; @@ -240,7 +252,8 @@ module rec Typ: { ) | Prod(tys) => ListUtil.flat_map(free_vars(~bound), tys) | Rec(x, ty) => free_vars(~bound=[x, ...bound], ty) - | Parameter(v) => List.mem(v, bound) ? [] : [v] + | Forall(x, ty) => free_vars(~bound=[x, ...bound], ty) + | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2) }; /* Lattice join on types. This is a LUB join in the hazel2 @@ -261,8 +274,6 @@ module rec Typ: { Some(Unknown(join_type_provenance(p1, p2))) | (Unknown(_), ty) | (ty, Unknown(Internal | SynSwitch)) => Some(ty) - | (Parameter(_), ty) => Some(ty) - | (ty, Parameter(_)) => Some(ty) | (Var(n1), Var(n2)) => if (n1 == n2) { Some(Var(n1)); @@ -278,6 +289,27 @@ module rec Typ: { let+ ty_join = join'(ty_name, ty); !resolve && eq(ty_name, ty_join) ? Var(name) : ty_join; /* Note: Ordering of Unknown, Var, and Rec above is load-bearing! */ + | (ty2, Ap(Var(name), ty)) + | (Ap(Var(name), ty), ty2) => + switch (Ctx.lookup_higher_kind(ctx, name)) { + | Some((arg, ty_out)) => join'(subst(ty, arg, ty_out), ty2) + + | _ => None + } + | (ty, Ap(Forall(name, t1), t2)) + | (Ap(Forall(name, t1), t2), ty) => + join(~resolve, ~fix, ctx, Typ.subst(t2, name, t1), ty) + | (Ap(ty1, ty2), Ap(ty1', ty2')) => + let* ty1 = join'(ty1, ty1'); + let+ ty2 = join'(ty2, ty2'); + Ap(ty1, ty2); + | (Ap(_), _) => None + | (Forall(name, t1), Forall(_, t2)) => + switch (join(~resolve, ~fix, Ctx.extend_dummy_tvar(ctx, name), t1, t2)) { + | Some(t) => Some(Forall(name, t)) + | None => None + } + | (Forall(_), _) => None | (Rec(x1, ty1), Rec(x2, ty2)) => /* TODO: This code isn't fully correct, as we may be doing @@ -390,7 +422,9 @@ module rec Typ: { as in current implementation Recs do not occur in the surface syntax, so we won't try to jump to them. */ Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) - | Parameter(_) => ty + | Forall(name, ty) => + Forall(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) + | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) }; }; @@ -441,7 +475,7 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type entry = | VarEntry(var_entry) - | ConstructorEntry(tvar_entry) + | ConstructorEntry(var_entry) | TVarEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] @@ -450,23 +484,24 @@ and Ctx: { let extend: (t, entry) => t; let extend_tvar: (t, tvar_entry) => t; let extend_alias: (t, TypVar.t, Id.t, Typ.t) => t; - let extend_higher_alias: (t, TypVar.t, TypVar.t, Id.t, Typ.t) => t; + let extend_higher_kind: (t, TypVar.t, TypVar.t, Id.t, Typ.t) => t; let extend_dummy_tvar: (t, TypVar.t) => t; let lookup_tvar: (t, TypVar.t) => option(tvar_entry); let lookup_alias: (t, TypVar.t) => option(Typ.t); - let lookup_higher_alias: (t, TypVar.t) => option((TypVar.t, Typ.t)); + let lookup_higher_kind: (t, TypVar.t) => option((TypVar.t, Typ.t)); let revise_tvar: (t, TypVar.t, Typ.t) => t; let get_id: entry => int; let lookup_var: (t, string) => option(var_entry); - let lookup_ctr: (t, string) => option(tvar_entry); + let lookup_ctr: (t, string) => option(var_entry); let is_alias: (t, TypVar.t) => bool; + let is_tyVar: (t, TypVar.t) => bool; let add_ctrs: (t, TypVar.t, Id.t, Typ.sum_map) => t; - let add_higher_ctrs: (t, TypVar.t, TypVar.t, Id.t, Typ.sum_map) => t; + let add_ctr_with_typ_parameter: + (t, TypVar.t, Id.t, Typ.sum_map, TypVar.t) => t; let subtract_prefix: (t, t) => option(t); let added_bindings: (t, t) => t; let filter_duplicates: t => t; let shadows_typ: (t, TypVar.t) => bool; - let find_parameter_type: (TypVar.t, Typ.t, Typ.t) => Typ.t; } = { [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { @@ -485,52 +520,11 @@ and Ctx: { [@deriving (show({with_path: false}), sexp, yojson)] type entry = | VarEntry(var_entry) - | ConstructorEntry(tvar_entry) + | ConstructorEntry(var_entry) | TVarEntry(tvar_entry); [@deriving (show({with_path: false}), sexp, yojson)] type t = list(entry); - let rec find_parameter_type = (name: TypVar.t, t1: Typ.t, t2: Typ.t): Typ.t => { - switch (t1, t2) { - | (Var(n1), ty) when n1 == name => ty - | (Rec(x1, t1), Rec(x2, t2)) => - find_parameter_type(name, t1, Typ.subst(Var(x1), x2, t2)) - | (Rec(_), _) => Unknown(Internal) - | (Int, _) => Unknown(Internal) - | (Float, _) => Unknown(Internal) - | (Bool, _) => Unknown(Internal) - | (String, _) => Unknown(Internal) - | (Unknown(_), _) => Unknown(Internal) - | (Arrow(t1, t2), Arrow(t1', t2')) => - switch (find_parameter_type(name, t1, t1')) { - | Unknown(Internal) => find_parameter_type(name, t2, t2') - | _ => find_parameter_type(name, t1, t1') - } - | (Arrow(_), _) => Unknown(Internal) - | (Prod(tys1), Prod(tys2)) => - switch (ListUtil.map2_opt(find_parameter_type(name), tys1, tys2)) { - | Some(tys) => - List.fold_left( - (a, b) => - if (a == Typ.Unknown(Internal)) { - b; - } else { - a; - }, - Unknown(Internal), - tys, - ) - | _ => Unknown(Internal) - } - | (Prod(_), _) => Unknown(Internal) - | (List(t1), List(t2)) => find_parameter_type(name, t1, t2) - | (List(_), _) => Unknown(Internal) - //| (Sum(sm1), Sum(sm2)) => - | (Sum(_), _) => Unknown(Internal) - | (Var(_), _) => Unknown(Internal) - | (Parameter(_), _) => Unknown(Internal) - }; - }; let extend = (ctx, entry) => List.cons(entry, ctx); let extend_tvar = (ctx: t, tvar_entry: tvar_entry): t => @@ -538,10 +532,14 @@ and Ctx: { let extend_alias = (ctx: t, name: TypVar.t, id: Id.t, ty: Typ.t): t => extend_tvar(ctx, {name, id, kind: Singleton(ty)}); - let extend_higher_alias = + let extend_higher_kind = (ctx: t, name: TypVar.t, arg: TypVar.t, id: Id.t, ty: Typ.t): t => { - let ctx = extend_tvar(ctx, {name, id, kind: Arrow(Var(arg), ty)}); - extend_tvar(ctx, {name: arg, id, kind: Singleton(Parameter(arg))}); + let ctx = + extend_tvar( + ctx, + {name, id, kind: Arrow(Singleton(Var(arg)), Singleton(ty))}, + ); + extend_tvar(ctx, {name: arg, id, kind: Abstract}); }; let extend_dummy_tvar = (ctx: t, name: TypVar.t) => extend_tvar(ctx, {kind: Abstract, name, id: Id.invalid}); @@ -568,11 +566,8 @@ and Ctx: { ); let lookup_alias = (ctx: t, t: TypVar.t): option(Typ.t) => switch (lookup_tvar(ctx, t)) { - | Some({kind: Arrow(_, ty), _}) | Some({kind: Singleton(ty), _}) => Some(ty) - - | Some({kind: Abstract, _}) - | None => None + | _ => None }; let get_id: entry => int = @@ -589,7 +584,7 @@ and Ctx: { ctx, ); - let lookup_ctr = (ctx: t, name: string): option(tvar_entry) => + let lookup_ctr = (ctx: t, name: string): option(var_entry) => List.find_map( fun | ConstructorEntry(t) when t.name == name => Some(t) @@ -602,9 +597,14 @@ and Ctx: { | Some(_) => true | None => false }; - let lookup_higher_alias = (ctx: t, t: TypVar.t): option((TypVar.t, Typ.t)) => - switch (lookup_ctr(ctx, t)) { - | Some({kind: Arrow(Var(arg), Arrow(typ, Var(_))), _}) => + let is_tyVar = (ctx: t, name: TypVar.t): bool => + switch (lookup_tvar(ctx, name)) { + | Some(_) => true + | _ => false + }; + let lookup_higher_kind = (ctx: t, t: TypVar.t): option((TypVar.t, Typ.t)) => + switch (lookup_tvar(ctx, t)) { + | Some({kind: Arrow(Singleton(Var(arg)), Singleton(typ)), _}) => Some((arg, typ)) | _ => None }; @@ -615,26 +615,27 @@ and Ctx: { ConstructorEntry({ name: ctr, id, - kind: + typ: switch (typ) { - | None => Singleton(Var(name)) - | Some(typ) => Singleton(Arrow(typ, Var(name))) + | None => Var(name) + | Some(typ) => Arrow(typ, Var(name)) }, }), ctrs, ) @ ctx; - let add_higher_ctrs = - (ctx: t, name: TypVar.t, arg: TypVar.t, id: Id.t, ctrs: Typ.sum_map): t => + let add_ctr_with_typ_parameter = + (ctx: t, name: TypVar.t, id: Id.t, ctrs: Typ.sum_map, arg: TypVar.t): t => List.map( ((ctr, typ)) => ConstructorEntry({ name: ctr, id, - kind: + typ: switch (typ) { - | None => Arrow(Var(arg), Var(name)) - | Some(typ) => Arrow(Var(arg), Arrow(typ, Var(name))) + | None => Forall(arg, Ap(Var(name), Var(arg))) + | Some(typ) => + Forall(arg, Arrow(typ, Ap(Var(name), Var(arg)))) }, }), ctrs, @@ -694,12 +695,12 @@ and Kind: { [@deriving (show({with_path: false}), sexp, yojson)] type t = | Singleton(Typ.t) - | Arrow(Typ.t, Typ.t) + | Arrow(t, t) | Abstract; } = { [@deriving (show({with_path: false}), sexp, yojson)] type t = | Singleton(Typ.t) - | Arrow(Typ.t, Typ.t) + | Arrow(t, t) | Abstract; }; diff --git a/src/haz3lweb/view/CtxInspector.re b/src/haz3lweb/view/CtxInspector.re index 98d0ea6b40..f160250ff1 100644 --- a/src/haz3lweb/view/CtxInspector.re +++ b/src/haz3lweb/view/CtxInspector.re @@ -15,6 +15,7 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { ]), ); switch (entry) { + | ConstructorEntry({name, typ, _}) | VarEntry({name, typ, _}) => div_c( "context-entry", @@ -24,7 +25,6 @@ let context_entry_view = (~inject, entry: Haz3lcore.Ctx.entry): Node.t => { Type.view(typ), ], ) - | ConstructorEntry({name, kind, _}) | TVarEntry({name, kind, _}) => div_c( "context-entry", diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index bc8cfeeeb9..9c88a933ed 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -667,6 +667,21 @@ let get_doc = ), [], ); + | TypFun(_, _) => + // TODO (typfun) + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.triv_exp_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.triv_exp_group, + doc.explanation.message, + [], + ); + | Fun(pat, body) => let basic = (doc: LangDocMessages.form, group_id, options) => { let pat_id = List.nth(pat.ids, 0); @@ -1902,6 +1917,20 @@ let get_doc = LangDocMessages.funapp_exp_coloring_ids, ); }; + | TypAp(_, _) => + // TODO (typfun) + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.triv_exp_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.triv_exp_group, + doc.explanation.message, + [], + ); | If(cond, then_, else_) => let (doc, options) = LangDocMessages.get_form_and_options( diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 2dc53757b5..ecece46d5d 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -60,6 +60,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => { | FailedCast(_) | InvalidOperation(_) | Fun(_) + | TypFun(_) | Closure(_) => DHDoc_common.precedence_const | Cast(d1, _, _) => show_casts ? DHDoc_common.precedence_const : precedence'(d1) @@ -71,7 +72,8 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => { | BinIntOp(op, _, _) => precedence_bin_int_op(op) | BinFloatOp(op, _, _) => precedence_bin_float_op(op) | BinStringOp(op, _, _) => precedence_bin_string_op(op) - | Ap(_) => DHDoc_common.precedence_Ap + | Ap(_) + | TypAp(_) => DHDoc_common.precedence_Ap | ApBuiltin(_) => DHDoc_common.precedence_Ap | Cons(_) => DHDoc_common.precedence_Cons | ListConcat(_) => DHDoc_common.precedence_Plus @@ -193,6 +195,12 @@ let rec mk = go'(~parenthesize=false, d2), ); DHDoc_common.mk_Ap(mk_cast(doc1), mk_cast(doc2)); + | TypAp(d1, ty) => + DHDoc_common.mk_Ap( + mk_cast(go(~enforce_inline, d1)), + DHDoc_Typ.mk(~enforce_inline=true, ty), + ) + | ApBuiltin(ident, args) => switch (args) { | [hd, ...tl] => @@ -338,6 +346,9 @@ let rec mk = | Some(name) => annot(DHAnnot.Collapsed, text("<" ++ name ++ ">")) }; } + | TypFun(_tpat, _dbody) => + annot(DHAnnot.Collapsed, text("")) + | FixF(x, ty, dbody) => if (settings.show_fn_bodies) { let doc_body = (~enforce_inline) => diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 7a525ed73f..10ad518d2c 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -50,8 +50,20 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | Float => (text("Float"), parenthesize) | Bool => (text("Bool"), parenthesize) | String => (text("String"), parenthesize) - | Parameter(name) | Var(name) => (text(name), parenthesize) + | Ap(_) => (text("Ap"), parenthesize) + | Forall(name, ty) => ( + hcats([ + text("Forall " ++ name ++ ".{"), + ( + (~enforce_inline) => + annot(HTypAnnot.Step(0), mk(~enforce_inline, ty)) + ) + |> pad_child(~enforce_inline), + mk_delim("}"), + ]), + parenthesize, + ) | List(ty) => ( hcats([ mk_delim("["), From 9ccf6191411ba48114dc64ac4c8a52571d5f06f8 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Sun, 27 Aug 2023 11:17:04 -0400 Subject: [PATCH 06/14] Add: parameterized-types, leave the case branch not working --- src/haz3lcore/statics/MakeTerm.re | 6 +- src/haz3lcore/statics/Statics.re | 155 +++++++++++++++-------------- src/haz3lcore/statics/Term.re | 23 +++-- src/haz3lcore/statics/TermBase.re | 4 + src/haz3lcore/zipper/EditorUtil.re | 2 + src/haz3lweb/view/Kind.re | 4 +- src/haz3lweb/view/Type.re | 11 +- 7 files changed, 121 insertions(+), 84 deletions(-) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 41527e08dd..7cc8f39339 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -57,7 +57,9 @@ let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => { ts |> List.map( fun - | (_, (["|", "=>"], [Pat(p)])) => Some(p) + | (_, (["|", "=>"], [Pat(p)])) => { + Some(p); + } | _ => None, ) |> OptUtil.sequence @@ -182,6 +184,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["-"], []) => UnOp(Int(Minus), r) | (["!"], []) => UnOp(Bool(Not), r) | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) + | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => TyAlias(tpat, def, r) @@ -198,6 +201,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { switch (t) { | (["()"], []) => (l.term, l.ids) //TODO(andrew): new ap error | (["(", ")"], [Exp(arg)]) => ret(Ap(l, arg)) + | (["@<", ">"], [Typ(ty)]) => ret(TypAp(l, ty)) | _ => ret(hole(tm)) } | _ => ret(hole(tm)) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 7284955ede..51b51071eb 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -236,6 +236,21 @@ and uexp_to_info_map = ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m, ); + | TypAp(fn, utyp) => + /* Might need something similar to Ap's case where we check analysis mode when tagged? */ + let typfn_mode = + /* switch(fn) { + | {term: Tag(name), _} => Typ.tag_typap_mode(ctx, mode, name) + | _ => Typ.typap_mode + }; */ Mode.SynTypFun; + let (fn, m_fn) = go(~mode=typfn_mode, fn, m); + let (name, ty_body) = Typ.matched_forall(fn.ty); + let ty = Term.UTyp.to_typ(ctx, utyp); + add( + ~self=Just(Typ.subst(ty, name, ty_body)), + ~co_ctx=CoCtx.union([fn.co_ctx]), + m_fn, + ); | Fun(p, e) => let (mode_pat, mode_body) = Mode.of_arrow(ctx, mode); let (p, m) = go_pat(~is_synswitch=false, ~mode=mode_pat, p, m); @@ -245,52 +260,28 @@ and uexp_to_info_map = ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m, ); + | TypFun({term: Var(name), _} as utpat, body) => + let mode_body = Mode.of_forall(mode); + let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd; + let ctx_body = Ctx.extend_dummy_tvar(ctx, name); + let (body, m) = go'(~ctx=ctx_body, ~mode=mode_body, body, m); + add(~self=Just(Forall(name, body.ty)), ~co_ctx=body.co_ctx, m); + | TypFun(utpat, body) => + let mode_body = Mode.of_forall(mode); + let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd; + let (body, m) = go(~mode=mode_body, body, m); + add( + ~self=Just(Forall("expected_type_variable", body.ty)), + ~co_ctx=body.co_ctx, + m, + ); | Let(p, def, body) => let (p_syn, _m) = go_pat(~is_synswitch=true, ~mode=Syn, p, m); let def_ctx = extend_let_def_ctx(ctx, p, p_syn.ctx, def); - //let def_ctx = - // switch (def.term) { - // | Ap(fn, arg) => - // switch (fn.term) { - // | Constructor(ctr) => - // switch (Ctx.lookup_higher_alias(def_ctx, ctr)) { - // | Some((name_in, ty_in1)) => - // let (ty_in2, _) = go(~mode=Syn, arg, m); - // let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); - // let ctx' = Ctx.revise_tvar(def_ctx, name_in, ty); - // ctx'; - // | None => def_ctx - // } - // | _ => def_ctx - // } - // | _ => def_ctx - // }; let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m); /* Analyze pattern to incorporate def type into ctx */ let (p_ana, m) = go_pat(~is_synswitch=false, ~mode=Ana(def.ty), p, m); - let (body, m) = - go'( - ~ctx=p_ana.ctx, - //switch (def.term.term) { - //| Ap(fn, arg) => - // switch (fn.term) { - // | Constructor(ctr) => - // switch (Ctx.lookup_higher_alias(p_ana.ctx, ctr)) { - // | Some((name_in, ty_in1)) => - // let (ty_in2, _) = go(~mode=Syn, arg, m); - // let ty = Ctx.find_parameter_type(name_in, ty_in1, ty_in2.ty); - // let ctx' = Ctx.revise_tvar(p_ana.ctx, name_in, ty); - // ctx'; - // | None => p_ana.ctx - // } - // | _ => p_ana.ctx - // } - //| _ => p_ana.ctx - //}, - ~mode, - body, - m, - ); + let (body, m) = go'(~ctx=p_ana.ctx, ~mode, body, m); add( ~self=Just(body.ty), ~co_ctx= @@ -308,6 +299,15 @@ and uexp_to_info_map = m, ); | Match(scrut, rules) => + List.iter( + a => + Printf.printf( + "Upat: %s, UExp: %s\n", + UPat.show(fst(a)), + UExp.show(snd(a)), + ), + rules, + ); let (scrut, m) = go(~mode=Syn, scrut, m); let (ps, es) = List.split(rules); let branch_ids = List.map(UExp.rep_id, es); @@ -366,7 +366,7 @@ and uexp_to_info_map = let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd; add(~self=Just(ty_escape), ~co_ctx, m); | Ap(t1, t2) => - let constructor = + let name = switch (t1.term) { | Var(s) => s | _ => "" @@ -376,57 +376,68 @@ and uexp_to_info_map = | Var(s) => s | _ => "" }; - let utyp = UTyp.remove_ap_in_def(constructor, arg, utyp); + let utyp_without_ap = UTyp.remove_ap_in_def(name, arg, utyp); let (ty_def, ctx_def, ctx_body) = { let ty_pre = UTyp.to_typ( - Ctx.extend_dummy_tvar( - Ctx.extend_dummy_tvar(ctx, constructor), - arg, - ), + Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg), utyp, ); + Printf.printf("ty_pre: %s\n", Typ.show(ty_pre)); switch (utyp.term) { - | Sum(_) when List.mem(constructor, Typ.free_vars(ty_pre)) => - let ty_rec = - Typ.Rec("α", Typ.subst(Var("α"), constructor, ty_pre)); + | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) => + let ty_pre = + UTyp.to_typ( + Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg), + utyp_without_ap, + ); + let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre)); let ctx_def = - Ctx.extend_higher_alias( + Ctx.extend_higher_kind( ctx, - constructor, + name, arg, UTPat.rep_id(typat), ty_rec, ); (ty_rec, ctx_def, ctx_def); | _ => - let ctx_def = - Ctx.extend_higher_alias( - ctx, - constructor, - arg, - UTPat.rep_id(typat), - ty_pre, - ); - (ty_pre, ctx_def, ctx_def); + let ty = UTyp.to_typ(ctx, utyp); + ( + ty, + ctx, + Ctx.extend_higher_kind(ctx, name, arg, UTPat.rep_id(typat), ty), + ); }; }; let ctx_body = - switch (Typ.get_sum_constructors(ctx, ty_def)) { - | Some(sm) => - Ctx.add_higher_ctrs( - ctx_body, - constructor, - arg, - UTyp.rep_id(utyp), - sm, - ) - | None => ctx_body - }; + Ctx.add_ctr_with_typ_parameter( + ctx_body, + name, + UTyp.rep_id(utyp), + [ + ("Nil", None), + ("Cons", Some(Prod([Var(arg), Ap(Var(name), Var(arg))]))), + ], + arg, + ); + //switch (Typ.get_sum_constructors(ctx, ty_def)) { + //| Some(sm) => + // Printf.printf("sm: %s\n", Typ.show_sum_map(sm)); + // Ctx.add_ctr_with_typ_parameter( + // ctx_body, + // name, + // UTyp.rep_id(utyp), + // sm, + // arg, + // ); + //| None => ctx_body + //}; + Printf.printf("ctx_body: %s\n", Ctx.show(ctx_body)); let ({co_ctx, ty: ty_body, _}: Info.exp, m) = go'(~ctx=ctx_body, ~mode, body, m); /* Make sure types don't escape their scope */ - let ty_escape = Typ.subst(ty_def, constructor, ty_body); + let ty_escape = Typ.subst(ty_def, name, ty_body); let m = utyp_to_info_map(~ctx=ctx_def, ~ancestors, utyp, m) |> snd; add(~self=Just(ty_escape), ~co_ctx, m); | Var(_) diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 3609e0d0c5..297c4ae173 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -139,13 +139,10 @@ module UTyp = { switch (Ctx.lookup_tvar(ctx, name)) { | Some(ty) => switch (ty.kind) { - | Arrow(ty_in, ty_out) => - switch (ty_in) { - | Var(arg) => Typ.subst(to_typ(ctx, t2), arg, ty_out) - | _ => Unknown(Internal) - } - | Singleton(_) - | Abstract => Unknown(Internal) + | Arrow(Singleton(Var(arg)), Singleton(ty_out)) => + Typ.subst(to_typ(ctx, t2), arg, ty_out) + | Abstract => Ap(Var(name), to_typ(ctx, t2)) + | _ => Unknown(Internal) } | None => Unknown(Free(name)) }; @@ -501,11 +498,13 @@ module UExp = { | ListLit | Constructor | Fun + | TypFun | Tuple | Var | Let | TyAlias | Ap + | TypAp | If | Seq | Test @@ -540,11 +539,13 @@ module UExp = { | ListLit(_) => ListLit | Constructor(_) => Constructor | Fun(_) => Fun + | TypFun(_) => TypFun | Tuple(_) => Tuple | Var(_) => Var | Let(_) => Let | TyAlias(_) => TyAlias | Ap(_) => Ap + | TypAp(_) => TypAp | If(_) => If | Seq(_) => Seq | Test(_) => Test @@ -626,11 +627,13 @@ module UExp = { | ListLit => "List literal" | Constructor => "Constructor" | Fun => "Function literal" + | TypFun => "Type Function Literal" | Tuple => "Tuple literal" | Var => "Variable reference" | Let => "Let expression" | TyAlias => "Type Alias definition" | Ap => "Application" + | TypAp => "Type Application" | If => "If expression" | Seq => "Sequence expression" | Test => "Test" @@ -644,7 +647,8 @@ module UExp = { let rec is_fun = (e: t) => { switch (e.term) { | Parens(e) => is_fun(e) - | Fun(_) => true + | Fun(_) + | TypFun(_) => true | Invalid(_) | EmptyHole | MultiHole(_) @@ -659,6 +663,7 @@ module UExp = { | Let(_) | TyAlias(_) | Ap(_) + | TypAp(_) | If(_) | Seq(_) | Test(_) @@ -687,10 +692,12 @@ module UExp = { | String(_) | ListLit(_) | Fun(_) + | TypFun(_) | Var(_) | Let(_) | TyAlias(_) | Ap(_) + | TypAp(_) | If(_) | Seq(_) | Test(_) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 585c331842..ac7ea4f5fe 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -110,11 +110,13 @@ and UExp: { | ListLit(list(t)) | Constructor(string) | Fun(UPat.t, t) + | TypFun(UTPat.t, t) | Tuple(list(t)) | Var(Var.t) | Let(UPat.t, t, t) | TyAlias(UTPat.t, UTyp.t, t) | Ap(t, t) + | TypAp(t, UTyp.t) | If(t, t, t) | Seq(t, t) | Test(t) @@ -206,11 +208,13 @@ and UExp: { | ListLit(list(t)) | Constructor(string) | Fun(UPat.t, t) + | TypFun(UTPat.t, t) | Tuple(list(t)) | Var(Var.t) | Let(UPat.t, t, t) | TyAlias(UTPat.t, UTyp.t, t) | Ap(t, t) + | TypAp(t, UTyp.t) | If(t, t, t) | Seq(t, t) | Test(t) diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index 4483997e1d..29bac63f20 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -66,9 +66,11 @@ let rec append_exp = (id, e1: TermBase.UExp.t, e2: TermBase.UExp.t) => { | ListLit(_) | Constructor(_) | Fun(_) + | TypFun(_) | Tuple(_) | Var(_) | Ap(_) + | TypAp(_) | If(_) | Test(_) | Parens(_) diff --git a/src/haz3lweb/view/Kind.re b/src/haz3lweb/view/Kind.re index 416427a9d1..704412e818 100644 --- a/src/haz3lweb/view/Kind.re +++ b/src/haz3lweb/view/Kind.re @@ -2,10 +2,10 @@ open Virtual_dom.Vdom; open Node; open Util.Web; -let view = (kind: Haz3lcore.Kind.t): Node.t => +let rec view = (kind: Haz3lcore.Kind.t): Node.t => switch (kind) { | Arrow(ty1, ty2) => - div_c("kind-view", [Type.view(ty1), text(" -> "), Type.view(ty2)]) + div_c("kind-view", [view(ty1), text(" -> "), view(ty2)]) | Singleton(ty) => div_c("kind-view", [Type.view(ty)]) | Abstract => div_c("kind-view", [text("Type")]) }; diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index cc14fc3fd4..acaab163af 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -33,13 +33,22 @@ let rec view_ty = (ty: Haz3lcore.Typ.t): Node.t => | Float => ty_view("Float", "Float") | String => ty_view("String", "String") | Bool => ty_view("Bool", "Bool") - | Parameter(name) => ty_view("Parameter", name) + | Ap(t1, t2) => + div( + ~attr=clss(["typ-view", "Ap"]), + [view_ty(t1), text("("), view_ty(t2), text(")")], + ) | Var(name) => ty_view("Var", name) | Rec(x, t) => div( ~attr=clss(["typ-view", "Rec"]), [text("Rec " ++ x ++ ". "), view_ty(t)], ) + | Forall(name, t) => + div( + ~attr=clss(["typ-view", "Forall"]), + [text("Forall " ++ name ++ ". "), view_ty(t)], + ) | List(t) => div( ~attr=clss(["typ-view", "atom", "List"]), From 57f725e902ee72da48570ba22b966fbaca11d427 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Mon, 28 Aug 2023 21:15:50 -0400 Subject: [PATCH 07/14] Revise info and evaluator pattern match to fix the case branch inconsistent --- src/haz3lcore/dynamics/Evaluator.re | 3 ++- src/haz3lcore/statics/Info.re | 11 ++++++++++- src/haz3lcore/statics/Statics.re | 1 - src/haz3lcore/statics/TypBase.re | 21 ++++++++++++++------- 4 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 7f82fed3ad..ddcb7e8e2d 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -183,7 +183,7 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => } | (Ap(_, _), Cast(d, Sum(_) | Rec(_, Sum(_)), Unknown(_))) - | (Ap(_, _), Cast(d, Unknown(_), Sum(_) | Rec(_, Sum(_)))) => + | (Ap(_, _), Cast(d, Unknown(_) | Ap(_), Sum(_) | Rec(_, Sum(_)))) => matches(dp, d) | (Ap(_, _), _) => DoesNotMatch @@ -201,6 +201,7 @@ let rec matches = (dp: DHPat.t, d: DHExp.t): match_result => matches(dp, d) | (Constructor(_), Cast(d, Unknown(_), Sum(_) | Rec(_, Sum(_)))) => matches(dp, d) + | (Constructor(_) as a, TypAp(Constructor(_) as b, _)) => matches(a, b) | (Constructor(_), _) => DoesNotMatch | (Tuple(dps), Tuple(ds)) => diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index cd49f4529d..141302cf08 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -314,10 +314,19 @@ let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => { we catch them here, diverting to an ExpectedConstructor error. But we avoid capturing the second case above, as these will ultimately get a (more precise) unbound ctr via status_common */ + let self_pat: Self.t = + switch (self_pat) { + | IsConstructor({name, syn_ty: Some(Forall(name2, ty))}) => + IsConstructor({ + name, + syn_ty: Some(Typ.subst(Unknown(Internal), name2, ty)), + }) + | _ => self_pat + }; switch (status_common(ctx, mode, self_pat)) { | NotInHole(ok_exp) => NotInHole(ok_exp) | InHole(err_pat) => InHole(Common(err_pat)) - } + }; | (SynFun, _) => InHole(ExpectedConstructor) }; }; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 51b51071eb..1d7da30a23 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -383,7 +383,6 @@ and uexp_to_info_map = Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg), utyp, ); - Printf.printf("ty_pre: %s\n", Typ.show(ty_pre)); switch (utyp.term) { | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) => let ty_pre = diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 197bfa6b65..8eff449245 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -289,23 +289,30 @@ module rec Typ: { let+ ty_join = join'(ty_name, ty); !resolve && eq(ty_name, ty_join) ? Var(name) : ty_join; /* Note: Ordering of Unknown, Var, and Rec above is load-bearing! */ + | (Ap(ty1, ty2), Ap(ty1', ty2')) => + let* ty1 = join'(ty1, ty1'); + let+ ty2 = join'(ty2, ty2'); + Ap(ty1, ty2); | (ty2, Ap(Var(name), ty)) | (Ap(Var(name), ty), ty2) => switch (Ctx.lookup_higher_kind(ctx, name)) { | Some((arg, ty_out)) => join'(subst(ty, arg, ty_out), ty2) - | _ => None } | (ty, Ap(Forall(name, t1), t2)) | (Ap(Forall(name, t1), t2), ty) => join(~resolve, ~fix, ctx, Typ.subst(t2, name, t1), ty) - | (Ap(ty1, ty2), Ap(ty1', ty2')) => - let* ty1 = join'(ty1, ty1'); - let+ ty2 = join'(ty2, ty2'); - Ap(ty1, ty2); | (Ap(_), _) => None - | (Forall(name, t1), Forall(_, t2)) => - switch (join(~resolve, ~fix, Ctx.extend_dummy_tvar(ctx, name), t1, t2)) { + | (Forall(name, t1), Forall(name2, t2)) => + switch ( + join( + ~resolve, + ~fix, + Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name2), name), + t1, + t2, + ) + ) { | Some(t) => Some(Forall(name, t)) | None => None } From 58e5cd7430a4ab56c0fa07a7f890e91ce77d2877 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Mon, 28 Aug 2023 21:28:48 -0400 Subject: [PATCH 08/14] Rmove debug print code --- src/haz3lcore/statics/Statics.re | 52 ++++++++++++-------------------- src/haz3lcore/statics/TypBase.re | 1 - 2 files changed, 19 insertions(+), 34 deletions(-) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 1d7da30a23..8e0bda633c 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -299,15 +299,6 @@ and uexp_to_info_map = m, ); | Match(scrut, rules) => - List.iter( - a => - Printf.printf( - "Upat: %s, UExp: %s\n", - UPat.show(fst(a)), - UExp.show(snd(a)), - ), - rules, - ); let (scrut, m) = go(~mode=Syn, scrut, m); let (ps, es) = List.split(rules); let branch_ids = List.map(UExp.rep_id, es); @@ -409,30 +400,25 @@ and uexp_to_info_map = ); }; }; - let ctx_body = - Ctx.add_ctr_with_typ_parameter( - ctx_body, - name, - UTyp.rep_id(utyp), - [ - ("Nil", None), - ("Cons", Some(Prod([Var(arg), Ap(Var(name), Var(arg))]))), - ], - arg, - ); - //switch (Typ.get_sum_constructors(ctx, ty_def)) { - //| Some(sm) => - // Printf.printf("sm: %s\n", Typ.show_sum_map(sm)); - // Ctx.add_ctr_with_typ_parameter( - // ctx_body, - // name, - // UTyp.rep_id(utyp), - // sm, - // arg, - // ); - //| None => ctx_body - //}; - Printf.printf("ctx_body: %s\n", Ctx.show(ctx_body)); + let ctx_body = { + let ty_pre = + UTyp.to_typ( + Ctx.extend_dummy_tvar(Ctx.extend_dummy_tvar(ctx, name), arg), + utyp, + ); + + switch (ty_pre) { + | Sum(sm_map) => + Ctx.add_ctr_with_typ_parameter( + ctx_body, + name, + UTyp.rep_id(utyp), + sm_map, + arg, + ) + | _ => ctx_body + }; + }; let ({co_ctx, ty: ty_body, _}: Info.exp, m) = go'(~ctx=ctx_body, ~mode, body, m); /* Make sure types don't escape their scope */ diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 8eff449245..1ef1c2d331 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -434,7 +434,6 @@ module rec Typ: { | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) }; }; - let sum_entry = (ctr: Constructor.t, ctrs: sum_map): option(sum_entry) => List.find_map( fun From 644203431b9a01f378b570011d593d4aaeb568cc Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Tue, 29 Aug 2023 00:04:55 -0400 Subject: [PATCH 09/14] Fix: incorrect type of ctrs --- src/haz3lcore/dynamics/Elaborator.re | 9 +++-- src/haz3lcore/dynamics/Evaluator.re | 9 ++++- src/haz3lcore/prog/Interface.re | 1 + src/haz3lcore/statics/Statics.re | 1 + src/haz3lcore/statics/TypBase.re | 55 +++++++++++++++++++++++----- 5 files changed, 59 insertions(+), 16 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index ae0c5840ec..2c1ec48e44 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -27,7 +27,7 @@ let fixed_pat_typ = (m: Statics.Map.t, p: Term.UPat.t): option(Typ.t) => | _ => None }; -let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => +let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => { switch (mode) { | Syn => d | SynFun => @@ -74,12 +74,13 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => DHExp.cast(d, Prod(us), Unknown(prov)); | _ => d } - | Ap(Constructor(_), _) + | Ap(Constructor(_) | TypAp(_), _) | TypAp(Constructor(_), _) | Constructor(_) => switch (ana_ty, self_ty) { | (Unknown(prov), Rec(_, Sum(_))) - | (Unknown(prov), Sum(_)) => DHExp.cast(d, self_ty, Unknown(prov)) + | (Unknown(prov), Ap(_) | Sum(_)) => + DHExp.cast(d, self_ty, Unknown(prov)) | _ => d } /* Forms with special ana rules but no particular typing requirements */ @@ -116,7 +117,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => | TestLit(_) => DHExp.cast(d, self_ty, ana_ty) }; }; - +}; /* Handles cast insertion and non-empty-hole wrapping for elaborated expressions */ let wrap = (ctx: Ctx.t, u: Id.t, mode: Mode.t, self, d: DHExp.t): DHExp.t => diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index ddcb7e8e2d..13f02d3d5f 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -49,6 +49,8 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Var(_) | Rec(_) | Arrow(Unknown(_), Unknown(_)) + | Ap(Unknown(_), Unknown(_)) + | Forall("_", Unknown(_)) | List(Unknown(_)) => Ground | Prod(tys) => if (List.for_all( @@ -66,7 +68,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Arrow(_, _) => grounded_Arrow | List(_) => grounded_List | Forall(_) => grounded_Forall - | Ap(_) => grounded_Ap + | Ap(_, _) => grounded_Ap }; }; @@ -697,7 +699,8 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = (env, d) => { /* Increment number of evaluation steps (calls to `evaluate`). */ let* () = take_step; - + //Printf.printf("env: %s\n", ClosureEnvironment.show(env)); + //Printf.printf("d: %s\n", DHExp.show(d)); switch (d) { | BoundVar(x) => let d = @@ -748,7 +751,9 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = | TypFun(_) => BoxedValue(Closure(env, d)) |> return | TypAp(d1, tau) => + //Printf.printf("TypAp, env: %s\n", ClosureEnvironment.show(env)); let* r1 = evaluate(env, d1); + //Printf.printf("r1: %s\n", EvaluatorResult.show(r1)); switch (r1) { | BoxedValue(Closure(closure_env, TypFun({term: Var(name), _}, d2))) => // TODO: Maybe additional cases to be done? diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index 04c9493bb5..13dc646919 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -56,6 +56,7 @@ let evaluate = // }; let evaluate = (d: DHExp.t): ProgramResult.t => { + //Printf.printf("Evaluating: %s\n", DHExp.show(d)); let result = try(evaluate(d)) { | EvaluatorError.Exception(reason) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 8e0bda633c..c6f2bfdd9a 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -415,6 +415,7 @@ and uexp_to_info_map = UTyp.rep_id(utyp), sm_map, arg, + ty_def, ) | _ => ctx_body }; diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 1ef1c2d331..9bea4c4db6 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -60,6 +60,7 @@ module rec Typ: { let matched_list: t => t; let precedence: t => int; let subst: (t, TypVar.t, t) => t; + let subst_ap: (t, TypVar.t, TypVar.t, t) => t; let unroll: t => t; let eq: (t, t) => bool; let free_vars: (~bound: list(Var.t)=?, t) => list(Var.t); @@ -172,7 +173,27 @@ module rec Typ: { | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow }; - + let rec subst_ap = (s: t, ctr: TypVar.t, arg: TypVar.t, ty: t) => { + switch (ty) { + | Int => Int + | Float => Float + | Bool => Bool + | String => String + | Unknown(prov) => Unknown(prov) + | Arrow(ty1, ty2) => + Arrow(subst_ap(s, ctr, arg, ty1), subst_ap(s, ctr, arg, ty2)) + | Prod(tys) => Prod(List.map(subst_ap(s, ctr, arg), tys)) + | Sum(sm) => + Sum(ConstructorMap.map(Option.map(subst_ap(s, ctr, arg)), sm)) + | Rec(y, ty) => Rec(y, subst_ap(s, ctr, arg, ty)) + | List(ty) => List(subst_ap(s, ctr, arg, ty)) + | Var(y) => Var(y) + | Forall(y, ty) => Forall(y, subst_ap(s, ctr, arg, ty)) + | Ap(Var(v1), Var(v2)) when v1 == ctr && v2 == arg => s + | Ap(ty1, ty2) => + Ap(subst_ap(s, ctr, arg, ty1), subst_ap(s, ctr, arg, ty2)) + }; + }; let rec subst = (s: t, x: TypVar.t, ty: t) => { switch (ty) { | Int => Int @@ -289,10 +310,6 @@ module rec Typ: { let+ ty_join = join'(ty_name, ty); !resolve && eq(ty_name, ty_join) ? Var(name) : ty_join; /* Note: Ordering of Unknown, Var, and Rec above is load-bearing! */ - | (Ap(ty1, ty2), Ap(ty1', ty2')) => - let* ty1 = join'(ty1, ty1'); - let+ ty2 = join'(ty2, ty2'); - Ap(ty1, ty2); | (ty2, Ap(Var(name), ty)) | (Ap(Var(name), ty), ty2) => switch (Ctx.lookup_higher_kind(ctx, name)) { @@ -302,6 +319,10 @@ module rec Typ: { | (ty, Ap(Forall(name, t1), t2)) | (Ap(Forall(name, t1), t2), ty) => join(~resolve, ~fix, ctx, Typ.subst(t2, name, t1), ty) + | (Ap(ty1, ty2), Ap(ty1', ty2')) => + let* ty1 = join'(ty1, ty1'); + let+ ty2 = join'(ty2, ty2'); + Ap(ty1, ty2); | (Ap(_), _) => None | (Forall(name, t1), Forall(name2, t2)) => switch ( @@ -395,9 +416,9 @@ module rec Typ: { ts, ); - let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool => + let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool => { join(~fix=false, ctx, ty1, ty2) != None; - + }; let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t => switch (ty) { | Var(x) => @@ -503,7 +524,7 @@ and Ctx: { let is_tyVar: (t, TypVar.t) => bool; let add_ctrs: (t, TypVar.t, Id.t, Typ.sum_map) => t; let add_ctr_with_typ_parameter: - (t, TypVar.t, Id.t, Typ.sum_map, TypVar.t) => t; + (t, TypVar.t, Id.t, Typ.sum_map, TypVar.t, Typ.t) => t; let subtract_prefix: (t, t) => option(t); let added_bindings: (t, t) => t; let filter_duplicates: t => t; @@ -631,7 +652,15 @@ and Ctx: { ) @ ctx; let add_ctr_with_typ_parameter = - (ctx: t, name: TypVar.t, id: Id.t, ctrs: Typ.sum_map, arg: TypVar.t): t => + ( + ctx: t, + name: TypVar.t, + id: Id.t, + ctrs: Typ.sum_map, + arg: TypVar.t, + ty: Typ.t, + ) + : t => List.map( ((ctr, typ)) => ConstructorEntry({ @@ -641,7 +670,13 @@ and Ctx: { switch (typ) { | None => Forall(arg, Ap(Var(name), Var(arg))) | Some(typ) => - Forall(arg, Arrow(typ, Ap(Var(name), Var(arg)))) + Forall( + arg, + Arrow( + Typ.subst_ap(ty, name, arg, typ), + Ap(Var(name), Var(arg)), + ), + ) }, }), ctrs, From 3142ed32af0876feb2a0ec45699b6f14f2477d07 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Tue, 29 Aug 2023 11:55:47 -0400 Subject: [PATCH 10/14] Fix: typeann typehole cause case match failed --- src/haz3lcore/dynamics/Evaluator.re | 4 ---- src/haz3lcore/prog/Interface.re | 1 - src/haz3lcore/statics/TypBase.re | 5 +++++ 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 13f02d3d5f..6e75f48870 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -699,8 +699,6 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = (env, d) => { /* Increment number of evaluation steps (calls to `evaluate`). */ let* () = take_step; - //Printf.printf("env: %s\n", ClosureEnvironment.show(env)); - //Printf.printf("d: %s\n", DHExp.show(d)); switch (d) { | BoundVar(x) => let d = @@ -751,9 +749,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) = | TypFun(_) => BoxedValue(Closure(env, d)) |> return | TypAp(d1, tau) => - //Printf.printf("TypAp, env: %s\n", ClosureEnvironment.show(env)); let* r1 = evaluate(env, d1); - //Printf.printf("r1: %s\n", EvaluatorResult.show(r1)); switch (r1) { | BoxedValue(Closure(closure_env, TypFun({term: Var(name), _}, d2))) => // TODO: Maybe additional cases to be done? diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index 13dc646919..04c9493bb5 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -56,7 +56,6 @@ let evaluate = // }; let evaluate = (d: DHExp.t): ProgramResult.t => { - //Printf.printf("Evaluating: %s\n", DHExp.show(d)); let result = try(evaluate(d)) { | EvaluatorError.Exception(reason) => diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 9bea4c4db6..9c1fb559c1 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -452,6 +452,11 @@ module rec Typ: { Rec(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) | Forall(name, ty) => Forall(name, normalize(Ctx.extend_dummy_tvar(ctx, name), ty)) + | Ap(Var(name), t2) => + switch (Ctx.lookup_higher_kind(ctx, name)) { + | Some((arg, ty_out)) => normalize(ctx, subst(t2, arg, ty_out)) + | None => Ap(Var(name), normalize(ctx, t2)) + } | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) }; }; From 21e33659a00cf7ad1b8b3d3f988d1356889e39ac Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Tue, 29 Aug 2023 19:34:13 -0400 Subject: [PATCH 11/14] Fix: ctr_ap type error --- src/haz3lcore/statics/Info.re | 20 +++++++++----------- src/haz3lcore/statics/Statics.re | 25 +++++++++++++++++-------- src/haz3lcore/statics/TypBase.re | 28 ++++++++++------------------ src/haz3lweb/view/CursorInspector.re | 3 ++- 4 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 141302cf08..6d27d350ac 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -170,7 +170,8 @@ type error_tpat = [@deriving (show({with_path: false}), sexp, yojson)] type ok_tpat = | Empty - | Var(TypVar.t); + | Var(TypVar.t) + | Ap(TypVar.t, TypVar.t); [@deriving (show({with_path: false}), sexp, yojson)] type status_tpat = @@ -416,16 +417,13 @@ let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat => | Var(name) => NotInHole(Var(name)) | Invalid(_) => InHole(NotAVar(NotCapitalized)) | MultiHole(_) => InHole(NotAVar(Other)) - | Ap(t, _) => - switch (t.term) { - | Var(name) => - if (Form.is_base_typ(name) || Ctx.lookup_alias(ctx, name) != None) { - InHole(ShadowsType(name)); - } else { - NotInHole(Var(name)); - } - | _ => InHole(NotAVar(Other)) - } + | Ap({term: Var(name1), _}, {term: Var(_), _}) + when Form.is_base_typ(name1) || Ctx.lookup_alias(ctx, name1) != None => + InHole(ShadowsType(name1)) + | Ap({term: Var(name1), _}, {term: Var(name2), _}) => + NotInHole(Ap(name1, name2)) + + | Ap(_) => InHole(NotAVar(Other)) }; /* Determines whether any term is in an error hole. */ diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index c6f2bfdd9a..6f4e99a053 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -391,13 +391,23 @@ and uexp_to_info_map = ty_rec, ); (ty_rec, ctx_def, ctx_def); - | _ => - let ty = UTyp.to_typ(ctx, utyp); - ( - ty, - ctx, - Ctx.extend_higher_kind(ctx, name, arg, UTPat.rep_id(typat), ty), - ); + | _ => ( + ty_pre, + Ctx.extend_higher_kind( + ctx, + name, + arg, + UTPat.rep_id(typat), + ty_pre, + ), + Ctx.extend_higher_kind( + ctx, + name, + arg, + UTPat.rep_id(typat), + ty_pre, + ), + ) }; }; let ctx_body = { @@ -415,7 +425,6 @@ and uexp_to_info_map = UTyp.rep_id(utyp), sm_map, arg, - ty_def, ) | _ => ctx_body }; diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 9c1fb559c1..ce9422e550 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -468,8 +468,9 @@ module rec Typ: { ctrs, ); - let get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { + let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { let ty = weak_head_normalize(ctx, ty); + Printf.printf("get_sum_constructors: %s\n", show(ty)); switch (ty) { | Sum(sm) => Some(sm) | Rec(_) => @@ -479,6 +480,11 @@ module rec Typ: { | Sum(sm) => Some(sm) | _ => None } + | Ap(Var(name), ty_arg) => + switch (Ctx.lookup_higher_kind(ctx, name)) { + | Some((arg, ty)) => get_sum_constructors(ctx, subst(ty_arg, arg, ty)) + | None => None + } | _ => None }; }; @@ -529,7 +535,7 @@ and Ctx: { let is_tyVar: (t, TypVar.t) => bool; let add_ctrs: (t, TypVar.t, Id.t, Typ.sum_map) => t; let add_ctr_with_typ_parameter: - (t, TypVar.t, Id.t, Typ.sum_map, TypVar.t, Typ.t) => t; + (t, TypVar.t, Id.t, Typ.sum_map, TypVar.t) => t; let subtract_prefix: (t, t) => option(t); let added_bindings: (t, t) => t; let filter_duplicates: t => t; @@ -657,15 +663,7 @@ and Ctx: { ) @ ctx; let add_ctr_with_typ_parameter = - ( - ctx: t, - name: TypVar.t, - id: Id.t, - ctrs: Typ.sum_map, - arg: TypVar.t, - ty: Typ.t, - ) - : t => + (ctx: t, name: TypVar.t, id: Id.t, ctrs: Typ.sum_map, arg: TypVar.t): t => List.map( ((ctr, typ)) => ConstructorEntry({ @@ -675,13 +673,7 @@ and Ctx: { switch (typ) { | None => Forall(arg, Ap(Var(name), Var(arg))) | Some(typ) => - Forall( - arg, - Arrow( - Typ.subst_ap(ty, name, arg, typ), - Ap(Var(name), Var(arg)), - ), - ) + Forall(arg, Arrow(typ, Ap(Var(name), Var(arg)))) }, }), ctrs, diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 50bc3c36e7..6f4ed17085 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -3,7 +3,6 @@ open Node; open Util.Web; open Util; open Haz3lcore; - let errc = "error"; let okc = "ok"; let div_err = div(~attr=clss([errc])); @@ -182,6 +181,8 @@ let tpat_view = (_: Term.Cls.t, status: Info.status_tpat) => switch (status) { | NotInHole(Empty) => div_ok([text("Fillable with a new alias")]) | NotInHole(Var(name)) => div_ok([Type.alias_view(name)]) + | NotInHole(Ap(name1, name2)) => + div_ok([Type.alias_view(name1), Type.alias_view(name2)]) | InHole(NotAVar(NotCapitalized)) => div_err([text("Must begin with a capital letter")]) | InHole(NotAVar(_)) => div_err([text("Expected an alias")]) From 6ea7f14545e53d6e100e630acbc8a73ae9cc3446 Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Sun, 10 Sep 2023 15:00:42 -0400 Subject: [PATCH 12/14] Fix: sort-inconsistent in mold/labels --- src/haz3lcore/lang/Form.re | 9 ++++++++- src/haz3lcore/statics/TypBase.re | 1 - src/haz3lweb/view/CursorInspector.re | 7 ++++++- 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 3cf1699707..423c9e5f16 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -185,7 +185,13 @@ let bad_token_cls: string => bad_token_cls = priority for forms with overlapping regexps */ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ ("bad_lit", (is_bad_lit, [mk_op(Any, [])])), - ("var", (is_var, [mk_op(Exp, []), mk_op(Pat, [])])), + ( + "var", + ( + is_var, + [mk_op(Exp, []), mk_op(Pat, []), mk_op(TPat, []), mk_op(Typ, [])], + ), + ), ("ty_var", (is_typ_var, [mk_op(Typ, [])])), ("ty_var_p", (is_typ_var, [mk_op(TPat, [])])), ("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])), @@ -253,6 +259,7 @@ let forms: list((string, t)) = [ ("parens_exp", mk(ii, ["(", ")"], mk_op(Exp, [Exp]))), ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))), ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))), + ("parens_tpat", mk(ii, ["(", ")"], mk_op(TPat, [TPat]))), ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))), ("typfun", mk(ds, ["typfun", "->"], mk_pre(P.fun_, Exp, [TPat]))), ("forall", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [TPat]))), diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index ec97478c15..15c02d85a4 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -473,7 +473,6 @@ module rec Typ: { let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { let ty = weak_head_normalize(ctx, ty); - Printf.printf("get_sum_constructors: %s\n", show(ty)); switch (ty) { | Sum(sm) => Some(sm) | Rec(_) => diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 579ea2c326..493341410c 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -182,7 +182,12 @@ let tpat_view = (_: Term.Cls.t, status: Info.status_tpat) => | NotInHole(Empty) => div_ok([text("Fillable with a new alias")]) | NotInHole(Var(name)) => div_ok([Type.alias_view(name)]) | NotInHole(Ap(name1, name2)) => - div_ok([Type.alias_view(name1), Type.alias_view(name2)]) + div_ok([ + Type.alias_view(name1), + Type.alias_view("("), + Type.alias_view(name2), + Type.alias_view(")"), + ]) | InHole(NotAVar(NotCapitalized)) => div_err([text("Must begin with a capital letter")]) | InHole(NotAVar(_)) => div_err([text("Expected an alias")]) From d197606e50edcdb78e0d681d0c3ef466d056c6de Mon Sep 17 00:00:00 2001 From: ZhenXu Date: Mon, 25 Sep 2023 17:48:07 -0400 Subject: [PATCH 13/14] format error --- src/haz3lcore/statics/TypBase.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index c012a7d310..d813b8fd95 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -498,7 +498,7 @@ module rec Typ: { switch (ty) { | Sum(sm) => Some(sm) | _ => None - } + }; | Ap(Var(name), ty_arg) => switch (Ctx.lookup_higher_kind(ctx, name)) { | Some((arg, ty)) => get_sum_constructors(ctx, subst(ty_arg, arg, ty)) From 233f55ae853f7623ce10575838a47dc8fe92a816 Mon Sep 17 00:00:00 2001 From: Zhen Xu Date: Thu, 7 Mar 2024 15:11:52 -0500 Subject: [PATCH 14/14] Fix and merge ploy-adt-after2 --- src/haz3lcore/dynamics/Transition.re | 3 +++ src/haz3lcore/lang/Form.re | 8 ++++---- src/haz3lcore/statics/MakeTerm.re | 3 ++- src/haz3lcore/statics/TypBase.re | 4 +++- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 46b35fa6e1..b615344d6c 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -279,6 +279,9 @@ module Transition = (EV: EV_MODE) => { /* Treat a hole or invalid tyvar name as a unique type variable that doesn't appear anywhere else. Thus instantiating it at anything doesn't produce any substitutions. */ Step({apply: () => tfbody, kind: TypFunAp, value: false}) } + | Constructor(name) => + /* Rule ITTCon */ + Step({apply: () => Constructor(name), kind: TypFunAp, value: false}) | Cast(d'', Forall(x, t), Forall(x', t')) => /* Rule ITTApCast */ Step({ diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 5a93de22ba..88ac697305 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -217,10 +217,10 @@ let bad_token_cls: string => bad_token_cls = Order in this list determines relative remolding priority for forms with overlapping regexps */ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ - //("ty_var", (is_typ_var, [mk_op(Typ, [])])), - //("ty_var_p", (is_typ_var, [mk_op(TPat, [])])), - //("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])), - //("type", (is_base_typ, [mk_op(Typ, [])])), + ("ty_var", (is_typ_var, [mk_op(Typ, [])])), + ("ty_var_p", (is_typ_var, [mk_op(TPat, [])])), + ("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])), + ("type", (is_base_typ, [mk_op(Typ, [])])), ("var", (is_var, [mk_op(Exp, []), mk_op(Pat, [])])), ( "explicit_hole", diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 5ba15a19ff..bdcdcc55b8 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -408,6 +408,7 @@ and tpat = unsorted => { return(ty => TPat(ty), ids, {ids, term}); } and tpat_term = (unsorted: unsorted): UTPat.term => { + Printf.printf("tpat_term: %s\n", show_unsorted(unsorted)); let ret = (term: UTPat.term) => term; let hole = unsorted => Term.UTPat.hole(kids_of_unsorted(unsorted)); switch (unsorted) { @@ -431,7 +432,7 @@ and tpat_term = (unsorted: unsorted): UTPat.term => { switch (tile) { | (["(", ")"], [TPat(arg)]) => switch (arg.term) { - | Invalid(s) when Form.is_type_input(s) => + | Var(s) when Form.is_type_input(s) => Ap(l, {ids: arg.ids, term: Var(s)}) | _ => ret(hole(tm)) } diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 6f4154201d..a31204e65c 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -366,7 +366,9 @@ module rec Typ: { | (ty2, Ap(Var(name), ty)) | (Ap(Var(name), ty), ty2) => switch (Ctx.lookup_higher_kind(ctx, name)) { - | Some((arg, ty_out)) => join'(subst(ty, arg, ty_out), ty2) + | Some((arg, ty_out)) => + Printf.printf("ty2: %s\n", show(ty2)); + join'(subst(ty, arg, ty_out), ty2); | _ => None } | (ty, Ap(Forall(name, t1), t2))