From 46709eae50c28cc5771acbacc73306ccecab62dc Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 4 Oct 2024 10:52:03 -0400 Subject: [PATCH] Make the data constructors in termbase distinct --- src/haz3lcore/assistant/AssistantForms.re | 2 +- src/haz3lcore/dynamics/Builtins.re | 74 ++--- src/haz3lcore/dynamics/Casts.re | 16 +- src/haz3lcore/dynamics/DHExp.re | 16 +- src/haz3lcore/dynamics/DHPat.re | 60 ++-- src/haz3lcore/dynamics/Elaborator.re | 63 ++-- src/haz3lcore/dynamics/EvaluatorStep.re | 4 +- src/haz3lcore/dynamics/FilterMatcher.re | 27 +- src/haz3lcore/dynamics/PatternMatch.re | 32 +- src/haz3lcore/dynamics/Stepper.re | 4 +- src/haz3lcore/dynamics/Substitution.re | 8 +- src/haz3lcore/dynamics/Transition.re | 64 ++-- src/haz3lcore/dynamics/TypeAssignment.re | 76 ++--- src/haz3lcore/dynamics/Unboxing.re | 14 +- src/haz3lcore/lang/term/TPat.re | 12 +- src/haz3lcore/lang/term/Typ.re | 120 ++++---- src/haz3lcore/statics/Ctx.re | 10 +- src/haz3lcore/statics/Info.re | 31 +- src/haz3lcore/statics/MakeTerm.re | 70 +++-- src/haz3lcore/statics/Mode.re | 7 +- src/haz3lcore/statics/Statics.re | 86 +++--- src/haz3lcore/statics/Term.re | 308 +++++++++---------- src/haz3lcore/statics/TermBase.re | 260 ++++++++-------- src/haz3lcore/zipper/EditorUtil.re | 8 +- src/haz3lschool/Exercise.re | 2 +- src/haz3lschool/SyntaxTest.re | 121 ++++---- src/haz3lweb/view/Cell.re | 2 +- src/haz3lweb/view/CursorInspector.re | 14 +- src/haz3lweb/view/ExplainThis.re | 149 ++++----- src/haz3lweb/view/Type.re | 8 +- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 20 +- src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re | 64 ++-- src/haz3lweb/view/dhcode/layout/HTypDoc.re | 12 +- 33 files changed, 899 insertions(+), 865 deletions(-) diff --git a/src/haz3lcore/assistant/AssistantForms.re b/src/haz3lcore/assistant/AssistantForms.re index f3551ac0eb..a66d711787 100644 --- a/src/haz3lcore/assistant/AssistantForms.re +++ b/src/haz3lcore/assistant/AssistantForms.re @@ -27,7 +27,7 @@ module Typ = { ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh), ( "typfun" ++ leading_expander, - Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh, + Forall(VarTPat("") |> TPat.fresh, unk) |> Typ.fresh, ), ("if" ++ leading_expander, unk), ("let" ++ leading_expander, unk), diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index c47617edc6..bf383eb9b8 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -41,13 +41,13 @@ let fn = module Pervasives = { module Impls = { /* constants */ - let infinity = Float(Float.infinity) |> fresh; - let neg_infinity = Float(Float.neg_infinity) |> fresh; - let nan = Float(Float.nan) |> fresh; - let epsilon_float = Float(epsilon_float) |> fresh; - let pi = Float(Float.pi) |> fresh; - let max_int = Int(Int.max_int) |> fresh; - let min_int = Int(Int.min_int) |> fresh; + let infinity = FloatLit(Float.infinity) |> fresh; + let neg_infinity = FloatLit(Float.neg_infinity) |> fresh; + let nan = FloatLit(Float.nan) |> fresh; + let epsilon_float = FloatLit(epsilon_float) |> fresh; + let pi = FloatLit(Float.pi) |> fresh; + let max_int = IntLit(Int.max_int) |> fresh; + let min_int = IntLit(Int.min_int) |> fresh; let unary = (f: DHExp.t => result, d: DHExp.t) => { switch (f(d)) { @@ -81,7 +81,7 @@ module Pervasives = { let is_finite = unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(Bool(Float.is_finite(f)))) + | FloatLit(f) => Ok(fresh(BoolLit(Float.is_finite(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -89,7 +89,7 @@ module Pervasives = { let is_infinite = unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(Bool(Float.is_infinite(f)))) + | FloatLit(f) => Ok(fresh(BoolLit(Float.is_infinite(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -97,7 +97,7 @@ module Pervasives = { let is_nan = unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(Bool(Float.is_nan(f)))) + | FloatLit(f) => Ok(fresh(BoolLit(Float.is_nan(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -105,7 +105,7 @@ module Pervasives = { let string_of_int = unary(d => switch (term_of(d)) { - | Int(n) => Ok(fresh(String(string_of_int(n)))) + | IntLit(n) => Ok(fresh(StringLit(string_of_int(n)))) | _ => Error(InvalidBoxedIntLit(d)) } ); @@ -113,7 +113,7 @@ module Pervasives = { let string_of_float = unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(String(string_of_float(f)))) + | FloatLit(f) => Ok(fresh(StringLit(string_of_float(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -121,7 +121,7 @@ module Pervasives = { let string_of_bool = unary(d => switch (term_of(d)) { - | Bool(b) => Ok(fresh(String(string_of_bool(b)))) + | BoolLit(b) => Ok(fresh(StringLit(string_of_bool(b)))) | _ => Error(InvalidBoxedBoolLit(d)) } ); @@ -129,7 +129,7 @@ module Pervasives = { let int_of_float = unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(Int(int_of_float(f)))) + | FloatLit(f) => Ok(fresh(IntLit(int_of_float(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -137,7 +137,7 @@ module Pervasives = { let float_of_int = unary(d => switch (term_of(d)) { - | Int(n) => Ok(fresh(Float(float_of_int(n)))) + | IntLit(n) => Ok(fresh(FloatLit(float_of_int(n)))) | _ => Error(InvalidBoxedIntLit(d)) } ); @@ -145,7 +145,7 @@ module Pervasives = { let abs = unary(d => switch (term_of(d)) { - | Int(n) => Ok(fresh(Int(abs(n)))) + | IntLit(n) => Ok(fresh(IntLit(abs(n)))) | _ => Error(InvalidBoxedIntLit(d)) } ); @@ -153,7 +153,7 @@ module Pervasives = { let float_op = fn => unary(d => switch (term_of(d)) { - | Float(f) => Ok(fresh(Float(fn(f)))) + | FloatLit(f) => Ok(fresh(FloatLit(fn(f)))) | _ => Error(InvalidBoxedFloatLit(d)) } ); @@ -176,7 +176,7 @@ module Pervasives = { (convert: string => option('a), wrap: 'a => DHExp.t, name: string) => unary(d => switch (term_of(d)) { - | String(s) => + | StringLit(s) => switch (convert(s)) { | Some(n) => Ok(wrap(n)) | None => @@ -190,17 +190,17 @@ module Pervasives = { ); let int_of_string = - of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh); + of_string(int_of_string_opt, n => IntLit(n) |> DHExp.fresh); let float_of_string = - of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh); + of_string(float_of_string_opt, f => FloatLit(f) |> DHExp.fresh); let bool_of_string = - of_string(bool_of_string_opt, b => Bool(b) |> DHExp.fresh); + of_string(bool_of_string_opt, b => BoolLit(b) |> DHExp.fresh); let int_mod = (name, d1) => binary( (d1, d2) => switch (term_of(d1), term_of(d2)) { - | (Int(_), Int(0)) => + | (IntLit(_), IntLit(0)) => Ok( fresh( DynamicErrorHole( @@ -209,8 +209,8 @@ module Pervasives = { ), ), ) - | (Int(n), Int(m)) => Ok(Int(n mod m) |> fresh) - | (Int(_), _) => + | (IntLit(n), IntLit(m)) => Ok(IntLit(n mod m) |> fresh) + | (IntLit(_), _) => raise(EvaluatorError.Exception(InvalidBoxedIntLit(d2))) | (_, _) => raise(EvaluatorError.Exception(InvalidBoxedIntLit(d1))) @@ -221,7 +221,7 @@ module Pervasives = { let string_length = unary(d => switch (term_of(d)) { - | String(s) => Ok(Int(String.length(s)) |> fresh) + | StringLit(s) => Ok(IntLit(String.length(s)) |> fresh) | _ => Error(InvalidBoxedStringLit(d)) } ); @@ -229,9 +229,9 @@ module Pervasives = { let string_compare = binary((d1, d2) => switch (term_of(d1), term_of(d2)) { - | (String(s1), String(s2)) => - Ok(Int(String.compare(s1, s2)) |> fresh) - | (String(_), _) => Error(InvalidBoxedStringLit(d2)) + | (StringLit(s1), StringLit(s2)) => + Ok(IntLit(String.compare(s1, s2)) |> fresh) + | (StringLit(_), _) => Error(InvalidBoxedStringLit(d2)) | (_, _) => Error(InvalidBoxedStringLit(d1)) } ); @@ -239,7 +239,7 @@ module Pervasives = { let string_trim = unary(d => switch (term_of(d)) { - | String(s) => Ok(String(String.trim(s)) |> fresh) + | StringLit(s) => Ok(StringLit(String.trim(s)) |> fresh) | _ => Error(InvalidBoxedStringLit(d)) } ); @@ -247,19 +247,19 @@ module Pervasives = { let string_of: DHExp.t => option(string) = d => switch (term_of(d)) { - | String(s) => Some(s) + | StringLit(s) => Some(s) | _ => None }; let string_concat = binary((d1, d2) => switch (term_of(d1), term_of(d2)) { - | (String(s1), ListLit(xs)) => + | (StringLit(s1), ListLit(xs)) => switch (xs |> List.map(string_of) |> Util.OptUtil.sequence) { | None => Error(InvalidBoxedStringLit(List.hd(xs))) - | Some(xs) => Ok(String(String.concat(s1, xs)) |> fresh) + | Some(xs) => Ok(StringLit(String.concat(s1, xs)) |> fresh) } - | (String(_), _) => Error(InvalidBoxedListLit(d2)) + | (StringLit(_), _) => Error(InvalidBoxedListLit(d2)) | (_, _) => Error(InvalidBoxedStringLit(d1)) } ); @@ -267,14 +267,14 @@ module Pervasives = { let string_sub = _ => ternary((d1, d2, d3) => switch (term_of(d1), term_of(d2), term_of(d3)) { - | (String(s), Int(idx), Int(len)) => - try(Ok(String(String.sub(s, idx, len)) |> fresh)) { + | (StringLit(s), IntLit(idx), IntLit(len)) => + try(Ok(StringLit(String.sub(s, idx, len)) |> fresh)) { | _ => // TODO: make it clear that the problem could be with d3 too Ok(DynamicErrorHole(d2, IndexOutOfBounds) |> fresh) } - | (String(_), Int(_), _) => Error(InvalidBoxedIntLit(d3)) - | (String(_), _, _) => Error(InvalidBoxedIntLit(d2)) + | (StringLit(_), IntLit(_), _) => Error(InvalidBoxedIntLit(d3)) + | (StringLit(_), _, _) => Error(InvalidBoxedIntLit(d2)) | (_, _, _) => Error(InvalidBoxedIntLit(d1)) } ); diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re index a69f560dd5..9f0a8ead4e 100644 --- a/src/haz3lcore/dynamics/Casts.re +++ b/src/haz3lcore/dynamics/Casts.re @@ -34,7 +34,7 @@ let grounded_Arrow = ); let grounded_Forall = NotGroundOrHole( - Forall(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp) + Forall(EmptyHoleTPat |> TPat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp, ); let grounded_Prod = length => @@ -58,12 +58,12 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Int | Float | String - | Var(_) + | TypVar(_) | Rec(_) | Forall(_, {term: Unknown(_), _}) | Arrow({term: Unknown(_), _}, {term: Unknown(_), _}) | List({term: Unknown(_), _}) => Ground - | Parens(ty) => ground_cases_of(ty) + | TypParens(ty) => ground_cases_of(ty) | Prod(tys) => if (List.for_all( fun @@ -81,7 +81,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Arrow(_, _) => grounded_Arrow | Forall(_) => grounded_Forall | List(_) => grounded_List - | Ap(_) => failwith("type application in dynamics") + | ApTyp(_) => failwith("type application in dynamics") }; }; @@ -183,7 +183,7 @@ let hole = EmptyHole |> DHExp.fresh; let pattern_fixup = (p: DHPat.t): DHPat.t => { let rec unwrap_casts = (p: DHPat.t): (DHPat.t, DHExp.t) => { switch (DHPat.term_of(p)) { - | Cast(p1, t1, t2) => + | CastPat(p1, t1, t2) => let (p1, d1) = unwrap_casts(p1); ( p1, @@ -198,13 +198,13 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => { | EmptyHole => p | Cast(d1, t1, t2) => let p1 = rewrap_casts((p, d1)); - {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids}; + {term: CastPat(p1, t1, t2), copied: d.copied, ids: d.ids}; | FailedCast(d1, t1, t2) => let p1 = rewrap_casts((p, d1)); { term: - Cast( - Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, + CastPat( + CastPat(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, Typ.fresh(Unknown(Internal)), t2, ), diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re index f7651ba963..ad9bd015b2 100644 --- a/src/haz3lcore/dynamics/DHExp.re +++ b/src/haz3lcore/dynamics/DHExp.re @@ -67,10 +67,10 @@ let rec strip_casts = | EmptyHole | Invalid(_) | Var(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | DynamicErrorHole(_) | Closure(_) @@ -135,10 +135,10 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => { | Undefined | Constructor(_) | Var(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | FailedCast(_, _, _) | MultiHole(_) | Deferral(_) diff --git a/src/haz3lcore/dynamics/DHPat.re b/src/haz3lcore/dynamics/DHPat.re index f9e4adbddb..c7e18cca3d 100644 --- a/src/haz3lcore/dynamics/DHPat.re +++ b/src/haz3lcore/dynamics/DHPat.re @@ -12,43 +12,43 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool => | Some(_) => false | None => switch (dp |> term_of) { - | EmptyHole - | MultiHole(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Invalid(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | Constructor(_) => false - | Cast(y, _, _) - | Parens(y) => binds_var(m, x, y) - | Var(y) => Var.eq(x, y) - | Tuple(dps) => dps |> List.exists(binds_var(m, x)) - | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2) - | ListLit(d_list) => + | InvalidPat(_) + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ConstructorPat(_) => false + | CastPat(y, _, _) + | ParensPat(y) => binds_var(m, x, y) + | VarPat(y) => Var.eq(x, y) + | TuplePat(dps) => dps |> List.exists(binds_var(m, x)) + | ConsPat(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2) + | ListLitPat(d_list) => let new_list = List.map(binds_var(m, x), d_list); List.fold_left((||), false, new_list); - | Ap(_, _) => false + | ApPat(_, _) => false } }; let rec bound_vars = (dp: t): list(Var.t) => switch (dp |> term_of) { - | EmptyHole - | MultiHole(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Invalid(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | Constructor(_) => [] - | Cast(y, _, _) - | Parens(y) => bound_vars(y) - | Var(y) => [y] - | Tuple(dps) => List.flatten(List.map(bound_vars, dps)) - | Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2) - | ListLit(dps) => List.flatten(List.map(bound_vars, dps)) - | Ap(_, dp1) => bound_vars(dp1) + | InvalidPat(_) + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ConstructorPat(_) => [] + | CastPat(y, _, _) + | ParensPat(y) => bound_vars(y) + | VarPat(y) => [y] + | TuplePat(dps) => List.flatten(List.map(bound_vars, dps)) + | ConsPat(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2) + | ListLitPat(dps) => List.flatten(List.map(bound_vars, dps)) + | ApPat(_, dp1) => bound_vars(dp1) }; diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index d50d462064..c4a571e93c 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -36,8 +36,8 @@ let fresh_pat_cast = (p: DHPat.t, t1: Typ.t, t2: Typ.t): DHPat.t => { Typ.eq(t1, t2) ? p : { - Cast( - DHPat.fresh(Cast(p, t1, Typ.temp(Unknown(Internal)))) + CastPat( + DHPat.fresh(CastPat(p, t1, Typ.temp(Unknown(Internal)))) |> Casts.pattern_fixup, Typ.temp(Unknown(Internal)), t2, @@ -66,7 +66,7 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => { Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); - let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); + let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHoleTPat)); Forall(tpat, ty) |> Typ.temp; // We need to remove the synswitches from this type. | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty) @@ -93,7 +93,7 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => { Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); - let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); + let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHoleTPat)); Forall(tpat, ty) |> Typ.temp; | Ana(ana_ty) => switch (prev_synswitch) { @@ -111,11 +111,11 @@ let rec elaborate_pattern = let (term, rewrap) = UPat.unwrap(upat); let dpat = switch (term) { - | Int(_) => upat |> cast_from(Int |> Typ.temp) - | Bool(_) => upat |> cast_from(Bool |> Typ.temp) - | Float(_) => upat |> cast_from(Float |> Typ.temp) - | String(_) => upat |> cast_from(String |> Typ.temp) - | ListLit(ps) => + | IntPat(_) => upat |> cast_from(Int |> Typ.temp) + | BoolPat(_) => upat |> cast_from(Bool |> Typ.temp) + | FloatPat(_) => upat |> cast_from(Float |> Typ.temp) + | StringPat(_) => upat |> cast_from(String |> Typ.temp) + | ListLitPat(ps) => let (ps, tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; let inner_type = tys @@ -125,9 +125,11 @@ let rec elaborate_pattern = |> List.map2((p, t) => fresh_pat_cast(p, t, inner_type), _, tys) |> ( ps' => - ListLit(ps') |> rewrap |> cast_from(List(inner_type) |> Typ.temp) + ListLitPat(ps') + |> rewrap + |> cast_from(List(inner_type) |> Typ.temp) ); - | Cons(p1, p2) => + | ConsPat(p1, p2) => let (p1', ty1) = elaborate_pattern(m, p1); let (p2', ty2) = elaborate_pattern(m, p2); let ty2_inner = Typ.matched_list(ctx, ty2); @@ -136,22 +138,22 @@ let rec elaborate_pattern = |> Option.value(~default=Typ.temp(Unknown(Internal))); let p1'' = fresh_pat_cast(p1', ty1, ty_inner); let p2'' = fresh_pat_cast(p2', ty2, List(ty_inner) |> Typ.temp); - Cons(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp); - | Tuple(ps) => + ConsPat(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp); + | TuplePat(ps) => let (ps', tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; - Tuple(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp); - | Ap(p1, p2) => + TuplePat(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp); + | ApPat(p1, p2) => let (p1', ty1) = elaborate_pattern(m, p1); let (p2', ty2) = elaborate_pattern(m, p2); let (ty1l, ty1r) = Typ.matched_arrow(ctx, ty1); let p1'' = fresh_pat_cast(p1', ty1, Arrow(ty1l, ty1r) |> Typ.temp); let p2'' = fresh_pat_cast(p2', ty2, ty1l); - Ap(p1'', p2'') |> rewrap |> cast_from(ty1r); - | Invalid(_) - | EmptyHole - | MultiHole(_) + ApPat(p1'', p2'') |> rewrap |> cast_from(ty1r); + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild => upat |> cast_from(Typ.temp(Unknown(Internal))) - | Var(v) => + | VarPat(v) => upat |> cast_from( Ctx.lookup_var(ctx, v) @@ -159,11 +161,11 @@ let rec elaborate_pattern = |> Option.value(~default=Typ.temp(Unknown(Internal))), ) // Type annotations should already appear - | Parens(p) - | Cast(p, _, _) => + | ParensPat(p) + | CastPat(p, _, _) => let (p', ty) = elaborate_pattern(m, p); p' |> cast_from(ty |> Typ.normalize(ctx)); - | Constructor(c, _) => + | ConstructorPat(c, _) => let mode = switch (Id.Map.find_opt(Pat.rep_id(upat), m)) { | Some(Info.InfoPat({mode, _})) => mode @@ -176,7 +178,7 @@ let rec elaborate_pattern = | _ => Unknown(Internal) |> Typ.temp }; let t = t |> Typ.normalize(ctx); - Constructor(c, t) |> rewrap |> cast_from(t); + ConstructorPat(c, t) |> rewrap |> cast_from(t); }; (dpat, elaborated_type); }; @@ -234,10 +236,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (e', ty) = elaborate(m, e); e' |> cast_from(ty); | Deferral(_) => uexp - | Int(_) => uexp |> cast_from(Int |> Typ.temp) - | Bool(_) => uexp |> cast_from(Bool |> Typ.temp) - | Float(_) => uexp |> cast_from(Float |> Typ.temp) - | String(_) => uexp |> cast_from(String |> Typ.temp) + | IntLit(_) => uexp |> cast_from(Int |> Typ.temp) + | BoolLit(_) => uexp |> cast_from(Bool |> Typ.temp) + | FloatLit(_) => uexp |> cast_from(Float |> Typ.temp) + | StringLit(_) => uexp |> cast_from(String |> Typ.temp) | ListLit(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; let inner_type = @@ -353,7 +355,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let tye'' = Typ.subst( ut', - tpat |> Option.value(~default=TPat.fresh(EmptyHole)), + tpat |> Option.value(~default=TPat.fresh(EmptyHoleTPat)), tye', ); TypAp(e', ut) |> rewrap |> cast_from(tye''); @@ -382,7 +384,8 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let kind' = switch (kind) { | Residue(_) => kind - | Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst}) + | FilterStepper({act, pat}) => + FilterStepper({act, pat: elaborate(m, pat) |> fst}) }; Filter(kind', e') |> rewrap |> cast_from(t); | Closure(env, e) => diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index f25f25603f..008541b676 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -243,10 +243,10 @@ let rec matches = | Closure(env, ctx) => let+ ctx = matches(env, flt, ctx, exp, act, idx); Closure(env, ctx) |> wrap_ids(ids); - | Filter(Filter(flt'), ctx) => + | Filter(FilterStepper(flt'), ctx) => let flt = flt |> FilterEnvironment.extends(flt'); let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Filter(flt'), ctx) |> wrap_ids(ids); + Filter(FilterStepper(flt'), ctx) |> wrap_ids(ids); | Filter(Residue(idx', act'), ctx) => let (ract, ridx, rctx) = if (idx > idx') { diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 61fd72f1bd..dcb3d324ef 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -202,17 +202,17 @@ let rec matches_exp = TermBase.StepperFilterKind.fast_equal(df, ff) && matches_exp(dd, fd) | (Filter(_), _) => false - | (Bool(dv), Bool(fv)) => dv == fv - | (Bool(_), _) => false + | (BoolLit(dv), BoolLit(fv)) => dv == fv + | (BoolLit(_), _) => false - | (Int(dv), Int(fv)) => dv == fv - | (Int(_), _) => false + | (IntLit(dv), IntLit(fv)) => dv == fv + | (IntLit(_), _) => false - | (Float(dv), Float(fv)) => dv == fv - | (Float(_), _) => false + | (FloatLit(dv), FloatLit(fv)) => dv == fv + | (FloatLit(_), _) => false - | (String(dv), String(fv)) => dv == fv - | (String(_), _) => false + | (StringLit(dv), StringLit(fv)) => dv == fv + | (StringLit(_), _) => false | ( Constructor(_), @@ -377,11 +377,12 @@ and matches_typ = (d: Typ.t, f: Typ.t) => { and matches_utpat = (d: TPat.t, f: TPat.t): bool => { switch (d.term, f.term) { - | (Invalid(_), _) => false - | (_, Invalid(_)) => false - | (_, EmptyHole) => true - | (MultiHole(l1), MultiHole(l2)) => List.length(l1) == List.length(l2) /* TODO: probably should define a matches_any and recurse in here...? */ - | (Var(t1), Var(t2)) => t1 == t2 + | (InvalidTPat(_), _) => false + | (_, InvalidTPat(_)) => false + | (_, EmptyHoleTPat) => true + | (MultiHoleTPat(l1), MultiHoleTPat(l2)) => + List.length(l1) == List.length(l2) /* TODO: probably should define a matches_any and recurse in here...? */ + | (VarTPat(t1), VarTPat(t2)) => t1 == t2 | _ => false }; }; diff --git a/src/haz3lcore/dynamics/PatternMatch.re b/src/haz3lcore/dynamics/PatternMatch.re index 329ca1efd8..2f282d88e1 100644 --- a/src/haz3lcore/dynamics/PatternMatch.re +++ b/src/haz3lcore/dynamics/PatternMatch.re @@ -13,23 +13,23 @@ let combine_result = (r1: match_result, r2: match_result): match_result => let rec matches = (dp: Pat.t, d: DHExp.t): match_result => switch (DHPat.term_of(dp)) { - | Invalid(_) - | EmptyHole - | MultiHole(_) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild => Matches(Environment.empty) - | Int(n) => + | IntPat(n) => let* n' = Unboxing.unbox(Int, d); n == n' ? Matches(Environment.empty) : DoesNotMatch; - | Float(n) => + | FloatPat(n) => let* n' = Unboxing.unbox(Float, d); n == n' ? Matches(Environment.empty) : DoesNotMatch; - | Bool(b) => + | BoolPat(b) => let* b' = Unboxing.unbox(Bool, d); b == b' ? Matches(Environment.empty) : DoesNotMatch; - | String(s) => + | StringPat(s) => let* s' = Unboxing.unbox(String, d); s == s' ? Matches(Environment.empty) : DoesNotMatch; - | ListLit(xs) => + | ListLitPat(xs) => let* s' = Unboxing.unbox(List, d); if (List.length(xs) == List.length(s')) { List.map2(matches, xs, s') @@ -37,24 +37,24 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result => } else { DoesNotMatch; }; - | Cons(x, xs) => + | ConsPat(x, xs) => let* (x', xs') = Unboxing.unbox(Cons, d); let* m_x = matches(x, x'); let* m_xs = matches(xs, xs'); Matches(Environment.union(m_x, m_xs)); - | Constructor(ctr, _) => + | ConstructorPat(ctr, _) => let* () = Unboxing.unbox(SumNoArg(ctr), d); Matches(Environment.empty); - | Ap({term: Constructor(ctr, _), _}, p2) => + | ApPat({term: ConstructorPat(ctr, _), _}, p2) => let* d2 = Unboxing.unbox(SumWithArg(ctr), d); matches(p2, d2); - | Ap(_, _) => IndetMatch // TODO: should this fail? - | Var(x) => Matches(Environment.singleton((x, d))) - | Tuple(ps) => + | ApPat(_, _) => IndetMatch // TODO: should this fail? + | VarPat(x) => Matches(Environment.singleton((x, d))) + | TuplePat(ps) => let* ds = Unboxing.unbox(Tuple(List.length(ps)), d); List.map2(matches, ps, ds) |> List.fold_left(combine_result, Matches(Environment.empty)); - | Parens(p) => matches(p, d) - | Cast(p, t1, t2) => + | ParensPat(p) => matches(p, d) + | CastPat(p, t1, t2) => matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple) }; diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 8b977cdf5f..34184941cb 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -52,10 +52,10 @@ let rec matches = | Closure(env, ctx) => let+ ctx = matches(env, flt, ctx, exp, act, idx); Closure(env, ctx) |> rewrap; - | Filter(Filter(flt'), ctx) => + | Filter(FilterStepper(flt'), ctx) => let flt = flt |> FilterEnvironment.extends(flt'); let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Filter(flt'), ctx) |> rewrap; + Filter(FilterStepper(flt'), ctx) |> rewrap; | Filter(Residue(idx', act'), ctx) => let (ract, ridx, rctx) = if (idx > idx') { diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index 5d918e520b..492e7c9ac8 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -60,10 +60,10 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => { Ap(dir, d3, d4) |> rewrap; | BuiltinFun(_) => d2 | Test(d3) => Test(subst_var(m, d1, x, d3)) |> rewrap - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) => d2 | ListLit(ds) => ListLit(List.map(subst_var(m, d1, x), ds)) |> rewrap | Cons(d3, d4) => diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a54c9d18d8..30393b8e2b 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -442,10 +442,10 @@ module Transition = (EV: EV_MODE) => { | Deferral(_) => let. _ = otherwise(env, d); Indet; - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | BuiltinFun(_) => let. _ = otherwise(env, d); @@ -477,7 +477,7 @@ module Transition = (EV: EV_MODE) => { ); let-unbox n = (Int, d1'); Step({ - expr: Int(- n) |> fresh, + expr: IntLit(- n) |> fresh, state_update, kind: UnOp(Int(Minus)), is_value: true, @@ -492,7 +492,7 @@ module Transition = (EV: EV_MODE) => { ); let-unbox b = (Bool, d1'); Step({ - expr: Bool(!b) |> fresh, + expr: BoolLit(!b) |> fresh, state_update, kind: UnOp(Bool(Not)), is_value: true, @@ -507,7 +507,7 @@ module Transition = (EV: EV_MODE) => { ); let-unbox b1 = (Bool, d1'); Step({ - expr: b1 ? d2 : Bool(false) |> fresh, + expr: b1 ? d2 : BoolLit(false) |> fresh, state_update, kind: BinBoolOp(And), is_value: false, @@ -522,7 +522,7 @@ module Transition = (EV: EV_MODE) => { ); let-unbox b1 = (Bool, d1'); Step({ - expr: b1 ? Bool(true) |> fresh : d2, + expr: b1 ? BoolLit(true) |> fresh : d2, state_update, kind: BinBoolOp(Or), is_value: false, @@ -547,27 +547,27 @@ module Transition = (EV: EV_MODE) => { expr: ( switch (op) { - | Plus => Int(n1 + n2) - | Minus => Int(n1 - n2) + | Plus => IntLit(n1 + n2) + | Minus => IntLit(n1 - n2) | Power when n2 < 0 => DynamicErrorHole( BinOp(Int(op), d1', d2') |> rewrap, NegativeExponent, ) - | Power => Int(IntUtil.ipow(n1, n2)) - | Times => Int(n1 * n2) + | Power => IntLit(IntUtil.ipow(n1, n2)) + | Times => IntLit(n1 * n2) | Divide when n2 == 0 => DynamicErrorHole( BinOp(Int(op), d1', d2') |> rewrap, DivideByZero, ) - | Divide => Int(n1 / n2) - | LessThan => Bool(n1 < n2) - | LessThanOrEqual => Bool(n1 <= n2) - | GreaterThan => Bool(n1 > n2) - | GreaterThanOrEqual => Bool(n1 >= n2) - | Equals => Bool(n1 == n2) - | NotEquals => Bool(n1 != n2) + | Divide => IntLit(n1 / n2) + | LessThan => BoolLit(n1 < n2) + | LessThanOrEqual => BoolLit(n1 <= n2) + | GreaterThan => BoolLit(n1 > n2) + | GreaterThanOrEqual => BoolLit(n1 >= n2) + | Equals => BoolLit(n1 == n2) + | NotEquals => BoolLit(n1 != n2) } ) |> fresh, @@ -597,17 +597,17 @@ module Transition = (EV: EV_MODE) => { expr: ( switch (op) { - | Plus => Float(n1 +. n2) - | Minus => Float(n1 -. n2) - | Power => Float(n1 ** n2) - | Times => Float(n1 *. n2) - | Divide => Float(n1 /. n2) - | LessThan => Bool(n1 < n2) - | LessThanOrEqual => Bool(n1 <= n2) - | GreaterThan => Bool(n1 > n2) - | GreaterThanOrEqual => Bool(n1 >= n2) - | Equals => Bool(n1 == n2) - | NotEquals => Bool(n1 != n2) + | Plus => FloatLit(n1 +. n2) + | Minus => FloatLit(n1 -. n2) + | Power => FloatLit(n1 ** n2) + | Times => FloatLit(n1 *. n2) + | Divide => FloatLit(n1 /. n2) + | LessThan => BoolLit(n1 < n2) + | LessThanOrEqual => BoolLit(n1 <= n2) + | GreaterThan => BoolLit(n1 > n2) + | GreaterThanOrEqual => BoolLit(n1 >= n2) + | Equals => BoolLit(n1 == n2) + | NotEquals => BoolLit(n1 != n2) } ) |> fresh, @@ -635,8 +635,8 @@ module Transition = (EV: EV_MODE) => { Step({ expr: switch (op) { - | Concat => String(s1 ++ s2) |> fresh - | Equals => Bool(s1 == s2) |> fresh + | Concat => StringLit(s1 ++ s2) |> fresh + | Equals => BoolLit(s1 == s2) |> fresh }, state_update, kind: BinStringOp(op), diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index 59b58aa56f..88da409502 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -34,43 +34,43 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) => let rec dhpat_var_entry = (dhpat: DHPat.t, ty: Typ.t): option(list(Ctx.entry)) => { switch (dhpat |> Pat.term_of) { - | Var(name) => + | VarPat(name) => let entry = Ctx.VarEntry({name, id: Id.invalid, typ: ty}); Some([entry]); - | Tuple(l1) => + | TuplePat(l1) => let* ts = Typ.matched_prod_strict(ctx, List.length(l1), ty); let* l = List.map2((dhp, typ) => {dhpat_var_entry(dhp, typ)}, l1, ts) |> OptUtil.sequence; Some(List.concat(l)); - | Cons(dhp1, dhp2) => + | ConsPat(dhp1, dhp2) => let* t = Typ.matched_list_strict(ctx, ty); let* l1 = dhpat_var_entry(dhp1, t); let* l2 = dhpat_var_entry(dhp2, List(t) |> Typ.temp); Some(l1 @ l2); - | ListLit(l) => + | ListLitPat(l) => let* t = Typ.matched_list_strict(ctx, ty); let* l = List.map(dhp => {dhpat_var_entry(dhp, t)}, l) |> OptUtil.sequence; Some(List.concat(l)); - | Ap({term: Constructor(name, _), _}, dhp) => + | ApPat({term: ConstructorPat(name, _), _}, dhp) => // TODO: make this stricter let* ctrs = Typ.get_sum_constructors(ctx, ty); let* typ = ConstructorMap.get_entry(name, ctrs); let* (ty1, ty2) = Typ.matched_arrow_strict(ctx, typ); Typ.eq(ty2, ty) ? dhpat_var_entry(dhp, ty1) : None; - | Ap(_) => None - | EmptyHole + | ApPat(_) => None + | EmptyHolePat | Wild - | Invalid(_) - | MultiHole(_) => Some([]) - | Parens(dhp) => dhpat_var_entry(dhp, ty) - | Int(_) => Typ.eq(ty, Int |> Typ.temp) ? Some([]) : None - | Float(_) => Typ.eq(ty, Float |> Typ.temp) ? Some([]) : None - | Bool(_) => Typ.eq(ty, Bool |> Typ.temp) ? Some([]) : None - | String(_) => Typ.eq(ty, String |> Typ.temp) ? Some([]) : None - | Constructor(_) => Some([]) // TODO: make this stricter - | Cast(dhp, ty1, ty2) => + | InvalidPat(_) + | MultiHolePat(_) => Some([]) + | ParensPat(dhp) => dhpat_var_entry(dhp, ty) + | IntPat(_) => Typ.eq(ty, Int |> Typ.temp) ? Some([]) : None + | FloatPat(_) => Typ.eq(ty, Float |> Typ.temp) ? Some([]) : None + | BoolPat(_) => Typ.eq(ty, Bool |> Typ.temp) ? Some([]) : None + | StringPat(_) => Typ.eq(ty, String |> Typ.temp) ? Some([]) : None + | ConstructorPat(_) => Some([]) // TODO: make this stricter + | CastPat(dhp, ty1, ty2) => Typ.eq(ty, ty2) ? dhpat_var_entry(dhp, ty1) : None }; }; @@ -81,29 +81,29 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) => /* patterns in functions and fixpoints must have a synthesizable type */ let rec dhpat_synthesize = (dhpat: DHPat.t, ctx: Ctx.t): option(Typ.t) => { switch (dhpat |> Pat.term_of) { - | Var(_) - | Constructor(_) - | Ap(_) => None - | Tuple(dhs) => + | VarPat(_) + | ConstructorPat(_) + | ApPat(_) => None + | TuplePat(dhs) => let* l = List.map(dhpat_synthesize(_, ctx), dhs) |> OptUtil.sequence; Some(Prod(l) |> Typ.temp); - | Cons(dhp1, _) => + | ConsPat(dhp1, _) => let* t = dhpat_synthesize(dhp1, ctx); Some(List(t) |> Typ.temp); - | ListLit([]) => Some(List(Unknown(Internal) |> Typ.temp) |> Typ.temp) - | ListLit([x, ..._]) => + | ListLitPat([]) => Some(List(Unknown(Internal) |> Typ.temp) |> Typ.temp) + | ListLitPat([x, ..._]) => let* t_x = dhpat_synthesize(x, ctx); Some(List(t_x) |> Typ.temp); - | EmptyHole => Some(Unknown(Internal) |> Typ.temp) + | EmptyHolePat => Some(Unknown(Internal) |> Typ.temp) | Wild => Some(Unknown(Internal) |> Typ.temp) - | Invalid(_) - | MultiHole(_) => Some(Unknown(Internal) |> Typ.temp) - | Parens(dhp) => dhpat_synthesize(dhp, ctx) - | Int(_) => Some(Int |> Typ.temp) - | Float(_) => Some(Float |> Typ.temp) - | Bool(_) => Some(Bool |> Typ.temp) - | String(_) => Some(String |> Typ.temp) - | Cast(_, _, ty) => Some(ty) + | InvalidPat(_) + | MultiHolePat(_) => Some(Unknown(Internal) |> Typ.temp) + | ParensPat(dhp) => dhpat_synthesize(dhp, ctx) + | IntPat(_) => Some(Int |> Typ.temp) + | FloatPat(_) => Some(Float |> Typ.temp) + | BoolPat(_) => Some(Bool |> Typ.temp) + | StringPat(_) => Some(String |> Typ.temp) + | CastPat(_, _, ty) => Some(ty) }; }; @@ -162,7 +162,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => let* ctx = dhpat_extend_ctx(dhp, ty_p, ctx); let* ty2 = typ_of_dhexp(ctx, m, d); Some(Arrow(ty_p, ty2) |> Typ.temp); - | TypFun({term: Var(name), _} as utpat, d, _) + | TypFun({term: VarTPat(name), _} as utpat, d, _) when !Ctx.shadows_typ(ctx, name) => let ctx = Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract}); @@ -170,7 +170,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => Some(Forall(utpat, ty) |> Typ.temp); | TypFun(_, d, _) => let* ty = typ_of_dhexp(ctx, m, d); - Some(Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp); + Some(Forall(VarTPat("?") |> TPat.fresh, ty) |> Typ.temp); | TypAp(d, ty1) => let* ty = typ_of_dhexp(ctx, m, d); let* (name, ty2) = Typ.matched_forall_strict(ctx, ty); @@ -222,10 +222,10 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => | Test(dtest) => let* ty = typ_of_dhexp(ctx, m, dtest); Typ.eq(ty, Bool |> Typ.temp) ? Some(Prod([]) |> Typ.temp) : None; - | Bool(_) => Some(Bool |> Typ.temp) - | Int(_) => Some(Int |> Typ.temp) - | Float(_) => Some(Float |> Typ.temp) - | String(_) => Some(String |> Typ.temp) + | BoolLit(_) => Some(Bool |> Typ.temp) + | IntLit(_) => Some(Int |> Typ.temp) + | FloatLit(_) => Some(Float |> Typ.temp) + | StringLit(_) => Some(String |> Typ.temp) | BinOp(Bool(_), d1, d2) => let* ty1 = typ_of_dhexp(ctx, m, d1); let* ty2 = typ_of_dhexp(ctx, m, d2); diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re index 400620026c..6cbad137c9 100644 --- a/src/haz3lcore/dynamics/Unboxing.re +++ b/src/haz3lcore/dynamics/Unboxing.re @@ -49,15 +49,15 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = (request, expr) => { switch (request, DHExp.term_of(expr)) { /* Remove parentheses from casts */ - | (_, Cast(d, {term: Parens(x), _}, y)) - | (_, Cast(d, x, {term: Parens(y), _})) => + | (_, Cast(d, {term: TypParens(x), _}, y)) + | (_, Cast(d, x, {term: TypParens(y), _})) => unbox(request, Cast(d, x, y) |> DHExp.fresh) /* Base types are always already unboxed because of the ITCastID rule*/ - | (Bool, Bool(b)) => Matches(b) - | (Int, Int(i)) => Matches(i) - | (Float, Float(f)) => Matches(f) - | (String, String(s)) => Matches(s) + | (Bool, BoolLit(b)) => Matches(b) + | (Int, IntLit(i)) => Matches(i) + | (Float, FloatLit(f)) => Matches(f) + | (String, StringLit(s)) => Matches(s) /* Lists can be either lists or list casts */ | (List, ListLit(l)) => Matches(l) @@ -145,7 +145,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = in elaboration or in the cast calculus. */ | ( _, - Bool(_) | Int(_) | Float(_) | String(_) | Constructor(_) | + BoolLit(_) | IntLit(_) | FloatLit(_) | StringLit(_) | Constructor(_) | BuiltinFun(_) | Deferral(_) | DeferredAp(_) | diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re index 583f805851..6a359be59d 100644 --- a/src/haz3lcore/lang/term/TPat.re +++ b/src/haz3lcore/lang/term/TPat.re @@ -12,16 +12,16 @@ let fresh: term => t = IdTagged.fresh; let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term => switch (tms) { - | [] => EmptyHole - | [_, ..._] => MultiHole(tms) + | [] => EmptyHoleTPat + | [_, ..._] => MultiHoleTPat(tms) }; let cls_of_term: term => cls = fun - | Invalid(_) => Invalid - | EmptyHole => EmptyHole - | MultiHole(_) => MultiHole - | Var(_) => Var; + | InvalidTPat(_) => Invalid + | EmptyHoleTPat => EmptyHole + | MultiHoleTPat(_) => MultiHole + | VarTPat(_) => Var; let show_cls: cls => string = fun diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index c9a6f0c204..d7936efb29 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -36,15 +36,15 @@ let rep_id: t => Id.t = IdTagged.rep_id; let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term => switch (tms) { - | [] => Unknown(Hole(EmptyHole)) - | [_, ..._] => Unknown(Hole(MultiHole(tms))) + | [] => Unknown(HoleProvenance(EmptyTypeHole)) + | [_, ..._] => Unknown(HoleProvenance(MultiTypeHole(tms))) }; let cls_of_term: term => cls = fun - | Unknown(Hole(Invalid(_))) => Invalid - | Unknown(Hole(EmptyHole)) => EmptyHole - | Unknown(Hole(MultiHole(_))) => MultiHole + | Unknown(HoleProvenance(InvalidTypeHole(_))) => Invalid + | Unknown(HoleProvenance(EmptyTypeHole)) => EmptyHole + | Unknown(HoleProvenance(MultiTypeHole(_))) => MultiHole | Unknown(SynSwitch) => SynSwitch | Unknown(Internal) => Internal | Int => Int @@ -53,10 +53,10 @@ let cls_of_term: term => cls = | String => String | List(_) => List | Arrow(_) => Arrow - | Var(_) => Var + | TypVar(_) => Var | Prod(_) => Prod - | Parens(_) => Parens - | Ap(_) => Ap + | TypParens(_) => Parens + | ApTyp(_) => Ap | Sum(_) => Sum | Rec(_) => Rec | Forall(_) => Forall; @@ -85,7 +85,7 @@ let show_cls: cls => string = let rec is_arrow = (typ: t) => { switch (typ.term) { - | Parens(typ) => is_arrow(typ) + | TypParens(typ) => is_arrow(typ) | Arrow(_) => true | Unknown(_) | Int @@ -94,8 +94,8 @@ let rec is_arrow = (typ: t) => { | String | List(_) | Prod(_) - | Var(_) - | Ap(_) + | TypVar(_) + | ApTyp(_) | Sum(_) | Forall(_) | Rec(_) => false @@ -104,7 +104,7 @@ let rec is_arrow = (typ: t) => { let rec is_forall = (typ: t) => { switch (typ.term) { - | Parens(typ) => is_forall(typ) + | TypParens(typ) => is_forall(typ) | Forall(_) => true | Unknown(_) | Int @@ -114,8 +114,8 @@ let rec is_forall = (typ: t) => { | Arrow(_) | List(_) | Prod(_) - | Var(_) - | Ap(_) + | TypVar(_) + | ApTyp(_) | Sum(_) | Rec(_) => false }; @@ -140,13 +140,18 @@ let join_type_provenance = (p1: TermBase.type_provenance, p2: TermBase.type_provenance) : TermBase.type_provenance => switch (p1, p2) { - | (Hole(h1), Hole(h2)) when h1 == h2 => Hole(h1) - | (Hole(EmptyHole), Hole(EmptyHole) | SynSwitch) - | (SynSwitch, Hole(EmptyHole)) => Hole(EmptyHole) + | (HoleProvenance(h1), HoleProvenance(h2)) when h1 == h2 => + HoleProvenance(h1) + | ( + HoleProvenance(EmptyTypeHole), + HoleProvenance(EmptyTypeHole) | SynSwitch, + ) + | (SynSwitch, HoleProvenance(EmptyTypeHole)) => + HoleProvenance(EmptyTypeHole) | (SynSwitch, Internal) | (Internal, SynSwitch) => SynSwitch - | (Internal | Hole(_), _) - | (_, Hole(_)) => Internal + | (Internal | HoleProvenance(_), _) + | (_, HoleProvenance(_)) => Internal | (SynSwitch, SynSwitch) => SynSwitch }; @@ -157,9 +162,9 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) => | Float | Bool | String => [] - | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2) - | Var(v) => List.mem(v, bound) ? [] : [v] - | Parens(ty) => free_vars(~bound, ty) + | ApTyp(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2) + | TypVar(v) => List.mem(v, bound) ? [] : [v] + | TypParens(ty) => free_vars(~bound, ty) | List(ty) => free_vars(~bound, ty) | Arrow(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2) | Sum(sm) => ConstructorMap.free_variables(free_vars(~bound), sm) @@ -194,9 +199,9 @@ let eq = (t1: t, t2: t): bool => fast_equal(t1, t2); let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => { let join' = join(~resolve, ~fix, ctx); switch (term_of(ty1), term_of(ty2)) { - | (_, Parens(ty2)) => join'(ty1, ty2) - | (Parens(ty1), _) => join'(ty1, ty2) - | (_, Unknown(Hole(_))) when fix => + | (_, TypParens(ty2)) => join'(ty1, ty2) + | (TypParens(ty1), _) => join'(ty1, ty2) + | (_, Unknown(HoleProvenance(_))) when fix => /* NOTE(andrew): This is load bearing for ensuring that function literals get appropriate casts. Documentation/Dynamics has regression tests */ @@ -205,7 +210,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => Some(Unknown(join_type_provenance(p1, p2)) |> temp) | (Unknown(_), _) => Some(ty2) | (_, Unknown(Internal | SynSwitch)) => Some(ty1) - | (Var(n1), Var(n2)) => + | (TypVar(n1), TypVar(n2)) => if (n1 == n2) { Some(ty1); } else { @@ -214,11 +219,11 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => let+ ty_join = join'(ty1, ty2); !resolve && eq(ty1, ty_join) ? ty1 : ty_join; } - | (Var(name), _) => + | (TypVar(name), _) => let* ty_name = Ctx.lookup_alias(ctx, name); let+ ty_join = join'(ty_name, ty2); !resolve && eq(ty_name, ty_join) ? ty1 : ty_join; - | (_, Var(name)) => + | (_, TypVar(name)) => let* ty_name = Ctx.lookup_alias(ctx, name); let+ ty_join = join'(ty_name, ty1); !resolve && eq(ty_name, ty_join) ? ty2 : ty_join; @@ -227,7 +232,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => let ctx = Ctx.extend_dummy_tvar(ctx, tp1); let ty1' = switch (TPat.tyvar_of_utpat(tp2)) { - | Some(x2) => subst(Var(x2) |> temp, tp1, ty1) + | Some(x2) => subst(TypVar(x2) |> temp, tp1, ty1) | None => ty1 }; let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2); @@ -237,7 +242,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => let ctx = Ctx.extend_dummy_tvar(ctx, x1); let ty1' = switch (TPat.tyvar_of_utpat(x2)) { - | Some(x2) => subst(Var(x2) |> temp, x1, ty1) + | Some(x2) => subst(TypVar(x2) |> temp, x1, ty1) | None => ty1 }; let+ ty_body = join(~resolve, ~fix, ctx, ty1', ty2); @@ -275,7 +280,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => let+ ty = join'(ty1, ty2); List(ty) |> temp; | (List(_), _) => None - | (Ap(_), _) => failwith("Type join of ap") + | (ApTyp(_), _) => failwith("Type join of ap") }; }; @@ -284,7 +289,7 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => let rec match_synswitch = (t1: t, t2: t) => { let (term1, rewrap1) = unwrap(t1); switch (term1, term_of(t2)) { - | (Parens(t1), _) => Parens(match_synswitch(t1, t2)) |> rewrap1 + | (TypParens(t1), _) => TypParens(match_synswitch(t1, t2)) |> rewrap1 | (Unknown(SynSwitch), _) => t2 // These cases can't have a synswitch inside | (Unknown(_), _) @@ -292,8 +297,8 @@ let rec match_synswitch = (t1: t, t2: t) => { | (Float, _) | (Bool, _) | (String, _) - | (Var(_), _) - | (Ap(_), _) + | (TypVar(_), _) + | (ApTyp(_), _) | (Rec(_), _) | (Forall(_), _) => t1 // These might @@ -327,8 +332,8 @@ let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool => let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t => switch (term_of(ty)) { - | Parens(t) => weak_head_normalize(ctx, t) - | Var(x) => + | TypParens(t) => weak_head_normalize(ctx, t) + | TypVar(x) => switch (Ctx.lookup_alias(ctx, x)) { | Some(ty) => weak_head_normalize(ctx, ty) | None => ty @@ -339,7 +344,7 @@ let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t => let rec normalize = (ctx: Ctx.t, ty: t): t => { let (term, rewrap) = unwrap(ty); switch (term) { - | Var(x) => + | TypVar(x) => switch (Ctx.lookup_alias(ctx, x)) { | Some(ty) => normalize(ctx, ty) | None => ty @@ -349,9 +354,10 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => { | Float | Bool | String => ty - | Parens(t) => Parens(normalize(ctx, t)) |> rewrap + | TypParens(t) => TypParens(normalize(ctx, t)) |> rewrap | List(t) => List(normalize(ctx, t)) |> rewrap - | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap + | ApTyp(t1, t2) => + ApTyp(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap | Arrow(t1, t2) => Arrow(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap | Prod(ts) => Prod(List.map(normalize(ctx), ts)) |> rewrap @@ -369,7 +375,7 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => { let rec matched_arrow_strict = (ctx, ty) => switch (term_of(weak_head_normalize(ctx, ty))) { - | Parens(ty) => matched_arrow_strict(ctx, ty) + | TypParens(ty) => matched_arrow_strict(ctx, ty) | Arrow(ty_in, ty_out) => Some((ty_in, ty_out)) | Unknown(SynSwitch) => Some((Unknown(SynSwitch) |> temp, Unknown(SynSwitch) |> temp)) @@ -384,7 +390,7 @@ let matched_arrow = (ctx, ty) => let rec matched_forall_strict = (ctx, ty) => switch (term_of(weak_head_normalize(ctx, ty))) { - | Parens(ty) => matched_forall_strict(ctx, ty) + | TypParens(ty) => matched_forall_strict(ctx, ty) | Forall(t, ty) => Some((Some(t), ty)) | Unknown(SynSwitch) => Some((None, Unknown(SynSwitch) |> temp)) | _ => None // (None, Unknown(Internal) |> temp) @@ -396,7 +402,7 @@ let matched_forall = (ctx, ty) => let rec matched_prod_strict = (ctx, length, ty) => switch (term_of(weak_head_normalize(ctx, ty))) { - | Parens(ty) => matched_prod_strict(ctx, length, ty) + | TypParens(ty) => matched_prod_strict(ctx, length, ty) | Prod(tys) when List.length(tys) == length => Some(tys) | Unknown(SynSwitch) => Some(List.init(length, _ => Unknown(SynSwitch) |> temp)) @@ -409,7 +415,7 @@ let matched_prod = (ctx, length, ty) => let rec matched_list_strict = (ctx, ty) => switch (term_of(weak_head_normalize(ctx, ty))) { - | Parens(ty) => matched_list_strict(ctx, ty) + | TypParens(ty) => matched_list_strict(ctx, ty) | List(ty) => Some(ty) | Unknown(SynSwitch) => Some(Unknown(SynSwitch) |> temp) | _ => None @@ -422,7 +428,7 @@ let matched_list = (ctx, ty) => let rec matched_args = (ctx, default_arity, ty) => { let ty' = weak_head_normalize(ctx, ty); switch (term_of(ty')) { - | Parens(ty) => matched_args(ctx, default_arity, ty) + | TypParens(ty) => matched_args(ctx, default_arity, ty) | Prod([_, ..._] as tys) => tys | Unknown(_) => List.init(default_arity, _ => ty') | _ => [ty'] @@ -432,7 +438,7 @@ let rec matched_args = (ctx, default_arity, ty) => { let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { let ty = weak_head_normalize(ctx, ty); switch (term_of(ty)) { - | Parens(ty) => get_sum_constructors(ctx, ty) + | TypParens(ty) => get_sum_constructors(ctx, ty) | Sum(sm) => Some(sm) | Rec(_) => /* Note: We must unroll here to get right ctr types; @@ -447,7 +453,7 @@ let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { the below code will be incorrect! */ let ty = switch (ty |> term_of) { - | Rec({term: Var(x), _}, ty_body) => + | Rec({term: VarTPat(x), _}, ty_body) => switch (Ctx.lookup_alias(ctx, x)) { | None => unroll(ty) | Some(_) => ty_body @@ -464,7 +470,7 @@ let rec get_sum_constructors = (ctx: Ctx.t, ty: t): option(sum_map) => { let rec is_unknown = (ty: t): bool => switch (ty |> term_of) { - | Parens(x) => is_unknown(x) + | TypParens(x) => is_unknown(x) | Unknown(_) => true | _ => false }; @@ -472,14 +478,14 @@ let rec is_unknown = (ty: t): bool => /* Does the type require parentheses when on the left of an arrow for printing? */ let rec needs_parens = (ty: t): bool => switch (term_of(ty)) { - | Parens(ty) => needs_parens(ty) - | Ap(_) + | TypParens(ty) => needs_parens(ty) + | ApTyp(_) | Unknown(_) | Int | Float | String | Bool - | Var(_) => false + | TypVar(_) => false | Rec(_, _) | Forall(_, _) => true | List(_) => false /* is already wrapped in [] */ @@ -490,23 +496,23 @@ let rec needs_parens = (ty: t): bool => let pretty_print_tvar = (tv: TPat.t): string => switch (IdTagged.term_of(tv)) { - | Var(x) => x - | Invalid(_) - | EmptyHole - | MultiHole(_) => "?" + | VarTPat(x) => x + | InvalidTPat(_) + | EmptyHoleTPat + | MultiHoleTPat(_) => "?" }; /* Essentially recreates haz3lweb/view/Type.re's view_ty but with string output */ let rec pretty_print = (ty: t): string => switch (term_of(ty)) { - | Parens(ty) => pretty_print(ty) - | Ap(_) + | TypParens(ty) => pretty_print(ty) + | ApTyp(_) | Unknown(_) => "?" | Int => "Int" | Float => "Float" | Bool => "Bool" | String => "String" - | Var(tvar) => tvar + | TypVar(tvar) => tvar | List(t) => "[" ++ pretty_print(t) ++ "]" | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2) | Sum(sm) => diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re index f213a18cb7..ecbe752d36 100644 --- a/src/haz3lcore/statics/Ctx.re +++ b/src/haz3lcore/statics/Ctx.re @@ -100,7 +100,8 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) => | Some(Abstract) => None | None => Some( - (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh, + (Unknown(HoleProvenance(InvalidTypeHole(name))): TermBase.Typ.term) + |> IdTagged.fresh, ) }; @@ -114,10 +115,13 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t = id, typ: switch (typ) { - | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh + | None => (TypVar(name): TermBase.typ_term) |> IdTagged.fresh | Some(typ) => ( - Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term + Arrow( + typ, + (TypVar(name): TermBase.typ_term) |> IdTagged.fresh, + ): TermBase.typ_term ) |> IdTagged.fresh }, diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 8aaaeaae3d..38e9180a00 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -339,7 +339,7 @@ let rec status_common = switch ( Typ.join_fix( ctx, - Forall(Var("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp) + Forall(VarTPat("?") |> TPat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp, ty, ) @@ -454,9 +454,10 @@ let rec 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, ty: Typ.t): status_typ => switch (ty.term) { - | Unknown(Hole(Invalid(token))) => InHole(BadToken(token)) - | Unknown(Hole(EmptyHole)) => NotInHole(Type(ty)) - | Var(name) => + | Unknown(HoleProvenance(InvalidTypeHole(token))) => + InHole(BadToken(token)) + | Unknown(HoleProvenance(EmptyTypeHole)) => NotInHole(Type(ty)) + | TypVar(name) => switch (expects) { | VariantExpected(Unique, sum_ty) | ConstructorExpected(Unique, sum_ty) => @@ -469,16 +470,16 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ => | false => switch (Ctx.is_abstract(ctx, name)) { | false => InHole(FreeTypeVariable(name)) - | true => NotInHole(Type(Var(name) |> Typ.temp)) + | true => NotInHole(Type(TypVar(name) |> Typ.temp)) } | true => NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty))) } } - | Ap(t1, ty_in) => + | ApTyp(t1, ty_in) => switch (expects) { | VariantExpected(status_variant, ty_variant) => switch (status_variant, t1.term) { - | (Unique, Var(name)) => + | (Unique, TypVar(name)) => NotInHole(Variant(name, Arrow(ty_in, ty_variant) |> Typ.temp)) | _ => NotInHole(VariantIncomplete(Arrow(ty_in, ty_variant) |> Typ.temp)) @@ -496,8 +497,8 @@ let status_typ = (ctx: Ctx.t, expects: typ_expects, ty: Typ.t): status_typ => let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat => switch (utpat.term) { - | EmptyHole => NotInHole(Empty) - | Var(name) when Ctx.shadows_typ(ctx, name) => + | EmptyHoleTPat => NotInHole(Empty) + | VarTPat(name) when Ctx.shadows_typ(ctx, name) => let f = src => InHole(ShadowsType(name, src)); if (Form.is_base_typ(name)) { f(BaseTyp); @@ -506,9 +507,9 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat => } else { f(TyVar); }; - | Var(name) => NotInHole(Var(name)) - | Invalid(_) => InHole(NotAVar(NotCapitalized)) - | MultiHole(_) => InHole(NotAVar(Other)) + | VarTPat(name) => NotInHole(Var(name)) + | InvalidTPat(_) => InHole(NotAVar(NotCapitalized)) + | MultiHoleTPat(_) => InHole(NotAVar(Other)) }; /* Determines whether any term is in an error hole. */ @@ -593,7 +594,7 @@ let fixed_constraint_pat = ) : Constraint.t => switch (upat.term) { - | Cast(_) => constraint_ + | CastPat(_) => constraint_ | _ => switch (fixed_typ_pat(ctx, mode, self) |> Typ.term_of) { | Unknown(_) => Constraint.Hole @@ -677,10 +678,10 @@ let get_binding_site = (info: t): option(Id.t) => { let+ entry = Ctx.lookup_var(ctx, name); entry.id; | InfoExp({term: {term: Constructor(name, _), _}, ctx, _}) - | InfoPat({term: {term: Constructor(name, _), _}, ctx, _}) => + | InfoPat({term: {term: ConstructorPat(name, _), _}, ctx, _}) => let+ entry = Ctx.lookup_ctr(ctx, name); entry.id; - | InfoTyp({term: {term: Var(name), _}, ctx, _}) => + | InfoTyp({term: {term: TypVar(name), _}, ctx, _}) => Ctx.lookup_tvar_id(ctx, name) | _ => None }; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index d1edb9d16a..ba5049547e 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -126,16 +126,16 @@ let rm_and_log_projectors = (seg: Segment.t): Segment.t => let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) = fun - | {term: Var(ctr), ids, _} => Variant(ctr, ids, None) - | {term: Ap({term: Var(ctr), ids: ids_ctr, _}, u), ids: ids_ap, _} => + | {term: TypVar(ctr), ids, _} => Variant(ctr, ids, None) + | {term: ApTyp({term: TypVar(ctr), ids: ids_ctr, _}, u), ids: ids_ap, _} => Variant(ctr, ids_ctr @ ids_ap, Some(u)) | t => BadEntry(t); let mk_bad = (ctr, ids, value) => { - let t: Typ.t = {ids, copied: false, term: Var(ctr)}; + let t: Typ.t = {ids, copied: false, term: TypVar(ctr)}; switch (value) { | None => t - | Some(u) => Ap(t, u) |> Typ.fresh + | Some(u) => ApTyp(t, u) |> Typ.fresh }; }; @@ -182,12 +182,13 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_empty_tuple(t) => ret(Tuple([])) | ([t], []) when Form.is_wild(t) => ret(Deferral(OutsideAp)) | ([t], []) when Form.is_empty_list(t) => ret(ListLit([])) - | ([t], []) when Form.is_bool(t) => ret(Bool(bool_of_string(t))) + | ([t], []) when Form.is_bool(t) => ret(BoolLit(bool_of_string(t))) | ([t], []) when Form.is_undefined(t) => ret(Undefined) - | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t))) + | ([t], []) when Form.is_int(t) => ret(IntLit(int_of_string(t))) | ([t], []) when Form.is_string(t) => - ret(String(Form.strip_quotes(t))) - | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t))) + ret(StringLit(Form.strip_quotes(t))) + | ([t], []) when Form.is_float(t) => + ret(FloatLit(float_of_string(t))) | ([t], []) when Form.is_var(t) => ret(Var(t)) | ([t], []) when Form.is_ctr(t) => ret(Constructor(t, Unknown(Internal) |> Typ.temp)) @@ -221,13 +222,13 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r, None) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) | (["hide", "in"], [Exp(filter)]) => - Filter(Filter({act: (Eval, One), pat: filter}), r) + Filter(FilterStepper({act: (Eval, One), pat: filter}), r) | (["eval", "in"], [Exp(filter)]) => - Filter(Filter({act: (Eval, All), pat: filter}), r) + Filter(FilterStepper({act: (Eval, All), pat: filter}), r) | (["pause", "in"], [Exp(filter)]) => - Filter(Filter({act: (Step, One), pat: filter}), r) + Filter(FilterStepper({act: (Step, One), pat: filter}), r) | (["debug", "in"], [Exp(filter)]) => - Filter(Filter({act: (Step, All), pat: filter}), r) + Filter(FilterStepper({act: (Step, All), pat: filter}), r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => TyAlias(tpat, def, r) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => @@ -335,23 +336,24 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | ([(_id, tile)], []) => ret( switch (tile) { - | ([t], []) when Form.is_empty_tuple(t) => Tuple([]) - | ([t], []) when Form.is_empty_list(t) => ListLit([]) - | ([t], []) when Form.is_bool(t) => Bool(bool_of_string(t)) - | ([t], []) when Form.is_float(t) => Float(float_of_string(t)) - | ([t], []) when Form.is_int(t) => Int(int_of_string(t)) - | ([t], []) when Form.is_string(t) => String(Form.strip_quotes(t)) - | ([t], []) when Form.is_var(t) => Var(t) + | ([t], []) when Form.is_empty_tuple(t) => TuplePat([]) + | ([t], []) when Form.is_empty_list(t) => ListLitPat([]) + | ([t], []) when Form.is_bool(t) => BoolPat(bool_of_string(t)) + | ([t], []) when Form.is_float(t) => FloatPat(float_of_string(t)) + | ([t], []) when Form.is_int(t) => IntPat(int_of_string(t)) + | ([t], []) when Form.is_string(t) => + StringPat(Form.strip_quotes(t)) + | ([t], []) when Form.is_var(t) => VarPat(t) | ([t], []) when Form.is_wild(t) => Wild | ([t], []) when Form.is_ctr(t) => - Constructor(t, Unknown(Internal) |> Typ.fresh) + ConstructorPat(t, Unknown(Internal) |> Typ.fresh) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => - Invalid(t) - | (["(", ")"], [Pat(body)]) => Parens(body) + InvalidPat(t) + | (["(", ")"], [Pat(body)]) => ParensPat(body) | (["[", "]"], [Pat(body)]) => switch (body) { - | {term: Tuple(ps), _} => ListLit(ps) - | term => ListLit([term]) + | {term: TuplePat(ps), _} => ListLitPat(ps) + | term => ListLitPat([term]) } | _ => hole(tm) }, @@ -363,7 +365,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | ([(_id, t)], []) => ret( switch (t) { - | (["(", ")"], [Pat(arg)]) => Ap(l, arg) + | (["(", ")"], [Pat(arg)]) => ApPat(l, arg) | _ => hole(tm) }, ) @@ -373,15 +375,15 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | Bin(Pat(p), tiles, Typ(ty)) as tm => switch (tiles) { | ([(_id, ([":"], []))], []) => - ret(Cast(p, ty, Unknown(Internal) |> Typ.fresh)) + ret(CastPat(p, ty, Unknown(Internal) |> Typ.fresh)) | _ => ret(hole(tm)) } | Bin(Pat(l), tiles, Pat(r)) as tm => switch (is_tuple_pat(tiles)) { - | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r])) + | Some(between_kids) => ret(TuplePat([l] @ between_kids @ [r])) | None => switch (tiles) { - | ([(_id, (["::"], []))], []) => ret(Cons(l, r)) + | ([(_id, (["::"], []))], []) => ret(ConsPat(l, r)) | _ => ret(hole(tm)) } } @@ -406,11 +408,11 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { | (["Int"], []) => Int | (["Float"], []) => Float | (["String"], []) => String - | ([t], []) when Form.is_typ_var(t) => Var(t) - | (["(", ")"], [Typ(body)]) => Parens(body) + | ([t], []) when Form.is_typ_var(t) => TypVar(t) + | (["(", ")"], [Typ(body)]) => TypParens(body) | (["[", "]"], [Typ(body)]) => List(body) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => - Unknown(Hole(Invalid(t))) + Unknown(HoleProvenance(InvalidTypeHole(t))) | _ => hole(tm) }, ) @@ -418,7 +420,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { } | Post(Typ(t), tiles) as tm => switch (tiles) { - | ([(_, (["(", ")"], [Typ(typ)]))], []) => ret(Ap(t, typ)) + | ([(_, (["(", ")"], [Typ(typ)]))], []) => ret(ApTyp(t, typ)) | _ => ret(hole(tm)) } /* forall and rec have to be before sum so that they bind tighter. @@ -476,9 +478,9 @@ and tpat_term: unsorted => TPat.term = { | ([(_id, tile)], []) => ret( switch (tile) { - | ([t], []) when Form.is_typ_var(t) => Var(t) + | ([t], []) when Form.is_typ_var(t) => VarTPat(t) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => - Invalid(t) + InvalidTPat(t) | _ => hole(tm) }, ) diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index 2415399627..645f6f5556 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -35,7 +35,10 @@ let ty_of: t => Typ.t = Arrow(Unknown(SynSwitch) |> Typ.temp, Unknown(SynSwitch) |> Typ.temp) |> Typ.temp | SynTypFun => - Forall(Var("syntypfun") |> TPat.fresh, Unknown(SynSwitch) |> Typ.temp) + Forall( + VarTPat("syntypfun") |> TPat.fresh, + Unknown(SynSwitch) |> Typ.temp, + ) |> Typ.temp; /* TODO: naming the type variable? */ let of_arrow = (ctx: Ctx.t, mode: t): (t, t) => @@ -55,7 +58,7 @@ let of_forall = (ctx: Ctx.t, name_opt: option(string), mode: t): t => let (name_expected_opt, item) = Typ.matched_forall(ctx, ty); switch (name_opt, name_expected_opt) { | (Some(name), Some(name_expected)) => - Ana(Typ.subst(Var(name) |> Typ.temp, name_expected, item)) + Ana(Typ.subst(TypVar(name) |> Typ.temp, name_expected, item)) | _ => Ana(item) }; }; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 443c94155b..e198f7bc04 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -120,7 +120,7 @@ let typ_exp_binop: Operators.op_bin => (Typ.t, Typ.t, Typ.t) = let typ_exp_unop: Operators.op_un => (Typ.t, Typ.t) = fun | Meta(Unquote) => ( - Var("$Meta") |> Typ.temp, + TypVar("$Meta") |> Typ.temp, Unknown(Internal) |> Typ.temp, ) | Bool(Not) => (Bool |> Typ.temp, Bool |> Typ.temp) @@ -226,11 +226,12 @@ and uexp_to_info_map = | EmptyHole => atomic(Just(Unknown(Internal) |> Typ.temp)) | Deferral(position) => add'(~self=IsDeferral(position), ~co_ctx=CoCtx.empty, m) - | Undefined => atomic(Just(Unknown(Hole(EmptyHole)) |> Typ.temp)) - | Bool(_) => atomic(Just(Bool |> Typ.temp)) - | Int(_) => atomic(Just(Int |> Typ.temp)) - | Float(_) => atomic(Just(Float |> Typ.temp)) - | String(_) => atomic(Just(String |> Typ.temp)) + | Undefined => + atomic(Just(Unknown(HoleProvenance(EmptyTypeHole)) |> Typ.temp)) + | BoolLit(_) => atomic(Just(Bool |> Typ.temp)) + | IntLit(_) => atomic(Just(Int |> Typ.temp)) + | FloatLit(_) => atomic(Just(Float |> Typ.temp)) + | StringLit(_) => atomic(Just(String |> Typ.temp)) | ListLit(es) => let ids = List.map(UExp.rep_id, es); let modes = Mode.of_list_lit(ctx, List.length(es), mode); @@ -281,7 +282,7 @@ and uexp_to_info_map = | _ => e.term }, }; - let ty_in = Var("$Meta") |> Typ.temp; + let ty_in = TypVar("$Meta") |> Typ.temp; let ty_out = Unknown(Internal) |> Typ.temp; let (e, m) = go(~mode=Ana(ty_in), e, m); add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m); @@ -311,7 +312,7 @@ and uexp_to_info_map = | Test(e) => let (e, m) = go(~mode=Ana(Bool |> Typ.temp), e, m); add(~self=Just(Prod([]) |> Typ.temp), ~co_ctx=e.co_ctx, m); - | Filter(Filter({pat: cond, _}), body) => + | Filter(FilterStepper({pat: cond, _}), body) => let (cond, m) = go(~mode=Syn, cond, m, ~is_in_filter=true); let (body, m) = go(~mode, body, m); add( @@ -373,7 +374,7 @@ and uexp_to_info_map = let self = is_exhaustive ? unwrapped_self : InexhaustiveMatch(unwrapped_self); add'(~self, ~co_ctx=CoCtx.mk(ctx, p.ctx, e.co_ctx), m); - | TypFun({term: Var(name), _} as utpat, body, _) + | TypFun({term: VarTPat(name), _} as utpat, body, _) when !Ctx.shadows_typ(ctx, name) => let mode_body = Mode.of_forall(ctx, Some(name), mode); let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd; @@ -600,7 +601,7 @@ and uexp_to_info_map = | TyAlias(typat, utyp, body) => let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd; switch (typat.term) { - | Var(name) when !Ctx.shadows_typ(ctx, name) => + | VarTPat(name) when !Ctx.shadows_typ(ctx, name) => /* Currently we disallow all type shadowing */ /* NOTE(andrew): Currently, UTyp.to_typ returns Unknown(TypeHole) for any type variable reference not in its ctx. So any free variables @@ -615,7 +616,8 @@ and uexp_to_info_map = use a different name than the alias for the recursive parameter */ //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre)); let ty_rec = - Rec((Var(name): TPat.term) |> IdTagged.fresh, utyp) |> Typ.temp; + Rec((VarTPat(name): TPat.term) |> IdTagged.fresh, utyp) + |> Typ.temp; let ctx_def = Ctx.extend_alias(ctx, name, TPat.rep_id(typat), ty_rec); (ty_rec, ctx_def, ctx_def); @@ -650,10 +652,10 @@ and uexp_to_info_map = let ty_escape = Typ.subst(ty_def, typat, 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 - | MultiHole(_) => + | VarTPat(_) + | InvalidTPat(_) + | EmptyHoleTPat + | MultiHoleTPat(_) => let ({co_ctx, ty: ty_body, _}: Info.exp, m) = go'(~ctx, ~mode, body, m); let m = utyp_to_info_map(~ctx, ~ancestors, utyp, m) |> snd; @@ -713,25 +715,25 @@ and upat_to_info_map = ); let hole = self => atomic(self, Constraint.Hole); switch (term) { - | MultiHole(tms) => + | MultiHolePat(tms) => let (_, m) = multi(~ctx, ~ancestors, m, tms); add(~self=IsMulti, ~ctx, ~constraint_=Constraint.Hole, m); - | Invalid(token) => hole(BadToken(token)) - | EmptyHole => hole(Just(unknown)) - | Int(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int)) - | Float(float) => + | InvalidPat(token) => hole(BadToken(token)) + | EmptyHolePat => hole(Just(unknown)) + | IntPat(int) => atomic(Just(Int |> Typ.temp), Constraint.Int(int)) + | FloatPat(float) => atomic(Just(Float |> Typ.temp), Constraint.Float(float)) - | Tuple([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth) - | Bool(bool) => + | TuplePat([]) => atomic(Just(Prod([]) |> Typ.temp), Constraint.Truth) + | BoolPat(bool) => atomic( Just(Bool |> Typ.temp), bool ? Constraint.InjL(Constraint.Truth) : Constraint.InjR(Constraint.Truth), ) - | String(string) => + | StringPat(string) => atomic(Just(String |> Typ.temp), Constraint.String(string)) - | ListLit(ps) => + | ListLitPat(ps) => let ids = List.map(UPat.rep_id, ps); let modes = Mode.of_list_lit(ctx, List.length(ps), mode); let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); @@ -747,7 +749,7 @@ and upat_to_info_map = ~constraint_=cons_fold_list(cons), m, ); - | Cons(hd, tl) => + | ConsPat(hd, tl) => let (hd, m) = go(~ctx, ~mode=Mode.of_cons_hd(ctx, mode), hd, m); let (tl, m) = go(~ctx=hd.ctx, ~mode=Mode.of_cons_tl(ctx, mode, hd.ty), tl, m); @@ -759,7 +761,7 @@ and upat_to_info_map = m, ); | Wild => atomic(Just(unknown), Constraint.Truth) - | Var(name) => + | VarPat(name) => /* NOTE: The self type assigned to pattern variables (Unknown) may be SynSwitch, but SynSwitch is never added to the context; Unknown(Internal) is used in this case */ @@ -776,7 +778,7 @@ and upat_to_info_map = ~constraint_=Constraint.Truth, m, ); - | Tuple(ps) => + | TuplePat(ps) => let modes = Mode.of_prod(ctx, mode, List.length(ps)); let (ctx, tys, cons, m) = ctx_fold(ctx, m, ps, modes); let rec cons_fold_tuple = cs => @@ -791,13 +793,13 @@ and upat_to_info_map = ~constraint_=cons_fold_tuple(cons), m, ); - | Parens(p) => + | ParensPat(p) => let (p, m) = go(~ctx, ~mode, p, m); add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m); - | Constructor(ctr, _) => + | ConstructorPat(ctr, _) => let self = Self.of_ctr(ctx, ctr); atomic(self, Constraint.of_ctr(ctx, mode, ctr, self)); - | Ap(fn, arg) => + | ApPat(fn, arg) => let ctr = UPat.ctr_name(fn); let fn_mode = Mode.of_ap(ctx, mode, ctr); let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m); @@ -810,7 +812,7 @@ and upat_to_info_map = Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)), m, ); - | Cast(p, ann, _) => + | CastPat(p, ann, _) => let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m); let (p, m) = go(~ctx, ~mode=Ana(ann.term), p, m); add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m); @@ -833,7 +835,7 @@ and utyp_to_info_map = let go' = utyp_to_info_map(~ctx, ~ancestors); let go = go'(~expects=TypeExpected); switch (term) { - | Unknown(Hole(MultiHole(tms))) => + | Unknown(HoleProvenance(MultiTypeHole(tms))) => let (_, m) = multi(~ctx, ~ancestors, m, tms); add(m); | Unknown(_) @@ -841,11 +843,11 @@ and utyp_to_info_map = | Float | Bool | String => add(m) - | Var(_) => + | TypVar(_) => /* Names are resolved in Info.status_typ */ add(m) | List(t) - | Parens(t) => add(go(t, m) |> snd) + | TypParens(t) => add(go(t, m) |> snd) | Arrow(t1, t2) => let m = go(t1, m) |> snd; let m = go(t2, m) |> snd; @@ -853,7 +855,7 @@ and utyp_to_info_map = | Prod(ts) => let m = map_m(go, ts, m) |> snd; add(m); - | Ap(t1, t2) => + | ApTyp(t1, t2) => let t1_mode: Info.typ_expects = switch (expects) { | VariantExpected(m, sum_ty) => @@ -875,7 +877,7 @@ and utyp_to_info_map = variants, ); add(m); - | Forall({term: Var(name), _} as utpat, tbody) => + | Forall({term: VarTPat(name), _} as utpat, tbody) => let body_ctx = Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract}); let m = @@ -895,7 +897,7 @@ and utyp_to_info_map = |> snd; let m = utpat_to_info_map(~ctx, ~ancestors, utpat, m) |> snd; add(m); // TODO: check with andrew - | Rec({term: Var(name), _} as utpat, tbody) => + | Rec({term: VarTPat(name), _} as utpat, tbody) => let body_ctx = Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract}); let m = @@ -926,12 +928,12 @@ and utpat_to_info_map = }; let ancestors = [TPat.rep_id(utpat)] @ ancestors; switch (term) { - | MultiHole(tms) => + | MultiHoleTPat(tms) => let (_, m) = multi(~ctx, ~ancestors, m, tms); add(m); - | Invalid(_) - | EmptyHole - | Var(_) => add(m) + | InvalidTPat(_) + | EmptyHoleTPat + | VarTPat(_) => add(m) }; } and variant_to_info_map = @@ -954,7 +956,7 @@ and variant_to_info_map = List.mem(ctr, ctrs) ? Duplicate : Unique, ty_sum, ), - {term: Var(ctr), ids, copied: false}, + {term: TypVar(ctr), ids, copied: false}, m, ) |> snd; diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 92eef8161e..18584ced4e 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -33,28 +33,28 @@ module Pat = { let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term => switch (tms) { - | [] => EmptyHole - | [_, ..._] => MultiHole(tms) + | [] => EmptyHolePat + | [_, ..._] => MultiHolePat(tms) }; let cls_of_term: term => cls = fun - | Invalid(_) => Invalid - | EmptyHole => EmptyHole - | MultiHole(_) => MultiHole + | InvalidPat(_) => Invalid + | EmptyHolePat => EmptyHole + | MultiHolePat(_) => MultiHole | Wild => Wild - | Int(_) => Int - | Float(_) => Float - | Bool(_) => Bool - | String(_) => String - | ListLit(_) => ListLit - | Constructor(_) => Constructor - | Cons(_) => Cons - | Var(_) => Var - | Tuple(_) => Tuple - | Parens(_) => Parens - | Ap(_) => Ap - | Cast(_) => Cast; + | IntPat(_) => Int + | FloatPat(_) => Float + | BoolPat(_) => Bool + | StringPat(_) => String + | ListLitPat(_) => ListLit + | ConstructorPat(_) => Constructor + | ConsPat(_) => Cons + | VarPat(_) => Var + | TuplePat(_) => Tuple + | ParensPat(_) => Parens + | ApPat(_) => Ap + | CastPat(_) => Cast; let show_cls: cls => string = fun @@ -77,44 +77,44 @@ module Pat = { let rec is_var = (pat: t) => { switch (pat.term) { - | Parens(pat) - | Cast(pat, _, _) => is_var(pat) - | Var(_) => true - | Invalid(_) - | EmptyHole - | MultiHole(_) + | ParensPat(pat) + | CastPat(pat, _, _) => is_var(pat) + | VarPat(_) => true + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Tuple(_) - | Constructor(_) - | Ap(_) => false + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | TuplePat(_) + | ConstructorPat(_) + | ApPat(_) => false }; }; let rec is_fun_var = (pat: t) => { switch (pat.term) { - | Parens(pat) => is_fun_var(pat) - | Cast(pat, typ, _) => + | ParensPat(pat) => is_fun_var(pat) + | CastPat(pat, typ, _) => is_var(pat) && (UTyp.is_arrow(typ) || Typ.is_forall(typ)) - | Invalid(_) - | EmptyHole - | MultiHole(_) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Tuple(_) - | Constructor(_) - | Ap(_) => false + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | TuplePat(_) + | ConstructorPat(_) + | ApPat(_) => false }; }; @@ -122,22 +122,22 @@ module Pat = { is_fun_var(pat) || ( switch (pat.term) { - | Parens(pat) => is_tuple_of_arrows(pat) - | Tuple(pats) => pats |> List.for_all(is_fun_var) - | Invalid(_) - | EmptyHole - | MultiHole(_) + | ParensPat(pat) => is_tuple_of_arrows(pat) + | TuplePat(pats) => pats |> List.for_all(is_fun_var) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Cast(_) - | Constructor(_) - | Ap(_) => false + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | CastPat(_) + | ConstructorPat(_) + | ApPat(_) => false } ); @@ -145,69 +145,69 @@ module Pat = { is_var(pat) || ( switch (pat.term) { - | Parens(pat) - | Cast(pat, _, _) => is_tuple_of_vars(pat) - | Tuple(pats) => pats |> List.for_all(is_var) - | Invalid(_) - | EmptyHole - | MultiHole(_) + | ParensPat(pat) + | CastPat(pat, _, _) => is_tuple_of_vars(pat) + | TuplePat(pats) => pats |> List.for_all(is_var) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Constructor(_) - | Ap(_) => false + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | ConstructorPat(_) + | ApPat(_) => false } ); let rec get_var = (pat: t) => { switch (pat.term) { - | Parens(pat) => get_var(pat) - | Var(x) => Some(x) - | Cast(x, _, _) => get_var(x) - | Invalid(_) - | EmptyHole - | MultiHole(_) + | ParensPat(pat) => get_var(pat) + | VarPat(x) => Some(x) + | CastPat(x, _, _) => get_var(x) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Tuple(_) - | Constructor(_) - | Ap(_) => None + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | TuplePat(_) + | ConstructorPat(_) + | ApPat(_) => None }; }; let rec get_fun_var = (pat: t) => { switch (pat.term) { - | Parens(pat) => get_fun_var(pat) - | Cast(pat, t1, _) => + | ParensPat(pat) => get_fun_var(pat) + | CastPat(pat, t1, _) => if (Typ.is_arrow(t1) || UTyp.is_forall(t1)) { get_var(pat) |> Option.map(var => var); } else { None; } - | Invalid(_) - | EmptyHole - | MultiHole(_) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Tuple(_) - | Constructor(_) - | Ap(_) => None + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | TuplePat(_) + | ConstructorPat(_) + | ApPat(_) => None }; }; @@ -216,28 +216,28 @@ module Pat = { | Some(x) => Some([x]) | None => switch (pat.term) { - | Parens(pat) - | Cast(pat, _, _) => get_bindings(pat) - | Tuple(pats) => + | ParensPat(pat) + | CastPat(pat, _, _) => get_bindings(pat) + | TuplePat(pats) => let vars = pats |> List.map(get_var); if (List.exists(Option.is_none, vars)) { None; } else { Some(List.map(Option.get, vars)); }; - | Invalid(_) - | EmptyHole - | MultiHole(_) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Constructor(_) - | Ap(_) => None + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | ConstructorPat(_) + | ApPat(_) => None } }; @@ -246,29 +246,29 @@ module Pat = { Some(1); } else { switch (pat.term) { - | Parens(pat) - | Cast(pat, _, _) => get_num_of_vars(pat) - | Tuple(pats) => + | ParensPat(pat) + | CastPat(pat, _, _) => get_num_of_vars(pat) + | TuplePat(pats) => is_tuple_of_vars(pat) ? Some(List.length(pats)) : None - | Invalid(_) - | EmptyHole - | MultiHole(_) + | InvalidPat(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Cons(_, _) - | Var(_) - | Constructor(_) - | Ap(_) => None + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConsPat(_, _) + | VarPat(_) + | ConstructorPat(_) + | ApPat(_) => None }; }; let ctr_name = (p: t): option(Constructor.t) => switch (p.term) { - | Constructor(name, _) => Some(name) + | ConstructorPat(name, _) => Some(name) | _ => None }; }; @@ -337,10 +337,10 @@ module Exp = { | FailedCast(_) => FailedCast | Deferral(_) => Deferral | Undefined => Undefined - | Bool(_) => Bool - | Int(_) => Int - | Float(_) => Float - | String(_) => String + | BoolLit(_) => Bool + | IntLit(_) => Int + | FloatLit(_) => Float + | StringLit(_) => String | ListLit(_) => ListLit | Constructor(_) => Constructor | Fun(_) => Fun @@ -425,10 +425,10 @@ module Exp = { | FailedCast(_) | Deferral(_) | Undefined - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | ListLit(_) | Tuple(_) | Var(_) @@ -466,10 +466,10 @@ module Exp = { | FailedCast(_) | Deferral(_) | Undefined - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | ListLit(_) | Fun(_) | TypFun(_) @@ -526,10 +526,10 @@ module Exp = { | Cast(_) | Deferral(_) | Undefined - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | ListLit(_) | Fun(_) | TypFun(_) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 02bd8400d4..0c888d8ef7 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -63,10 +63,10 @@ and exp_term = | FailedCast(exp_t, typ_t, typ_t) | Deferral(deferral_position_t) | Undefined - | Bool(bool) - | Int(int) - | Float(float) - | String(string) + | BoolLit(bool) + | IntLit(int) + | FloatLit(float) + | StringLit(string) | ListLit(list(exp_t)) | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions | Fun( @@ -102,22 +102,22 @@ and exp_term = | Cast(exp_t, typ_t, typ_t) and exp_t = IdTagged.t(exp_term) and pat_term = - | Invalid(string) - | EmptyHole - | MultiHole(list(any_t)) + | InvalidPat(string) + | EmptyHolePat + | MultiHolePat(list(any_t)) | Wild - | Int(int) - | Float(float) - | Bool(bool) - | String(string) - | ListLit(list(pat_t)) - | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic patterns - | Cons(pat_t, pat_t) - | Var(Var.t) - | Tuple(list(pat_t)) - | Parens(pat_t) - | Ap(pat_t, pat_t) - | Cast(pat_t, typ_t, typ_t) + | IntPat(int) + | FloatPat(float) + | BoolPat(bool) + | StringPat(string) + | ListLitPat(list(pat_t)) + | ConstructorPat(string, typ_t) // Typ.t field is only meaningful in dynamic patterns + | ConsPat(pat_t, pat_t) + | VarPat(Var.t) + | TuplePat(list(pat_t)) + | ParensPat(pat_t) + | ApPat(pat_t, pat_t) + | CastPat(pat_t, typ_t, typ_t) and pat_t = IdTagged.t(pat_term) and typ_term = | Unknown(type_provenance) @@ -125,39 +125,39 @@ and typ_term = | Float | Bool | String - | Var(string) + | TypVar(string) | List(typ_t) | Arrow(typ_t, typ_t) | Sum(ConstructorMap.t(typ_t)) | Prod(list(typ_t)) - | Parens(typ_t) - | Ap(typ_t, typ_t) + | TypParens(typ_t) + | ApTyp(typ_t, typ_t) | Rec(tpat_t, typ_t) | Forall(tpat_t, typ_t) and typ_t = IdTagged.t(typ_term) and tpat_term = - | Invalid(string) - | EmptyHole - | MultiHole(list(any_t)) - | Var(string) + | InvalidTPat(string) + | EmptyHoleTPat + | MultiHoleTPat(list(any_t)) + | VarTPat(string) and tpat_t = IdTagged.t(tpat_term) and rul_term = - | Invalid(string) + | InvalidRule(string) | Hole(list(any_t)) | Rules(exp_t, list((pat_t, exp_t))) and rul_t = IdTagged.t(rul_term) and environment_t = VarBstMap.Ordered.t_(exp_t) and closure_environment_t = (Id.t, environment_t) and stepper_filter_kind_t = - | Filter(filter) + | FilterStepper(filter) | Residue(int, FilterAction.t) and type_hole = - | Invalid(string) - | EmptyHole - | MultiHole(list(any_t)) + | InvalidTypeHole(string) + | EmptyTypeHole + | MultiTypeHole(list(any_t)) and type_provenance = | SynSwitch - | Hole(type_hole) + | HoleProvenance(type_hole) | Internal and filter = { pat: exp_t, @@ -296,11 +296,11 @@ and Exp: { switch (term) { | EmptyHole | Invalid(_) - | Bool(_) - | Int(_) - | Float(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) | Constructor(_) - | String(_) + | StringLit(_) | Deferral(_) | Var(_) | Undefined => term @@ -365,10 +365,10 @@ and Exp: { && Typ.fast_equal(t1, t3) && Typ.fast_equal(t2, t4) | (Deferral(d1), Deferral(d2)) => d1 == d2 - | (Bool(b1), Bool(b2)) => b1 == b2 - | (Int(i1), Int(i2)) => i1 == i2 - | (Float(f1), Float(f2)) => f1 == f2 - | (String(s1), String(s2)) => s1 == s2 + | (BoolLit(b1), BoolLit(b2)) => b1 == b2 + | (IntLit(i1), IntLit(i2)) => i1 == i2 + | (FloatLit(f1), FloatLit(f2)) => f1 == f2 + | (StringLit(s1), StringLit(s2)) => s1 == s2 | (ListLit(xs), ListLit(ys)) => List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys) | (Constructor(c1, ty1), Constructor(c2, ty2)) => @@ -431,10 +431,10 @@ and Exp: { | (Invalid(_), _) | (FailedCast(_), _) | (Deferral(_), _) - | (Bool(_), _) - | (Int(_), _) - | (Float(_), _) - | (String(_), _) + | (BoolLit(_), _) + | (IntLit(_), _) + | (FloatLit(_), _) + | (StringLit(_), _) | (ListLit(_), _) | (Constructor(_), _) | (Fun(_), _) @@ -509,23 +509,24 @@ and Pat: { ...exp, term: switch (term) { - | EmptyHole - | Invalid(_) + | EmptyHolePat + | InvalidPat(_) | Wild - | Bool(_) - | Int(_) - | Float(_) - | Constructor(_) - | String(_) - | Var(_) => term - | MultiHole(things) => MultiHole(List.map(any_map_term, things)) - | ListLit(ts) => ListLit(List.map(pat_map_term, ts)) - | Ap(e1, e2) => Ap(pat_map_term(e1), pat_map_term(e2)) - | Cons(e1, e2) => Cons(pat_map_term(e1), pat_map_term(e2)) - | Tuple(xs) => Tuple(List.map(pat_map_term, xs)) - | Parens(e) => Parens(pat_map_term(e)) - | Cast(e, t1, t2) => - Cast(pat_map_term(e), typ_map_term(t1), typ_map_term(t2)) + | BoolPat(_) + | IntPat(_) + | FloatPat(_) + | ConstructorPat(_) + | StringPat(_) + | VarPat(_) => term + | MultiHolePat(things) => + MultiHolePat(List.map(any_map_term, things)) + | ListLitPat(ts) => ListLitPat(List.map(pat_map_term, ts)) + | ApPat(e1, e2) => ApPat(pat_map_term(e1), pat_map_term(e2)) + | ConsPat(e1, e2) => ConsPat(pat_map_term(e1), pat_map_term(e2)) + | TuplePat(xs) => TuplePat(List.map(pat_map_term, xs)) + | ParensPat(e) => ParensPat(pat_map_term(e)) + | CastPat(e, t1, t2) => + CastPat(pat_map_term(e), typ_map_term(t1), typ_map_term(t2)) }, }; x |> f_pat(rec_call); @@ -533,45 +534,46 @@ and Pat: { let rec fast_equal = (p1: t, p2: t) => switch (p1 |> IdTagged.term_of, p2 |> IdTagged.term_of) { - | (Parens(x), _) => fast_equal(x, p2) - | (_, Parens(x)) => fast_equal(p1, x) - | (EmptyHole, EmptyHole) => true - | (MultiHole(xs), MultiHole(ys)) => + | (ParensPat(x), _) => fast_equal(x, p2) + | (_, ParensPat(x)) => fast_equal(p1, x) + | (EmptyHolePat, EmptyHolePat) => true + | (MultiHolePat(xs), MultiHolePat(ys)) => List.length(xs) == List.length(ys) && List.equal(Any.fast_equal, xs, ys) - | (Invalid(s1), Invalid(s2)) => s1 == s2 + | (InvalidPat(s1), InvalidPat(s2)) => s1 == s2 | (Wild, Wild) => true - | (Bool(b1), Bool(b2)) => b1 == b2 - | (Int(i1), Int(i2)) => i1 == i2 - | (Float(f1), Float(f2)) => f1 == f2 - | (String(s1), String(s2)) => s1 == s2 - | (Constructor(c1, t1), Constructor(c2, t2)) => + | (BoolPat(b1), BoolPat(b2)) => b1 == b2 + | (IntPat(i1), IntPat(i2)) => i1 == i2 + | (FloatPat(f1), FloatPat(f2)) => f1 == f2 + | (StringPat(s1), StringPat(s2)) => s1 == s2 + | (ConstructorPat(c1, t1), ConstructorPat(c2, t2)) => c1 == c2 && Typ.fast_equal(t1, t2) - | (Var(v1), Var(v2)) => v1 == v2 - | (ListLit(xs), ListLit(ys)) => + | (VarPat(v1), VarPat(v2)) => v1 == v2 + | (ListLitPat(xs), ListLitPat(ys)) => List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys) - | (Cons(x1, y1), Cons(x2, y2)) => + | (ConsPat(x1, y1), ConsPat(x2, y2)) => fast_equal(x1, x2) && fast_equal(y1, y2) - | (Tuple(xs), Tuple(ys)) => + | (TuplePat(xs), TuplePat(ys)) => List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys) - | (Ap(x1, y1), Ap(x2, y2)) => fast_equal(x1, x2) && fast_equal(y1, y2) - | (Cast(x1, t1, t2), Cast(x2, u1, u2)) => + | (ApPat(x1, y1), ApPat(x2, y2)) => + fast_equal(x1, x2) && fast_equal(y1, y2) + | (CastPat(x1, t1, t2), CastPat(x2, u1, u2)) => fast_equal(x1, x2) && Typ.fast_equal(t1, u1) && Typ.fast_equal(t2, u2) - | (EmptyHole, _) - | (MultiHole(_), _) - | (Invalid(_), _) + | (EmptyHolePat, _) + | (MultiHolePat(_), _) + | (InvalidPat(_), _) | (Wild, _) - | (Bool(_), _) - | (Int(_), _) - | (Float(_), _) - | (String(_), _) - | (ListLit(_), _) - | (Constructor(_), _) - | (Cons(_), _) - | (Var(_), _) - | (Tuple(_), _) - | (Ap(_), _) - | (Cast(_), _) => false + | (BoolPat(_), _) + | (IntPat(_), _) + | (FloatPat(_), _) + | (StringPat(_), _) + | (ListLitPat(_), _) + | (ConstructorPat(_), _) + | (ConsPat(_), _) + | (VarPat(_), _) + | (TuplePat(_), _) + | (ApPat(_), _) + | (CastPat(_), _) => false }; } and Typ: { @@ -625,21 +627,23 @@ and Typ: { ...exp, term: switch (term) { - | Unknown(Hole(EmptyHole)) - | Unknown(Hole(Invalid(_))) + | Unknown(HoleProvenance(EmptyTypeHole)) + | Unknown(HoleProvenance(InvalidTypeHole(_))) | Unknown(SynSwitch) | Unknown(Internal) | Bool | Int | Float | String - | Var(_) => term + | TypVar(_) => term | List(t) => List(typ_map_term(t)) - | Unknown(Hole(MultiHole(things))) => - Unknown(Hole(MultiHole(List.map(any_map_term, things)))) - | Ap(e1, e2) => Ap(typ_map_term(e1), typ_map_term(e2)) + | Unknown(HoleProvenance(MultiTypeHole(things))) => + Unknown( + HoleProvenance(MultiTypeHole(List.map(any_map_term, things))), + ) + | ApTyp(e1, e2) => ApTyp(typ_map_term(e1), typ_map_term(e2)) | Prod(xs) => Prod(List.map(typ_map_term, xs)) - | Parens(e) => Parens(typ_map_term(e)) + | TypParens(e) => TypParens(typ_map_term(e)) | Arrow(t1, t2) => Arrow(typ_map_term(t1), typ_map_term(t2)) | Sum(variants) => Sum( @@ -682,9 +686,9 @@ and Typ: { Rec(tp2, ty) |> rewrap | Rec(tp2, ty) => Rec(tp2, subst(s, x, ty)) |> rewrap | List(ty) => List(subst(s, x, ty)) |> rewrap - | Var(y) => str == y ? s : Var(y) |> rewrap - | Parens(ty) => Parens(subst(s, x, ty)) |> rewrap - | Ap(t1, t2) => Ap(subst(s, x, t1), subst(s, x, t2)) |> rewrap + | TypVar(y) => str == y ? s : TypVar(y) |> rewrap + | TypParens(ty) => TypParens(subst(s, x, ty)) |> rewrap + | ApTyp(t1, t2) => ApTyp(subst(s, x, t1), subst(s, x, t2)) |> rewrap }; | None => ty }; @@ -695,13 +699,13 @@ and Typ: { let rec eq_internal = (n: int, t1: t, t2: t) => { switch (IdTagged.term_of(t1), IdTagged.term_of(t2)) { - | (Parens(t1), _) => eq_internal(n, t1, t2) - | (_, Parens(t2)) => eq_internal(n, t1, t2) + | (TypParens(t1), _) => eq_internal(n, t1, t2) + | (_, TypParens(t2)) => eq_internal(n, t1, t2) | (Rec(x1, t1), Rec(x2, t2)) | (Forall(x1, t1), Forall(x2, t2)) => let alpha_subst = subst({ - term: Var("=" ++ string_of_int(n)), + term: TypVar("=" ++ string_of_int(n)), copied: false, ids: [Id.invalid], }); @@ -716,9 +720,9 @@ and Typ: { | (Bool, _) => false | (String, String) => true | (String, _) => false - | (Ap(t1, t2), Ap(t1', t2')) => + | (ApTyp(t1, t2), ApTyp(t1', t2')) => eq_internal(n, t1, t1') && eq_internal(n, t2, t2') - | (Ap(_), _) => false + | (ApTyp(_), _) => false | (Unknown(_), Unknown(_)) => true | (Unknown(_), _) => false | (Arrow(t1, t2), Arrow(t1', t2')) => @@ -732,8 +736,8 @@ and Typ: { /* Does not normalize the types. */ ConstructorMap.equal(eq_internal(n), sm1, sm2) | (Sum(_), _) => false - | (Var(n1), Var(n2)) => n1 == n2 - | (Var(_), _) => false + | (TypVar(n1), TypVar(n2)) => n1 == n2 + | (TypVar(_), _) => false }; }; @@ -782,10 +786,11 @@ and TPat: { ...exp, term: switch (term) { - | EmptyHole - | Invalid(_) - | Var(_) => term - | MultiHole(things) => MultiHole(List.map(any_map_term, things)) + | EmptyHoleTPat + | InvalidTPat(_) + | VarTPat(_) => term + | MultiHoleTPat(things) => + MultiHoleTPat(List.map(any_map_term, things)) }, }; x |> f_tpat(rec_call); @@ -793,22 +798,22 @@ and TPat: { let tyvar_of_utpat = ({term, _}: t) => switch (term) { - | Var(x) => Some(x) + | VarTPat(x) => Some(x) | _ => None }; let fast_equal = (tp1: t, tp2: t) => switch (tp1 |> IdTagged.term_of, tp2 |> IdTagged.term_of) { - | (EmptyHole, EmptyHole) => true - | (Invalid(s1), Invalid(s2)) => s1 == s2 - | (MultiHole(xs), MultiHole(ys)) => + | (EmptyHoleTPat, EmptyHoleTPat) => true + | (InvalidTPat(s1), InvalidTPat(s2)) => s1 == s2 + | (MultiHoleTPat(xs), MultiHoleTPat(ys)) => List.length(xs) == List.length(ys) && List.equal(Any.fast_equal, xs, ys) - | (Var(x), Var(y)) => x == y - | (EmptyHole, _) - | (Invalid(_), _) - | (MultiHole(_), _) - | (Var(_), _) => false + | (VarTPat(x), VarTPat(y)) => x == y + | (EmptyHoleTPat, _) + | (InvalidTPat(_), _) + | (MultiHoleTPat(_), _) + | (VarTPat(_), _) => false }; } and Rul: { @@ -856,7 +861,7 @@ and Rul: { ...exp, term: switch (term) { - | Invalid(_) => term + | InvalidRule(_) => term | Hole(things) => Hole(List.map(any_map_term, things)) | Rules(e, rls) => Rules( @@ -873,7 +878,7 @@ and Rul: { let fast_equal = (r1: t, r2: t) => switch (r1 |> IdTagged.term_of, r2 |> IdTagged.term_of) { - | (Invalid(s1), Invalid(s2)) => s1 == s2 + | (InvalidRule(s1), InvalidRule(s2)) => s1 == s2 | (Hole(xs), Hole(ys)) => List.length(xs) == List.length(ys) && List.equal(Any.fast_equal, xs, ys) @@ -886,7 +891,7 @@ and Rul: { rls1, rls2, ) - | (Invalid(_), _) + | (InvalidRule(_), _) | (Hole(_), _) | (Rules(_), _) => false }; @@ -1041,7 +1046,7 @@ and StepperFilterKind: { let map = (mapper, filter: t): t => { switch (filter) { - | Filter({act, pat}) => Filter({act, pat: mapper(pat)}) + | FilterStepper({act, pat}) => FilterStepper({act, pat: mapper(pat)}) | Residue(idx, act) => Residue(idx, act) }; }; @@ -1059,7 +1064,8 @@ and StepperFilterKind: { Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any); ( fun - | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act}) + | FilterStepper({pat: e, act}) => + FilterStepper({pat: exp_map_term(e), act}) | Residue(i, a) => Residue(i, a): t => t ); @@ -1067,10 +1073,10 @@ and StepperFilterKind: { let fast_equal = (f1: t, f2: t) => switch (f1, f2) { - | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) => + | (FilterStepper({pat: e1, act: a1}), FilterStepper({pat: e2, act: a2})) => Exp.fast_equal(e1, e2) && a1 == a2 | (Residue(i1, a1), Residue(i2, a2)) => i1 == i2 && a1 == a2 - | (Filter(_), _) + | (FilterStepper(_), _) | (Residue(_), _) => false }; }; diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index 23265f8a2a..6617e036ed 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -7,10 +7,10 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => { | FailedCast(_) | Undefined | Deferral(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | ListLit(_) | Constructor(_) | Closure(_) diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index 01050d5e7b..04d742d3a3 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -571,7 +571,7 @@ module F = (ExerciseEnv: ExerciseEnv) => { let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => { term: Filter( - Filter({ + FilterStepper({ act: FilterAction.(act, One), pat: { term: Constructor("$e", Unknown(Internal) |> Typ.temp), diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re index 23dff72251..a1722fbb6d 100644 --- a/src/haz3lschool/SyntaxTest.re +++ b/src/haz3lschool/SyntaxTest.re @@ -16,23 +16,24 @@ type syntax_result = { let rec find_var_upat = (name: string, upat: Pat.t): bool => { switch (upat.term) { - | Var(x) => x == name - | EmptyHole + | VarPat(x) => x == name + | EmptyHolePat | Wild - | Invalid(_) - | MultiHole(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | Constructor(_) => false - | Cons(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2) - | ListLit(l) - | Tuple(l) => + | InvalidPat(_) + | MultiHolePat(_) + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ConstructorPat(_) => false + | ConsPat(up1, up2) => + find_var_upat(name, up1) || find_var_upat(name, up2) + | ListLitPat(l) + | TuplePat(l) => List.fold_left((acc, up) => {acc || find_var_upat(name, up)}, false, l) - | Parens(up) => find_var_upat(name, up) - | Ap(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2) - | Cast(up, _, _) => find_var_upat(name, up) + | ParensPat(up) => find_var_upat(name, up) + | ApPat(up1, up2) => find_var_upat(name, up1) || find_var_upat(name, up2) + | CastPat(up, _, _) => find_var_upat(name, up) }; }; @@ -47,12 +48,12 @@ let rec find_in_let = (name: string, upat: UPat.t, def: UExp.t, l: list(UExp.t)) : list(UExp.t) => { switch (upat.term, def.term) { - | (Parens(up), Parens(ue)) => find_in_let(name, up, ue, l) - | (Parens(up), _) => find_in_let(name, up, def, l) + | (ParensPat(up), Parens(ue)) => find_in_let(name, up, ue, l) + | (ParensPat(up), _) => find_in_let(name, up, def, l) | (_, Parens(ue)) => find_in_let(name, upat, ue, l) - | (Cast(up, _, _), _) => find_in_let(name, up, def, l) - | (Var(x), Fun(_)) => x == name ? [def, ...l] : l - | (Tuple(pl), Tuple(ul)) => + | (CastPat(up, _, _), _) => find_in_let(name, up, def, l) + | (VarPat(x), Fun(_)) => x == name ? [def, ...l] : l + | (TuplePat(pl), Tuple(ul)) => if (List.length(pl) != List.length(ul)) { l; } else { @@ -63,15 +64,17 @@ let rec find_in_let = ul, ); } - | (Var(_), _) - | (Tuple(_), _) + | (VarPat(_), _) + | (TuplePat(_), _) | ( - EmptyHole | Wild | Invalid(_) | MultiHole(_) | Int(_) | Float(_) | Bool(_) | - String(_) | - ListLit(_) | - Constructor(_) | - Cons(_, _) | - Ap(_, _), + EmptyHolePat | Wild | InvalidPat(_) | MultiHolePat(_) | IntPat(_) | + FloatPat(_) | + BoolPat(_) | + StringPat(_) | + ListLitPat(_) | + ConstructorPat(_) | + ConsPat(_, _) | + ApPat(_, _), _, ) => l }; @@ -122,10 +125,10 @@ let rec find_fn = | MultiHole(_) | DynamicErrorHole(_) | FailedCast(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | Undefined | BuiltinFun(_) @@ -138,29 +141,29 @@ let rec find_fn = */ let rec var_mention_upat = (name: string, upat: Pat.t): bool => { switch (upat.term) { - | Var(x) => x == name - | EmptyHole + | VarPat(x) => x == name + | EmptyHolePat | Wild - | Invalid(_) - | MultiHole(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | Constructor(_) => false - | Cons(up1, up2) => + | InvalidPat(_) + | MultiHolePat(_) + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ConstructorPat(_) => false + | ConsPat(up1, up2) => var_mention_upat(name, up1) || var_mention_upat(name, up2) - | ListLit(l) - | Tuple(l) => + | ListLitPat(l) + | TuplePat(l) => List.fold_left( (acc, up) => {acc || var_mention_upat(name, up)}, false, l, ) - | Parens(up) => var_mention_upat(name, up) - | Ap(up1, up2) => + | ParensPat(up) => var_mention_upat(name, up) + | ApPat(up1, up2) => var_mention_upat(name, up1) || var_mention_upat(name, up2) - | Cast(up, _, _) => var_mention_upat(name, up) + | CastPat(up, _, _) => var_mention_upat(name, up) }; }; @@ -173,10 +176,10 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => { | EmptyHole | Invalid(_) | MultiHole(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | Undefined | Deferral(_) => false @@ -234,10 +237,10 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => { | EmptyHole | Invalid(_) | MultiHole(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | Undefined | Deferral(_) => false @@ -325,10 +328,10 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => { | MultiHole(_) | DynamicErrorHole(_) | FailedCast(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | Constructor(_) | Undefined | Var(_) diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index ba06d2a29e..55ded0cdfc 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -409,7 +409,7 @@ let locked = statics.info_map, statics.term, ) - : Bool(true) |> DHExp.fresh; + : BoolLit(true) |> DHExp.fresh; let elab: Elaborator.Elaboration.t = {d: elab}; let result: ModelResult.t = settings.core.dynamics diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 879b355999..1b38b6fdf3 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -142,12 +142,12 @@ let typ_ok_view = (cls: Cls.t, ok: Info.ok_typ) => | Type(_) when cls == Typ(EmptyHole) => [text("Fillable by any type")] | Type(ty) => [Type.view(ty), text("is a type")] | TypeAlias(name, ty_lookup) => [ - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), text("is an alias for"), Type.view(ty_lookup), ] | Variant(name, sum_ty) => [ - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), text("is a sum type constuctor of type"), Type.view(sum_ty), ] @@ -160,7 +160,7 @@ let typ_ok_view = (cls: Cls.t, ok: Info.ok_typ) => let typ_err_view = (ok: Info.error_typ) => switch (ok) { | FreeTypeVariable(name) => [ - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), text("not found"), ] | BadToken(token) => [ @@ -171,7 +171,7 @@ let typ_err_view = (ok: Info.error_typ) => | WantConstructorFoundType(_) => [text("Expected a constructor")] | WantTypeFoundAp => [text("Must be part of a sum type")] | DuplicateConstructor(name) => [ - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), text("already used in this sum"), ] }; @@ -242,17 +242,17 @@ let tpat_view = (_: Cls.t, status: Info.status_tpat) => | InHole(ShadowsType(name, BaseTyp)) => div_err([ text("Can't shadow base type"), - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), ]) | InHole(ShadowsType(name, TyAlias)) => div_err([ text("Can't shadow existing alias"), - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), ]) | InHole(ShadowsType(name, TyVar)) => div_err([ text("Can't shadow existing type variable"), - Type.view(Var(name) |> Typ.fresh), + Type.view(TypVar(name) |> Typ.fresh), ]) }; diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index a74a5187d8..7bea3e5041 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -394,15 +394,15 @@ let example_view = let rec bypass_parens_and_annot_pat = (pat: Pat.t) => { switch (pat.term) { - | Parens(p) - | Cast(p, _, _) => bypass_parens_and_annot_pat(p) + | ParensPat(p) + | CastPat(p, _, _) => bypass_parens_and_annot_pat(p) | _ => pat }; }; let rec bypass_parens_pat = (pat: Pat.t) => { switch (pat.term) { - | Parens(p) => bypass_parens_pat(p) + | ParensPat(p) => bypass_parens_pat(p) | _ => pat }; }; @@ -416,7 +416,7 @@ let rec bypass_parens_exp = (exp: Exp.t) => { let rec bypass_parens_typ = (typ: Typ.t) => { switch (typ.term) { - | Parens(t) => bypass_parens_typ(t) + | TypParens(t) => bypass_parens_typ(t) | _ => typ }; }; @@ -560,10 +560,10 @@ let get_doc = ); | Undefined => get_message(UndefinedExp.undefined_exps) | Deferral(_) => get_message(TerminalExp.deferral_exps) - | Bool(b) => get_message(TerminalExp.bool_exps(b)) - | Int(i) => get_message(TerminalExp.int_exps(i)) - | Float(f) => get_message(TerminalExp.float_exps(f)) - | String(s) => get_message(TerminalExp.string_exps(s)) + | BoolLit(b) => get_message(TerminalExp.bool_exps(b)) + | IntLit(i) => get_message(TerminalExp.int_exps(i)) + | FloatLit(f) => get_message(TerminalExp.float_exps(f)) + | StringLit(s) => get_message(TerminalExp.string_exps(s)) | ListLit(terms) => get_message( ~format= @@ -623,7 +623,7 @@ let get_doc = let pat_id = List.nth(pat.ids, 0); let body_id = List.nth(body.ids, 0); switch (pat.term) { - | EmptyHole => + | EmptyHolePat => if (FunctionExp.function_empty_hole_exp.id == get_specificity_level(FunctionExp.functions_empty_hole)) { get_message( @@ -647,7 +647,7 @@ let get_doc = } else { basic(FunctionExp.functions_empty_hole); } - | MultiHole(_) => + | MultiHolePat(_) => if (FunctionExp.function_multi_hole_exp.id == get_specificity_level(FunctionExp.functions_multi_hole)) { get_message( @@ -689,7 +689,7 @@ let get_doc = } else { basic(FunctionExp.functions_wild); } - | Int(i) => + | IntPat(i) => if (FunctionExp.function_intlit_exp.id == get_specificity_level(FunctionExp.functions_int)) { get_message( @@ -714,7 +714,7 @@ let get_doc = } else { basic(FunctionExp.functions_int); } - | Float(f) => + | FloatPat(f) => if (FunctionExp.function_floatlit_exp.id == get_specificity_level(FunctionExp.functions_float)) { get_message( @@ -739,7 +739,7 @@ let get_doc = } else { basic(FunctionExp.functions_float); } - | Bool(b) => + | BoolPat(b) => if (FunctionExp.function_boollit_exp.id == get_specificity_level(FunctionExp.functions_bool)) { get_message( @@ -764,7 +764,7 @@ let get_doc = } else { basic(FunctionExp.functions_bool); } - | String(s) => + | StringPat(s) => if (FunctionExp.function_strlit_exp.id == get_specificity_level(FunctionExp.functions_str)) { get_message( @@ -789,7 +789,7 @@ let get_doc = } else { basic(FunctionExp.functions_str); } - | Tuple([]) => + | TuplePat([]) => if (FunctionExp.function_triv_exp.id == get_specificity_level(FunctionExp.functions_triv)) { get_message( @@ -812,7 +812,7 @@ let get_doc = } else { basic(FunctionExp.functions_triv); } - | ListLit(elements) => + | ListLitPat(elements) => if (List.length(elements) == 0) { if (FunctionExp.function_listnil_exp.id == get_specificity_level(FunctionExp.functions_listnil)) { @@ -861,7 +861,7 @@ let get_doc = } else { basic(FunctionExp.functions_listlit); } - | Cons(hd, tl) => + | ConsPat(hd, tl) => if (FunctionExp.function_cons_exp.id == get_specificity_level(FunctionExp.functions_cons)) { let hd_id = List.nth(hd.ids, 0); @@ -888,7 +888,7 @@ let get_doc = } else { basic(FunctionExp.functions_cons); } - | Var(var) => + | VarPat(var) => if (FunctionExp.function_var_exp.id == get_specificity_level(FunctionExp.functions_var)) { get_message( @@ -909,7 +909,7 @@ let get_doc = } else { basic(FunctionExp.functions_var); } - | Tuple(elements) => + | TuplePat(elements) => let pat_id = List.nth(pat.ids, 0); let body_id = List.nth(body.ids, 0); let basic_tuple = group_id => { @@ -1004,7 +1004,7 @@ let get_doc = basic(FunctionExp.functions_tuple); } }; - | Ap(con, arg) => + | ApPat(con, arg) => if (FunctionExp.function_ap_exp.id == get_specificity_level(FunctionExp.functions_ap)) { let con_id = List.nth(con.ids, 0); @@ -1031,7 +1031,7 @@ let get_doc = } else { basic(FunctionExp.functions_ap); } - | Constructor(v, _) => + | ConstructorPat(v, _) => if (FunctionExp.function_ctr_exp.id == get_specificity_level(FunctionExp.functions_ctr)) { let pat_id = List.nth(pat.ids, 0); @@ -1055,9 +1055,9 @@ let get_doc = } else { basic(FunctionExp.functions_ctr); } - | Invalid(_) => default // Shouldn't get hit - | Parens(_) => default // Shouldn't get hit? - | Cast(_) => default // Shouldn't get hit? + | InvalidPat(_) => default // Shouldn't get hit + | ParensPat(_) => default // Shouldn't get hit? + | CastPat(_) => default // Shouldn't get hit? }; | Tuple(terms) => let basic = group_id => @@ -1147,7 +1147,7 @@ let get_doc = ); }; switch (pat.term) { - | EmptyHole => + | EmptyHolePat => if (LetExp.let_empty_hole_exp.id == get_specificity_level(LetExp.lets_emptyhole)) { get_message( @@ -1168,7 +1168,7 @@ let get_doc = } else { basic(LetExp.lets_emptyhole); } - | MultiHole(_) => + | MultiHolePat(_) => if (LetExp.let_multi_hole_exp.id == get_specificity_level(LetExp.lets_mutlihole)) { get_message( @@ -1209,7 +1209,7 @@ let get_doc = } else { basic(LetExp.lets_wild); } - | Int(i) => + | IntPat(i) => if (LetExp.let_int_exp.id == get_specificity_level(LetExp.lets_int)) { get_message( ~colorings= @@ -1234,7 +1234,7 @@ let get_doc = LetExp.lets_int, ); } - | Float(f) => + | FloatPat(f) => if (LetExp.let_float_exp.id == get_specificity_level(LetExp.lets_float)) { // TODO Make sure everywhere printing the float literal print it prettier @@ -1261,7 +1261,7 @@ let get_doc = LetExp.lets_float, ); } - | Bool(b) => + | BoolPat(b) => if (LetExp.let_bool_exp.id == get_specificity_level(LetExp.lets_bool)) { get_message( @@ -1287,7 +1287,7 @@ let get_doc = LetExp.lets_bool, ); } - | String(s) => + | StringPat(s) => if (LetExp.let_str_exp.id == get_specificity_level(LetExp.lets_str)) { get_message( ~colorings= @@ -1312,7 +1312,7 @@ let get_doc = LetExp.lets_str, ); } - | Tuple([]) => + | TuplePat([]) => if (LetExp.let_triv_exp.id == get_specificity_level(LetExp.lets_triv)) { get_message( @@ -1337,7 +1337,7 @@ let get_doc = LetExp.lets_triv, ); } - | ListLit(elements) => + | ListLitPat(elements) => if (List.length(elements) == 0) { if (LetExp.let_listnil_exp.id == get_specificity_level(LetExp.lets_listnil)) { @@ -1384,7 +1384,7 @@ let get_doc = } else { basic(LetExp.lets_listlit); } - | Cons(hd, tl) => + | ConsPat(hd, tl) => if (LetExp.let_cons_exp.id == get_specificity_level(LetExp.lets_cons)) { let hd_id = List.nth(hd.ids, 0); @@ -1407,7 +1407,7 @@ let get_doc = } else { basic(LetExp.lets_cons); } - | Var(var) => + | VarPat(var) => if (LetExp.let_var_exp.id == get_specificity_level(LetExp.lets_var)) { get_message( ~colorings= @@ -1428,7 +1428,7 @@ let get_doc = } else { basic(LetExp.lets_var); } - | Tuple(elements) => + | TuplePat(elements) => let basic_tuple = group_id => { get_message( ~colorings=LetExp.let_tuple_exp_coloring_ids(~pat_id, ~def_id), @@ -1517,7 +1517,7 @@ let get_doc = basic(LetExp.lets_tuple); } }; - | Ap(con, arg) => + | ApPat(con, arg) => if (LetExp.let_ap_exp.id == get_specificity_level(LetExp.lets_ap)) { let con_id = List.nth(con.ids, 0); let arg_id = List.nth(arg.ids, 0); @@ -1539,7 +1539,7 @@ let get_doc = } else { basic(LetExp.lets_ap); } - | Constructor(v, _) => + | ConstructorPat(v, _) => if (LetExp.let_ctr_exp.id == get_specificity_level(LetExp.lets_ctr)) { get_message( ~colorings= @@ -1561,9 +1561,9 @@ let get_doc = } else { basic(LetExp.lets_ctr); } - | Invalid(_) => default // Shouldn't get hit - | Parens(_) => default // Shouldn't get hit? - | Cast(_) => default // Shouldn't get hit? + | InvalidPat(_) => default // Shouldn't get hit + | ParensPat(_) => default // Shouldn't get hit? + | CastPat(_) => default // Shouldn't get hit? }; | FixF(pat, body, _) => message_single( @@ -1710,28 +1710,28 @@ let get_doc = ), SeqExp.seqs, ); - | Filter(Filter({act: (Step, One), pat}), body) => + | Filter(FilterStepper({act: (Step, One), pat}), body) => message_single( FilterExp.filter_pause( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Step, All), pat}), body) => + | Filter(FilterStepper({act: (Step, All), pat}), body) => message_single( FilterExp.filter_debug( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Eval, All), pat}), body) => + | Filter(FilterStepper({act: (Eval, All), pat}), body) => message_single( FilterExp.filter_eval( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Eval, One), pat}), body) => + | Filter(FilterStepper({act: (Eval, One), pat}), body) => message_single( FilterExp.filter_hide( ~p_id=UExp.rep_id(pat), @@ -1906,10 +1906,10 @@ let get_doc = get_message_exp(term.term); | Some(InfoPat({term, _})) => switch (bypass_parens_pat(term).term) { - | EmptyHole => get_message(HolePat.empty_hole) - | MultiHole(_) => get_message(HolePat.multi_hole) + | EmptyHolePat => get_message(HolePat.empty_hole) + | MultiHolePat(_) => get_message(HolePat.multi_hole) | Wild => get_message(TerminalPat.wild) - | Int(i) => + | IntPat(i) => get_message( ~format= Some( @@ -1918,7 +1918,7 @@ let get_doc = ), TerminalPat.intlit(i), ) - | Float(f) => + | FloatPat(f) => get_message( ~format= Some( @@ -1927,7 +1927,7 @@ let get_doc = ), TerminalPat.floatlit(f), ) - | Bool(b) => + | BoolPat(b) => get_message( ~format= Some( @@ -1936,7 +1936,7 @@ let get_doc = ), TerminalPat.boollit(b), ) - | String(s) => + | StringPat(s) => get_message( ~format= Some( @@ -1945,8 +1945,8 @@ let get_doc = ), TerminalPat.strlit(s), ) - | Tuple([]) => get_message(TerminalPat.triv) - | ListLit(elements) => + | TuplePat([]) => get_message(TerminalPat.triv) + | ListLitPat(elements) => if (List.length(elements) == 0) { get_message(ListPat.listnil); } else { @@ -1962,7 +1962,7 @@ let get_doc = ListPat.listlit, ); } - | Cons(hd, tl) => + | ConsPat(hd, tl) => let hd_id = List.nth(hd.ids, 0); let tl_id = List.nth(tl.ids, 0); let basic = doc => @@ -1980,7 +1980,7 @@ let get_doc = doc, ); switch (tl.term) { - | Cons(hd2, tl2) => + | ConsPat(hd2, tl2) => if (ListPat.cons2_pat.id == get_specificity_level(ListPat.cons2)) { let hd2_id = List.nth(hd2.ids, 0); let tl2_id = List.nth(tl2.ids, 0); @@ -2008,7 +2008,7 @@ let get_doc = } | _ => basic(ListPat.cons) }; - | Var(v) => + | VarPat(v) => get_message( ~format= Some( @@ -2016,7 +2016,7 @@ let get_doc = ), TerminalPat.var(v), ) - | Tuple(elements) => + | TuplePat(elements) => let basic = group => get_message( ~format= @@ -2082,7 +2082,7 @@ let get_doc = } | _ => basic(TuplePat.tuple) }; - | Ap(con, arg) => + | ApPat(con, arg) => let con_id = List.nth(con.ids, 0); let arg_id = List.nth(arg.ids, 0); get_message( @@ -2098,7 +2098,7 @@ let get_doc = ), AppPat.ap, ); - | Constructor(con, _) => + | ConstructorPat(con, _) => get_message( ~format= Some( @@ -2106,7 +2106,7 @@ let get_doc = ), TerminalPat.ctr(con), ) - | Cast(pat, typ, _) => + | CastPat(pat, typ, _) => let pat_id = List.nth(pat.ids, 0); let typ_id = List.nth(typ.ids, 0); get_message( @@ -2122,8 +2122,8 @@ let get_doc = ), TypAnnPat.typann, ); - | Invalid(_) => simple("Not a valid pattern") - | Parens(_) => + | InvalidPat(_) => simple("Not a valid pattern") + | ParensPat(_) => // Shouldn't be hit? default } @@ -2131,8 +2131,10 @@ let get_doc = switch (bypass_parens_typ(term).term) { | Unknown(SynSwitch) | Unknown(Internal) - | Unknown(Hole(EmptyHole)) => get_message(HoleTyp.empty_hole) - | Unknown(Hole(MultiHole(_))) => get_message(HoleTyp.multi_hole) + | Unknown(HoleProvenance(EmptyTypeHole)) => + get_message(HoleTyp.empty_hole) + | Unknown(HoleProvenance(MultiTypeHole(_))) => + get_message(HoleTyp.multi_hole) | Int => get_message(TerminalTyp.int) | Float => get_message(TerminalTyp.float) | Bool => get_message(TerminalTyp.bool) @@ -2302,9 +2304,9 @@ let get_doc = } | _ => basic(TupleTyp.tuple) }; - | Var(c) when Info.typ_is_constructor_expected(typ_info) => + | TypVar(c) when Info.typ_is_constructor_expected(typ_info) => get_message(SumTyp.sum_typ_nullary_constructor_defs(c)) - | Var(v) => + | TypVar(v) => get_message( ~format= Some( @@ -2313,18 +2315,19 @@ let get_doc = TerminalTyp.var(v), ) | Sum(_) => get_message(SumTyp.labelled_sum_typs) - | Ap({term: Var(c), _}, _) => + | ApTyp({term: TypVar(c), _}, _) => get_message(SumTyp.sum_typ_unary_constructor_defs(c)) - | Unknown(Hole(Invalid(_))) => simple("Not a type or type operator") - | Ap(_) - | Parens(_) => default // Shouldn't be hit? + | Unknown(HoleProvenance(InvalidTypeHole(_))) => + simple("Not a type or type operator") + | ApTyp(_) + | TypParens(_) => default // Shouldn't be hit? } | Some(InfoTPat(info)) => switch (info.term.term) { - | Invalid(_) => simple("Type names must begin with a capital letter") - | EmptyHole => get_message(HoleTPat.empty_hole_tpats) - | MultiHole(_) => get_message(HoleTPat.multi_hole_tpats) - | Var(v) => + | InvalidTPat(_) => simple("Type names must begin with a capital letter") + | EmptyHoleTPat => get_message(HoleTPat.empty_hole_tpats) + | MultiHoleTPat(_) => get_message(HoleTPat.multi_hole_tpats) + | VarTPat(v) => get_message( ~format= Some( diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 82dfd0a9e3..325ff58928 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -5,7 +5,7 @@ open Haz3lcore; let tpat_view = (tpat: Haz3lcore.TPat.t): string => switch (tpat.term) { - | Var(x) => x + | VarTPat(x) => x | _ => "?" }; @@ -25,12 +25,12 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => ], [text("?") /*, prov_view(prov)*/], ) - | Parens(ty) => view_ty(ty) + | TypParens(ty) => view_ty(ty) | Int => ty_view("Int", "Int") | Float => ty_view("Float", "Float") | String => ty_view("String", "String") | Bool => ty_view("Bool", "Bool") - | Var(name) => ty_view("Var", name) + | TypVar(name) => ty_view("Var", name) | Rec(name, t) => div( ~attrs=[clss(["typ-view", "Rec"])], @@ -94,7 +94,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => ctr_view(t0) @ ts_views; }, ) - | Ap(_) => + | ApTyp(_) => div( ~attrs=[ clss(["typ-view", "atom", "unknown"]), diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index ffb0eed0c5..d73aafba10 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -47,12 +47,12 @@ let rec precedence = (~show_function_bodies, ~show_casts: bool, d: DHExp.t) => { switch (DHExp.term_of(d)) { | Var(_) | Invalid(_) - | Bool(_) - | Int(_) | Seq(_) | Test(_) - | Float(_) - | String(_) + | BoolLit(_) + | IntLit(_) + | FloatLit(_) + | StringLit(_) | ListLit(_) | EmptyHole | Constructor(_) @@ -255,7 +255,7 @@ let mk = | Filter(flt, d') => if (settings.show_stepper_filters) { switch (flt) { - | Filter({pat, act}) => + | FilterStepper({pat, act}) => let keyword = FilterAction.string_of_t(act); let flt_doc = go_formattable(pat); vseps([ @@ -277,7 +277,7 @@ let mk = } else { switch (flt) { | Residue(_) => go'(d') - | Filter(_) => go'(d') + | FilterStepper(_) => go'(d') }; } @@ -315,10 +315,10 @@ let mk = } | BuiltinFun(f) => text(f) | Constructor(name, _) => DHDoc_common.mk_ConstructorLit(name) - | Bool(b) => DHDoc_common.mk_BoolLit(b) - | Int(n) => DHDoc_common.mk_IntLit(n) - | Float(f) => DHDoc_common.mk_FloatLit(f) - | String(s) => DHDoc_common.mk_StringLit(s) + | BoolLit(b) => DHDoc_common.mk_BoolLit(b) + | IntLit(n) => DHDoc_common.mk_IntLit(n) + | FloatLit(f) => DHDoc_common.mk_FloatLit(f) + | StringLit(s) => DHDoc_common.mk_StringLit(s) | Undefined => DHDoc_common.mk_Undefined() | Test(d) => DHDoc_common.mk_Test(go'(d)) | Deferral(_) => text("_") diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re index 8996bd4b03..77f53e41a0 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Pat.re @@ -3,22 +3,22 @@ open Haz3lcore; let precedence = (dp: Pat.t) => switch (DHPat.term_of(dp)) { - | EmptyHole - | MultiHole(_) + | EmptyHolePat + | MultiHolePat(_) | Wild - | Invalid(_) - | Var(_) - | Int(_) - | Float(_) - | Bool(_) - | String(_) - | ListLit(_) - | Constructor(_) => DHDoc_common.precedence_const - | Tuple(_) => DHDoc_common.precedence_Comma - | Cons(_) => DHDoc_common.precedence_Cons - | Ap(_) => DHDoc_common.precedence_Ap - | Parens(_) => DHDoc_common.precedence_const - | Cast(_) => DHDoc_common.precedence_Ap + | InvalidPat(_) + | VarPat(_) + | IntPat(_) + | FloatPat(_) + | BoolPat(_) + | StringPat(_) + | ListLitPat(_) + | ConstructorPat(_) => DHDoc_common.precedence_const + | TuplePat(_) => DHDoc_common.precedence_Comma + | ConsPat(_) => DHDoc_common.precedence_Cons + | ApPat(_) => DHDoc_common.precedence_Ap + | ParensPat(_) => DHDoc_common.precedence_const + | CastPat(_) => DHDoc_common.precedence_Ap }; let rec mk = @@ -41,27 +41,27 @@ let rec mk = ); let doc = switch (DHPat.term_of(dp)) { - | MultiHole(_) - | EmptyHole => DHDoc_common.mk_EmptyHole(ClosureEnvironment.empty) - | Invalid(t) => DHDoc_common.mk_InvalidText(t) - | Var(x) => Doc.text(x) + | MultiHolePat(_) + | EmptyHolePat => DHDoc_common.mk_EmptyHole(ClosureEnvironment.empty) + | InvalidPat(t) => DHDoc_common.mk_InvalidText(t) + | VarPat(x) => Doc.text(x) | Wild => DHDoc_common.Delim.wild - | Constructor(name, _) => DHDoc_common.mk_ConstructorLit(name) - | Int(n) => DHDoc_common.mk_IntLit(n) - | Float(f) => DHDoc_common.mk_FloatLit(f) - | Bool(b) => DHDoc_common.mk_BoolLit(b) - | String(s) => DHDoc_common.mk_StringLit(s) - | ListLit(d_list) => + | ConstructorPat(name, _) => DHDoc_common.mk_ConstructorLit(name) + | IntPat(n) => DHDoc_common.mk_IntLit(n) + | FloatPat(f) => DHDoc_common.mk_FloatLit(f) + | BoolPat(b) => DHDoc_common.mk_BoolLit(b) + | StringPat(s) => DHDoc_common.mk_StringLit(s) + | ListLitPat(d_list) => let ol = List.map(mk', d_list); DHDoc_common.mk_ListLit(ol); - | Cons(dp1, dp2) => + | ConsPat(dp1, dp2) => let (doc1, doc2) = mk_right_associative_operands(DHDoc_common.precedence_Cons, dp1, dp2); DHDoc_common.mk_Cons(doc1, doc2); - | Tuple([]) => DHDoc_common.Delim.triv - | Tuple(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds)) + | TuplePat([]) => DHDoc_common.Delim.triv + | TuplePat(ds) => DHDoc_common.mk_Tuple(List.map(mk', ds)) // TODO: Print type annotations - | Cast(dp, t1, t2) when show_casts => + | CastPat(dp, t1, t2) when show_casts => Doc.hcats([ mk'(dp), Doc.annot( @@ -75,10 +75,10 @@ let rec mk = ]), ), ]) - | Cast(dp, _, _) => mk'(~parenthesize, dp) - | Parens(dp) => + | CastPat(dp, _, _) => mk'(~parenthesize, dp) + | ParensPat(dp) => mk(~enforce_inline, ~parenthesize=true, ~infomap, ~show_casts, dp) - | Ap(dp1, dp2) => + | ApPat(dp1, dp2) => let (doc1, doc2) = mk_left_associative_operands(DHDoc_common.precedence_Ap, dp1, dp2); DHDoc_common.mk_Ap(doc1, doc2); diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 996d01f607..b1ad3f746d 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -19,15 +19,15 @@ let precedence = (ty: Typ.t): int => | Bool | String | Unknown(_) - | Var(_) + | TypVar(_) | Forall(_) | Rec(_) | Sum(_) => precedence_Sum | List(_) => precedence_Const | Prod(_) => precedence_Prod | Arrow(_, _) => precedence_Arrow - | Parens(_) => precedence_Const - | Ap(_) => precedence_Ap + | TypParens(_) => precedence_Const + | ApTyp(_) => precedence_Ap }; let pad_child = @@ -66,7 +66,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { ); let (doc, parenthesize) = switch (Typ.term_of(ty)) { - | Parens(ty) => (mk(~parenthesize=true, ~enforce_inline, ty), false) + | TypParens(ty) => (mk(~parenthesize=true, ~enforce_inline, ty), false) | Unknown(_) => ( annot(HTypAnnot.Delim, annot(HTypAnnot.HoleLabel, text("?"))), parenthesize, @@ -75,7 +75,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) - | Var(name) => (text(name), parenthesize) + | TypVar(name) => (text(name), parenthesize) | List(ty) => ( hcats([ mk_delim("["), @@ -173,7 +173,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { ) |> hcats; (center, true); - | Ap(t1, t2) => ( + | ApTyp(t1, t2) => ( hcats([mk'(t1), text("("), mk'(t2), text(")")]), parenthesize, )