package rfsm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Typing

module Syntax : SYNTAX
module Types : TYPES

Typing environment

type env
val mk_env : unit -> env

mk_env () should return the initial typing environment. This environment should contain, in particular, bindings for builtins primitives, type and value constructors.

val lookup_var : loc:Location.t -> Ident.t -> env -> Types.typ

lookup_var l x env should return the type bound to identifier x in environment env. The behaviour when x is not bound in env is left to guest definition. A possibility is to raise Ident.Undefined for example.

val add_var : scope:Ident.scope -> env -> (Ident.t * Types.typ) -> env

add_var scope env (x,t) should return the environment obtained by the binding (x,t) to env. The scope parameter is a hint to the guest type inference system. Typically, it will be used to determine, in the case the added type contains type variables, whether these variables will be generalized (scope=Local) or not (scope=Global). The behaviour when x is already bound in env is left to guest definition.

val add_param : env -> (Ident.t * Syntax.expr) -> env

add_param env (x,t) should return the environment obtained by the binding (x,t) as a model parameter to env.

val pp_env : Stdlib.Format.formatter -> env -> unit

pp_env fmt env should print a readable representation of typing environment env on formatter fmt.

Low-level interface to the the type-checking engine

val type_check : loc:Location.t -> Types.typ -> Types.typ -> unit

type_check loc t t' should be called whenever types t and t' have to be unified at program location loc.

High-level interface to the type-checking engine

val type_type_decl : env -> Syntax.type_decl -> env

type_type_decl env td should return the typing environment obtained by type checking the type declaration td in environment env.

val type_expression : env -> Syntax.expr -> Types.typ

type_expression env e should return the type of expression e in environment env.

val type_of_type_expr : env -> Syntax.type_expr -> Types.typ

type_of_type_expr env te should return the type denoted by the type expression te in environment env.

val type_lval : env -> Syntax.lval -> Types.typ

type_lval env l should return the type of l-value l in environment env.