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_iter_typ : 
  Ctx.t ->
  Lang.Il.typ ->
  (Lang.Il.typ * Lang.Il.iter) Attempt.attempt

val as_tuple_typ : Ctx.t -> Lang.Il.typ -> Lang.Il.typ list Attempt.attempt

val as_list_typ : Ctx.t -> Lang.Il.typ -> Lang.Il.typ 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_deftyp : 
  Ctx.t ->
  Lang.El.id ->
  Lang.El.tparam list ->
  Lang.El.deftyp ->
  Runtime.Type.Typdef.t * Lang.Il.deftyp

val elab_deftyp_plain : 
  Ctx.t ->
  Lang.El.tparam list ->
  Lang.El.plaintyp ->
  Runtime.Type.Typdef.t * Lang.Il.deftyp

val elab_typfield : Ctx.t -> Lang.El.typfield -> Lang.Il.typfield

val elab_deftyp_struct : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.tparam list ->
  Lang.El.typfield list ->
  Runtime.Type.Typdef.t * Lang.Il.deftyp

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 elab_deftyp_variant : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.El.tparam list ->
  Lang.El.typcase list ->
  Runtime.Type.Typdef.t * Lang.Il.deftyp

val fail_infer : Util.Source.region -> string -> 'a Attempt.attempt

val infer_exp : 
  Ctx.t ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp * Lang.Il.typ) Attempt.attempt

val infer_exp' : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.exp' ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') 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_num_exp : 
  Ctx.t ->
  Lang.Xl.Num.t ->
  (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_var_exp : 
  Ctx.t ->
  Lang.El.id ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_unop : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.unop ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  (Lang.Il.optyp * Lang.Il.exp * Lang.Il.typ') Attempt.attempt

val infer_unop_exp : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.unop ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_binop : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.binop ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  (Lang.Il.optyp * Lang.Il.exp * Lang.Il.exp * Lang.Il.typ') Attempt.attempt

val infer_binop_exp : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.binop ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_cmpop_exp_bool : 
  Ctx.t ->
  Lang.Xl.Bool.cmpop ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_cmpop_num : 
  Ctx.t ->
  Util.Source.region ->
  Lang.Xl.Num.cmpop ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  (Lang.Il.optyp * Lang.Il.exp * Lang.Il.exp) Attempt.attempt

val infer_cmpop_exp_num : 
  Ctx.t ->
  Util.Source.region ->
  Lang.Xl.Num.cmpop ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_cmpop_exp : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.cmpop ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_arith_exp : 
  Ctx.t ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_list_exp : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.exp list ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_cons_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_cat_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_idx_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_slice_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_mem_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_dot_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.atom ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_upd_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.path ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_len_exp : 
  Ctx.t ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_paren_exp : 
  Ctx.t ->
  Lang.El.exp ->
  (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 infer_call_exp : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.El.targ list ->
  Lang.El.arg list ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_iter_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.iter ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val infer_sub_exp : 
  Ctx.t ->
  Lang.El.exp ->
  Lang.El.plaintyp ->
  (Ctx.t * Lang.Il.exp' * Lang.Il.typ') Attempt.attempt

val elab_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp) Attempt.attempt

val elab_exp' : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp) 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_iter : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.Il.typ ->
  Lang.Il.iter ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp) Attempt.attempt

val fail_cast : 
  Util.Source.region ->
  Lang.Il.typ ->
  Lang.Il.typ ->
  Lang.Il.exp Attempt.attempt

val cast_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.Il.typ ->
  Lang.Il.exp ->
  Lang.Il.exp Attempt.attempt

val elab_exp_normal : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp) Attempt.attempt

val elab_exp_wildcard : 
  Ctx.t ->
  Util.Source.region ->
  Lang.Il.typ ->
  (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_exp_plain' : 
  Ctx.t ->
  Util.Source.region ->
  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_cons_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp') Attempt.attempt

val elab_cat_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  Lang.El.exp ->
  (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 elab_paren_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp') Attempt.attempt

val elab_iter_exp : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.exp ->
  Lang.El.iter ->
  (Ctx.t * Lang.Il.exp') Attempt.attempt

val fail_elab_not : 
  Util.Source.region ->
  string ->
  (Ctx.t * Lang.Il.notexp) Attempt.attempt

val elab_exp_not : 
  Ctx.t ->
  Lang.Il.nottyp ->
  Lang.El.exp ->
  (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_expfields : 
  Ctx.t ->
  Util.Source.region ->
  Lang.Il.typfield list ->
  (Lang.El.atom * Lang.El.exp) list ->
  (Ctx.t * (Lang.Il.atom * Lang.Il.exp) list) Attempt.attempt

val elab_exp_struct : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.Il.typfield list ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.exp) 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_path : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.path ->
  (Ctx.t * Lang.Il.path * Lang.Il.typ) Attempt.attempt

val elab_path' : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.path' ->
  (Ctx.t * Lang.Il.path' * Lang.Il.typ') Attempt.attempt

val elab_root_path : 
  Ctx.t ->
  Lang.Il.typ ->
  (Ctx.t * Lang.Il.path' * Lang.Il.typ') Attempt.attempt

val elab_idx_path : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.path ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.path' * Lang.Il.typ') Attempt.attempt

val elab_slice_path : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.path ->
  Lang.El.exp ->
  Lang.El.exp ->
  (Ctx.t * Lang.Il.path' * Lang.Il.typ') Attempt.attempt

val elab_dot_path : 
  Ctx.t ->
  Lang.Il.typ ->
  Lang.El.path ->
  Lang.El.atom ->
  (Ctx.t * Lang.Il.path' * Lang.Il.typ') 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' =

| SomePr of Lang.Il.prem'
| VarPr
| 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 =

| SomeRule of Lang.Il.rule
| ElseRule of Lang.Il.rule

type rulegroup_internal =

| Group of Lang.Il.rulegroup
| ElseGroup of Lang.Il.elsegroup

val is_else_rule_internal : rule_internal -> bool

val elab_rule : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.Il.nottyp ->
  Lang.El.exp ->
  Lang.El.prem list ->
  rule_internal

val elab_rulegroup : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.El.id ->
  Lang.El.rule list ->
  rulegroup_internal

type clause_internal =

| Clause of Lang.Il.clause
| ElseClause of Lang.Il.clause

val elab_clause : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.El.tparam list ->
  Lang.El.arg list ->
  Lang.El.exp ->
  Lang.El.prem list ->
  clause_internal

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_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_tablerow : 
  Ctx.t ->
  Util.Source.region ->
  Lang.El.id ->
  Lang.Il.param list ->
  Lang.Il.typ ->
  Lang.El.tablerow ->
  Lang.Il.tablerow

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/p4spectec.pass/Pass/Elaborate/Elab/index.html

Module `Elaborate.Elab`

package p4spectec

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/p4spectec.pass/Pass/Elaborate/Elab/index.html

Module Elaborate.Elab

dune-project
Dependency

Module `Elaborate.Elab`