From a07e1153f24b6d46e739474633fa9f3f6312e0cf Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 12 Sep 2024 11:15:46 -0400 Subject: [PATCH 1/3] In progress commit --- src/haz3lcore/dynamics/FilterEnvironment.re | 2 +- src/haz3lcore/lang/term/TPat.re | 2 +- src/haz3lcore/lang/term/Typ.re | 5 +- src/haz3lcore/statics/Ctx.re | 15 +- src/haz3lcore/statics/Term.re | 6 +- src/haz3lcore/statics/TermBase.re | 439 ++++++++------------ 6 files changed, 179 insertions(+), 290 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterEnvironment.re b/src/haz3lcore/dynamics/FilterEnvironment.re index 284e7353d3..ac59a874bc 100644 --- a/src/haz3lcore/dynamics/FilterEnvironment.re +++ b/src/haz3lcore/dynamics/FilterEnvironment.re @@ -1,2 +1,2 @@ -type t = list(TermBase.StepperFilterKind.filter); +type t = list(TermBase.filter); let extends = (flt, env) => [flt, ...env]; diff --git a/src/haz3lcore/lang/term/TPat.re b/src/haz3lcore/lang/term/TPat.re index 3dade36b54..583f805851 100644 --- a/src/haz3lcore/lang/term/TPat.re +++ b/src/haz3lcore/lang/term/TPat.re @@ -10,7 +10,7 @@ include TermBase.TPat; let rep_id: t => Id.t = IdTagged.rep_id; let fresh: term => t = IdTagged.fresh; -let hole = (tms: list(TermBase.Any.t)) => +let hole = (tms: list(TermBase.Any.t)): TermBase.TPat.term => switch (tms) { | [] => EmptyHole | [_, ..._] => MultiHole(tms) diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index 5dc0b73aaa..c9a6f0c204 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -34,7 +34,7 @@ let fresh: term => t = IdTagged.fresh; let temp: term => t = term => {term, ids: [Id.invalid], copied: false}; let rep_id: t => Id.t = IdTagged.rep_id; -let hole = (tms: list(TermBase.Any.t)) => +let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term => switch (tms) { | [] => Unknown(Hole(EmptyHole)) | [_, ..._] => Unknown(Hole(MultiHole(tms))) @@ -137,7 +137,8 @@ let of_source = List.map((source: source) => source.ty); but right now TypeHole strictly predominates over Internal which strictly predominates over SynSwitch. */ let join_type_provenance = - (p1: type_provenance, p2: type_provenance): 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) diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re index 9791b6cd0f..f213a18cb7 100644 --- a/src/haz3lcore/statics/Ctx.re +++ b/src/haz3lcore/statics/Ctx.re @@ -2,14 +2,14 @@ open Util; [@deriving (show({with_path: false}), sexp, yojson)] type kind = - | Singleton(TermBase.Typ.t) + | Singleton(TermBase.typ_t) | Abstract; [@deriving (show({with_path: false}), sexp, yojson)] type var_entry = { name: Var.t, id: Id.t, - typ: TermBase.Typ.t, + typ: TermBase.typ_t, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -99,7 +99,9 @@ let lookup_alias = (ctx: t, name: string): option(TermBase.Typ.t) => | Some(Singleton(ty)) => Some(ty) | Some(Abstract) => None | None => - Some(TermBase.Typ.Unknown(Hole(Invalid(name))) |> IdTagged.fresh) + Some( + (Unknown(Hole(Invalid(name))): TermBase.Typ.term) |> IdTagged.fresh, + ) }; let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t => @@ -112,11 +114,10 @@ let add_ctrs = (ctx: t, name: string, id: Id.t, ctrs: TermBase.Typ.sum_map): t = id, typ: switch (typ) { - | None => TermBase.Typ.Var(name) |> IdTagged.fresh + | None => (Var(name): TermBase.typ_term) |> IdTagged.fresh | Some(typ) => - TermBase.Typ.Arrow( - typ, - TermBase.Typ.Var(name) |> IdTagged.fresh, + ( + Arrow(typ, (Var(name): TermBase.typ_term) |> IdTagged.fresh): TermBase.typ_term ) |> IdTagged.fresh }, diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 0493150865..92eef8161e 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -31,7 +31,7 @@ module Pat = { let fresh: term => t = IdTagged.fresh; - let hole = (tms: list(TermBase.Any.t)) => + let hole = (tms: list(TermBase.Any.t)): TermBase.Pat.term => switch (tms) { | [] => EmptyHole | [_, ..._] => MultiHole(tms) @@ -597,7 +597,7 @@ module Any = { | Typ(t) => Some(t) | _ => None; - let rec ids = + let rec ids: TermBase.any_t => list(Id.t) = fun | Exp(tm) => tm.ids | Pat(tm) => tm.ids @@ -620,7 +620,7 @@ module Any = { // (This would change for n-tuples if we decided parentheses are necessary.) let rep_id = fun - | Exp(tm) => Exp.rep_id(tm) + | (Exp(tm): TermBase.any_t) => Exp.rep_id(tm) | Pat(tm) => Pat.rep_id(tm) | Typ(tm) => Typ.rep_id(tm) | TPat(tm) => TPat.rep_id(tm) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index f0585955c6..67e6f1ecde 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -2,6 +2,10 @@ open Util; let continue = x => x; let stop = (_, x) => x; +[@deriving (show({with_path: false}), sexp, yojson)] +type deferral_position = + | InAp + | OutsideAp; /* This megafile contains the definitions of the expression data types in @@ -42,16 +46,126 @@ let stop = (_, x) => x; the id of the closure. */ +[@deriving (show({with_path: false}), sexp, yojson)] +type any_t = + | Exp(exp_t) + | Pat(pat_t) + | Typ(typ_t) + | TPat(tpat_t) + | Rul(rul_t) + | Nul(unit) + | Any(unit) +and exp_term = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) + | DynamicErrorHole(exp_t, InvalidOperationError.t) + | FailedCast(exp_t, typ_t, typ_t) + | Deferral(deferral_position) + | Undefined + | Bool(bool) + | Int(int) + | Float(float) + | String(string) + | ListLit(list(exp_t)) + | Constructor(string, typ_t) // Typ.t field is only meaningful in dynamic expressions + | Fun( + pat_t, + exp_t, + [@show.opaque] option(closure_environment_t), + option(Var.t), + ) + | TypFun(tpat_t, exp_t, option(Var.t)) + | Tuple(list(exp_t)) + | Var(Var.t) + | Let(pat_t, exp_t, exp_t) + | FixF(pat_t, exp_t, option(closure_environment_t)) + | TyAlias(tpat_t, typ_t, exp_t) + | Ap(Operators.ap_direction, exp_t, exp_t) + | TypAp(exp_t, typ_t) + | DeferredAp(exp_t, list(exp_t)) + | If(exp_t, exp_t, exp_t) + | Seq(exp_t, exp_t) + | Test(exp_t) + | Filter(stepper_filter_kind_t, exp_t) + | Closure([@show.opaque] closure_environment_t, exp_t) + | Parens(exp_t) // ( + | Cons(exp_t, exp_t) + | ListConcat(exp_t, exp_t) + | UnOp(Operators.op_un, exp_t) + | BinOp(Operators.op_bin, exp_t, exp_t) + | BuiltinFun(string) + | Match(exp_t, list((pat_t, exp_t))) + /* INVARIANT: in dynamic expressions, casts must be between + two consistent types. Both types should be normalized in + dynamics for the cast calculus to work right. */ + | Cast(exp_t, typ_t, typ_t) +and exp_t = IdTagged.t(exp_term) +and pat_term = + | Invalid(string) + | EmptyHole + | MultiHole(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) +and pat_t = IdTagged.t(pat_term) +and typ_term = + | Unknown(type_provenance) + | Int + | Float + | Bool + | String + | Var(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) + | 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) +and tpat_t = IdTagged.t(tpat_term) +and rul_term = + | Invalid(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) + | Residue(int, FilterAction.t) +and type_hole = + | Invalid(string) + | EmptyHole + | MultiHole(list(any_t)) +and type_provenance = + | SynSwitch + | Hole(type_hole) + | Internal +and filter = { + pat: exp_t, + act: FilterAction.t, +}; + module rec Any: { - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Exp(Exp.t) - | Pat(Pat.t) - | Typ(Typ.t) - | TPat(TPat.t) - | Rul(Rul.t) - | Nul(unit) - | Any(unit); + type t = any_t; let map_term: ( @@ -67,15 +181,7 @@ module rec Any: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Exp(Exp.t) - | Pat(Pat.t) - | Typ(Typ.t) - | TPat(TPat.t) - | Rul(Rul.t) - | Nul(unit) - | Any(unit); + type t = any_t; let map_term = ( @@ -126,58 +232,8 @@ module rec Any: { }; } and Exp: { - [@deriving (show({with_path: false}), sexp, yojson)] - type deferral_position = - | InAp - | OutsideAp; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | DynamicErrorHole(t, InvalidOperationError.t) - | FailedCast(t, Typ.t, Typ.t) - | Deferral(deferral_position) - | Undefined - | Bool(bool) - | Int(int) - | Float(float) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic expressions - | Fun( - Pat.t, - t, - [@show.opaque] option(ClosureEnvironment.t), - option(Var.t), - ) - | TypFun(TPat.t, t, option(Var.t)) - | Tuple(list(t)) - | Var(Var.t) - | Let(Pat.t, t, t) - | FixF(Pat.t, t, option(ClosureEnvironment.t)) - | TyAlias(TPat.t, Typ.t, t) - | Ap(Operators.ap_direction, t, t) - | TypAp(t, Typ.t) - | DeferredAp(t, list(t)) - | If(t, t, t) - | Seq(t, t) - | Test(t) - | Filter(StepperFilterKind.t, t) - | Closure([@show.opaque] ClosureEnvironment.t, t) - | Parens(t) // ( - | Cons(t, t) - | ListConcat(t, t) - | UnOp(Operators.op_un, t) - | BinOp(Operators.op_bin, t, t) - | BuiltinFun(string) - | Match(t, list((Pat.t, t))) - /* INVARIANT: in dynamic expressions, casts must be between - two consistent types. Both types should be normalized in - dynamics for the cast calculus to work right. */ - | Cast(t, Typ.t, Typ.t) // first Typ.t field is only meaningful in dynamic expressions - and t = IdTagged.t(term); + type term = exp_term; + type t = exp_t; let map_term: ( @@ -193,55 +249,8 @@ and Exp: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type deferral_position = - | InAp - | OutsideAp; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | DynamicErrorHole(t, InvalidOperationError.t) - | FailedCast(t, Typ.t, Typ.t) - | Deferral(deferral_position) - | Undefined - | Bool(bool) - | Int(int) - | Float(float) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) - | Fun( - Pat.t, - t, - [@show.opaque] option(ClosureEnvironment.t), - option(Var.t), - ) - | TypFun(TPat.t, t, option(string)) - | Tuple(list(t)) - | Var(Var.t) - | Let(Pat.t, t, t) - | FixF(Pat.t, t, [@show.opaque] option(ClosureEnvironment.t)) - | TyAlias(TPat.t, Typ.t, t) - | Ap(Operators.ap_direction, t, t) // note: function is always first then argument; even in pipe mode - | TypAp(t, Typ.t) - | DeferredAp(t, list(t)) - | If(t, t, t) - | Seq(t, t) - | Test(t) - | Filter(StepperFilterKind.t, t) - | Closure([@show.opaque] ClosureEnvironment.t, t) - | Parens(t) - | Cons(t, t) - | ListConcat(t, t) - | UnOp(Operators.op_un, t) - | BinOp(Operators.op_bin, t, t) - | BuiltinFun(string) /// Doesn't currently have a distinguishable syntax - | Match(t, list((Pat.t, t))) - | Cast(t, Typ.t, Typ.t) - and t = IdTagged.t(term); + type term = exp_term; + type t = exp_t; let map_term = ( @@ -447,25 +456,8 @@ and Exp: { }; } and Pat: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Wild - | Int(int) - | Float(float) - | Bool(bool) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) // Typ.t field is only meaningful in dynamic patterns - | Cons(t, t) - | Var(Var.t) - | Tuple(list(t)) - | Parens(t) - | Ap(t, t) - | Cast(t, Typ.t, Typ.t) // The second Typ.t field is only meaningful in dynamic patterns - and t = IdTagged.t(term); + type term = pat_term; // The second Typ.t field is only meaningful in dynamic patterns + type t = pat_t; let map_term: ( @@ -481,25 +473,8 @@ and Pat: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Wild - | Int(int) - | Float(float) - | Bool(bool) - | String(string) - | ListLit(list(t)) - | Constructor(string, Typ.t) - | Cons(t, t) - | Var(Var.t) - | Tuple(list(t)) - | Parens(t) - | Ap(t, t) - | Cast(t, Typ.t, Typ.t) // The second one is hidden from the user - and t = IdTagged.t(term); + type term = pat_term; + type t = pat_t; let map_term = ( @@ -543,7 +518,7 @@ and Pat: { x |> f_pat(rec_call); }; - let rec fast_equal = (p1, p2) => + 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) @@ -588,38 +563,9 @@ and Pat: { } and Typ: { [@deriving (show({with_path: false}), sexp, yojson)] - type type_hole = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)); - - /* TYPE_PROVENANCE: From whence does an unknown type originate? - Is it generated from an unannotated pattern variable (SynSwitch), - a pattern variable annotated with a type hole (TypeHole), or - generated by an internal judgement (Internal)? */ - [@deriving (show({with_path: false}), sexp, yojson)] - type type_provenance = - | SynSwitch - | Hole(type_hole) - | Internal; - + type term = typ_term; [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Unknown(Typ.type_provenance) - | Int - | Float - | Bool - | String - | Var(string) - | List(t) - | Arrow(t, t) - | Sum(ConstructorMap.t(t)) - | Prod(list(t)) - | Parens(t) - | Ap(t, t) - | Rec(TPat.t, t) - | Forall(TPat.t, t) - and t = IdTagged.t(term); + type t = typ_t; type sum_map = ConstructorMap.t(t); @@ -640,38 +586,9 @@ and Typ: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type type_hole = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)); - - /* TYPE_PROVENANCE: From whence does an unknown type originate? - Is it generated from an unannotated pattern variable (SynSwitch), - a pattern variable annotated with a type hole (TypeHole), or - generated by an internal judgement (Internal)? */ + type term = typ_term; [@deriving (show({with_path: false}), sexp, yojson)] - type type_provenance = - | SynSwitch - | Hole(type_hole) - | Internal; - - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Unknown(Typ.type_provenance) - | Int - | Float - | Bool - | String - | Var(string) - | List(t) - | Arrow(t, t) - | Sum(ConstructorMap.t(t)) - | Prod(list(t)) - | Parens(t) - | Ap(t, t) - | Rec(TPat.t, t) - | Forall(TPat.t, t) - and t = IdTagged.t(term); + type t = typ_t; type sum_map = ConstructorMap.t(t); @@ -729,12 +646,12 @@ and Typ: { x |> f_typ(rec_call); }; - let rec subst = (s: t, x: TPat.t, ty: t) => { + let rec subst = (s: t, x: TPat.t, ty: t): typ_t => { switch (TPat.tyvar_of_utpat(x)) { | Some(str) => let (term, rewrap) = IdTagged.unwrap(ty); switch (term) { - | Int => Int |> rewrap + | Int => (Int: typ_term) |> rewrap | Float => Float |> rewrap | Bool => Bool |> rewrap | String => String |> rewrap @@ -811,12 +728,8 @@ and Typ: { } and TPat: { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Var(string) - and t = IdTagged.t(term); + type term = tpat_term; + type t = tpat_t; let map_term: ( @@ -835,12 +748,8 @@ and TPat: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | EmptyHole - | MultiHole(list(Any.t)) - | Var(string) - and t = IdTagged.t(term); + type term = tpat_term; + type t = tpat_t; let map_term = ( @@ -889,11 +798,8 @@ and TPat: { } and Rul: { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | Hole(list(Any.t)) - | Rules(Exp.t, list((Pat.t, Exp.t))) - and t = IdTagged.t(term); + type term = rul_term; + type t = rul_t; let map_term: ( @@ -910,11 +816,9 @@ and Rul: { let fast_equal: (t, t) => bool; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Invalid(string) - | Hole(list(Any.t)) - | Rules(Exp.t, list((Pat.t, Exp.t))) - and t = IdTagged.t(term); + type term = rul_term; + [@deriving (show({with_path: false}), sexp, yojson)] + type t = rul_t; let map_term = ( @@ -977,13 +881,11 @@ and Environment: { (module type of VarBstMap.Ordered) with type t_('a) = VarBstMap.Ordered.t_('a); - [@deriving (show({with_path: false}), sexp, yojson)] - type t = t_(Exp.t); + type t = environment_t; } = { include VarBstMap.Ordered; - [@deriving (show({with_path: false}), sexp, yojson)] - type t = t_(Exp.t); + type t = environment_t; } and ClosureEnvironment: { @@ -999,7 +901,7 @@ and ClosureEnvironment: { let of_environment: Environment.t => t; - let id_equal: (t, t) => bool; + let id_equal: (closure_environment_t, closure_environment_t) => bool; let empty: t; let is_empty: t => bool; @@ -1025,7 +927,7 @@ and ClosureEnvironment: { } = { module Inner: { [@deriving (show({with_path: false}), sexp, yojson)] - type t; + type t = closure_environment_t; let wrap: (Id.t, Environment.t) => t; @@ -1033,7 +935,7 @@ and ClosureEnvironment: { let map_of: t => Environment.t; } = { [@deriving (show({with_path: false}), sexp, yojson)] - type t = (Id.t, Environment.t); + type t = closure_environment_t; let wrap = (ei, map): t => (ei, map); @@ -1099,16 +1001,7 @@ and ClosureEnvironment: { let without_keys = keys => update(Environment.without_keys(keys)); } and StepperFilterKind: { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; - - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); + type t = stepper_filter_kind_t; let map_term: ( @@ -1126,18 +1019,9 @@ and StepperFilterKind: { let fast_equal: (t, t) => bool; } = { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; + type t = stepper_filter_kind_t; - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); - - let map = (mapper, filter) => { + let map = (mapper, filter: t): t => { switch (filter) { | Filter({act, pat}) => Filter({act, pat: mapper(pat)}) | Residue(idx, act) => Residue(idx, act) @@ -1155,12 +1039,15 @@ and StepperFilterKind: { ) => { let exp_map_term = 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}) - | Residue(i, a) => Residue(i, a); + ( + fun + | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act}) + | Residue(i, a) => Residue(i, a): + t => t + ); }; - let fast_equal = (f1, f2) => + let fast_equal = (f1: t, f2: t) => switch (f1, f2) { | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) => Exp.fast_equal(e1, e2) && a1 == a2 From 370e7aa06979aac3463ca9aa71768e2fd73b72b1 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 12 Sep 2024 12:29:28 -0400 Subject: [PATCH 2/3] Finished the refactor --- src/haz3lcore/dynamics/Builtins.re | 21 ++- src/haz3lcore/dynamics/Casts.re | 18 +- src/haz3lcore/dynamics/Elaborator.re | 77 ++++----- src/haz3lcore/dynamics/EvalCtx.re | 199 +++++++++++------------ src/haz3lcore/dynamics/FilterMatcher.re | 32 ++-- src/haz3lcore/dynamics/TypeAssignment.re | 12 +- src/haz3lcore/dynamics/ValueChecker.re | 1 - src/haz3lcore/prog/CachedStatics.re | 6 +- src/haz3lcore/statics/MakeTerm.re | 10 +- src/haz3lcore/statics/Mode.re | 3 +- src/haz3lcore/statics/Statics.re | 17 +- src/haz3lcore/statics/TermBase.re | 26 ++- src/haz3lcore/zipper/Editor.re | 6 +- src/haz3lcore/zipper/EditorUtil.re | 94 ++++++----- src/haz3lschool/Exercise.re | 33 ++-- src/haz3lweb/view/Cell.re | 2 +- src/haz3lweb/view/ExplainThis.re | 6 +- src/haz3lweb/view/Type.re | 4 +- 18 files changed, 285 insertions(+), 282 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 4479989fd5..c47617edc6 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 = DHExp.Float(Float.infinity) |> fresh; - let neg_infinity = DHExp.Float(Float.neg_infinity) |> fresh; - let nan = DHExp.Float(Float.nan) |> fresh; - let epsilon_float = DHExp.Float(epsilon_float) |> fresh; - let pi = DHExp.Float(Float.pi) |> fresh; - let max_int = DHExp.Int(Int.max_int) |> fresh; - let min_int = DHExp.Int(Int.min_int) |> fresh; + 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 unary = (f: DHExp.t => result, d: DHExp.t) => { switch (f(d)) { @@ -180,8 +180,8 @@ module Pervasives = { switch (convert(s)) { | Some(n) => Ok(wrap(n)) | None => - let d' = DHExp.BuiltinFun(name) |> DHExp.fresh; - let d' = DHExp.Ap(Forward, d', d) |> DHExp.fresh; + let d' = BuiltinFun(name) |> DHExp.fresh; + let d' = Ap(Forward, d', d) |> DHExp.fresh; let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh; Ok(d'); } @@ -204,8 +204,7 @@ module Pervasives = { Ok( fresh( DynamicErrorHole( - DHExp.Ap(Forward, DHExp.BuiltinFun(name) |> fresh, d1) - |> fresh, + Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh, DivideByZero, ), ), diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re index 170d057e76..a69f560dd5 100644 --- a/src/haz3lcore/dynamics/Casts.re +++ b/src/haz3lcore/dynamics/Casts.re @@ -39,7 +39,7 @@ let grounded_Forall = ); let grounded_Prod = length => NotGroundOrHole( - Prod(ListUtil.replicate(length, Typ.Unknown(Internal) |> Typ.temp)) + Prod(ListUtil.replicate(length, Unknown(Internal) |> Typ.temp)) |> Typ.temp, ); let grounded_Sum: unit => Typ.sum_map = @@ -50,7 +50,7 @@ let grounded_List = let rec ground_cases_of = (ty: Typ.t): ground_cases => { let is_hole: Typ.t => bool = fun - | {term: Typ.Unknown(_), _} => true + | {term: Unknown(_), _} => true | _ => false; switch (Typ.term_of(ty)) { | Unknown(_) => Hole @@ -67,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Prod(tys) => if (List.for_all( fun - | ({term: Typ.Unknown(_), _}: Typ.t) => true + | ({term: Unknown(_), _}: Typ.t) => true | _ => false, tys, )) { @@ -132,12 +132,12 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => { | Some(d1) => d1 | None => inner_cast }; - Some(DHExp.Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh); + Some(Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh); | (NotGroundOrHole(t1_grounded), Hole) => /* ITGround rule */ Some( - DHExp.Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2) + Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2) |> DHExp.fresh, ) @@ -187,7 +187,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => { let (p1, d1) = unwrap_casts(p1); ( p1, - {term: DHExp.Cast(d1, t1, t2), copied: p.copied, ids: p.ids} + {term: Cast(d1, t1, t2), copied: p.copied, ids: p.ids} |> transition_multiple, ); | _ => (p, hole) @@ -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: DHPat.Cast(p1, t1, t2), copied: d.copied, ids: d.ids}; + {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids}; | FailedCast(d1, t1, t2) => let p1 = rewrap_casts((p, d1)); { term: - DHPat.Cast( - DHPat.Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, + Cast( + Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh, Typ.fresh(Unknown(Internal)), t2, ), diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..d50d462064 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -23,10 +23,10 @@ let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => { ? d : { let d' = - DHExp.Cast(d, t1, Typ.temp(Unknown(Internal))) + Cast(d, t1, Typ.temp(Unknown(Internal))) |> DHExp.fresh |> Casts.transition_multiple; - DHExp.Cast(d', Typ.temp(Unknown(Internal)), t2) + Cast(d', Typ.temp(Unknown(Internal)), t2) |> DHExp.fresh |> Casts.transition_multiple; }; @@ -63,11 +63,11 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => { | Syn => self_ty | SynFun => let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty); - Typ.Arrow(ty1, ty2) |> Typ.temp; + Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); - Typ.Forall(tpat, ty) |> Typ.temp; + Forall(tpat, ty) |> Typ.temp; // We need to remove the synswitches from this type. | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty) }; @@ -90,11 +90,11 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => { | Syn => self_ty | SynFun => let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty); - Typ.Arrow(ty1, ty2) |> Typ.temp; + Arrow(ty1, ty2) |> Typ.temp; | SynTypFun => let (tpat, ty) = Typ.matched_forall(ctx, self_ty); let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole)); - Typ.Forall(tpat, ty) |> Typ.temp; + Forall(tpat, ty) |> Typ.temp; | Ana(ana_ty) => switch (prev_synswitch) { | None => ana_ty @@ -125,9 +125,7 @@ let rec elaborate_pattern = |> List.map2((p, t) => fresh_pat_cast(p, t, inner_type), _, tys) |> ( ps' => - DHPat.ListLit(ps') - |> rewrap - |> cast_from(List(inner_type) |> Typ.temp) + ListLit(ps') |> rewrap |> cast_from(List(inner_type) |> Typ.temp) ); | Cons(p1, p2) => let (p1', ty1) = elaborate_pattern(m, p1); @@ -138,19 +136,17 @@ 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); - DHPat.Cons(p1'', p2'') - |> rewrap - |> cast_from(List(ty_inner) |> Typ.temp); + Cons(p1'', p2'') |> rewrap |> cast_from(List(ty_inner) |> Typ.temp); | Tuple(ps) => let (ps', tys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; - DHPat.Tuple(ps') |> rewrap |> cast_from(Typ.Prod(tys) |> Typ.temp); + Tuple(ps') |> rewrap |> cast_from(Prod(tys) |> Typ.temp); | Ap(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); - DHPat.Ap(p1'', p2'') |> rewrap |> cast_from(ty1r); + Ap(p1'', p2'') |> rewrap |> cast_from(ty1r); | Invalid(_) | EmptyHole | MultiHole(_) @@ -213,7 +209,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { switch (term) { | Invalid(_) | Undefined - | EmptyHole => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal))) + | EmptyHole => uexp |> cast_from(Typ.temp(Unknown(Internal))) | MultiHole(stuff) => Any.map_term( ~f_exp=(_, exp) => {elaborate(m, exp) |> fst}, @@ -223,9 +219,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { |> List.map(_, stuff) |> ( stuff => - DHExp.MultiHole(stuff) + MultiHole(stuff) |> rewrap - |> cast_from(Typ.temp(Typ.Unknown(Internal))) + |> cast_from(Typ.temp(Unknown(Internal))) ) | DynamicErrorHole(e, err) => let (e', _) = elaborate(m, e); @@ -245,10 +241,10 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | ListLit(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; let inner_type = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, tys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, tys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let ds' = List.map2((d, t) => fresh_cast(d, t, inner_type), ds, tys); - Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp); + ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp); | Constructor(c, _) => let mode = switch (Id.Map.find_opt(Exp.rep_id(uexp), m)) { @@ -266,23 +262,23 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | Fun(p, e, env, n) => let (p', typ) = elaborate_pattern(m, p); let (e', tye) = elaborate(m, e); - Exp.Fun(p', e', env, n) + Fun(p', e', env, n) |> rewrap |> cast_from(Arrow(typ, tye) |> Typ.temp); | TypFun(tpat, e, name) => let (e', tye) = elaborate(m, e); - Exp.TypFun(tpat, e', name) + TypFun(tpat, e', name) |> rewrap - |> cast_from(Typ.Forall(tpat, tye) |> Typ.temp); + |> cast_from(Forall(tpat, tye) |> Typ.temp); | Tuple(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; - Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp); + Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp); | Var(v) => uexp |> cast_from( Ctx.lookup_var(ctx, v) |> Option.map((x: Ctx.var_entry) => x.typ |> Typ.normalize(ctx)) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))), + |> Option.value(~default=Typ.temp(Unknown(Internal))), ) | Let(p, def, body) => let add_name: (option(string), DHExp.t) => DHExp.t = ( @@ -305,9 +301,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let def = add_name(Pat.get_var(p), def); let (def, ty2) = elaborate(m, def); let (body, ty) = elaborate(m, body); - Exp.Let(p, fresh_cast(def, ty2, ty1), body) - |> rewrap - |> cast_from(ty); + Let(p, fresh_cast(def, ty2, ty1), body) |> rewrap |> cast_from(ty); } else { // TODO: Add names to mutually recursive functions // TODO: Don't add fixpoint if there already is one @@ -315,14 +309,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (def, ty2) = elaborate(m, def); let (body, ty) = elaborate(m, body); let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh; - Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty); + Let(p, fixf, body) |> rewrap |> cast_from(ty); }; | FixF(p, e, env) => let (p', typ) = elaborate_pattern(m, p); let (e', tye) = elaborate(m, e); - Exp.FixF(p', fresh_cast(e', tye, typ), env) - |> rewrap - |> cast_from(typ); + FixF(p', fresh_cast(e', tye, typ), env) |> rewrap |> cast_from(typ); | TyAlias(_, _, e) => let (e', tye) = elaborate(m, e); e' |> cast_from(tye); @@ -332,7 +324,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf); let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp); let a'' = fresh_cast(a', tya, tyf1); - Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2); + Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2); | DeferredAp(f, args) => let (f', tyf) = elaborate(m, f); let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip; @@ -371,11 +363,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (f', tyf) = elaborate(m, f); let ty = Typ.join(~fix=false, ctx, tyt, tyf) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + |> Option.value(~default=Typ.temp(Unknown(Internal))); let c'' = fresh_cast(c', tyc, Bool |> Typ.temp); let t'' = fresh_cast(t', tyt, ty); let f'' = fresh_cast(f', tyf, ty); - Exp.If(c'', t'', f'') |> rewrap |> cast_from(ty); + If(c'', t'', f'') |> rewrap |> cast_from(ty); | Seq(e1, e2) => let (e1', _) = elaborate(m, e1); let (e2', ty2) = elaborate(m, e2); @@ -427,10 +419,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { Constructor("$e", Unknown(Internal) |> Typ.temp) |> rewrap | Var("v") => Constructor("$v", Unknown(Internal) |> Typ.temp) |> rewrap - | _ => - DHExp.EmptyHole - |> rewrap - |> cast_from(Typ.temp(Typ.Unknown(Internal))) + | _ => EmptyHole |> rewrap |> cast_from(Typ.temp(Unknown(Internal))) } | UnOp(Int(Minus), e) => let (e', t) = elaborate(m, e); @@ -533,7 +522,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { |> cast_from( Ctx.lookup_var(Builtins.ctx_init, fn) |> Option.map((x: Ctx.var_entry) => x.typ) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))), + |> Option.value(~default=Typ.temp(Unknown(Internal))), ) | Match(e, cases) => let (e', t) = elaborate(m, e); @@ -541,15 +530,15 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let (ps', ptys) = List.map(elaborate_pattern(m), ps) |> ListUtil.unzip; let joined_pty = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, ptys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, ptys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let ps'' = List.map2((p, t) => fresh_pat_cast(p, t, joined_pty), ps', ptys); let e'' = fresh_cast(e', t, joined_pty); let (es', etys) = List.map(elaborate(m), es) |> ListUtil.unzip; let joined_ety = - Typ.join_all(~empty=Typ.Unknown(Internal) |> Typ.temp, ctx, etys) - |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))); + Typ.join_all(~empty=Unknown(Internal) |> Typ.temp, ctx, etys) + |> Option.value(~default=Typ.temp(Unknown(Internal))); let es'' = List.map2((e, t) => fresh_cast(e, t, joined_ety), es', etys); Match(e'', List.combine(ps'', es'')) diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re index bed931c8d3..1f60bfa70a 100644 --- a/src/haz3lcore/dynamics/EvalCtx.re +++ b/src/haz3lcore/dynamics/EvalCtx.re @@ -51,106 +51,103 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => { | Mark => d | Term({term, ids}) => let wrap = DHExp.mk(ids); - DHExp.( - switch (term) { - | Closure(env, ctx) => - let d = compose(ctx, d); - Closure(env, d) |> wrap; - | Filter(flt, ctx) => - let d = compose(ctx, d); - Filter(flt, d) |> wrap; - | Seq1(ctx, d2) => - let d1 = compose(ctx, d); - Seq(d1, d2) |> wrap; - | Seq2(d1, ctx) => - let d2 = compose(ctx, d); - Seq(d1, d2) |> wrap; - | Ap1(dir, ctx, d2) => - let d1 = compose(ctx, d); - Ap(dir, d1, d2) |> wrap; - | Ap2(dir, d1, ctx) => - let d2 = compose(ctx, d); - Ap(dir, d1, d2) |> wrap; - | DeferredAp1(ctx, d2s) => - let d1 = compose(ctx, d); - DeferredAp(d1, d2s) |> wrap; - | DeferredAp2(d1, ctx, (ld, rd)) => - let d2 = compose(ctx, d); - DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap; - | If1(ctx, d2, d3) => - let d' = compose(ctx, d); - If(d', d2, d3) |> wrap; - | If2(d1, ctx, d3) => - let d' = compose(ctx, d); - If(d1, d', d3) |> wrap; - | If3(d1, d2, ctx) => - let d' = compose(ctx, d); - If(d1, d2, d') |> wrap; - | Test(ctx) => - let d1 = compose(ctx, d); - Test(d1) |> wrap; - | UnOp(op, ctx) => - let d1 = compose(ctx, d); - UnOp(op, d1) |> wrap; - | BinOp1(op, ctx, d2) => - let d1 = compose(ctx, d); - BinOp(op, d1, d2) |> wrap; - | BinOp2(op, d1, ctx) => - let d2 = compose(ctx, d); - BinOp(op, d1, d2) |> wrap; - | Cons1(ctx, d2) => - let d1 = compose(ctx, d); - Cons(d1, d2) |> wrap; - | Cons2(d1, ctx) => - let d2 = compose(ctx, d); - Cons(d1, d2) |> wrap; - | ListConcat1(ctx, d2) => - let d1 = compose(ctx, d); - ListConcat(d1, d2) |> wrap; - | ListConcat2(d1, ctx) => - let d2 = compose(ctx, d); - ListConcat(d1, d2) |> wrap; - | Tuple(ctx, (ld, rd)) => - let d = compose(ctx, d); - Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; - | ListLit(ctx, (ld, rd)) => - let d = compose(ctx, d); - ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; - | MultiHole(ctx, (ld, rd)) => - let d = compose(ctx, d); - MultiHole(ListUtil.rev_concat(ld, [TermBase.Any.Exp(d), ...rd])) - |> wrap; - | Let1(dp, ctx, d2) => - let d = compose(ctx, d); - Let(dp, d, d2) |> wrap; - | Let2(dp, d1, ctx) => - let d = compose(ctx, d); - Let(dp, d1, d) |> wrap; - | Fun(dp, ctx, env, v) => - let d = compose(ctx, d); - Fun(dp, d, env, v) |> wrap; - | FixF(v, ctx, env) => - let d = compose(ctx, d); - FixF(v, d, env) |> wrap; - | Cast(ctx, ty1, ty2) => - let d = compose(ctx, d); - Cast(d, ty1, ty2) |> wrap; - | FailedCast(ctx, ty1, ty2) => - let d = compose(ctx, d); - FailedCast(d, ty1, ty2) |> wrap; - | DynamicErrorHole(ctx, err) => - let d = compose(ctx, d); - DynamicErrorHole(d, err) |> wrap; - | MatchScrut(ctx, rules) => - let d = compose(ctx, d); - Match(d, rules) |> wrap; - | MatchRule(scr, p, ctx, (lr, rr)) => - let d = compose(ctx, d); - Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap; - | TypAp(ctx, ty) => - let d = compose(ctx, d); - TypAp(d, ty) |> wrap; - } - ); + switch (term) { + | Closure(env, ctx) => + let d = compose(ctx, d); + Closure(env, d) |> wrap; + | Filter(flt, ctx) => + let d = compose(ctx, d); + Filter(flt, d) |> wrap; + | Seq1(ctx, d2) => + let d1 = compose(ctx, d); + Seq(d1, d2) |> wrap; + | Seq2(d1, ctx) => + let d2 = compose(ctx, d); + Seq(d1, d2) |> wrap; + | Ap1(dir, ctx, d2) => + let d1 = compose(ctx, d); + Ap(dir, d1, d2) |> wrap; + | Ap2(dir, d1, ctx) => + let d2 = compose(ctx, d); + Ap(dir, d1, d2) |> wrap; + | DeferredAp1(ctx, d2s) => + let d1 = compose(ctx, d); + DeferredAp(d1, d2s) |> wrap; + | DeferredAp2(d1, ctx, (ld, rd)) => + let d2 = compose(ctx, d); + DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap; + | If1(ctx, d2, d3) => + let d' = compose(ctx, d); + If(d', d2, d3) |> wrap; + | If2(d1, ctx, d3) => + let d' = compose(ctx, d); + If(d1, d', d3) |> wrap; + | If3(d1, d2, ctx) => + let d' = compose(ctx, d); + If(d1, d2, d') |> wrap; + | Test(ctx) => + let d1 = compose(ctx, d); + Test(d1) |> wrap; + | UnOp(op, ctx) => + let d1 = compose(ctx, d); + UnOp(op, d1) |> wrap; + | BinOp1(op, ctx, d2) => + let d1 = compose(ctx, d); + BinOp(op, d1, d2) |> wrap; + | BinOp2(op, d1, ctx) => + let d2 = compose(ctx, d); + BinOp(op, d1, d2) |> wrap; + | Cons1(ctx, d2) => + let d1 = compose(ctx, d); + Cons(d1, d2) |> wrap; + | Cons2(d1, ctx) => + let d2 = compose(ctx, d); + Cons(d1, d2) |> wrap; + | ListConcat1(ctx, d2) => + let d1 = compose(ctx, d); + ListConcat(d1, d2) |> wrap; + | ListConcat2(d1, ctx) => + let d2 = compose(ctx, d); + ListConcat(d1, d2) |> wrap; + | Tuple(ctx, (ld, rd)) => + let d = compose(ctx, d); + Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; + | ListLit(ctx, (ld, rd)) => + let d = compose(ctx, d); + ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; + | MultiHole(ctx, (ld, rd)) => + let d = compose(ctx, d); + MultiHole(ListUtil.rev_concat(ld, [Exp(d), ...rd])) |> wrap; + | Let1(dp, ctx, d2) => + let d = compose(ctx, d); + Let(dp, d, d2) |> wrap; + | Let2(dp, d1, ctx) => + let d = compose(ctx, d); + Let(dp, d1, d) |> wrap; + | Fun(dp, ctx, env, v) => + let d = compose(ctx, d); + Fun(dp, d, env, v) |> wrap; + | FixF(v, ctx, env) => + let d = compose(ctx, d); + FixF(v, d, env) |> wrap; + | Cast(ctx, ty1, ty2) => + let d = compose(ctx, d); + Cast(d, ty1, ty2) |> wrap; + | FailedCast(ctx, ty1, ty2) => + let d = compose(ctx, d); + FailedCast(d, ty1, ty2) |> wrap; + | DynamicErrorHole(ctx, err) => + let d = compose(ctx, d); + DynamicErrorHole(d, err) |> wrap; + | MatchScrut(ctx, rules) => + let d = compose(ctx, d); + Match(d, rules) |> wrap; + | MatchRule(scr, p, ctx, (lr, rr)) => + let d = compose(ctx, d); + Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap; + | TypAp(ctx, ty) => + let d = compose(ctx, d); + TypAp(d, ty) |> wrap; + }; }; }; diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d6d0bcc543..61fd72f1bd 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -24,7 +24,9 @@ let evaluate_extend_env_with_pat = { ids, copied, - IdTagged.term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), + IdTagged.term: ( + FixF(pat, exp, Some(to_extend)): TermBase.exp_term + ), }, )), to_extend, @@ -36,14 +38,12 @@ let evaluate_extend_env_with_pat = binding => ( binding, - TermBase.Exp.Let( - pat, - { - ids, - copied, - term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), - }, - TermBase.Exp.Var(binding) |> IdTagged.fresh, + ( + Let( + pat, + {ids, copied, term: FixF(pat, exp, Some(to_extend))}, + (Var(binding): TermBase.exp_term) |> IdTagged.fresh, + ): TermBase.exp_term ) |> IdTagged.fresh, ), @@ -75,13 +75,13 @@ let tangle = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); @@ -356,13 +356,13 @@ and matches_fun = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); @@ -387,11 +387,7 @@ and matches_utpat = (d: TPat.t, f: TPat.t): bool => { }; let matches = - ( - ~env: ClosureEnvironment.t, - ~exp: DHExp.t, - ~flt: TermBase.StepperFilterKind.filter, - ) + (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: TermBase.filter) : option(FilterAction.t) => if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) { Some(flt.act); diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index f4979d94bf..59b58aa56f 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -161,16 +161,16 @@ 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(Typ.Arrow(ty_p, ty2) |> Typ.temp); + Some(Arrow(ty_p, ty2) |> Typ.temp); | TypFun({term: Var(name), _} as utpat, d, _) when !Ctx.shadows_typ(ctx, name) => let ctx = Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract}); let* ty = typ_of_dhexp(ctx, m, d); - Some(Typ.Forall(utpat, ty) |> Typ.temp); + Some(Forall(utpat, ty) |> Typ.temp); | TypFun(_, d, _) => let* ty = typ_of_dhexp(ctx, m, d); - Some(Typ.Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp); + Some(Forall(Var("?") |> 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); @@ -209,8 +209,8 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => |> OptUtil.sequence; switch (tys) { | [] => Some(tyr) - | [ty] => Some(Typ.Arrow(ty, tyr) |> Typ.temp) - | tys => Some(Typ.Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp) + | [ty] => Some(Arrow(ty, tyr) |> Typ.temp) + | tys => Some(Arrow(Prod(tys) |> Typ.temp, tyr) |> Typ.temp) }; } else { None; @@ -221,7 +221,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => Some(var.typ); | Test(dtest) => let* ty = typ_of_dhexp(ctx, m, dtest); - Typ.eq(ty, Bool |> Typ.temp) ? Some(Typ.Prod([]) |> Typ.temp) : None; + 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) diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index 39f43daeed..d6af00f4a4 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -1,4 +1,3 @@ -open DHExp; open Transition; type t = diff --git a/src/haz3lcore/prog/CachedStatics.re b/src/haz3lcore/prog/CachedStatics.re index f2bc13d113..3df0669dc3 100644 --- a/src/haz3lcore/prog/CachedStatics.re +++ b/src/haz3lcore/prog/CachedStatics.re @@ -8,7 +8,11 @@ type statics = { }; let empty_statics: statics = { - term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])}, + term: { + ids: [Id.invalid], + copied: false, + term: Tuple([]), + }, info_map: Id.Map.empty, error_ids: [], }; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 673af0bb89..d1edb9d16a 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -61,11 +61,11 @@ let is_grout = tiles => let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => { open OptUtil.Syntax; let+ ps = - ts + (ts: list(tile)) |> List.map( fun - | (_, (["|", "=>"], [Any.Pat(p)])) => Some(p) - | _ => None, + | (_, (["|", "=>"], [Pat(p)])) => Some(p) + | _ => None: tile => option(TermBase.pat_t), ) |> OptUtil.sequence and+ clauses = @@ -73,7 +73,7 @@ let is_rules = ((ts, kids): tiles): option(Aba.t(UPat.t, UExp.t)) => { |> List.map( fun | Exp(clause) => Some(clause) - | _ => None, + | _ => None: TermBase.any_t => option(TermBase.exp_t), ) |> OptUtil.sequence; Aba.mk(ps, clauses); @@ -494,7 +494,7 @@ and tpat_term: unsorted => TPat.term = { // return(r => Rul(r), ids, {ids, term}); // } and rul = (unsorted: unsorted): Rul.t => { - let hole = Rul.Hole(kids_of_unsorted(unsorted)); + let hole: Rul.term = Hole(kids_of_unsorted(unsorted)); switch (exp(unsorted)) { | {term: MultiHole(_), _} => switch (unsorted) { diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re index 5a85dbecd9..2415399627 100644 --- a/src/haz3lcore/statics/Mode.re +++ b/src/haz3lcore/statics/Mode.re @@ -152,6 +152,7 @@ let typap_mode: t = SynTypFun; let of_deferred_ap_args = (length: int, ty_ins: list(Typ.t)): list(t) => ( List.length(ty_ins) == length - ? ty_ins : List.init(length, _ => Typ.Unknown(Internal) |> Typ.temp) + ? ty_ins + : List.init(length, _ => (Unknown(Internal): Typ.term) |> Typ.temp) ) |> List.map(ty => Ana(ty)); diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index aca1ce0389..443c94155b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -276,13 +276,13 @@ and uexp_to_info_map = copied: false, term: switch (e.term) { - | Var("e") => UExp.Constructor("$e", Unknown(Internal) |> Typ.temp) - | Var("v") => UExp.Constructor("$v", Unknown(Internal) |> Typ.temp) + | Var("e") => Constructor("$e", Unknown(Internal) |> Typ.temp) + | Var("v") => Constructor("$v", Unknown(Internal) |> Typ.temp) | _ => e.term }, }; - let ty_in = Typ.Var("$Meta") |> Typ.temp; - let ty_out = Typ.Unknown(Internal) |> Typ.temp; + let ty_in = Var("$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); | UnOp(op, e) => @@ -426,8 +426,7 @@ and uexp_to_info_map = let def_ctx = p_ana'.ctx; let (def_base2, _) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m); let ana_ty_fn = ((ty_fn1, ty_fn2), ty_p) => { - Typ.term_of(ty_p) == Typ.Unknown(SynSwitch) - && !Typ.eq(ty_fn1, ty_fn2) + Typ.term_of(ty_p) == Unknown(SynSwitch) && !Typ.eq(ty_fn1, ty_fn2) ? ty_fn1 : ty_p; }; let ana = @@ -438,7 +437,7 @@ and uexp_to_info_map = | ((Prod(ty_fns1), Prod(ty_fns2)), Prod(ty_ps)) => let tys = List.map2(ana_ty_fn, List.combine(ty_fns1, ty_fns2), ty_ps); - Typ.Prod(tys) |> Typ.temp; + Prod(tys) |> Typ.temp; | ((_, _), _) => ana_ty_fn((def_base.ty, def_base2.ty), p_syn.ty) }; let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(ana), def, m); @@ -616,7 +615,7 @@ 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 = - Typ.Rec(TPat.Var(name) |> IdTagged.fresh, utyp) |> Typ.temp; + Rec((Var(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); @@ -697,7 +696,7 @@ and upat_to_info_map = let atomic = (self, constraint_) => add(~self, ~ctx, ~constraint_, m); let ancestors = [UPat.rep_id(upat)] @ ancestors; let go = upat_to_info_map(~is_synswitch, ~ancestors, ~co_ctx); - let unknown = Typ.Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp; + let unknown = Unknown(is_synswitch ? SynSwitch : Internal) |> Typ.temp; let ctx_fold = (ctx: Ctx.t, m) => List.fold_left2( ((ctx, tys, cons, m), e, mode) => diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 67e6f1ecde..02bd8400d4 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -3,7 +3,7 @@ open Util; let continue = x => x; let stop = (_, x) => x; [@deriving (show({with_path: false}), sexp, yojson)] -type deferral_position = +type deferral_position_t = | InAp | OutsideAp; @@ -61,7 +61,7 @@ and exp_term = | MultiHole(list(any_t)) | DynamicErrorHole(exp_t, InvalidOperationError.t) | FailedCast(exp_t, typ_t, typ_t) - | Deferral(deferral_position) + | Deferral(deferral_position_t) | Undefined | Bool(bool) | Int(int) @@ -165,6 +165,7 @@ and filter = { }; module rec Any: { + [@deriving (show({with_path: false}), sexp, yojson)] type t = any_t; let map_term: @@ -181,6 +182,7 @@ module rec Any: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type t = any_t; let map_term = @@ -232,9 +234,12 @@ module rec Any: { }; } and Exp: { + [@deriving (show({with_path: false}), sexp, yojson)] type term = exp_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = exp_t; - + [@deriving (show({with_path: false}), sexp, yojson)] + type deferral_position = deferral_position_t; let map_term: ( ~f_exp: (Exp.t => Exp.t, Exp.t) => Exp.t=?, @@ -249,8 +254,12 @@ and Exp: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type term = exp_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = exp_t; + [@deriving (show({with_path: false}), sexp, yojson)] + type deferral_position = deferral_position_t; let map_term = ( @@ -456,7 +465,9 @@ and Exp: { }; } and Pat: { + [@deriving (show({with_path: false}), sexp, yojson)] type term = pat_term; // The second Typ.t field is only meaningful in dynamic patterns + [@deriving (show({with_path: false}), sexp, yojson)] type t = pat_t; let map_term: @@ -473,7 +484,9 @@ and Pat: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type term = pat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = pat_t; let map_term = @@ -729,6 +742,7 @@ and Typ: { and TPat: { [@deriving (show({with_path: false}), sexp, yojson)] type term = tpat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = tpat_t; let map_term: @@ -749,6 +763,7 @@ and TPat: { } = { [@deriving (show({with_path: false}), sexp, yojson)] type term = tpat_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = tpat_t; let map_term = @@ -799,6 +814,7 @@ and TPat: { and Rul: { [@deriving (show({with_path: false}), sexp, yojson)] type term = rul_term; + [@deriving (show({with_path: false}), sexp, yojson)] type t = rul_t; let map_term: @@ -890,7 +906,7 @@ and Environment: { and ClosureEnvironment: { [@deriving (show({with_path: false}), sexp, yojson)] - type t; + type t = closure_environment_t; let wrap: (Id.t, Environment.t) => t; @@ -1001,6 +1017,7 @@ and ClosureEnvironment: { let without_keys = keys => update(Environment.without_keys(keys)); } and StepperFilterKind: { + [@deriving (show({with_path: false}), sexp, yojson)] type t = stepper_filter_kind_t; let map_term: @@ -1019,6 +1036,7 @@ and StepperFilterKind: { let fast_equal: (t, t) => bool; } = { + [@deriving (show({with_path: false}), sexp, yojson)] type t = stepper_filter_kind_t; let map = (mapper, filter: t): t => { diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index cd05476fd9..bdb3e014cc 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -8,7 +8,11 @@ module CachedStatics = { }; let empty: t = { - term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])}, + term: { + ids: [Id.invalid], + copied: false, + term: Tuple([]), + }, info_map: Id.Map.empty, error_ids: [], }; diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index ff59e48f55..23265f8a2a 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -1,50 +1,48 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => { - Exp.( - switch (e1.term) { - | EmptyHole - | Invalid(_) - | MultiHole(_) - | DynamicErrorHole(_) - | FailedCast(_) - | Undefined - | Deferral(_) - | Bool(_) - | Int(_) - | Float(_) - | String(_) - | ListLit(_) - | Constructor(_) - | Closure(_) - | Fun(_) - | TypFun(_) - | FixF(_) - | Tuple(_) - | Var(_) - | Ap(_) - | TypAp(_) - | DeferredAp(_) - | If(_) - | Test(_) - | Parens(_) - | Cons(_) - | ListConcat(_) - | UnOp(_) - | BinOp(_) - | BuiltinFun(_) - | Cast(_) - | Match(_) => Exp.{ids: [Id.mk()], copied: false, term: Seq(e1, e2)} - | Seq(e11, e12) => - let e12' = append_exp(e12, e2); - {ids: e1.ids, copied: false, term: Seq(e11, e12')}; - | Filter(kind, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: Filter(kind, ebody')}; - | Let(p, edef, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: Let(p, edef, ebody')}; - | TyAlias(tp, tdef, ebody) => - let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')}; - } - ); + switch (e1.term) { + | EmptyHole + | Invalid(_) + | MultiHole(_) + | DynamicErrorHole(_) + | FailedCast(_) + | Undefined + | Deferral(_) + | Bool(_) + | Int(_) + | Float(_) + | String(_) + | ListLit(_) + | Constructor(_) + | Closure(_) + | Fun(_) + | TypFun(_) + | FixF(_) + | Tuple(_) + | Var(_) + | Ap(_) + | TypAp(_) + | DeferredAp(_) + | If(_) + | Test(_) + | Parens(_) + | Cons(_) + | ListConcat(_) + | UnOp(_) + | BinOp(_) + | BuiltinFun(_) + | Cast(_) + | Match(_) => {ids: [Id.mk()], copied: false, term: Seq(e1, e2)} + | Seq(e11, e12) => + let e12' = append_exp(e12, e2); + {ids: e1.ids, copied: false, term: Seq(e11, e12')}; + | Filter(kind, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: Filter(kind, ebody')}; + | Let(p, edef, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: Let(p, edef, ebody')}; + | TyAlias(tp, tdef, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: TyAlias(tp, tdef, ebody')}; + }; }; diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index b5e7dfc76d..01050d5e7b 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -568,23 +568,22 @@ module F = (ExerciseEnv: ExerciseEnv) => { hidden_tests: 'a, }; - let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => - Exp.{ - term: - Exp.Filter( - Filter({ - act: FilterAction.(act, One), - pat: { - term: Constructor("$e", Unknown(Internal) |> Typ.temp), - copied: false, - ids: [Id.mk()], - }, - }), - term, - ), - copied: false, - ids: [Id.mk()], - }; + let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => { + term: + Filter( + Filter({ + act: FilterAction.(act, One), + pat: { + term: Constructor("$e", Unknown(Internal) |> Typ.temp), + copied: false, + ids: [Id.mk()], + }, + }), + term, + ), + copied: false, + ids: [Id.mk()], + }; let term_of = (editor: Editor.t): UExp.t => MakeTerm.from_zip_for_sem(editor.state.zipper).term; diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 65c01e1a6f..ba06d2a29e 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -409,7 +409,7 @@ let locked = statics.info_map, statics.term, ) - : DHExp.Bool(true) |> DHExp.fresh; + : Bool(true) |> DHExp.fresh; let elab: Elaborator.Elaboration.t = {d: elab}; let result: ModelResult.t = settings.core.dynamics diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index cbfdf4df9f..a74a5187d8 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -533,7 +533,7 @@ let get_doc = (term) : (list(Node.t), (list(Node.t), ColorSteps.t), list(Node.t)) => switch ((term: Exp.term)) { - | Exp.Invalid(_) => simple("Not a valid expression") + | Invalid(_) => simple("Not a valid expression") | DynamicErrorHole(_) | FailedCast(_) | Closure(_) @@ -1980,7 +1980,7 @@ let get_doc = doc, ); switch (tl.term) { - | Pat.Cons(hd2, tl2) => + | Cons(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); @@ -2201,7 +2201,7 @@ let get_doc = doc, ); switch (result.term) { - | Typ.Arrow(arg2, result2) => + | Arrow(arg2, result2) => if (ArrowTyp.arrow3_typ.id == get_specificity_level(ArrowTyp.arrow3)) { let arg2_id = List.nth(arg2.ids, 0); let result2_id = List.nth(result2.ids, 0); diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 622dcf766e..82dfd0a9e3 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -21,7 +21,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => div( ~attrs=[ clss(["typ-view", "atom", "unknown"]), - Attr.title(Typ.show_type_provenance(prov)), + Attr.title(TermBase.show_type_provenance(prov)), ], [text("?") /*, prov_view(prov)*/], ) @@ -98,7 +98,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => div( ~attrs=[ clss(["typ-view", "atom", "unknown"]), - Attr.title(Typ.show_type_provenance(Internal)), + Attr.title(TermBase.show_type_provenance(Internal)), ], [text("?") /*, prov_view(prov)*/], ) From 518a33970fdbed09f80c0786bfee9af2a636a3fd Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 3 Oct 2024 12:15:02 -0400 Subject: [PATCH 3/3] Fix module reference --- test/Test_Evaluator.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index fc159425b2..9e4ade6651 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -16,7 +16,7 @@ let type_of = f => { }; let int_evaluation = - Evaluator.evaluate(Builtins.env_init, {d: Exp.Int(8) |> Exp.fresh}); + Evaluator.evaluate(Builtins.env_init, {d: Int(8) |> Exp.fresh}); let evaluation_test = (msg, expected, unevaluated) => check(