zelus 2.2 · OCaml Package

reduce expressions that are tagged to be static; leave other unchanged

type fun_defs = {

fundefs : (Deftypes.name * Zelus.funexp) list;

}

val empty : fun_defs

val num : int Stdlib.ref

val gfresh : unit -> string

val build : 'a Zident.Env.t -> 'b Zident.Env.t * Zident.t Zident.Env.t

Build a renaming from an environment

val rename : Zident.Env.key -> 'a Zident.Env.t -> 'b

rename a variable

val remove : 'a Zident.Env.t -> 'b Zident.Env.t -> 'b Zident.Env.t

Remove entries in venv that are defined in renaming

val type_expression : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  Zelus.type_expression ->
  Zelus.type_expression

type expressions

val size : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  Zelus.size ->
  Zelus.size

val operator : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  Zelus.op ->
  Zelus.op

Rename an operator

val pattern : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  Zelus.pattern ->
  Zelus.pattern

Renaming of patterns

val expression : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  fun_defs ->
  Zelus.exp ->
  Zelus.exp * fun_defs

Simplify an expression.

val static : 
  Global.value_code Zident.Env.t ->
  fun_defs ->
  Zelus.exp ->
  Zelus.exp * fun_defs

val local : 
  Global.value_code Zident.Env.t ->
  (Zident.t Zident.Env.t * fun_defs) ->
  Zelus.local ->
  Zelus.local * (Zident.t Zident.Env.t * fun_defs)

Simplify a local declaration

val equation : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  fun_defs ->
  Zelus.eq ->
  Zelus.eq * fun_defs

Simplify an equation.

val scondpat : 
  Global.value_code Zident.Env.t ->
  Zident.t Zident.Env.t ->
  fun_defs ->
  Zelus.scondpat ->
  Zelus.scondpat * fun_defs

val vardec : Zident.t Zident.Env.t -> Zelus.vardec -> Zelus.vardec

val block : 
  Global.value_code Zident.Env.t ->
  (Zident.t Zident.Env.t * fun_defs) ->
  Zelus.eq list Zelus.block ->
  Zelus.eq list Zelus.block * (Zident.t Zident.Env.t * fun_defs)

val exp_of_value : fun_defs -> Global.value_code -> Zelus.exp * fun_defs

Convert a value into an expression.

val lambda : 
  Global.value_code Zident.Env.t ->
  fun_defs ->
  Zelus.funexp ->
  Zelus.funexp * fun_defs

val implementation_list : 
  'a ->
  Zelus.implementation_desc Zelus.localized list ->
  Zelus.implementation_desc Zelus.localized list

package zelus