failed grammar

grammar.re

module type GrammarFactory = {
  module Typ: {
    type t;
  };
  module Exp: {
    type t;
  };
  module Pat: {
    type t;
  };
  module TPat: {
    type t;
  };
  module Rul: {
    type t;
  };
  module Any: {
    type t;
  };
  module TypeHole: {
    type t;
  };
  module TypeProvenance: {
    type t;
  };

  type typ = Typ.t;
  type exp = Exp.t;
  type pat = Pat.t;
  type tpat = TPat.t;
  type type_provenance = TypeProvenance.t;
  type type_hole = TypeHole.t;
  type any = Any.t;
  type rul = Rul.t;
  type environment;
  type deferral_position =
    | InAp
    | OutsideAp;
  type filter = {
    pat: exp,
    act: FilterAction.t,
  };
  type stepper_filter_kind =
    | Filter(filter)
    | Residue(int, FilterAction.t);
  type closure_environment = {
    id: Id.t,
    env: environment,
    call_stack: Probe.call_stack,
  };
};

module Typ = (G: GrammarFactory) => {
  type t =
    | Unknown(G.type_provenance)
    | Atom(Atom.cls)
    | Var(string)
    | List(G.typ)
    | Arrow(G.typ, G.typ)
    | Sum(ConstructorMap.t(G.typ))
    | Prod(list(G.typ))
    | Label(string)
    | TupLabel(G.typ, G.typ)
    | Parens(G.typ)
    | Ap(G.typ, G.typ)
    | Rec(G.tpat, G.typ)
    | Forall(G.tpat, G.typ);
};

module Exp = (G: GrammarFactory) => {
  type t =
    | Invalid(string)
    | EmptyHole
    | MultiHole(list(G.any))
    | DynamicErrorHole(G.exp, InvalidOperationError.t)
    | Deferral(G.deferral_position)
    | Undefined
    | Atom(Atom.t)
    | ListLit(list(G.exp))
    /* The type double-option field of this constructor is required to assign the correct
       statics to constructors after evaluation. In dynamic expressions `Some(None)` means
       that it is a free constructor, while Some(Some(t)) means it has type t. In user expressions
       this field is None.*/
    | Constructor(string, option(option(G.typ)))
    | Fun(G.pat, G.exp, option(G.typ), option(Var.t)) // typ_t field is only used to display types in results
    | TypFun(G.tpat, G.exp, option(Var.t))
    | Tuple(list(G.exp))
    | Label(string)
    | TupLabel(G.exp, G.exp)
    | Dot(G.exp, G.exp)
    | LivelitName(string)
    | Var(Var.t)
    | Let(G.pat, G.exp, G.exp)
    | FixF(G.pat, G.exp, option(G.closure_environment))
    | TyAlias(G.tpat, G.typ, G.exp)
    | Use(G.typ, G.exp)
    | Ap(Operators.ap_direction, G.exp, G.exp)
    | TypAp(G.exp, G.typ)
    | DeferredAp(G.exp, list(G.exp))
    | If(G.exp, G.exp, G.exp)
    | Seq(G.exp, G.exp)
    | Test(G.exp)
    | HintedTest(G.exp, G.exp)
    | Filter(G.stepper_filter_kind, G.exp)
    | Closure([@show.opaque] G.closure_environment, G.exp)
    | Parens(G.exp) // (
    | Probe(G.exp, Probe.t)
    | Cons(G.exp, G.exp)
    | ListConcat(G.exp, G.exp)
    | UnOp(Operators.op_un, G.exp)
    | BinOp(Operators.op_bin, G.exp, G.exp)
    | BuiltinFun(string)
    | Match(G.exp, list((G.pat, G.exp)))
    | TupleExtension(G.exp, G.exp)
    | Asc(G.exp, G.typ);
};

module Pat = (G: GrammarFactory) => {
  type t =
    | Invalid(string)
    | EmptyHole
    | MultiHole(list(G.any))
    | Wild
    | Atom(Atom.t)
    | ListLit(list(G.pat))
    | Constructor(string, option(option(G.typ))) // see comment on constructor expressions
    | Cons(G.pat, G.pat)
    | Var(Var.t)
    | Tuple(list(G.pat))
    | Label(string)
    | TupLabel(G.pat, G.pat)
    | Parens(G.pat)
    | Probe(G.pat, Probe.t)
    | Ap(G.pat, G.pat)
    | Asc(G.pat, G.typ);
};

module TPat = (G: GrammarFactory) => {
  type t =
    | Invalid(string)
    | EmptyHole
    | MultiHole(list(G.any))
    | Var(string);
};

module Rul = (G: GrammarFactory) => {
  type t =
    | Invalid(string)
    | MultiHole(list(G.any))
    | Rules(G.exp, list((G.pat, G.exp)));
};

module Any = (G: GrammarFactory) => {
  type t =
    | Exp(G.exp)
    | Pat(G.pat)
    | Typ(G.typ)
    | TPat(G.tpat)
    | Rul(G.rul)
    | Any(unit);
};

module TypeHole = (G: GrammarFactory) => {
  type t =
    | Invalid(string)
    | EmptyHole
    | MultiHole(list(G.any));
};

module TypeProvenance = (G: GrammarFactory) => {
  type t =
    | SynSwitch
    | Hole(G.type_hole)
    | Internal;
};

module rec PureGrammar: GrammarFactory = {
  module Typ = Typ(PureGrammar);
  module Exp = Exp(PureGrammar);
  module Pat = Pat(PureGrammar);
  module TPat = TPat(PureGrammar);
  module Rul = Rul(PureGrammar);
  module Any = Any(PureGrammar);
  module TypeHole = TypeHole(PureGrammar);
  module TypeProvenance = TypeProvenance(PureGrammar);
  type typ = Typ.t;
  type exp = Exp.t;
  type pat = Pat.t;
  type tpat = TPat.t;
  type type_provenance = TypeProvenance.t;
  type type_hole = TypeHole.t;
  type any = Any.t;
  type rul = Rul.t;
  type environment = VarBstMap.Ordered.t_(exp);

  type deferral_position =
    | InAp
    | OutsideAp;
  type filter = {
    pat: exp,
    act: FilterAction.t,
  };
  type stepper_filter_kind =
    | Filter(filter)
    | Residue(int, FilterAction.t);
  type closure_environment = {
    id: Id.t,
    env: environment,
    call_stack: Probe.call_stack,
  };
};

/* Define types outside the recursive module to access constructors */
type typ = PureGrammar.typ;
type exp = PureGrammar.exp;
type pat = PureGrammar.pat;
type tpat = PureGrammar.tpat;
type rul = PureGrammar.rul;
type any = PureGrammar.any;

let x: typ = Var("t");