From 2be1b1f08d0bffb6ef9741bf342db379cf45dfdd Mon Sep 17 00:00:00 2001 From: ZhiyaoZhong Date: Fri, 4 Oct 2024 09:32:08 -0400 Subject: [PATCH] merge sort --- src/haz3lcore/derivation/DrvElab.re | 71 ++- src/haz3lcore/derivation/DrvInfo.re | 190 +++----- src/haz3lcore/derivation/DrvTerm.re | 151 ++----- src/haz3lcore/dynamics/Transition.re | 92 +--- src/haz3lcore/lang/Form.re | 119 ++--- src/haz3lcore/lang/Sort.re | 25 +- src/haz3lcore/lang/term/Drv.re | 3 - src/haz3lcore/statics/MakeTerm.re | 189 +++----- src/haz3lcore/statics/Statics.re | 114 ++--- src/haz3lcore/statics/Term.re | 10 +- src/haz3lcore/statics/TermBase.re | 440 ++++--------------- src/haz3lcore/tiles/Segment.re | 6 +- src/haz3lcore/zipper/action/Select.re | 4 +- src/haz3lschool/ProofCore.re | 2 +- src/haz3lschool/ProofGrade.re | 4 +- src/haz3lweb/view/Code.re | 5 + src/haz3lweb/view/CursorInspector.re | 31 +- src/haz3lweb/view/exercise/NinjaKeysRules.re | 7 +- src/haz3lweb/view/exercise/ProofView.re | 8 +- 19 files changed, 408 insertions(+), 1063 deletions(-) diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re index 99328d527c..4fe10fae35 100644 --- a/src/haz3lcore/derivation/DrvElab.re +++ b/src/haz3lcore/derivation/DrvElab.re @@ -6,57 +6,45 @@ let to_list = d => | _ => [d] }; -let rec elaborate: Drv.t => t = - fun - | Jdmt(jdmt) => elab_jdmt(jdmt) - | Ctxt(ctxt) => elab_ctxt(ctxt) - | Prop(prop) => elab_prop(prop) - | Exp(exp) => elab_exp(exp) - | Pat(pat) => elab_pat(pat) - | Typ(typ) => elab_typ(typ) - | TPat(tpat) => elab_tpat(tpat) -and elab_jdmt: Drv.Jdmt.t => t = +let rec exp_term_of: Drv.Exp.t => Drv.Exp.term = + exp => + switch (exp.term) { + | Parens(p) => exp_term_of(p) + | p => p + } +and elab_jdmt: Drv.Exp.t => t = jdmt => { let term: term = - switch (jdmt.term) { + switch (exp_term_of(jdmt)) { | Hole(s) => Hole(TermBase.TypeHole.show(s)) | Val(e) => Val(elab_exp(e)) | Eval(e1, e2) => Eval(elab_exp(e1), elab_exp(e2)) | Entail(ctx, p) => Entail(elab_ctxt(ctx), elab_prop(p)) + | _ => Hole(Drv.Exp.show(jdmt)) }; {...jdmt, term}; } -and elab_ctxt: Drv.Ctxt.t => t = - ctxt => { - let rec prop_term_of: Drv.Prop.t => Drv.Prop.term = - pat => - switch (pat.term) { - | Parens(p) => prop_term_of(p) - | p => p - }; +and elab_ctxt: Drv.Exp.t => t = + ctx => { let term: term = - switch (ctxt.term) { + switch (exp_term_of(ctx)) { | Hole(s) => Hole(TermBase.TypeHole.show(s)) - | Ctxt(p) => - switch (prop_term_of(p)) { - | Tuple(ps) => - Ctx( - ps - |> List.map(elab_prop) - |> List.map(to_list) - |> List.concat - |> List.fold_left(cons_ctx, []), - ) - | _ => Ctx([elab_prop(p)]) - } + | Ctx(ps) => + Ctx( + ps + |> List.map(elab_prop) + |> List.map(to_list) + |> List.concat + |> List.fold_left(cons_ctx, []), + ) + | _ => Hole(Drv.Exp.show(ctx)) }; - {...ctxt, term}; + {...ctx, term}; } -and elab_prop: Drv.Prop.t => t = +and elab_prop: Drv.Exp.t => t = prop => { - let hole: term = Hole(Drv.Prop.show(prop)); let term: term = - switch (prop.term) { + switch (exp_term_of(prop)) { | Hole(s) => Hole(TermBase.TypeHole.show(s)) | HasType(e, t) => HasType(elab_exp(e), elab_typ(t)) | Syn(e, t) => Syn(elab_exp(e), elab_typ(t)) @@ -67,9 +55,7 @@ and elab_prop: Drv.Prop.t => t = | Impl(p1, p2) => Impl(elab_prop(p1), elab_prop(p2)) | Truth => Truth | Falsity => Falsity - | Tuple(_) => hole - | Abbr(_) => hole - | Parens(p) => IdTagged.term_of(elab_prop(p)) + | _ => Hole(Drv.Exp.show(prop)) }; {...prop, term}; } @@ -89,7 +75,7 @@ and elab_exp: Drv.Exp.t => t = }; let hole: term = Hole(Drv.Exp.show(exp)); let term: term = - switch (exp.term) { + switch (exp_term_of(exp)) { | Hole(s) => Hole(TermBase.TypeHole.show(s)) | NumLit(i) => NumLit(i) | Neg(e) => Neg(elab_exp(e)) @@ -135,7 +121,7 @@ and elab_exp: Drv.Exp.t => t = | Unroll => Unroll(e2) | _ => Ap(elab_exp(e1), e2) }; - | Pair(e1, e2) => Pair(elab_exp(e1), elab_exp(e2)) + | Tuple([e1, e2]) => Pair(elab_exp(e1), elab_exp(e2)) | Triv => Triv | PrjL(e) => PrjL(elab_exp(e)) | PrjR(e) => PrjR(elab_exp(e)) @@ -155,8 +141,7 @@ and elab_exp: Drv.Exp.t => t = }; | Roll => hole | Unroll => hole - | Abbr(_) => hole - | Parens(e) => IdTagged.term_of(elab_exp(e)) + | _ => hole }; {...exp, term}; } diff --git a/src/haz3lcore/derivation/DrvInfo.re b/src/haz3lcore/derivation/DrvInfo.re index 45fa90680b..fab42d8a3e 100644 --- a/src/haz3lcore/derivation/DrvInfo.re +++ b/src/haz3lcore/derivation/DrvInfo.re @@ -17,45 +17,18 @@ type status_common = | InHole(error_common); [@deriving (show({with_path: false}), sexp, yojson)] -type jdmt = { - term: Drv.Jdmt.t, - cls: Cls.t, - ancestors, - status: status_common, -}; - -[@deriving (show({with_path: false}), sexp, yojson)] -type ctxt = { - term: Drv.Ctxt.t, - cls: Cls.t, - ancestors, - status: status_common, -}; - -[@deriving (show({with_path: false}), sexp, yojson)] -type error_prop = - | BadToken(Token.t) - | MultiHole - | NotAllowTuple; - -[@deriving (show({with_path: false}), sexp, yojson)] -type status_prop = - | NotInHole(ok_common) - | InHole(error_prop); - -[@deriving (show({with_path: false}), sexp, yojson)] -type prop = { - term: Drv.Prop.t, - cls: Cls.t, - ancestors, - status: status_prop, -}; +type ty_merged = + | Jdmt + | Ctx + | Prop + | Exp + | Arrow; [@deriving (show({with_path: false}), sexp, yojson)] type error_exp = | BadToken(Token.t) | MultiHole - | NotAllowSingle; + | NoJoin(ty_merged); // expected [@deriving (show({with_path: false}), sexp, yojson)] type status_exp = @@ -68,6 +41,7 @@ type exp = { cls: Cls.t, ancestors, status: status_exp, + ty: ty_merged, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -118,9 +92,6 @@ type tpat = { [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Jdmt(jdmt) - | Ctxt(ctxt) - | Prop(prop) | Exp(exp) | Pat(pat) | Typ(typ) @@ -128,9 +99,6 @@ type t = [@deriving (show({with_path: false}), sexp, yojson)] type error = - | Jdmt(error_common) - | Ctxt(error_common) - | Prop(error_prop) | Exp(error_exp) | Pat(error_pat) | Typ(error_common) @@ -138,9 +106,9 @@ type error = let sort_of: t => Sort.DrvSort.t = fun - | Jdmt(_) => Jdmt - | Ctxt(_) => Ctxt - | Prop(_) => Prop + | Exp({ty: Jdmt, _}) => Jdmt + | Exp({ty: Ctx, _}) => Ctx + | Exp({ty: Prop, _}) => Prop | Exp(_) => Exp | Pat(_) => Pat | Typ(_) => Typ @@ -148,9 +116,6 @@ let sort_of: t => Sort.DrvSort.t = let cls_of: t => Cls.t = fun - | Jdmt(jdmt) => jdmt.cls - | Ctxt(ctxt) => ctxt.cls - | Prop(prop) => prop.cls | Exp(exp) => exp.cls | Pat(pat) => pat.cls | Typ(typ) => typ.cls @@ -158,9 +123,6 @@ let cls_of: t => Cls.t = let id_of: t => Id.t = fun - | Jdmt(jdmt) => Drv.Jdmt.rep_id(jdmt.term) - | Ctxt(ctxt) => Drv.Ctxt.rep_id(ctxt.term) - | Prop(prop) => Drv.Prop.rep_id(prop.term) | Exp(exp) => Drv.Exp.rep_id(exp.term) | Pat(pat) => Drv.Pat.rep_id(pat.term) | Typ(typ) => Drv.Typ.rep_id(typ.term) @@ -168,16 +130,10 @@ let id_of: t => Id.t = let error_of: t => option(error) = fun - | Jdmt({status: NotInHole(_), _}) - | Ctxt({status: NotInHole(_), _}) - | Prop({status: NotInHole(_), _}) | Exp({status: NotInHole(_), _}) | Pat({status: NotInHole(_), _}) | Typ({status: NotInHole(_), _}) | TPat({status: NotInHole(_), _}) => None - | Jdmt({status: InHole(err), _}) => Some(Jdmt(err)) - | Ctxt({status: InHole(err), _}) => Some(Ctxt(err)) - | Prop({status: InHole(err), _}) => Some(Prop(err)) | Exp({status: InHole(err), _}) => Some(Exp(err)) | Pat({status: InHole(err), _}) => Some(Pat(err)) | Typ({status: InHole(err), _}) => Some(Typ(err)) @@ -185,39 +141,61 @@ let error_of: t => option(error) = [@deriving (show({with_path: false}), sexp, yojson)] type status_drv = - | Jdmt(status_common) - | Ctxt(status_common) - | Prop(status_prop) | Exp(status_exp) | Pat(status_pat) | Typ(status_common) | TPat(status_common); -let status_jdmt = (jdmt: Drv.Jdmt.t): status_common => - switch (jdmt.term) { - | Hole(Invalid(token)) => InHole(BadToken(token)) - | Hole(MultiHole(_)) => InHole(MultiHole) - | _ => NotInHole() - }; - -let status_ctxt = (ctxt: Drv.Ctxt.t): status_common => - switch (ctxt.term) { - | Hole(Invalid(token)) => InHole(BadToken(token)) - | Hole(MultiHole(_)) => InHole(MultiHole) - | _ => NotInHole() - }; - -let status_prop = (prop: Drv.Prop.t): status_prop => - switch (prop.term) { - | Hole(Invalid(token)) => InHole(BadToken(token)) - | Hole(MultiHole(_)) => InHole(MultiHole) - | _ => NotInHole() +let types_of_exp = (exp: Drv.Exp.t): list(ty_merged) => + switch (exp.term) { + | Hole(_) + | Abbr(_) + | Parens(_) => [Jdmt, Ctx, Prop, Exp, Arrow] + | Var(_) => [Prop, Exp, Arrow] + | Tuple(es) when List.length(es) == 2 => [Exp] + | Tuple(_) => [] + | Val(_) + | Eval(_) + | Entail(_) => [Jdmt] + | Ctx(_) => [Ctx] + | HasType(_) + | Syn(_) + | Ana(_) + | And(_) + | Or(_) + | Impl(_) + | Truth + | Falsity => [Prop] + | NumLit(_) + | Neg(_) + | Plus(_) + | Minus(_) + | Times(_) + | Eq(_) + | Lt(_) + | Gt(_) + | True + | False + | If(_) + | Let(_) + | Fix(_) + | Fun(_) + | Ap(_) + | Triv + | PrjL(_) + | PrjR(_) + | Case(_) => [Exp, Arrow] + | InjL + | InjR + | Roll + | Unroll => [Arrow] }; -let status_exp = (exp: Drv.Exp.t): status_exp => +let status_exp = (exp: Drv.Exp.t, ty: ty_merged): status_exp => switch (exp.term) { | Hole(Invalid(token)) => InHole(BadToken(token)) | Hole(MultiHole(_)) => InHole(MultiHole) + | _ when !List.mem(ty, types_of_exp(exp)) => InHole(NoJoin(ty)) | _ => NotInHole() }; @@ -242,29 +220,12 @@ let status_tpat = (tpat: Drv.TPat.t): status_common => | _ => NotInHole() }; -let status_drv = (drv: Drv.t): status_drv => - switch (drv) { - | Jdmt(term) => Jdmt(status_jdmt(term)) - | Ctxt(term) => Ctxt(status_ctxt(term)) - | Prop(term) => Prop(status_prop(term)) - | Exp(term) => Exp(status_exp(term)) - | Pat(term) => Pat(status_pat(term)) - | Typ(term) => Typ(status_typ(term)) - | TPat(term) => TPat(status_tpat(term)) - }; - let is_error = (ci: t): bool => { switch (ci) { - | Jdmt({status: InHole(_), _}) - | Ctxt({status: InHole(_), _}) - | Prop({status: InHole(_), _}) | Exp({status: InHole(_), _}) | Pat({status: InHole(_), _}) | Typ({status: InHole(_), _}) | TPat({status: InHole(_), _}) => true - | Jdmt({status: NotInHole(_), _}) - | Ctxt({status: NotInHole(_), _}) - | Prop({status: NotInHole(_), _}) | Exp({status: NotInHole(_), _}) | Pat({status: NotInHole(_), _}) | Typ({status: NotInHole(_), _}) @@ -274,36 +235,15 @@ let is_error = (ci: t): bool => { let ancestors_of: t => ancestors = fun - | Jdmt({ancestors, _}) - | Ctxt({ancestors, _}) - | Prop({ancestors, _}) | Exp({ancestors, _}) | Pat({ancestors, _}) | Typ({ancestors, _}) | TPat({ancestors, _}) => ancestors; -let derived_jdmt = (jdmt: Drv.Jdmt.t, ~ancestors): jdmt => { - let cls = Cls.Drv(Jdmt(Drv.Jdmt.cls_of_term(jdmt.term))); - let status = status_jdmt(jdmt); - {term: jdmt, cls, status, ancestors}; -}; - -let derived_ctxt = (ctxt: Drv.Ctxt.t, ~ancestors): ctxt => { - let cls = Cls.Drv(Ctxt(Drv.Ctxt.cls_of_term(ctxt.term))); - let status = status_ctxt(ctxt); - {term: ctxt, cls, status, ancestors}; -}; - -let derived_prop = (prop: Drv.Prop.t, ~ancestors): prop => { - let cls = Cls.Drv(Prop(Drv.Prop.cls_of_term(prop.term))); - let status = status_prop(prop); - {term: prop, cls, status, ancestors}; -}; - -let derived_exp = (exp: Drv.Exp.t, ~ancestors): exp => { +let derived_exp = (exp: Drv.Exp.t, ~ancestors, ~ty): exp => { let cls = Cls.Drv(Exp(Drv.Exp.cls_of_term(exp.term))); - let status = status_exp(exp); - {term: exp, cls, status, ancestors}; + let status = status_exp(exp, ty); + {term: exp, cls, status, ancestors, ty}; }; let derived_pat = (pat: Drv.Pat.t, ~ancestors): pat => { @@ -323,15 +263,3 @@ let derived_tpat = (tpat: Drv.TPat.t, ~ancestors): tpat => { let status = status_tpat(tpat); {term: tpat, cls, status, ancestors}; }; - -let derived_drv = (drv: Drv.t, ~ancestors): t => { - switch (drv) { - | Jdmt(jdmt) => Jdmt(derived_jdmt(jdmt, ~ancestors)) - | Ctxt(ctxt) => Ctxt(derived_ctxt(ctxt, ~ancestors)) - | Prop(prop) => Prop(derived_prop(prop, ~ancestors)) - | Exp(exp) => Exp(derived_exp(exp, ~ancestors)) - | Pat(pat) => Pat(derived_pat(pat, ~ancestors)) - | Typ(typ) => Typ(derived_typ(typ, ~ancestors)) - | TPat(tpat) => TPat(derived_tpat(tpat, ~ancestors)) - }; -}; diff --git a/src/haz3lcore/derivation/DrvTerm.re b/src/haz3lcore/derivation/DrvTerm.re index 4a07ef32fa..7e691171ee 100644 --- a/src/haz3lcore/derivation/DrvTerm.re +++ b/src/haz3lcore/derivation/DrvTerm.re @@ -1,117 +1,23 @@ -module Jdmt = { +module ALFA_Exp = { [@deriving (show({with_path: false}), sexp, yojson)] type cls = | Hole + | Var + | Abbr + | Parens + | Tuple | Val | Eval - | Entail; - - include TermBase.Jdmt; - - let hole = (tms: list(TermBase.Any.t)): term => - Hole(List.is_empty(tms) ? EmptyHole : MultiHole(tms)); - - let rep_id = ({ids, _}: t) => { - assert(ids != []); - List.hd(ids); - }; - - let term_of: t => term = IdTagged.term_of; - - let unwrap: t => (term, term => t) = IdTagged.unwrap; - - let fresh: term => t = IdTagged.fresh; - - let cls_of_term: term => cls = - fun - | Hole(_) => Hole - | Val(_) => Val - | Eval(_) => Eval - | Entail(_) => Entail; -}; - -module Ctxt = { - [@deriving (show({with_path: false}), sexp, yojson)] - type cls = - | Hole - | Ctxt; - - include TermBase.Ctxt; - - let hole = (tms: list(TermBase.Any.t)): term => - Hole(List.is_empty(tms) ? EmptyHole : MultiHole(tms)); - - let rep_id = ({ids, _}: t) => { - assert(ids != []); - List.hd(ids); - }; - - let term_of: t => term = IdTagged.term_of; - - let unwrap: t => (term, term => t) = IdTagged.unwrap; - - let fresh: term => t = IdTagged.fresh; - - let cls_of_term: term => cls = - fun - | Hole(_) => Hole - | Ctxt(_) => Ctxt; -}; - -module Prop = { - [@deriving (show({with_path: false}), sexp, yojson)] - type cls = - | Hole + | Entail + | Ctx | HasType | Syn | Ana - | Var | And | Or | Impl | Truth | Falsity - | Tuple - | Abbr - | Parens; - - include TermBase.Prop; - - let hole = (tms: list(TermBase.Any.t)): term => - Hole(List.is_empty(tms) ? EmptyHole : MultiHole(tms)); - - let rep_id = ({ids, _}: t) => { - assert(ids != []); - List.hd(ids); - }; - - let term_of: t => term = IdTagged.term_of; - - let unwrap: t => (term, term => t) = IdTagged.unwrap; - - let fresh: term => t = IdTagged.fresh; - - let cls_of_term: term => cls = - fun - | Hole(_) => Hole - | HasType(_) => HasType - | Syn(_) => Syn - | Ana(_) => Ana - | Var(_) => Var - | And(_) => And - | Or(_) => Or - | Impl(_) => Impl - | Truth => Truth - | Falsity => Falsity - | Tuple(_) => Tuple - | Abbr(_) => Abbr - | Parens(_) => Parens; -}; - -module ALFA_Exp = { - [@deriving (show({with_path: false}), sexp, yojson)] - type cls = - | Hole | NumLit | Neg | Plus @@ -123,12 +29,10 @@ module ALFA_Exp = { | True | False | If - | Var | Let | Fix | Fun | Ap - | Pair | Triv | PrjL | PrjR @@ -136,9 +40,7 @@ module ALFA_Exp = { | InjR | Case | Roll - | Unroll - | Abbr - | Parens; + | Unroll; include TermBase.ALFA_Exp; @@ -159,6 +61,22 @@ module ALFA_Exp = { let cls_of_term: term => cls = fun | Hole(_) => Hole + | Var(_) => Var + | Abbr(_) => Abbr + | Parens(_) => Parens + | Val(_) => Val + | Eval(_) => Eval + | Entail(_) => Entail + | Ctx(_) => Ctx + | HasType(_) => HasType + | Syn(_) => Syn + | Ana(_) => Ana + | And(_) => And + | Or(_) => Or + | Impl(_) => Impl + | Truth => Truth + | Falsity => Falsity + | Tuple(_) => Tuple | NumLit(_) => NumLit | Neg(_) => Neg | Plus(_) => Plus @@ -170,12 +88,10 @@ module ALFA_Exp = { | True => True | False => False | If(_) => If - | Var(_) => Var | Let(_) => Let | Fix(_) => Fix | Fun(_) => Fun | Ap(_) => Ap - | Pair(_) => Pair | Triv => Triv | PrjL(_) => PrjL | PrjR(_) => PrjR @@ -183,9 +99,7 @@ module ALFA_Exp = { | InjR => InjR | Case(_) => Case | Roll => Roll - | Unroll => Unroll - | Abbr(_) => Abbr - | Parens(_) => Parens; + | Unroll => Unroll; }; module ALFA_Pat = { @@ -303,9 +217,6 @@ module ALFA_TPat = { module Drv = { [@deriving (show({with_path: false}), sexp, yojson)] type cls = - | Jdmt(Jdmt.cls) - | Ctxt(Ctxt.cls) - | Prop(Prop.cls) | Exp(ALFA_Exp.cls) | Pat(ALFA_Pat.cls) | Typ(ALFA_Typ.cls) @@ -315,9 +226,6 @@ module Drv = { let sort_of: t => Sort.DrvSort.t = fun - | Jdmt(_) => Jdmt - | Ctxt(_) => Ctxt - | Prop(_) => Prop | Exp(_) => Exp | Pat(_) => Pat | Typ(_) => Typ @@ -325,9 +233,6 @@ module Drv = { let rep_id: t => Id.t = fun - | Jdmt(jdmt) => Jdmt.rep_id(jdmt) - | Ctxt(ctxt) => Ctxt.rep_id(ctxt) - | Prop(prop) => Prop.rep_id(prop) | Exp(exp) => ALFA_Exp.rep_id(exp) | Pat(pat) => ALFA_Pat.rep_id(pat) | Typ(typ) => ALFA_Typ.rep_id(typ) @@ -335,9 +240,6 @@ module Drv = { let of_id: t => list(Id.t) = fun - | Jdmt(jdmt) => jdmt.ids - | Ctxt(ctxt) => ctxt.ids - | Prop(prop) => prop.ids | Exp(exp) => exp.ids | Pat(pat) => pat.ids | Typ(typ) => typ.ids @@ -345,9 +247,6 @@ module Drv = { let cls_of: t => cls = fun - | Jdmt(jdmt) => Jdmt(Jdmt.cls_of_term(jdmt.term)) - | Ctxt(ctxt) => Ctxt(Ctxt.cls_of_term(ctxt.term)) - | Prop(prop) => Prop(Prop.cls_of_term(prop.term)) | Exp(exp) => Exp(ALFA_Exp.cls_of_term(exp.term)) | Pat(pat) => Pat(ALFA_Pat.cls_of_term(pat.term)) | Typ(typ) => Typ(ALFA_Typ.cls_of_term(typ.term)) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 08aaa1aa59..33ddc46ed7 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -246,46 +246,18 @@ module Transition = (EV: EV_MODE) => { // }; let replace_drv_abbrs = (env, d: t): t => { - let rec go_jdmt = jdmt => { - let (term, rewrap) = Drv.Jdmt.unwrap(jdmt); - let term: Drv.Jdmt.term = - switch (term) { - | Hole(s) => Hole(s) - | Val(e) => Val(go_exp(e)) - | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2)) - | Entail(ctx, p) => Entail(go_ctxt(ctx), go_prop(p)) - }; - term |> rewrap; - } - and go_ctxt = ctxt => { - let (term, rewrap) = Drv.Ctxt.unwrap(ctxt); - let term: Drv.Ctxt.term = - switch (term) { - | Hole(s) => Hole(s) - | Ctxt(p) => Ctxt(go_prop(p)) - }; - term |> rewrap; - } - and go_prop = prop => { - let (term, rewrap) = Drv.Prop.unwrap(prop); - let term: Drv.Prop.term = + let rec go_exp = exp => { + let (term, rewrap) = Drv.Exp.unwrap(exp); + let term: Drv.Exp.term = switch (term) { | Hole(s) => Hole(s) - | HasType(e, t) => HasType(go_exp(e), t) - | Syn(e, t) => Syn(go_exp(e), t) - | Ana(e, t) => Ana(go_exp(e), t) | Var(x) => Var(x) - | And(p1, p2) => And(go_prop(p1), go_prop(p2)) - | Or(p1, p2) => Or(go_prop(p1), go_prop(p2)) - | Impl(p1, p2) => Impl(go_prop(p1), go_prop(p2)) - | Truth => Truth - | Falsity => Falsity - | Tuple(ps) => Tuple(List.map(go_prop, ps)) | Abbr(p) => + // TODO(zhiyao): Fix this let (let+) = (x, f) => switch (x) { | Ok(x) => f(x) - | Error(s) => (Hole(Invalid(s)): Drv.Prop.term) + | Error(s) => (Hole(Invalid(s)): Drv.Exp.term) }; let+ p = switch (IdTagged.term_of(p)) { @@ -299,19 +271,23 @@ module Transition = (EV: EV_MODE) => { }; let+ e = switch (DHExp.term_of(d)) { - | Term(Drv(Prop(e))) => Ok(e) - | _ => Error("Pat Not Prop type") + | Term(Drv(Exp(e))) => Ok(e) + | _ => Error("Pat Not ALFA_Exp type") }; e |> IdTagged.unwrap |> fst; - | Parens(p) => Parens(go_prop(p)) - }; - term |> rewrap; - } - and go_exp = exp => { - let (term, rewrap) = Drv.Exp.unwrap(exp); - let term: Drv.Exp.term = - switch (term) { - | Hole(s) => Hole(s) + | Parens(e) => Parens(go_exp(e)) + | Val(e) => Val(go_exp(e)) + | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2)) + | Entail(ctx, p) => Entail(go_exp(ctx), go_exp(p)) + | Ctx(es) => Ctx(List.map(go_exp, es)) + | HasType(e, t) => HasType(go_exp(e), t) + | Syn(e, t) => Syn(go_exp(e), t) + | Ana(e, t) => Ana(go_exp(e), t) + | And(p1, p2) => And(go_exp(p1), go_exp(p2)) + | Or(p1, p2) => Or(go_exp(p1), go_exp(p2)) + | Impl(p1, p2) => Impl(go_exp(p1), go_exp(p2)) + | Truth => Truth + | Falsity => Falsity | NumLit(n) => NumLit(n) | Neg(e) => Neg(go_exp(e)) | Plus(e1, e2) => Plus(go_exp(e1), go_exp(e2)) @@ -323,12 +299,11 @@ module Transition = (EV: EV_MODE) => { | True => True | False => False | If(e1, e2, e3) => If(go_exp(e1), go_exp(e2), go_exp(e3)) - | Var(x) => Var(x) | Let(x, e1, e2) => Let(x, go_exp(e1), go_exp(e2)) | Fix(x, e) => Fix(x, go_exp(e)) | Fun(x, e) => Fun(x, go_exp(e)) | Ap(e1, e2) => Ap(go_exp(e1), go_exp(e2)) - | Pair(e1, e2) => Pair(go_exp(e1), go_exp(e2)) + | Tuple(es) => Tuple(List.map(go_exp, es)) | Triv => Triv | PrjL(e) => PrjL(go_exp(e)) | PrjR(e) => PrjR(go_exp(e)) @@ -338,37 +313,12 @@ module Transition = (EV: EV_MODE) => { Case(go_exp(e1), x, go_exp(e2), y, go_exp(e3)) | Roll => Roll | Unroll => Unroll - | Abbr(p) => - let (let+) = (x, f) => - switch (x) { - | Ok(x) => f(x) - | Error(s) => (Hole(Invalid(s)): Drv.Exp.term) - }; - let+ p = - switch (IdTagged.term_of(p)) { - | Var(x) => Ok(x) - | _ => Error("Pat Not Var") - }; - let+ d = - switch (ClosureEnvironment.lookup(env, p)) { - | Some(d) => Ok(d) - | None => Error("Pat Not Found") - }; - let+ e = - switch (DHExp.term_of(d)) { - | Term(Drv(Exp(e))) => Ok(e) - | _ => Error("Pat Not ALFA_Exp type") - }; - e |> IdTagged.unwrap |> fst; - | Parens(e) => Parens(go_exp(e)) }; term |> rewrap; }; let (term, rewrap) = IdTagged.unwrap(d); let term: term = switch (term) { - | Term(Drv(Jdmt(jdmt))) => Term(Drv(Jdmt(go_jdmt(jdmt)))) - | Term(Drv(Prop(prop))) => Term(Drv(Prop(go_prop(prop)))) | Term(Drv(Exp(exp))) => Term(Drv(Exp(go_exp(exp)))) | _ => term }; diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 8622257523..fef39cdeeb 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -252,7 +252,7 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ "empty_list", ( is_empty_list, - [mk_op(Exp, []), mk_op(Pat, []), mk_op(Drv(Ctxt), [])], + [mk_op(Exp, []), mk_op(Pat, []), mk_op(Drv(Exp), [])], ), ), ( @@ -277,7 +277,6 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ ( is_typ_var, [ - mk_op(Drv(Prop), []), mk_op(Drv(Exp), []), mk_op(Drv(Pat), []), mk_op(Drv(Typ), []), @@ -367,7 +366,8 @@ let forms: list((string, t)) = [ ("pipeline", mk_infix("|>", Exp, P.eqs)), // in OCaml, pipeline precedence is in same class as '=', '<', etc. // DOUBLE DELIMITERS ("filter_hide", mk(ds, ["hide", "in"], mk_pre(P.let_, Exp, [Exp]))), - ("filter_eval", mk(ds, ["eval", "in"], mk_pre(P.let_, Exp, [Exp]))), + // TODO(zhiyao): change it back to "eval", "in" + ("filter_eval", mk(ds, ["eval", "to"], mk_pre(P.let_, Exp, [Exp]))), ("filter_pause", mk(ds, ["pause", "in"], mk_pre(P.let_, Exp, [Exp]))), ("filter_debug", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))), // TRIPLE DELIMITERS @@ -380,115 +380,52 @@ let forms: list((string, t)) = [ // Drv // ("of_alfa_typ", mk(ds, ["of_Typ", "end"], mk_op(Exp, [Drv(Typ)]))), ( + // TODO(zhiyao): fix this "of_alfa_exp", mk(ds, ["of_alfa_exp", "end"], mk_op(Exp, [Drv(Exp)])), ), // ("of_alfa_pat", mk(ds, ["of_Pat", "end"], mk_op(Exp, [Drv(Pat)]))), // ("of_alfa_tpat", mk(ds, ["of_TPat", "end"], mk_op(Exp, [Drv(TPat)]))), - ("of_prop", mk(ds, ["of_prop", "end"], mk_op(Exp, [Drv(Prop)]))), - ("of_ctxt", mk(ds, ["of_ctxt", "end"], mk_op(Exp, [Drv(Ctxt)]))), - // ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Jdmt)]))), + ("of_prop", mk(ds, ["of_prop", "end"], mk_op(Exp, [Drv(Exp)]))), + ("of_ctxt", mk(ds, ["of_ctxt", "end"], mk_op(Exp, [Drv(Exp)]))), + // ("of_jdmt", mk(ds, ["of_Jdmt", "end"], mk_op(Exp, [Drv(Exp)]))), // ( // "prop_alias", - // mk(ds, ["prop", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Prop)])), + // mk(ds, ["prop", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Exp)])), // ), // ( // "alfa_alias", // mk(ds, ["alfa", "=", "in"], mk_pre(P.let_, Exp, [Pat, Drv(Exp)])), // ), + // Drv(Jdmt) ("fake_val", mk(ds, ["val", "end"], mk_op(Exp, [Exp]))), - ("val", mk(ds, ["val", "end"], mk_op(Drv(Jdmt), [Drv(Exp)]))), - ("fake_eval", mk(ds, ["eval", "to", "end"], mk_op(Exp, [Exp, Exp]))), - ( - "eval", - mk( - ii, - ["eval", "to", "end"], - mk_op(Drv(Jdmt), [Drv(Exp), Drv(Exp)]), - ), - ), - // Note(zhiyao): there is no "fake_entail" because it will diable entail_hastype, entail_syn, and entail_ana - ( - "entail", - mk( - ds, - ["entail", "|-", "end"], - mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Prop)]), - ), - ), - ( - "fake_entail_hastype", - mk( - ds, - ["entail_hastype", "|-", ":", "end"], - mk_op(Exp, [Exp, Exp, Exp]), - ), - ), - ( - "entail_hastype", - mk( - ii, - ["entail_hastype", "|-", ":", "end"], - mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]), - ), - ), - ( - "fake_entail_syn", - mk(ds, ["entail_syn", "|-", "=>", "end"], mk_op(Exp, [Exp, Exp, Exp])), - ), - ( - "entail_syn", - mk( - ii, - ["entail_syn", "|-", "=>", "end"], - mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]), - ), - ), - ( - "fake_entail_ana", - mk(ds, ["entail_ana", "|-", "<=", "end"], mk_op(Exp, [Exp, Exp, Exp])), - ), - ( - "entail_ana", - mk( - ii, - ["entail_ana", "|-", "<=", "end"], - mk_op(Drv(Jdmt), [Drv(Ctxt), Drv(Exp), Drv(Typ)]), - ), - ), - // Drv(Ctxt) - ("list_lit_ctxt", mk(ii, ["[", "]"], mk_op(Drv(Ctxt), [Drv(Prop)]))), - // Drv(Prop) + ("val", mk(ds, ["val", "end"], mk_op(Drv(Exp), [Drv(Exp)]))), + ("val_simple", mk(ii, [".val"], mk_post(P.min, Drv(Exp), []))), + ("fake_eval", mk(ds, ["eval", "to"], mk_pre(P.min, Exp, [Exp]))), + ("eval", mk(ds, ["eval", "to"], mk_pre(P.min, Drv(Exp), [Drv(Exp)]))), + ("eval_simple", mk_infix("$>", Drv(Exp), P.min)), + ("entail", mk_infix("|-", Drv(Exp), P.min)), + // Drv(Ctx) + ("alfa_exp_list", mk(ii, ["[", "]"], mk_op(Drv(Exp), [Drv(Exp)]))), + ("alfa_cons", mk_infix(",", Drv(Exp), P.comma)), + ("alfa_paren", mk(ii, ["(", ")"], mk_op(Drv(Exp), [Drv(Exp)]))), + ("alfa_abbr", mk(ii, ["{", "}"], mk_op(Drv(Exp), [Pat]))), + // Drv(Exp) ( "hastype", - mk( - ds, - ["hastype", ":"], - mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)), - ), + mk(ss, [":"], mk_bin'(P.filter, Drv(Exp), Drv(Exp), [], Drv(Typ))), ), ( "syn", - mk( - ds, - ["syn", "=>"], - mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)), - ), + mk(ss, ["=>"], mk_bin'(P.filter, Drv(Exp), Drv(Exp), [], Drv(Typ))), ), ( "ana", - mk( - ds, - ["ana", "<="], - mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)), - ), + mk(ss, ["<="], mk_bin'(P.filter, Drv(Exp), Drv(Exp), [], Drv(Typ))), ), - ("and", mk_infix("/\\", Drv(Prop), P.and_)), - ("or", mk_infix("\\/", Drv(Prop), P.or_)), - ("impl", mk_infix("==>", Drv(Prop), P.ann)), - ("cons", mk_infix(",", Drv(Prop), P.comma)), - ("parens_prop", mk(ii, ["(", ")"], mk_op(Drv(Prop), [Drv(Prop)]))), - ("abbr_prop", mk(ii, ["{", "}"], mk_op(Drv(Prop), [Pat]))), + ("and", mk_infix("/\\", Drv(Exp), P.and_)), + ("or", mk_infix("\\/", Drv(Exp), P.or_)), + ("impl", mk_infix("==>", Drv(Exp), P.ann)), // Drv(Exp) ("exp_neg", mk(ds, ["-"], mk_pre(P.neg, Drv(Exp), []))), ("exp_plus", mk_infix("+", Drv(Exp), P.plus)), @@ -537,8 +474,6 @@ let forms: list((string, t)) = [ ), ), ), - ("exp_parens", mk(ii, ["(", ")"], mk_op(Drv(Exp), [Drv(Exp)]))), - ("abbr_exp", mk(ii, ["{", "}"], mk_op(Drv(Exp), [Pat]))), // Drv(Pat) ( "pat_cast", diff --git a/src/haz3lcore/lang/Sort.re b/src/haz3lcore/lang/Sort.re index 3aedde2c90..c9df823fc8 100644 --- a/src/haz3lcore/lang/Sort.re +++ b/src/haz3lcore/lang/Sort.re @@ -2,7 +2,7 @@ module DrvSort = { [@deriving (show({with_path: false}), sexp, yojson)] type t = | Jdmt - | Ctxt + | Ctx | Prop | Exp | Pat @@ -13,7 +13,7 @@ module DrvSort = { fun | Jdmt => "Jdmt" | Prop => "Prop" - | Ctxt => "Ctxt" + | Ctx => "Ctx" | Exp => "ALFA_Exp" | Pat => "ALFA_Pat" | Typ => "ALFA_Typ" @@ -22,19 +22,19 @@ module DrvSort = { let class_of = fun | Jdmt => "Drv" - | Ctxt => "Drv" - | Prop => "Drv" + | Ctx => "Drv" + | Prop => "Exp" | Exp => "Exp" | Pat => "Pat" | Typ => "Typ" | TPat => "TPat"; - let all = [Jdmt, Prop, Exp, Pat, Typ, TPat]; + let all = [Jdmt, Ctx, Prop, Exp, Pat, Typ, TPat]; let to_string = fun | Jdmt => "Jdmt" - | Ctxt => "Ctxt" + | Ctx => "Ctx" | Prop => "Prop" | Exp => "ALFA_Exp" | Pat => "ALFA_Pat" @@ -44,12 +44,23 @@ module DrvSort = { let to_string_verbose = fun | Jdmt => "judgement" - | Ctxt => "context" + | Ctx => "context" | Prop => "proposition" | Exp => "ALFA expression" | Pat => "ALFA pattern" | Typ => "ALFA type" | TPat => "ALFA type pattern"; + + let detail_sort: list(string) => t = + fun + | [".val"] => Jdmt + | ["val", "end"] => Jdmt + | ["eval", "to"] => Jdmt + | ["|-"] => Jdmt + | ["$>"] => Jdmt + | ["[]"] => Ctx + | ["[", _] => Ctx + | _ => Exp; }; [@deriving (show({with_path: false}), sexp, yojson)] diff --git a/src/haz3lcore/lang/term/Drv.re b/src/haz3lcore/lang/term/Drv.re index 9ba5c1f24e..94a406eed0 100644 --- a/src/haz3lcore/lang/term/Drv.re +++ b/src/haz3lcore/lang/term/Drv.re @@ -1,7 +1,4 @@ include Term.Drv; -module Jdmt = Term.Jdmt; -module Ctxt = Term.Ctxt; -module Prop = Term.Prop; module Exp = Term.ALFA_Exp; module Pat = Term.ALFA_Pat; module Typ = Term.ALFA_Typ; diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 111b071ee2..437703e512 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -53,7 +53,7 @@ let is_nary = let is_tuple_exp = is_nary(Any.is_exp, ","); let is_tuple_pat = is_nary(Any.is_pat, ","); let is_tuple_typ = is_nary(Any.is_typ, ","); -let is_tuple_prop = is_nary(Any.is_prop, ","); +let is_tuple_prop = is_nary(Any.is_alfa_exp, ","); let is_typ_bsum = is_nary(Any.is_typ, "+"); let is_grout = tiles => @@ -145,9 +145,9 @@ let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t => | Drv(drv) => Drv( switch (drv) { - | Jdmt => Jdmt(jdmt(unsorted(skel, seg))) - | Ctxt => Ctxt(ctxt(unsorted(skel, seg))) - | Prop => Prop(prop(unsorted(skel, seg))) + | Jdmt + | Ctx + | Prop => failwith("unexpected drv sort") | Exp => Exp(alfa_exp(unsorted(skel, seg))) | Pat => Pat(alfa_pat(unsorted(skel, seg))) | Typ => Typ(alfa_typ(unsorted(skel, seg))) @@ -177,137 +177,74 @@ let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t => } }; } - -and jdmt = unsorted => { - let (term, inner_ids) = jdmt_term(unsorted); +and alfa_exp = unsorted => { + let (term, inner_ids) = alfa_exp_term(unsorted); let ids = ids(unsorted) @ inner_ids; - return(e => Drv(Jdmt(e)), ids, {ids, copied: false, term}); + return(e => Drv(Exp(e)), ids, {ids, copied: false, term}); } -and jdmt_term: unsorted => (Drv.Jdmt.term, list(Id.t)) = { - let ret = (tm: Drv.Jdmt.term) => (tm, []); - let hole = unsorted => Drv.Jdmt.hole(kids_of_unsorted(unsorted)); +and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = { + let ret = (tm: Drv.Exp.term) => (tm, []); + let hole = unsorted => Drv.Exp.hole(kids_of_unsorted(unsorted)); fun | Op(([(_id, t)], [])) as tm => switch (t) { + | ([t], []) => + switch (t) { + | "Truth" => ret(Truth) + | "Falsity" => ret(Falsity) + | "True" => ret(True) + | "False" => ret(False) + | "L" => ret(InjL) + | "R" => ret(InjR) + | "roll" => ret(Roll) + | "unroll" => ret(Unroll) + | _ when Form.is_empty_list(t) => ret(Ctx([])) + | _ when Form.is_empty_tuple(t) => ret(Triv) + | _ when Form.is_int(t) => ret(NumLit(int_of_string(t))) + | _ when Form.is_typ_var(t) => ret(Var(t)) + | _ => ret(hole(tm)) + } | (["val", "end"], [Drv(Exp(e))]) => ret(Val(e)) - | (["eval", "to", "end"], [Drv(Exp(l)), Drv(Exp(r))]) => - ret(Eval(l, r)) - | (["entail", "|-", "end"], [Drv(Ctxt(l)), Drv(Prop(r))]) => - ret(Entail(l, r)) - | ( - ["entail_hastype", "|-", ":", "end"], - [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))], - ) => - ret(Entail(l, HasType(e, t) |> Drv.Prop.fresh)) - | ( - ["entail_syn", "|-", "=>", "end"], - [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))], - ) => - ret(Entail(l, Syn(e, t) |> Drv.Prop.fresh)) - | ( - ["entail_ana", "|-", "<=", "end"], - [Drv(Ctxt(l)), Drv(Exp(e)), Drv(Typ(t))], - ) => - ret(Entail(l, Ana(e, t) |> Drv.Prop.fresh)) - | _ => ret(hole(tm)) - } - // | Post(Drv(Exp(l)), ([(_id, ([".val"], []))], [])) => ret(Val(l)) - // | Bin(Drv(Exp(l)), ([(_id, (["$>"], []))], []), Drv(Exp(r))) => - // ret(Eval(l, r)) - // | Bin(Drv(Prop(l)), ([(_id, (["|-"], []))], []), Drv(Prop(r))) => - // ret(Entail(l, r)) - | _ as tm => ret(hole(tm)); -} - -and ctxt = unsorted => { - let (term, inner_ids) = ctxt_term(unsorted); - let ids = ids(unsorted) @ inner_ids; - return(p => Drv(Ctxt(p)), ids, {ids, copied: false, term}); -} - -and ctxt_term: unsorted => (Drv.Ctxt.term, list(Id.t)) = { - let ret = (tm: Drv.Ctxt.term) => (tm, []); - let hole = unsorted => Drv.Ctxt.hole(kids_of_unsorted(unsorted)); - fun - | Op(([(_id, t)], [])) as tm => - switch (t) { - | ([t], []) when Form.is_empty_list(t) => - ret(Ctxt(Drv.Prop.fresh(Tuple([])))) - | (["[", "]"], [Drv(Prop(body))]) => ret(Ctxt(body)) - | _ => ret(hole(tm)) - } - | _ as tm => ret(hole(tm)); -} - -and prop = unsorted => { - let (term, inner_ids) = prop_term(unsorted); - let ids = ids(unsorted) @ inner_ids; - return(p => Drv(Prop(p)), ids, {ids, copied: false, term}); -} -and prop_term: unsorted => (Drv.Prop.term, list(Id.t)) = { - let ret = (tm: Drv.Prop.term) => (tm, []); - let hole = unsorted => Drv.Prop.hole(kids_of_unsorted(unsorted)); - fun - | Op(([(_id, ([t], []))], [])) as tm => - switch (t) { - | "Truth" => ret(Truth) - | "Falsity" => ret(Falsity) - | _ when Form.is_typ_var(t) => ret(Var(t)) - | _ => ret(hole(tm)) - } - | Op(([(_id, (["(", ")"], [Drv(Prop(body))]))], [])) => - ret(Parens(body)) - | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var)) - | Pre(([(_id, ([t1, t2], [Drv(Exp(l))]))], []), Drv(Typ(r))) as tm => - switch (t1, t2) { - | ("hastype", ":") => ret(HasType(l, r)) - | ("syn", "=>") => ret(Syn(l, r)) - | ("ana", "<=") => ret(Ana(l, r)) + | (["[", "]"], [Drv(Exp(body))]) => + switch (body) { + | {ids, copied: false, term: Tuple(es)} => (Ctx(es), ids) + | term => ret(Ctx([term])) + } + | (["(", ")"], [Drv(Exp(body))]) => ret(Parens(body)) + | (["{", "}"], [Pat(var)]) => ret(Abbr(var)) | _ => ret(hole(tm)) } - | Bin(Drv(Prop(l)), ([(_id, ([t], []))], []), Drv(Prop(r))) as tm => + | Bin(Drv(Exp(l)), ([(_id, ([t], []))], []), Drv(Exp(r))) as tm => switch (t) { + | "$>" => ret(Eval(l, r)) + | "|-" => ret(Entail(l, r)) | "/\\" => ret(And(l, r)) | "\\/" => ret(Or(l, r)) | "==>" => ret(Impl(l, r)) + | "+" => ret(Plus(l, r)) + | "-" => ret(Minus(l, r)) + | "*" => ret(Times(l, r)) + | "==" => ret(Eq(l, r)) + | "<" => ret(Lt(l, r)) + | ">" => ret(Gt(l, r)) | "," => ret(Tuple([l, r])) | _ => ret(hole(tm)) } - | Bin(Drv(Prop(l)), tiles, Drv(Prop(r))) as tm => + | Bin(Drv(Exp(l)), tiles, Drv(Exp(r))) as tm => switch (is_tuple_prop(tiles)) { | Some(between_kids) => ret(Tuple([l] @ between_kids @ [r])) | None => ret(hole(tm)) } - | _ as tm => ret(hole(tm)); -} - -and alfa_exp = unsorted => { - let (term, inner_ids) = alfa_exp_term(unsorted); - let ids = ids(unsorted) @ inner_ids; - return(e => Drv(Exp(e)), ids, {ids, copied: false, term}); -} -and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = { - let ret = (tm: Drv.Exp.term) => (tm, []); - let hole = unsorted => Drv.Exp.hole(kids_of_unsorted(unsorted)); - fun - | Op(([(_id, ([t], []))], [])) as tm => + | Bin(Drv(Exp(l)), ([(_id, ([t], []))], []), Drv(Typ(r))) as tm => switch (t) { - | _ when Form.is_empty_tuple(t) => ret(Triv) - | _ when Form.is_int(t) => ret(NumLit(int_of_string(t))) - | "True" => ret(True) - | "False" => ret(False) - | "L" => ret(InjL) - | "R" => ret(InjR) - | "roll" => ret(Roll) - | "unroll" => ret(Unroll) - | _ when Form.is_typ_var(t) => ret(Var(t)) + | ":" => ret(HasType(l, r)) + | "=>" => ret(Syn(l, r)) + | "<=" => ret(Ana(l, r)) | _ => ret(hole(tm)) } - | Op(([(_id, (["(", ")"], [Drv(Exp(body))]))], [])) => - ret(Parens(body)) - | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var)) | Pre(([(_id, t)], []), Drv(Exp(r))) as tm => switch (t) { + | (["eval", "to"], [Drv(Exp(l))]) => ret(Eval(l, r)) | (["-"], []) => ret(Neg(r)) | (["if", "then", "else"], [Drv(Exp(cond)), Drv(Exp(conseq))]) => ret(If(cond, conseq, r)) @@ -324,22 +261,12 @@ and alfa_exp_term: unsorted => (Drv.Exp.term, list(Id.t)) = { } | Post(Drv(Exp(l)), ([(_id, t)], [])) as tm => switch (t) { + | ([".val"], []) => ret(Val(l)) | ([".fst"], []) => ret(PrjL(l)) | ([".snd"], []) => ret(PrjR(l)) | (["(", ")"], [Drv(Exp(r))]) => ret(Ap(l, r)) | _ => ret(hole(tm)) } - | Bin(Drv(Exp(l)), ([(_id, ([t], []))], []), Drv(Exp(r))) as tm => - switch (t) { - | "+" => ret(Plus(l, r)) - | "-" => ret(Minus(l, r)) - | "*" => ret(Times(l, r)) - | "==" => ret(Eq(l, r)) - | "<" => ret(Lt(l, r)) - | ">" => ret(Gt(l, r)) - | "," => ret(Pair(l, r)) - | _ => ret(hole(tm)) - } | _ as tm => ret(hole(tm)); } @@ -419,10 +346,10 @@ and exp = unsorted => { let (term, inner_ids) = exp_term(unsorted); switch (term) { | MultiHole([Drv(_), ..._]) => - let (term, inner_ids) = jdmt_term(unsorted); + let (term, inner_ids) = alfa_exp_term(unsorted); let ids = ids(unsorted) @ inner_ids; - let jdmt = return(e => Drv(Jdmt(e)), ids, {ids, copied: false, term}); - TermBase.Exp.Term(Drv(Jdmt(jdmt))) |> IdTagged.fresh; + let exp = return(e => Drv(Exp(e)), ids, {ids, copied: false, term}); + TermBase.Exp.Term(Drv(Exp(exp))) |> IdTagged.fresh; | _ => let ids = ids(unsorted) @ inner_ids; return(e => Exp(e), ids, {ids, copied: false, term}); @@ -466,10 +393,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { // | (["of_pat", "end"], [Drv(Pat(p))]) => ret(Term(Drv(Pat(p)))) // | (["of_tpat", "end"], [Drv(TPat(tp))]) => // ret(Term(Drv(TPat(tp)))) - | (["of_ctxt", "end"], [Drv(Ctxt(ctx))]) => - ret(Term(Drv(Ctxt(ctx)))) - | (["of_prop", "end"], [Drv(Prop(p))]) => ret(Term(Drv(Prop(p)))) - // | (["of_jdmt", "end"], [Drv(Jdmt(j))]) => ret(Term(Drv(Jdmt(j)))) + | (["of_ctxt", "end"], [Drv(Exp(ctx))]) => + ret(Term(Drv(Exp(ctx)))) + | (["of_prop", "end"], [Drv(Exp(p))]) => ret(Term(Drv(Exp(p)))) + // | (["of_jdmt", "end"], [Drv(Exp(j))]) => ret(Term(Drv(Exp(j)))) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => ret(Invalid(t)) | _ => ret(hole(tm)) @@ -498,8 +425,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { Filter(Filter({act: (Step, All), pat: filter}), r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => TyAlias(tpat, def, r) - | (["prop", "=", "in"], [Pat(pat), Drv(Prop(def))]) => - Let(pat, UExp.Term(Drv(Prop(def))) |> UExp.fresh, r) + | (["prop", "=", "in"], [Pat(pat), Drv(Exp(def))]) => + Let(pat, UExp.Term(Drv(Exp(def))) |> UExp.fresh, r) | (["alfa", "=", "in"], [Pat(pat), Drv(Exp(def))]) => Let(pat, UExp.Term(Drv(Exp(def))) |> UExp.fresh, r) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 7da1b5701f..0916159003 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -176,76 +176,43 @@ and drv_to_info_map = info, add_info(Drv.of_id(drv), InfoDrv(info), m), ); - let rec go_jdmt = (jdmt, m) => { - let info: DrvInfo.t = Jdmt(DrvInfo.derived_jdmt(jdmt, ~ancestors)); - let m = - switch (jdmt.term) { - | Hole(_) => m - | Val(e) => m |> go_exp'(e) |> snd - | Eval(e1, e2) => m |> go_exp'(e1) |> snd |> go_exp'(e2) |> snd - | Entail(ctx, p) => - m |> go_ctxt(ctx) |> snd |> go_prop(p, ~can_tuple=false) |> snd - }; - add(Jdmt(jdmt), info, m); - } - and go_ctxt = (ctxt: Drv.Ctxt.t, m) => { - let info = DrvInfo.derived_ctxt(ctxt, ~ancestors); - let add' = add(Ctxt(ctxt), Ctxt(info)); - switch (ctxt.term) { - | Hole(_) => m |> add' - | Ctxt(p) => m |> go_prop(p, ~can_tuple=true) |> snd |> add' - }; - } - and go_prop = (prop: Drv.Prop.t, m, ~can_tuple: bool) => { - let info = DrvInfo.derived_prop(prop, ~ancestors); - let add' = add(Prop(prop), Prop(info)); - // let m = - switch (prop.term) { + let rec go_exp = (exp: Drv.Exp.t, m, ~ty: DrvInfo.ty_merged) => { + let info = DrvInfo.derived_exp(exp, ~ancestors, ~ty); + let info': DrvInfo.t = Exp(info); + let add = add(Exp(exp)); + let add' = add(info'); + switch (exp.term) { | Hole(_) => m |> add' - | HasType(e, t) - | Syn(e, t) - | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd |> add' | Var(_) => m |> add' - | And(p1, p2) - | Or(p1, p2) - | Impl(p1, p2) => - m - |> go_prop(p1, ~can_tuple=false) - |> snd - |> go_prop(p2, ~can_tuple=false) - |> snd - |> add' - - | Truth - | Falsity => m |> add' - | Tuple(_) when !can_tuple => - m |> add(Prop(prop), Prop({...info, status: InHole(NotAllowTuple)})) - | Tuple(ps) => - List.fold_left((m, p) => m |> go_prop(p, ~can_tuple) |> snd, m, ps) - |> add' | Abbr(p) => - m + m // TODO(zhiyao): change abbr |> upat_to_info_map( ~is_synswitch=false, ~co_ctx=CoCtx.empty, ~ctx, ~ancestors, - ~mode=Mode.Ana(Term(Drv(Prop)) |> Typ.fresh), + ~mode=Mode.Ana(Term(Drv(Exp)) |> Typ.fresh), p, ) |> snd |> add' - | Parens(p) => m |> go_prop(p, ~can_tuple) |> snd |> add' - }; - // add(Prop(prop), info, m); - } - and go_exp = (exp: Drv.Exp.t, m, ~left_ap: bool) => { - let info = DrvInfo.derived_exp(exp, ~ancestors); - let info': DrvInfo.t = Exp(info); - let add = add(Exp(exp)); - let add' = add(info'); - switch (exp.term) { - | Hole(_) => m |> add' + | Parens(e) => m |> go_exp(e, ~ty) |> snd |> add' + | Val(e) => m |> go_exp'(e) |> snd |> add' + | Eval(e1, e2) => m |> go_exp'(e1) |> snd |> go_exp'(e2) |> snd |> add' + | Entail(ctx, p) => + m |> go_exp(ctx, ~ty=Ctx) |> snd |> go_exp(p, ~ty=Prop) |> snd |> add' + | Ctx(es) => + List.fold_left((m, e) => m |> go_exp(e, ~ty=Prop) |> snd, m, es) + |> add' + | HasType(e, t) + | Syn(e, t) + | Ana(e, t) => m |> go_exp'(e) |> snd |> go_typ(t) |> snd |> add' + | And(p1, p2) + | Or(p1, p2) + | Impl(p1, p2) => + m |> go_exp(p1, ~ty=Prop) |> snd |> go_exp(p2, ~ty=Prop) |> snd |> add' + | Truth + | Falsity => m |> add' | NumLit(_) => m |> add' | Neg(e) => m |> go_exp'(e) |> snd |> add' | Plus(e1, e2) @@ -262,7 +229,6 @@ and drv_to_info_map = let m = m |> go_exp'(e1) |> snd; let m = m |> go_exp'(e2) |> snd; m |> go_exp'(e3) |> snd |> add'; - | Var(_) => m |> add' | Let(p, e1, e2) => let m = m |> go_pat(p, ~expect=Pair_Or_Case_Var) |> snd; let m = m |> go_exp'(e1) |> snd; @@ -272,19 +238,15 @@ and drv_to_info_map = | Fun(p, e) => m |> go_pat(p, ~expect=Cast_Var) |> snd |> go_exp'(e) |> snd |> add' | Ap(e1, e2) => - m |> go_exp(e1, ~left_ap=true) |> snd |> go_exp'(e2) |> snd |> add' - | Pair(e1, e2) => m |> go_exp'(e1) |> snd |> go_exp'(e2) |> snd |> add' + m |> go_exp(e1, ~ty=Arrow) |> snd |> go_exp'(e2) |> snd |> add' + | Tuple(es) => + List.fold_left((m, e) => m |> go_exp'(e) |> snd, m, es) |> add' | Triv => m |> add' | PrjL(e) | PrjR(e) => m |> go_exp'(e) |> snd |> add' | InjL | InjR | Roll - | Unroll when !left_ap => - m |> add(Exp({...info, status: InHole(NotAllowSingle)})) - | InjL - | InjR - | Roll | Unroll => m |> add' | Case(e, p1, e1, p2, e2) => let m = m |> go_exp'(e) |> snd; @@ -292,22 +254,9 @@ and drv_to_info_map = let m = m |> go_exp'(e1) |> snd; let m = m |> go_pat(p2, ~expect=Ap_InjR) |> snd; m |> go_exp'(e2) |> snd |> add'; - | Abbr(p) => - m - |> upat_to_info_map( - ~is_synswitch=false, - ~co_ctx=CoCtx.empty, - ~ctx, - ~ancestors, - ~mode=Mode.Ana(Term(Drv(Exp)) |> Typ.fresh), - p, - ) - |> snd - |> add' - | Parens(e) => m |> go_exp(e, ~left_ap) |> snd |> add' }; } - and go_exp' = go_exp(~left_ap=false) + and go_exp' = go_exp(~ty=Exp) and go_pat = (pat: Drv.Pat.t, m, ~expect: DrvInfo.pat_expect) => { let info = DrvInfo.derived_pat(pat, ~ancestors); let add = add(Pat(pat)); @@ -359,10 +308,7 @@ and drv_to_info_map = add(TPat(tpat), info, m); }; switch (drv) { - | Jdmt(jdmt) => go_jdmt(jdmt, m) - | Ctxt(ctxt) => go_ctxt(ctxt, m) - | Prop(prop) => go_prop(prop, m, ~can_tuple=true) - | Exp(exp) => go_exp(exp, m, ~left_ap=false) + | Exp(exp) => go_exp(exp, m, ~ty=Jdmt) | Pat(pat) => go_pat(pat, m, ~expect=Var) | Typ(ty) => go_typ(ty, m) | TPat(tp) => go_tpat(tp, m) diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index c06fd683af..ea0a3840be 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -606,9 +606,9 @@ module Any = { fun | Typ(t) => Some(t) | _ => None; - let is_prop: t => option(TermBase.Prop.t) = + let is_alfa_exp: t => option(TermBase.ALFA_Exp.t) = fun - | Drv(Prop(p)) => Some(p) + | Drv(Exp(e)) => Some(e) | _ => None; let sort_of: t => Sort.t = @@ -624,9 +624,6 @@ module Any = { let rec ids = fun - | Drv(Jdmt(tm)) => tm.ids - | Drv(Ctxt(tm)) => tm.ids - | Drv(Prop(tm)) => tm.ids | Drv(Exp(tm)) => tm.ids | Drv(Pat(tm)) => tm.ids | Drv(Typ(tm)) => tm.ids @@ -652,9 +649,6 @@ module Any = { // (This would change for n-tuples if we decided parentheses are necessary.) let rep_id = fun - | Drv(Jdmt(tm)) => Jdmt.rep_id(tm) - | Drv(Ctxt(tm)) => Ctxt.rep_id(tm) - | Drv(Prop(tm)) => Prop.rep_id(tm) | Drv(Exp(tm)) => ALFA_Exp.rep_id(tm) | Drv(Pat(tm)) => ALFA_Pat.rep_id(tm) | Drv(Typ(tm)) => ALFA_Typ.rep_id(tm) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 05df8988fb..1a1280f115 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -1246,18 +1246,12 @@ and StepperFilterKind: { and Drv: { [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Jdmt(Jdmt.t) - | Ctxt(Ctxt.t) - | Prop(Prop.t) | Exp(ALFA_Exp.t) | Pat(ALFA_Pat.t) | Typ(ALFA_Typ.t) | TPat(ALFA_TPat.t); type mapper = { - f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t, - f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.t, - f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t, f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t, f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t, f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t, @@ -1272,18 +1266,12 @@ and Drv: { } = { [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Jdmt(Jdmt.t) - | Ctxt(Ctxt.t) - | Prop(Prop.t) | Exp(ALFA_Exp.t) | Pat(ALFA_Pat.t) | Typ(ALFA_Typ.t) | TPat(ALFA_TPat.t); type mapper = { - f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t, - f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.t, - f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t, f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t, f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t, f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t, @@ -1291,9 +1279,6 @@ and Drv: { }; let drv_continue = { - f_jdmt: continue, - f_ctxt: continue, - f_prop: continue, f_exp: continue, f_pat: continue, f_typ: continue, @@ -1301,47 +1286,8 @@ and Drv: { }; let map_term = (~f_hazel_pat=continue, ~f_drv=drv_continue, x: t) => { - let {f_jdmt, f_ctxt, f_prop, f_exp, f_pat, f_typ, f_tpat} = f_drv; + let {f_exp, f_pat, f_typ, f_tpat} = f_drv; switch (x) { - | Jdmt(jdmt) => - Jdmt( - Jdmt.map_term( - ~f_hazel_pat, - ~f_jdmt, - ~f_ctxt, - ~f_prop, - ~f_exp, - ~f_pat, - ~f_typ, - ~f_tpat, - jdmt, - ), - ) - | Ctxt(ctxt) => - Ctxt( - Ctxt.map_term( - ~f_hazel_pat, - ~f_ctxt, - ~f_prop, - ~f_exp, - ~f_pat, - ~f_typ, - ~f_tpat, - ctxt, - ), - ) - | Prop(prop) => - Prop( - Prop.map_term( - ~f_hazel_pat, - ~f_prop, - ~f_exp, - ~f_pat, - ~f_typ, - ~f_tpat, - prop, - ), - ) | Exp(exp) => Exp( ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat, exp), @@ -1354,12 +1300,6 @@ and Drv: { let fast_equal = (x, y) => switch (x, y) { - | (Jdmt(j1), Jdmt(j2)) => Jdmt.fast_equal(j1, j2) - | (Jdmt(_), _) => false - | (Ctxt(c1), Ctxt(c2)) => Ctxt.fast_equal(c1, c2) - | (Ctxt(_), _) => false - | (Prop(p1), Prop(p2)) => Prop.fast_equal(p1, p2) - | (Prop(_), _) => false | (Exp(e1), Exp(e2)) => ALFA_Exp.fast_equal(e1, e2) | (Exp(_), _) => false | (Pat(p1), Pat(p2)) => ALFA_Pat.fast_equal(p1, p2) @@ -1370,275 +1310,30 @@ and Drv: { | (TPat(_), _) => false }; } -and Jdmt: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) - | Val(ALFA_Exp.t) - | Eval(ALFA_Exp.t, ALFA_Exp.t) - | Entail(Ctxt.t, Prop.t) - and t = IdTagged.t(term); - - let map_term: - ( - ~f_hazel_pat: Pat.t => Pat.t=?, - ~f_jdmt: (Jdmt.t => Jdmt.t, Jdmt.t) => Jdmt.t=?, - ~f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.t=?, - ~f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t=?, - ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?, - ~f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t=?, - ~f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t=?, - ~f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t=?, - t - ) => - t; - - let fast_equal: (t, t) => bool; -} = { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) - | Val(ALFA_Exp.t) - | Eval(ALFA_Exp.t, ALFA_Exp.t) - | Entail(Ctxt.t, Prop.t) - and t = IdTagged.t(term); - - let map_term = - ( - ~f_hazel_pat=continue, - ~f_jdmt=continue, - ~f_ctxt=continue, - ~f_prop=continue, - ~f_exp=continue, - ~f_pat=continue, - ~f_typ=continue, - ~f_tpat=continue, - x, - ) => { - let ctxt_map_term = - Ctxt.map_term( - ~f_hazel_pat, - ~f_ctxt, - ~f_prop, - ~f_exp, - ~f_pat, - ~f_typ, - ~f_tpat, - ); - let prop_map_term = - Prop.map_term(~f_hazel_pat, ~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat); - let exp_map_term = - ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat); - let rec_call = ({term, _} as exp: t) => { - ...exp, - term: - switch (term) { - | Hole(_) => term - | Val(e) => Val(exp_map_term(e)) - | Eval(e1, e2) => Eval(exp_map_term(e1), exp_map_term(e2)) - | Entail(ctx, p) => Entail(ctxt_map_term(ctx), prop_map_term(p)) - }, - }; - x |> f_jdmt(rec_call); - }; - - let fast_equal = (x, y) => - switch (x |> IdTagged.term_of, y |> IdTagged.term_of) { - | (Hole(_), _) => false - | (Val(p1), Val(p2)) => ALFA_Exp.fast_equal(p1, p2) - | (Val(_), _) => false - | (Eval(p1, p2), Eval(p1', p2')) => - ALFA_Exp.fast_equal(p1, p1') && ALFA_Exp.fast_equal(p2, p2') - | (Eval(_, _), _) => false - | (Entail(p1, p2), Entail(p1', p2')) => - Ctxt.fast_equal(p1, p1') && Prop.fast_equal(p2, p2') - | (Entail(_, _), _) => false - }; -} -and Ctxt: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) - | Ctxt(Prop.t) - and t = IdTagged.t(term); - - let map_term: - ( - ~f_hazel_pat: Pat.t => Pat.t=?, - ~f_ctxt: (Ctxt.t => Ctxt.t, Ctxt.t) => Ctxt.t=?, - ~f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t=?, - ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?, - ~f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t=?, - ~f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t=?, - ~f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t=?, - t - ) => - t; - - let fast_equal: (t, t) => bool; -} = { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) - | Ctxt(Prop.t) - and t = IdTagged.t(term); - - let map_term = - ( - ~f_hazel_pat=continue, - ~f_ctxt=continue, - ~f_prop=continue, - ~f_exp=continue, - ~f_pat=continue, - ~f_typ=continue, - ~f_tpat=continue, - x, - ) => { - let prop_map_term = - Prop.map_term(~f_hazel_pat, ~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat); - let rec_call = ({term, _} as exp: t) => { - ...exp, - term: - switch (term) { - | Hole(_) => term - | Ctxt(x) => Ctxt(prop_map_term(x)) - }, - }; - x |> f_ctxt(rec_call); - }; - - let fast_equal = (x, y) => { - switch (x |> IdTagged.term_of, y |> IdTagged.term_of) { - | (Ctxt(x), Ctxt(y)) => Prop.fast_equal(x, y) - | _ => false - }; - }; -} -and Prop: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) - | HasType(ALFA_Exp.t, ALFA_Typ.t) - | Syn(ALFA_Exp.t, ALFA_Typ.t) - | Ana(ALFA_Exp.t, ALFA_Typ.t) - | Var(Var.t) - | And(t, t) - | Or(t, t) - | Impl(t, t) - | Truth - | Falsity - | Tuple(list(t)) - | Abbr(Pat.t) - | Parens(t) - and t = IdTagged.t(term); - - let map_term: - ( - ~f_hazel_pat: Pat.t => Pat.t=?, - ~f_prop: (Prop.t => Prop.t, Prop.t) => Prop.t=?, - ~f_exp: (ALFA_Exp.t => ALFA_Exp.t, ALFA_Exp.t) => ALFA_Exp.t=?, - ~f_pat: (ALFA_Pat.t => ALFA_Pat.t, ALFA_Pat.t) => ALFA_Pat.t=?, - ~f_typ: (ALFA_Typ.t => ALFA_Typ.t, ALFA_Typ.t) => ALFA_Typ.t=?, - ~f_tpat: (ALFA_TPat.t => ALFA_TPat.t, ALFA_TPat.t) => ALFA_TPat.t=?, - t - ) => - t; - - let fast_equal: (t, t) => bool; -} = { +and ALFA_Exp: { [@deriving (show({with_path: false}), sexp, yojson)] type term = | Hole(TypeHole.t) - | HasType(ALFA_Exp.t, ALFA_Typ.t) - | Syn(ALFA_Exp.t, ALFA_Typ.t) - | Ana(ALFA_Exp.t, ALFA_Typ.t) - | Var(Var.t) + | Var(Var.t) // Prop / Exp + | Abbr(Pat.t) // Jdmt / Ctxt / Prop / Exp + | Parens(t) // Jdmt / Ctxt / Prop / Exp + | Tuple(list(t)) // [invalid] / Exp + // Jdmt + | Val(t) + | Eval(t, t) + | Entail(t, t) + // Ctx + | Ctx(list(t)) + // Prop + | HasType(t, ALFA_Typ.t) + | Syn(t, ALFA_Typ.t) + | Ana(t, ALFA_Typ.t) | And(t, t) | Or(t, t) | Impl(t, t) | Truth | Falsity - | Tuple(list(t)) - | Abbr(Pat.t) - | Parens(t) - and t = IdTagged.t(term); - - let map_term = - ( - ~f_hazel_pat=continue, - ~f_prop=continue, - ~f_exp=continue, - ~f_pat=continue, - ~f_typ=continue, - ~f_tpat=continue, - x, - ) => { - let exp_map_term = - ALFA_Exp.map_term(~f_hazel_pat, ~f_exp, ~f_pat, ~f_typ, ~f_tpat); - let typ_map_term = ALFA_Typ.map_term(~f_typ, ~f_tpat); - let prop_map_term = - Prop.map_term(~f_prop, ~f_exp, ~f_pat, ~f_typ, ~f_tpat); - let rec_call = ({term, _} as exp: t) => { - ...exp, - term: - switch (term) { - | Hole(_) => term - | HasType(e, t) => HasType(exp_map_term(e), typ_map_term(t)) - | Syn(e, t) => Syn(exp_map_term(e), typ_map_term(t)) - | Ana(e, t) => Ana(exp_map_term(e), typ_map_term(t)) - | Var(v) => Var(v) - | And(p1, p2) => And(prop_map_term(p1), prop_map_term(p2)) - | Or(p1, p2) => Or(prop_map_term(p1), prop_map_term(p2)) - | Impl(p1, p2) => Impl(prop_map_term(p1), prop_map_term(p2)) - | Truth => Truth - | Falsity => Falsity - | Tuple(pl) => Tuple(List.map(prop_map_term, pl)) - | Abbr(e) => Abbr(f_hazel_pat(e)) - | Parens(p) => Parens(prop_map_term(p)) - }, - }; - x |> f_prop(rec_call); - }; - - let fast_equal = (x, y) => - switch (x |> IdTagged.term_of, y |> IdTagged.term_of) { - | (Hole(_), _) => false - | (HasType(e1, t1), HasType(e2, t2)) => - ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) - | (HasType(_), _) => false - | (Syn(e1, t1), Syn(e2, t2)) => - ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) - | (Syn(_), _) => false - | (Ana(e1, t1), Ana(e2, t2)) => - ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) - | (Ana(_), _) => false - | (Var(v1), Var(v2)) => v1 == v2 - | (Var(_), _) => false - | (And(p1, p2), And(p1', p2')) => - Prop.fast_equal(p1, p1') && Prop.fast_equal(p2, p2') - | (And(_), _) => false - | (Or(p1, p2), Or(p1', p2')) => - Prop.fast_equal(p1, p1') && Prop.fast_equal(p2, p2') - | (Or(_), _) => false - | (Impl(p1, p2), Impl(p1', p2')) => - Prop.fast_equal(p1, p1') && Prop.fast_equal(p2, p2') - | (Impl(_), _) => false - | (Truth, Truth) - | (Truth, _) => false - | (Falsity, Falsity) - | (Falsity, _) => false - | (Tuple(pl1), Tuple(pl2)) => List.equal(Prop.fast_equal, pl1, pl2) - | (Tuple(_), _) => false - | (Abbr(p1), Abbr(p2)) => Pat.fast_equal(p1, p2) - | (Abbr(_), _) => false - | (Parens(p1), Parens(p2)) => Prop.fast_equal(p1, p2) - | (Parens(_), _) => false - }; -} -and ALFA_Exp: { - [@deriving (show({with_path: false}), sexp, yojson)] - type term = - | Hole(TypeHole.t) + // Exp | NumLit(int) | Neg(t) | Plus(t, t) @@ -1650,12 +1345,10 @@ and ALFA_Exp: { | True | False | If(t, t, t) - | Var(Var.t) | Let(ALFA_Pat.t, t, t) | Fix(ALFA_Pat.t, t) | Fun(ALFA_Pat.t, t) | Ap(t, t) - | Pair(t, t) | Triv | PrjL(t) | PrjR(t) @@ -1664,8 +1357,6 @@ and ALFA_Exp: { | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t) | Roll | Unroll - | Abbr(Pat.t) - | Parens(t) and t = IdTagged.t(term); let map_term: @@ -1684,6 +1375,26 @@ and ALFA_Exp: { [@deriving (show({with_path: false}), sexp, yojson)] type term = | Hole(TypeHole.t) + | Var(Var.t) // Prop / Exp + | Abbr(Pat.t) // Jdmt / Ctxt / Prop / Exp + | Parens(t) // Jdmt / Ctxt / Prop / Exp + | Tuple(list(t)) // [invalid] / Exp + // Jdmt + | Val(t) + | Eval(t, t) + | Entail(t, t) + // Ctx + | Ctx(list(t)) + // Prop + | HasType(t, ALFA_Typ.t) + | Syn(t, ALFA_Typ.t) + | Ana(t, ALFA_Typ.t) + | And(t, t) + | Or(t, t) + | Impl(t, t) + | Truth + | Falsity + // Exp | NumLit(int) | Neg(t) | Plus(t, t) @@ -1695,12 +1406,10 @@ and ALFA_Exp: { | True | False | If(t, t, t) - | Var(Var.t) | Let(ALFA_Pat.t, t, t) | Fix(ALFA_Pat.t, t) | Fun(ALFA_Pat.t, t) | Ap(t, t) - | Pair(t, t) | Triv | PrjL(t) | PrjR(t) @@ -1709,8 +1418,6 @@ and ALFA_Exp: { | Case(t, ALFA_Pat.t, t, ALFA_Pat.t, t) | Roll | Unroll - | Abbr(Pat.t) - | Parens(t) and t = IdTagged.t(term); let map_term = @@ -1730,6 +1437,22 @@ and ALFA_Exp: { term: switch (term) { | Hole(_) => term + | Var(v) => Var(v) + | Abbr(e) => Abbr(f_hazel_pat(e)) + | Parens(e) => Parens(exp_map_term(e)) + | Val(e) => Val(exp_map_term(e)) + | Eval(e1, e2) => Eval(exp_map_term(e1), exp_map_term(e2)) + | Entail(e1, e2) => Entail(exp_map_term(e1), exp_map_term(e2)) + | Ctx(e) => Ctx(List.map(exp_map_term, e)) + | HasType(e, t) => HasType(exp_map_term(e), t) + | Syn(e, t) => Syn(exp_map_term(e), t) + | Ana(e, t) => Ana(exp_map_term(e), t) + | And(e1, e2) => And(exp_map_term(e1), exp_map_term(e2)) + | Or(e1, e2) => Or(exp_map_term(e1), exp_map_term(e2)) + | Impl(e1, e2) => Impl(exp_map_term(e1), exp_map_term(e2)) + | Truth => Truth + | Falsity => Falsity + | Tuple(es) => Tuple(List.map(exp_map_term, es)) | NumLit(n) => NumLit(n) | Neg(e) => Neg(exp_map_term(e)) | Plus(e1, e2) => Plus(exp_map_term(e1), exp_map_term(e2)) @@ -1742,13 +1465,11 @@ and ALFA_Exp: { | False => False | If(e1, e2, e3) => If(exp_map_term(e1), exp_map_term(e2), exp_map_term(e3)) - | Var(v) => Var(v) | Let(p, e1, e2) => Let(pat_map_term(p), exp_map_term(e1), exp_map_term(e2)) | Fix(p, e) => Fix(pat_map_term(p), exp_map_term(e)) | Fun(p, e) => Fun(pat_map_term(p), exp_map_term(e)) | Ap(e1, e2) => Ap(exp_map_term(e1), exp_map_term(e2)) - | Pair(e1, e2) => Pair(exp_map_term(e1), exp_map_term(e2)) | Triv => Triv | PrjL(e) => PrjL(exp_map_term(e)) | PrjR(e) => PrjR(exp_map_term(e)) @@ -1764,8 +1485,6 @@ and ALFA_Exp: { ) | Roll => Roll | Unroll => Unroll - | Abbr(e) => Abbr(f_hazel_pat(e)) - | Parens(e) => Parens(exp_map_term(e)) }, }; x |> f_exp(rec_call); @@ -1774,6 +1493,50 @@ and ALFA_Exp: { let fast_equal = (x, y) => switch (x |> IdTagged.term_of, y |> IdTagged.term_of) { | (Hole(_), _) => false + | (Var(v1), Var(v2)) => v1 == v2 + | (Var(_), _) => false + | (Abbr(p1), Abbr(p2)) => Pat.fast_equal(p1, p2) + | (Abbr(_), _) => false + | (Parens(e1), Parens(e2)) => ALFA_Exp.fast_equal(e1, e2) + | (Parens(_), _) => false + | (Val(e1), Val(e2)) => ALFA_Exp.fast_equal(e1, e2) + | (Val(_), _) => false + | (Eval(e11, e12), Eval(e21, e22)) => + ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) + | (Eval(_), _) => false + | (Entail(e11, e12), Entail(e21, e22)) => + ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) + | (Entail(_), _) => false + | (Ctx(es1), Ctx(es2)) => + List.length(es1) == List.length(es2) + && List.for_all2(ALFA_Exp.fast_equal, es1, es2) + | (Ctx(_), _) => false + | (HasType(e1, t1), HasType(e2, t2)) => + ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) + | (HasType(_), _) => false + | (Syn(e1, t1), Syn(e2, t2)) => + ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) + | (Syn(_), _) => false + | (Ana(e1, t1), Ana(e2, t2)) => + ALFA_Exp.fast_equal(e1, e2) && ALFA_Typ.fast_equal(t1, t2) + | (Ana(_), _) => false + | (And(e11, e12), And(e21, e22)) => + ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) + | (And(_), _) => false + | (Or(e11, e12), Or(e21, e22)) => + ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) + | (Or(_), _) => false + | (Impl(e11, e12), Impl(e21, e22)) => + ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) + | (Impl(_), _) => false + | (Truth, Truth) => true + | (Truth, _) => false + | (Falsity, Falsity) => true + | (Falsity, _) => false + | (Tuple(es1), Tuple(es2)) => + List.length(es1) == List.length(es2) + && List.for_all2(ALFA_Exp.fast_equal, es1, es2) + | (Tuple(_), _) => false | (NumLit(n1), NumLit(n2)) => n1 == n2 | (NumLit(_), _) => false | (Neg(e1), Neg(e2)) => ALFA_Exp.fast_equal(e1, e2) @@ -1805,8 +1568,6 @@ and ALFA_Exp: { && ALFA_Exp.fast_equal(e2, e2') && ALFA_Exp.fast_equal(e3, e3') | (If(_), _) => false - | (Var(v1), Var(v2)) => v1 == v2 - | (Var(_), _) => false | (Let(p1, e11, e12), Let(p2, e21, e22)) => ALFA_Pat.fast_equal(p1, p2) && ALFA_Exp.fast_equal(e11, e21) @@ -1821,9 +1582,6 @@ and ALFA_Exp: { | (Ap(e11, e12), Ap(e21, e22)) => ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) | (Ap(_), _) => false - | (Pair(e11, e12), Pair(e21, e22)) => - ALFA_Exp.fast_equal(e11, e21) && ALFA_Exp.fast_equal(e12, e22) - | (Pair(_), _) => false | (Triv, Triv) => true | (Triv, _) => false | (PrjL(e1), PrjL(e2)) => ALFA_Exp.fast_equal(e1, e2) @@ -1845,10 +1603,6 @@ and ALFA_Exp: { | (Roll, _) => false | (Unroll, Unroll) => true | (Unroll, _) => false - | (Abbr(p1), Abbr(p2)) => Pat.fast_equal(p1, p2) - | (Abbr(_), _) => false - | (Parens(e1), Parens(e2)) => ALFA_Exp.fast_equal(e1, e2) - | (Parens(_), _) => false }; } and ALFA_Pat: { diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re index 1224901351..82aad0424b 100644 --- a/src/haz3lcore/tiles/Segment.re +++ b/src/haz3lcore/tiles/Segment.re @@ -123,9 +123,9 @@ and subsort_of = (sort: Sort.t): list(Sort.t) => | Drv(drv) => ( switch (drv) { - | Jdmt => [Ctxt, Prop, Exp, Pat, Typ, TPat] - | Ctxt => [Prop, Exp, Pat, Typ, TPat] - | Prop => [Exp, Pat, Typ, TPat] + | Jdmt + | Ctx + | Prop => failwith("subsort_of unexpected") | Exp => [Pat, Typ, TPat] | Pat => [Typ] | Typ => [] diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re index 2da0e732af..713b047fde 100644 --- a/src/haz3lcore/zipper/action/Select.re +++ b/src/haz3lcore/zipper/action/Select.re @@ -186,9 +186,9 @@ module Make = (M: Editor.Meta.S) => { switch (Info.cls_of(ci_parent), Info.cls_of(ci_gp)) { | ( Exp(Tuple) | Pat(Tuple) | Typ(Prod) | - Drv(Prop(Tuple) | Exp(Pair) | Pat(Pair) | Typ(Prod)), + Drv(Exp(Tuple) | Pat(Pair) | Typ(Prod)), Exp(Parens) | Pat(Parens) | Typ(Parens) | - Drv(Prop(Parens) | Exp(Parens) | Pat(Parens) | Typ(Parens)), + Drv(Exp(Parens) | Pat(Parens) | Typ(Parens)), ) => /* If parent is tuple, check if it's in parens, * and if so, select the parens as well */ diff --git a/src/haz3lschool/ProofCore.re b/src/haz3lschool/ProofCore.re index 725f35c217..4abad224e5 100644 --- a/src/haz3lschool/ProofCore.re +++ b/src/haz3lschool/ProofCore.re @@ -164,7 +164,7 @@ module ModelUtil = { switch (pos) { | Prelude => Exp | Setup => Exp - | Trees(_, _) => Drv(Jdmt) + | Trees(_, _) => Drv(Exp) }; }; diff --git a/src/haz3lschool/ProofGrade.re b/src/haz3lschool/ProofGrade.re index 2ca13a596e..239dfd5a62 100644 --- a/src/haz3lschool/ProofGrade.re +++ b/src/haz3lschool/ProofGrade.re @@ -72,8 +72,8 @@ module F = (ExerciseEnv: Exercise.ExerciseEnv) => { | ResultOk({result, _}) => ignore(rule); switch (result) { - | BoxedValue({term: Term(Drv(d)), _}) => - Ok({jdmt: DrvElab.elaborate(d), rule}) + | BoxedValue({term: Term(Drv(Exp(d))), _}) => + Ok({jdmt: DrvElab.elab_jdmt(d), rule}) | Indet(_) => Error(EvalIndet) | _ => Error(EvalIndet) }; diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index df8c73aeb3..cec1610ecc 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -8,6 +8,11 @@ let of_delim' = Core.Memo.general( ~cache_size_bound=10000, ((label, is_in_buffer, sort, is_consistent, is_complete, indent, i)) => { + let sort = + switch (sort) { + | Sort.Drv(Exp) => Sort.Drv(Sort.DrvSort.detail_sort(label)) + | _ => sort + }; let cls = switch (label) { | _ when is_in_buffer => "in-buffer" diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re index 11f1934141..85521d739f 100644 --- a/src/haz3lweb/view/CursorInspector.re +++ b/src/haz3lweb/view/CursorInspector.re @@ -184,17 +184,11 @@ let drv_view = (status: DrvInfo.t) => { | None => div_ok([text("Fillable by any derivation element")]) | Some(err) => switch (err) { - | Jdmt(BadToken(token)) - | Ctxt(BadToken(token)) - | Prop(BadToken(token)) | Exp(BadToken(token)) | Pat(BadToken(token)) | Typ(BadToken(token)) | TPat(BadToken(token)) => div_err([text(Printf.sprintf("\"%s\" isn't a valid token", token))]) - | Jdmt(MultiHole) - | Ctxt(MultiHole) - | Prop(MultiHole) | Exp(MultiHole) | Pat(MultiHole) | Typ(MultiHole) @@ -212,10 +206,27 @@ let drv_view = (status: DrvInfo.t) => { | InjR => "A Right Injection pattern" }; div_err([text("Expected " ++ expect)]); - | Exp(NotAllowSingle) => - div_err([text("Expected a compound expression of this")]) - | Prop(NotAllowTuple) => - div_err([text("Expected no comma in this position")]) + | Exp(NoJoin(ty)) when ty == Arrow => + // TODO(zhiyao): not sufficient + div_err([text("Function argument type inconsistent with arrow type")]) + | Exp(NoJoin(ty)) => + // TODO(zhiyao): not sufficient + div_err([ + text( + "Expect sort " + ++ ( + ty + |> ( + fun + | Jdmt => "Jdmt" + | Ctx => "Ctx" + | Prop => "Prop" + | Exp => "ALFA_Exp" + | Arrow => "???" + ) + ), + ), + ]) } }; }; diff --git a/src/haz3lweb/view/exercise/NinjaKeysRules.re b/src/haz3lweb/view/exercise/NinjaKeysRules.re index 1d2b0d6be3..6f6b623ec6 100644 --- a/src/haz3lweb/view/exercise/NinjaKeysRules.re +++ b/src/haz3lweb/view/exercise/NinjaKeysRules.re @@ -7,8 +7,11 @@ let staged = ref(false); let init = () => "" - |> Exercise.zipper_of_code(~root=Haz3lcore.Sort.Drv(Jdmt)) - |> Haz3lcore.Editor.init(~settings=Haz3lcore.CoreSettings.on, ~sort=Exp); + |> Exercise.zipper_of_code(~root=Haz3lcore.Sort.Drv(Exp)) + |> Haz3lcore.Editor.init( + ~settings=Haz3lcore.CoreSettings.on, + ~sort=Drv(Exp), + ); let map_model = (f, state: Exercise.state): Exercise.state => { ...state, diff --git a/src/haz3lweb/view/exercise/ProofView.re b/src/haz3lweb/view/exercise/ProofView.re index b0c03e32df..15dd237284 100644 --- a/src/haz3lweb/view/exercise/ProofView.re +++ b/src/haz3lweb/view/exercise/ProofView.re @@ -71,7 +71,7 @@ let proof_view = Exercise.Proof.add_premise( ~pos, ~index, - ~init=init(~sort=Drv(Jdmt)), + ~init=init(~sort=Drv(Exp)), ), ) |> (m => {...m, pos: make_pos(pos, index)}), @@ -185,7 +185,7 @@ let proof_view = Exercise.Proof.switch_rule( ~pos, ~rule=None, - ~init=init(~sort=Drv(Jdmt)), + ~init=init(~sort=Drv(Exp)), ), ), ), @@ -335,7 +335,7 @@ let proof_view = ~editor, ~di, ~caption=None, - ~sort=Drv(Jdmt), + ~sort=Drv(Exp), ~footer=[], ), ], @@ -403,7 +403,7 @@ let proof_view = |> map_model( Exercise.Proof.add_abbr( ~index, - ~init=init(~sort=Drv(Jdmt)), + ~init=init(~sort=Drv(Exp)), ), ) |> (m => {...m, pos: Proof(Trees(index, Value))}),