hazelnut.re

open Sexplib.Std;
// open Monad_lib.Monad; // Uncomment this line to use the maybe monad

let compare_string = String.compare;
let compare_int = Int.compare;
// let compare_bool = Bool.compare;

module Htyp = {
  [@deriving (sexp, compare, show({with_path: false}))]
  type t =
    | Arrow(t, t)
    | Num
    | Hole;
};

module Ztyp = {
  [@deriving (sexp, compare, show({with_path: false}))]
  type t =
    | Cursor(Htyp.t)
    | LArrow(t, Htyp.t)
    | RArrow(Htyp.t, t);
};

// Error marks from the marked lambda calculus (Zhao et al. 2024, Fig. 2).
// Free:         free variable — L x M□
// NonArrowAp:   applicand synthesizes a non-arrow type — L ě M⇒▶̸→
// LamAscIncon:  lambda's annotation is inconsistent with the expected
//               input type — L λx:τ. ě M:
// Inconsistent: expression synthesizes a type inconsistent with the
//               expected type — L ě M≁
module Mark = {
  [@deriving (sexp, compare, show({with_path: false}))]
  type t =
    | Free
    | NonArrowAp
    | LamAscIncon
    | Inconsistent;
};

module Hexp = {
  [@deriving (sexp, compare, show({with_path: false}))]
  type t =
    | Var(string) // x
    | NumLit(int) // n
    | Plus(t, t) // e + e
    | Lam(string, Htyp.t, t) // λx:τ.e
    | Ap(t, t) // e e
    | Asc(t, Htyp.t) // e : τ
    | EHole // empty hole
    | Mark(t, Mark.t); // marked expression
};

module Zexp = {
  [@deriving (sexp, compare, show({with_path: false}))]
  type t =
    | Cursor(Hexp.t)
    | LPlus(t, Hexp.t)
    | RPlus(Hexp.t, t)
    | LLam(string, Ztyp.t, Hexp.t)
    | RLam(string, Htyp.t, t)
    | LAsc(t, Htyp.t)
    | RAsc(Hexp.t, Ztyp.t)
    | LAp(t, Hexp.t)
    | RAp(Hexp.t, t)
    | Mark(t, Mark.t);
};

module Child = {
  [@deriving (sexp, compare)]
  type t =
    | One
    | Two;
};

module Dir = {
  [@deriving (sexp, compare)]
  type t =
    | Child(Child.t)
    | Parent;
};

module Shape = {
  [@deriving (sexp, compare)]
  type t =
    | Arrow
    | Num
    | Var(string)
    | NumLit(int)
    | Plus
    | Lam(string)
    | Asc
    | Ap;
};

module Action = {
  [@deriving (sexp, compare)]
  type t =
    | Move(Dir.t)
    | Construct(Shape.t)
    | Del;
};

module TypCtx = Map.Make(String);
type typctx = TypCtx.t(Htyp.t);

exception Unimplemented;

// =====================================================================
// STEP 1: Type compatibility helpers
//
// These auxiliary judgements are shared between Hazelnut (2017) and
// the marked lambda calculus (2024).  Implement them first — the rest
// of the system depends on them, and the test suite can verify them in
// isolation.
// =====================================================================

// Matched arrow types (Zhao et al. 2024, Fig. 5):
//   TMAArr:     τ₁→τ₂ ▸→ τ₁→τ₂
//   TMAUnknown: ?    ▸→ ?→?
// In diy-marking we identify Hole with ?.
let matched_arrow_typ = (t: Htyp.t): option((Htyp.t, Htyp.t)) => {
  let _ = t;
  raise(Unimplemented);
};

// Type consistency (Zhao et al. 2024, Fig. 4):
//   TCUnknown1: ? ∼ τ
//   TCUnknown2: τ ∼ ?
//   TCRefl:     τ ∼ τ        (base types)
//   TCArr:      τ₁∼τ₁' ∧ τ₂∼τ₂'  →  τ₁→τ₂ ∼ τ₁'→τ₂'
// Inconsistency, written τ ≁ τ', is just ¬(τ ∼ τ').
let type_consistent = (t1: Htyp.t, t2: Htyp.t): bool => {
  let _ = (t1, t2);
  raise(Unimplemented);
};

// =====================================================================
// STEP 2: Cursor erasure (Hazelnut 2017, Appendix A.2)
//
// Strip the cursor from a zipper, recovering the underlying H-type or
// H-expression.  Needed by the action semantics and by the webapp, which
// re-marks the entire program after every edit.
// =====================================================================

// Type cursor erasure (Hazelnut 2017, Appendix A.2.1):
//   ETTop:   erase(▶τ◀)   = τ
//   ETArrL:  erase(τ̂ → τ) = erase(τ̂) → τ
//   ETArrR:  erase(τ → τ̂) = τ → erase(τ̂)
let erase_typ = (t: Ztyp.t): Htyp.t => {
  switch (t) {
  | Cursor(_) => raise(Unimplemented) // ETTop
  | LArrow(_, _) => raise(Unimplemented) // ETArrL
  | RArrow(_, _) => raise(Unimplemented) // ETArrR
  };
};

// Expression cursor erasure (Hazelnut 2017, Appendix A.2.2, extended
// with Lam-annotation, Lam-body, and Mark zippers for diy-marking):
//   EETop:    erase(▶e◀)     = e
//   EELamL:   erase(λx:τ̂.e)  = λx:erase_typ(τ̂).e
//   EELamR:   erase(λx:τ.ê)  = λx:τ.erase(ê)
//   EEAscL:   erase(ê : τ)   = erase(ê) : τ
//   EEAscR:   erase(e : τ̂)   = e : erase_typ(τ̂)
//   EEApL:    erase(ê e)     = erase(ê) e
//   EEApR:    erase(e ê)     = e erase(ê)
//   EEPlusL:  erase(ê + e)   = erase(ê) + e
//   EEPlusR:  erase(e + ê)   = e + erase(ê)
//   EEMark:   erase(L ê Mm)  = L erase(ê) Mm
let erase_exp = (e: Zexp.t): Hexp.t => {
  let _ = e;
  raise(Unimplemented);
};

// =====================================================================
// STEP 3: Marking (Zhao et al. 2024, Section 2.1)
//
// The marking judgement  Γ ⊢ e ↬ ě ⇒ τ  /  Γ ⊢ e ↬ ě ⇐ τ  is the core
// contribution of the marked lambda calculus.  It is TOTAL: for every
// (Γ, e) there exist ě and τ such that marking succeeds (Theorem 2.1).
// That is why mark_syn and mark_ana return values directly, never
// option.
//
// The two functions are mutually recursive and may be written in the
// simplest way that treats each syntactic form in turn.  mark_syn maps
// (Γ, e) to (ě, τ); mark_ana maps (Γ, τ, e) to ě.
//
// The recipe from the paper: for each unmarked rule, recurse into the
// subterms (recursively marking them) and, if any premise fails, wrap
// the result with the appropriate Mark instead of propagating an error.
//
// Synthesis rules (MKS*, Zhao et al. 2024):
//   MKSVar       (2.1.3): x ∈ Γ  →  Γ ⊢ x ↬ x ⇒ Γ(x)
//   MKSFree      (2.1.3): x ∉ Γ  →  Γ ⊢ x ↬ L x M_Free ⇒ Hole
//   MKSNum       (2.1.1): Γ ⊢ n ↬ n ⇒ Num
//   MKSPlus      (2.1.1): Γ ⊢ e₁ ↬ ě₁ ⇐ Num, Γ ⊢ e₂ ↬ ě₂ ⇐ Num  →
//                         Γ ⊢ e₁+e₂ ↬ ě₁+ě₂ ⇒ Num
//   MKSLam       (2.1.4): Γ,x:τ₁ ⊢ e ↬ ě ⇒ τ₂  →
//                         Γ ⊢ λx:τ₁.e ↬ λx:τ₁.ě ⇒ τ₁→τ₂
//   MKSAp1       (2.1.5): Γ ⊢ e₁ ↬ ě₁ ⇒ τ, τ▸→τ₁→τ₂, Γ ⊢ e₂ ↬ ě₂ ⇐ τ₁
//                         → Γ ⊢ e₁ e₂ ↬ ě₁ ě₂ ⇒ τ₂
//   MKSAp2       (2.1.5): Γ ⊢ e₁ ↬ ě₁ ⇒ τ, τ▸̸→, Γ ⊢ e₂ ↬ ě₂ ⇐ Hole
//                         → Γ ⊢ e₁ e₂ ↬ L ě₁ M_NonArrowAp ě₂ ⇒ Hole
//   MKSHole      (2.1.8): Γ ⊢ LM ↬ LM ⇒ Hole
// Ascription is not in the base calculus, but we include it here with
//   MKSAsc: Γ ⊢ e ↬ ě ⇐ τ → Γ ⊢ (e:τ) ↬ (ě:τ) ⇒ τ
// For Mark(e, _) we strip the incoming mark and re-mark e from scratch,
// since marks are not part of the unmarked language.
let rec mark_syn = (ctx: typctx, e: Hexp.t): (Hexp.t, Htyp.t) => {
  let _ = (ctx, e, mark_ana); // silence unused-rec warnings
  raise(Unimplemented);
}

// Analysis rules (MKA*, Zhao et al. 2024):
//   MKASubsume            (2.1.2): Γ ⊢ e ↬ ě ⇒ τ', τ ∼ τ', e subsumable
//                                  →  Γ ⊢ e ↬ ě ⇐ τ
//   MKAInconsistentTypes  (2.1.2): Γ ⊢ e ↬ ě ⇒ τ', τ ≁ τ', e subsumable
//                                  →  Γ ⊢ e ↬ L ě M_Inconsistent ⇐ τ
//   MKALam1               (2.1.4): τ₃▸→τ₁→τ₂, τ ∼ τ₁,
//                                  Γ,x:τ ⊢ e ↬ ě ⇐ τ₂
//                                  →  Γ ⊢ λx:τ.e ↬ λx:τ.ě ⇐ τ₃
//   MKALam2               (2.1.4): τ₃▸̸→, Γ,x:τ ⊢ e ↬ ě ⇐ Hole
//                                  →  Γ ⊢ λx:τ.e ↬ L λx:τ.ě M_NonArrowAp ⇐ τ₃
//                         Note: in this template we reuse NonArrowAp to
//                         stand for the "lambda checked against non-arrow"
//                         mark, since it has the same semantic flavour.
//   MKALam3               (2.1.4): τ₃▸→τ₁→τ₂, τ ≁ τ₁,
//                                  Γ,x:τ ⊢ e ↬ ě ⇐ τ₂
//                                  →  Γ ⊢ λx:τ.e ↬ L λx:τ.ě M_LamAscIncon ⇐ τ₃
// Lam is the only non-subsumable form in this minimal calculus.
and mark_ana = (ctx: typctx, t: Htyp.t, e: Hexp.t): Hexp.t => {
  let _ = (ctx, t, e, mark_syn); // silence unused-rec warnings
  raise(Unimplemented);
};

// =====================================================================
// STEP 4: Edit action semantics (Hazelnut 2017, Section 3.3; Zhao
//         et al. 2024, Section 3.2)
//
// Unlike Hazelnut-2017, this calculus uses the *decoupled* action
// design from Zhao et al. 2024, §3.2: edit actions operate on unmarked
// zippered expressions (Zexp.t) and never fail. After each action, the
// webapp cursor-erases the result, re-marks it with mark_syn, and folds
// the marks back into the zipper with fold_zexp_mexp.
//
// Because actions never fail, every function below returns a plain
// Zexp.t (or Ztyp.t), defaulting to the original on invalid inputs.
//
// You will need to implement the following internal helpers first:
//   move_typ    : type zipper movement rules (Ztyp.t, Dir.t) => Ztyp.t
//   move_action : expression zipper movement rules
//                 (Zexp.t, Dir.t) => Zexp.t
//   typ_action  : type actions (move, del, construct, zipper recursion)
//
// A suggested order within each function:
//   1. Movement (Move)      — just walks the cursor
//   2. Deletion (Del)       — replaces cursor target with a hole
//   3. Construction (...)   — the bulk of the rules
//   4. Zipper recursion     — propagate actions through the tree
// =====================================================================

// Type-zipper movement (analogous to Hazelnut 2017, Appendix A.3.2).
//   TMArrChild1:  ▶τ₁→τ₂◀ --child1--> ▶τ₁◀ → τ₂
//   TMArrChild2:  ▶τ₁→τ₂◀ --child2--> τ₁ → ▶τ₂◀
//   TMArrParent1: ▶τ₁◀ → τ₂ --parent--> ▶τ₁→τ₂◀
//   TMArrParent2: τ₁ → ▶τ₂◀ --parent--> ▶τ₁→τ₂◀
//   Zipper:       recurse into LArrow/RArrow subterms.
let move_typ = (t: Ztyp.t, a: Dir.t): Ztyp.t => {
  let _ = (t, a);
  raise(Unimplemented);
};

// Expression-zipper movement — extends A.3.2 with Lam-annotation and
// Lam-body zippers (since Lam has two children here) and with a Mark
// zipper (which behaves like any other unary wrapper).
//   EMAscChild1/2/Parent1/Parent2, EMLamChild1/2/Parent1/Parent2,
//   EMPlusChild1/2/Parent1/Parent2, EMApChild1/2/Parent1/Parent2,
//   EMMarkChild1/Parent, plus zipper recursion.
let move_action = (e: Zexp.t, a: Dir.t): Zexp.t => {
  let _ = (e, a);
  raise(Unimplemented);
};

// Type actions (Hazelnut 2017, Appendix A.3.1):
//   TAMove: delegate to move_typ
//   TADel:  Cursor(_) --del--> Cursor(Hole)
//   TAConArrow: Cursor(τ) --construct arrow--> τ → ▶Hole◀
//               (or the paper variant ▶τ→Hole◀; we pick a single
//                convention and stick with it)
//   TAConNum:   Cursor(Hole) --construct num--> Cursor(Num)
//   TAZipArrL/R: propagate action into LArrow/RArrow subterms
let typ_action = (t: Ztyp.t, a: Action.t): Ztyp.t => {
  let _ = (t, a);
  raise(Unimplemented);
};

// Synthetic action on unmarked expression zippers.  Because marking is
// total and performed separately, this function never returns None;
// invalid actions simply return the input unchanged.
//
// Construction rules (fire only when the cursor is on a suitable hole):
//   Construct(Var(x))      — ▶LM◀ --> ▶x◀     (mark will be added later if x∉Γ)
//   Construct(NumLit(n))   — ▶LM◀ --> ▶n◀
//   Construct(Lam(x))      — ▶LM◀ --> λx:▶Hole◀.LM
//   Construct(Asc)         — ▶e◀  --> e : ▶Hole◀
//   Construct(Ap)          — ▶e◀  --> e ▶LM◀
//   Construct(Plus)        — ▶e◀  --> e + ▶LM◀
// Shape constructors for types (Arrow/Num) are no-ops on Zexp and should
// only fire in type-zipper contexts (via zipper recursion).
//
// Zipper recursion: for every non-Cursor Zexp form, recurse into the
// zippered subterm, using move_typ / typ_action for type children.
let syn_action = (e: Zexp.t, a: Action.t): Zexp.t => {
  let _ = (e, a);
  raise(Unimplemented);
};

// =====================================================================
// STEP 5: Folding marks back into a zipper (Zhao et al. 2024, §3.2)
//
// After an edit, the webapp:
//   1. Cursor-erases the Zexp to get an Hexp.
//   2. Calls mark_syn on the Hexp to get a (marked) Hexp.
//   3. Calls fold_zexp_mexp to transport the marks back onto the
//      original Zexp, preserving the cursor position.
//
// fold_zexp_mexp(z, e) should traverse (z, e) in lock-step, copying
// marks from e onto matching positions in z. Whenever e carries a Mark
// that z does not, wrap that part of z in Mark(_, _).
// =====================================================================
let fold_zexp_mexp = (z: Zexp.t, e: Hexp.t): Zexp.t => {
  let _ = (z, e);
  raise(Unimplemented);
};