Module Elaborate.Elab

module Mixfix = Domain.Mixfix
module F = Format
val valid_tid : Lang.El.id -> bool
val elab_iter : Lang.El.iter -> Lang.Il.iter
val as_text_typ : Ctx.t -> Lang.Il.typ -> unit Attempt.attempt
val as_tuple_typ : Ctx.t -> Lang.Il.typ -> Lang.Il.typ list Attempt.attempt
val as_struct_typ : Ctx.t -> Lang.Il.typ -> Lang.Il.typfield list Attempt.attempt
val elab_plaintyp : Ctx.t -> Lang.El.plaintyp -> Lang.Il.typ
val elab_plaintyp' : Ctx.t -> Lang.El.plaintyp' -> Lang.Il.typ'
val elab_nottyp : Ctx.t -> Lang.El.typ -> Lang.Il.nottyp
val elab_typfield : Ctx.t -> Lang.El.typfield -> Lang.Il.typfield
val elab_typcase_plain : Ctx.t -> Lang.Il.typ -> Lang.Il.typcase list
val elab_typcase : Ctx.t -> Lang.Il.typorigin -> Lang.El.typcase -> Lang.Il.typcase list
val fail_infer : Util.Source.region -> string -> 'a Attempt.attempt
val infer_exps : Ctx.t -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp list * Lang.Il.typ list) Attempt.attempt
val infer_bool_exp : Ctx.t -> bool -> (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt
val infer_text_exp : Ctx.t -> Lang.El.text -> (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt
val infer_tuple_exp : Ctx.t -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt
val elab_exps : Ctx.t -> Lang.Il.typ list -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp list) Attempt.attempt
val elab_exp_normal : Ctx.t -> Lang.Il.typ -> Lang.El.exp -> (Ctx.t * Lang.Il.exp) Attempt.attempt
val fail_elab_plain : Util.Source.region -> string -> (Ctx.t * Lang.Il.exp') Attempt.attempt
val elab_exp_plain : Ctx.t -> Lang.Il.typ -> Lang.El.exp -> (Ctx.t * Lang.Il.exp) Attempt.attempt
val elab_eps_exp : Ctx.t -> Lang.Il.typ -> (Ctx.t * Lang.Il.exp') Attempt.attempt
val elab_list_exp_elementwise : Ctx.t -> Lang.Il.typ -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp list) Attempt.attempt
val elab_list_exp : Ctx.t -> Lang.Il.typ -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp') Attempt.attempt
val elab_tuple_exp : Ctx.t -> Lang.Il.typ -> Lang.El.exp list -> (Ctx.t * Lang.Il.exp') Attempt.attempt
val fail_elab_not : Util.Source.region -> string -> (Ctx.t * Lang.Il.notexp) Attempt.attempt
val fail_elab_struct : Util.Source.region -> string -> (Ctx.t * (Lang.Il.atom * Lang.Il.exp) list) Attempt.attempt
val elab_exp_struct' : Ctx.t -> Lang.Il.typfield list -> Lang.El.exp -> (Ctx.t * (Lang.Il.atom * Lang.Il.exp) list) Attempt.attempt
val fail_elab_variant : Util.Source.region -> string -> (Ctx.t * Lang.Il.exp) Attempt.attempt
val elab_exp_variant : Ctx.t -> Lang.Il.typ -> Lang.Il.typcase list -> Lang.El.exp -> (Ctx.t * Lang.Il.exp) Attempt.attempt
val elab_param : Ctx.t -> Lang.El.param -> Lang.Il.param
val elab_arg : ?as_def:??? -> Ctx.t -> Lang.Il.param -> Lang.El.arg -> Ctx.t * Lang.Il.arg
val elab_args : ?as_def:??? -> Util.Source.region -> Ctx.t -> Lang.Il.param list -> Lang.El.arg list -> Ctx.t * Lang.Il.arg list
type prem_internal = prem_internal' Util.Source.phrase
and prem_internal' =
  1. | SomePr of Lang.Il.prem'
  2. | VarPr
  3. | ElsePr
val internalize_prem : Lang.Il.prem -> prem_internal
val externalize_prem : prem_internal -> Lang.Il.prem option
val is_else_prem_internal : prem_internal -> bool
val check_prems_internal : Util.Source.region -> prem_internal list -> unit
val elab_prem : Ctx.t -> Lang.El.prem -> Ctx.t * prem_internal
val elab_prem' : Ctx.t -> Lang.El.prem' -> Ctx.t * prem_internal'
val elab_prems : Ctx.t -> Lang.El.prem list -> Ctx.t * prem_internal list
val elab_var_prem : Ctx.t -> Lang.El.id -> Lang.El.plaintyp -> Ctx.t
val elab_rule_prem : Ctx.t -> Lang.El.id -> Lang.El.exp -> Ctx.t * Lang.Il.prem'
val elab_rule_not_prem : Ctx.t -> Lang.El.id -> Lang.El.exp -> Ctx.t * Lang.Il.prem'
val elab_if_prem : Ctx.t -> Lang.El.exp -> Ctx.t * Lang.Il.prem'
val elab_iter_prem : Ctx.t -> Lang.El.prem -> Lang.El.iter -> Ctx.t * Lang.Il.prem'
val elab_debug_prem : Ctx.t -> Lang.El.exp -> Ctx.t * Lang.Il.prem'
type rule_internal =
  1. | SomeRule of Lang.Il.rule
  2. | ElseRule of Lang.Il.rule
type rulegroup_internal =
  1. | Group of Lang.Il.rulegroup
  2. | ElseGroup of Lang.Il.elsegroup
val is_else_rule_internal : rule_internal -> bool
type clause_internal =
  1. | Clause of Lang.Il.clause
  2. | ElseClause of Lang.Il.clause
val elab_def : Ctx.t -> Lang.El.def -> Ctx.t * Lang.Il.def option
val elab_defs : Ctx.t -> Lang.El.def list -> Ctx.t * Lang.Il.def list
val elab_extern_syn_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_syn_def : Ctx.t -> (Lang.El.id * Lang.El.tparam list) list -> Ctx.t
val elab_typ_def : Ctx.t -> Lang.El.id -> Lang.El.tparam list -> Lang.El.deftyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_var_def : Ctx.t -> Lang.El.id -> Lang.El.plaintyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val fetch_rel_input_hint : Util.Source.region -> Lang.Il.nottyp -> Lang.El.hint list -> Lang.Hints.Input.t
val elab_extern_rel_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.nottyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_rulegroup_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.id -> Lang.El.rule list -> Ctx.t
val elab_extern_dec_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.tparam list -> Lang.El.param list -> Lang.El.plaintyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_builtin_dec_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.tparam list -> Lang.El.param list -> Lang.El.plaintyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_table_dec_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.param list -> Lang.El.plaintyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_func_dec_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.tparam list -> Lang.El.param list -> Lang.El.plaintyp -> Lang.El.hint list -> Ctx.t * Lang.Il.def
val elab_tablerows : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.Il.param list -> Lang.Il.typ -> Lang.El.tablerow list -> Lang.Il.tablerow list
val elab_table_def_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.tablerow list -> Ctx.t
val elab_func_def : Ctx.t -> Util.Source.region -> Lang.El.id -> Lang.El.tparam list -> Lang.El.arg list -> Lang.El.exp -> Lang.El.prem list -> Ctx.t
val populate_typs : Ctx.t -> unit
val populate_rule : Ctx.t -> Lang.Il.def -> Lang.Il.def
val populate_rules : Ctx.t -> Lang.Il.spec -> Lang.Il.spec
val populate_clause : Ctx.t -> Lang.Il.def -> Lang.Il.def
val populate_clauses : Ctx.t -> Lang.Il.spec -> Lang.Il.spec
val elab_spec : Lang.El.spec -> Lang.Il.spec