PAst (mlsem-app.Mlsem

exception SymbolError of string

exception LexicalError of Mlsem_common.Position.t * string

exception SyntaxError of Mlsem_common.Position.t * string

Expr AST

type 'typ lambda_annot = 'typ option

type 'typ vkind =

| Immut
| AnnotMut of 'typ
| Mut

type ('typ, 'v) vdef = 'typ vkind * 'v

type ('a, 'typ, 'gty, 'tag, 'v) pattern =

| PatType of 'typ
| PatVar of ('gty, 'v) vdef
| PatLit of Mlsem_lang.Const.t
| PatTag of 'tag * ('a, 'typ, 'gty, 'tag, 'v) pattern
| PatAnd of ('a, 'typ, 'gty, 'tag, 'v) pattern * ('a, 'typ, 'gty, 'tag, 'v) pattern
| PatOr of ('a, 'typ, 'gty, 'tag, 'v) pattern * ('a, 'typ, 'gty, 'tag, 'v) pattern
| PatTuple of ('a, 'typ, 'gty, 'tag, 'v) pattern list
| PatCons of ('a, 'typ, 'gty, 'tag, 'v) pattern * ('a, 'typ, 'gty, 'tag, 'v) pattern
| PatRecord of (string * ('a, 'typ, 'gty, 'tag, 'v) pattern) list * bool
| PatAssign of ('gty, 'v) vdef * Mlsem_lang.Const.t

and ('a, 'typ, 'gty, 'enu, 'tag, 'v) ast =

| Magic of 'gty
| Const of Mlsem_lang.Const.t
| Var of 'v
| Enum of 'enu
| Tag of 'tag * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| TagProj of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'tag
| Suggest of 'v * 'typ list * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Lambda of 'v * 'gty lambda_annot * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| LambdaRec of ('v * 'gty lambda_annot * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t) list
| Ite of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'gty * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| App of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Let of ('gty, 'v) vdef * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Declare of ('gty, 'v) vdef * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Tuple of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t list
| TupleProj of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * int * int
| Cons of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Hd of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Tl of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Record of (string * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t) list
| RecordUpdate of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * string * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t option
| RecordProj of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * string
| TypeCast of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'gty * Mlsem_system.Ast.check
| TypeCoerce of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'gty * Mlsem_system.Ast.check
| VarAssign of 'v * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| PatMatch of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * (('a, 'typ, 'gty, 'tag, 'v) pattern * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t) list
| Cond of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'gty * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t option
| While of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * 'gty * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Seq of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Alt of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t * ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Return of ('a, 'typ, 'gty, 'enu, 'tag, 'v) t
| Break
| Continue

and ('a, 'typ, 'gty, 'enu, 'tag, 'v) t =
  'a * ('a, 'typ, 'gty, 'enu, 'tag, 'v) ast

type expr =
  (Mlsem_common.Eid.t,
    Mlsem_types.Ty.t,
    Mlsem_types.GTy.t,
    Mlsem_types.Enum.t,
    Mlsem_types.Tag.t,
    Mlsem_common.Variable.t)
    t

Program AST

type varname = string

type annotation = Mlsem_common.Eid.t Mlsem_common.Position.located

val new_annot : Mlsem_common.Position.t -> annotation

type pexpr =
  (annotation,
    Mlsem_types.TyExpr.t,
    Mlsem_types.TyExpr.t,
    string,
    string,
    varname)
    t

type pat =
  (annotation, Mlsem_types.TyExpr.t, Mlsem_types.TyExpr.t, string, varname)
    pattern

module NameMap : Stdlib.Map.S with type key = string

type name_var_map = Mlsem_common.Variable.t NameMap.t

val empty_name_var_map : name_var_map

val to_expr : 
  Mlsem_types.Builder.benv ->
  name_var_map ->
  pexpr ->
  expr * Mlsem_types.Builder.benv

type element =

| Definitions of ((Mlsem_types.TyExpr.t, string) vdef * pexpr) list
| SigDef of string * bool * Mlsem_types.TyExpr.t
| Types of (string * string list * Mlsem_types.TyExpr.t) list
| AbsType of string * int
| Command of string * Mlsem_lang.Const.t

type program = (annotation * element) list