Grammar.re

open Util;
[@deriving (show({with_path: false}), sexp, yojson)]
type deferral_position_t =
  | InAp
  | OutsideAp;

[@deriving (show({with_path: false}), sexp, yojson)]
type any('e, 't, 'tp, 'r, 'a, 'p) =
  | Exp('e)
  | Pat('p)
  | Typ('t)
  | TPat('tp)
  | Rul('r)
  | Any(unit)
and exp('e, 't, 'tp, 'r, 'a, 'p) =
  | Invalid(string)
  | EmptyHole
  | MultiHole(list('a))
  | DynamicErrorHole('e, InvalidOperationError.t)
  | FailedCast('e, 't, 't)
  | Deferral(deferral_position_t)
  | Undefined
  | Bool(bool)
  | Int(int)
  | Float(float)
  | String(string)
  | ListLit(list('e))
  | Constructor(string, 'tp) // Typ.t field is only meaningful in dynamic expressions
  | Fun('p, 'e, option('t), option(Var.t)) // 't field is only used to display types in results
  | TypFun('tp, 'e, option(Var.t))
  | Tuple(list('e))
  | Var(Var.t)
  | Let('p, 'e, 'e)
  | FixF('p, 'e, option(closure_environment_t('e, 't, 'tp, 'r, 'a, 'p)))
  | TyAlias('tp, 't, 'e)
  | Ap(Operators.ap_direction, 'e, 'e)
  | TypAp('e, 't)
  | DeferredAp('e, list('e))
  | If('e, 'e, 'e)
  | Seq('e, 'e)
  | Test('e)
  | Filter(stepper_filter_kind_t('e), 'e)
  | Closure(
      [@show.opaque] closure_environment_t('e, 't, 'tp, 'r, 'a, 'p),
      'e,
    )
  | Parens('e) // (
  | Cons('e, 'e)
  | ListConcat('e, 'e)
  | UnOp(Operators.op_un, 'e)
  | BinOp(Operators.op_bin, 'e, 'e)
  | BuiltinFun(string)
  | Match('e, list(('p, 'e)))
  /* 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('e, 't, 't)
and pat('e, 't, 'tp, 'r, 'a, 'p) =
  | Invalid(string)
  | EmptyHole
  | MultiHole(list('a))
  | Wild
  | Int(int)
  | Float(float)
  | Bool(bool)
  | String(string)
  | ListLit(list('p))
  | Constructor(string, 't) // Typ.t field is only meaningful in dynamic patterns
  | Cons('p, 'p)
  | Var(Var.t)
  | Tuple(list('p))
  | Parens('p)
  | Ap('p, 'p)
  | Cast('p, 't, 't)
and typ('e, 't, 'tp, 'r, 'a, 'p) =
  | Unknown(type_provenance('a))
  | Int
  | Float
  | Bool
  | String
  | Var(string)
  | List('t)
  | Arrow('t, 't)
  | Sum(ConstructorMap.t('t))
  | Prod(list('t))
  | Parens('t)
  | Ap('t, 't)
  | Rec('tp, 't)
  | Forall('tp, 't)
and tpat('e, 't, 'tp, 'r, 'a, 'p) =
  | Invalid(string)
  | EmptyHole
  | MultiHole(list('a))
  | Var(string)
and rul('e, 't, 'tp, 'r, 'a, 'p) =
  | Invalid(string)
  | Hole(list('a))
  | Rules('e, list(('p, 'e)))
and environment_t('e, 't, 'tp, 'r, 'a, 'p) = VarBstMap.Ordered.t_('e)
and closure_environment_t('e, 't, 'tp, 'r, 'a, 'p) = (
  Id.t,
  environment_t('e, 't, 'tp, 'r, 'a, 'p),
)
and stepper_filter_kind_t('e) =
  | Filter(filter('e))
  | Residue(int, FilterAction.t)
and type_hole('a) =
  | Invalid(string)
  | EmptyHole
  | MultiHole(list('a))
and type_provenance('a) =
  | SynSwitch
  | Hole(type_hole('a))
  | Internal
and filter('e) = {
  pat: 'e,
  act: FilterAction.t,
};

type exp_term =
  | Exp(exp(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term))
and pat_term =
  | Pat(pat(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term))
and typ_term =
  | Typ(typ(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term))
and tpat_term =
  | TPat(tpat(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term))
and rul_term =
  | Rul(rul(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term))
and any_term =
  | Any(any(exp_term, typ_term, tpat_term, rul_term, any_term, pat_term));

let exp: exp_term = Exp(Cast(Exp(Var("x")), Typ(Int), Typ(Int)));

type exp_t =
  | Exp(IdTagged.t(exp(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t)))
and pat_t =
  | Pat(IdTagged.t(pat(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t)))
and typ_t =
  | Typ(IdTagged.t(typ(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t)))
and tpat_t =
  | TPat(IdTagged.t(tpat(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t)))
and rul_t =
  | Rul(IdTagged.t(rul(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t)))
and any_t =
  | Any(any(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t));

let exp: exp_t =
  Exp(
    Cast(
      Exp(Var("x") |> IdTagged.fresh),
      Typ(IdTagged.fresh(Int : typ(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t))),
      Typ(IdTagged.fresh(Int : typ(exp_t, typ_t, tpat_t, rul_t, any_t, pat_t))),
    )
    |> IdTagged.fresh,
  );