Module Evalenv.Evalenv

module Evalenv: sig .. end

Evaluation environment.

type constraintenv = Constraint.Constraint.cexp list AstUtils.VarMap.t

For storing information about data values/user-defined types along with their associated constraints.

type typeconstraint = string ->
       Ast.Ast.relation ->
       constraintenv -> constraintenv

type evalenv = {

	`typeconstraints : typeconstraint MapUtils.StringMap.t;`
	`tyenv : Ast.Ast.typerep MapUtils.StringMap.t;`
	`tydefenv : Ast.Ast.userty MapUtils.StringMap.t;`
	`functions : Ast.Ast.fundecl MapUtils.StringMap.t;`
	`globalbindings : Ast.Ast.exp AstUtils.VarMap.t;`
	`localbindings : Ast.Ast.exp AstUtils.VarMap.t;`
	`constraintbindings : constraintenv;`

}

val default_tyconstraint : string ->
       Ast.Ast.relation ->
       constraintenv -> constraintenv

Default type constraint.

Default empty environment.

val empty_evalenv : evalenv

val addFunDecl : evalenv -> Ast.Ast.fundecl -> evalenv

val lookupFunDecl : evalenv -> string -> Ast.Ast.fundecl option

val bindTypeGlobalEnv : evalenv ->
       string -> Ast.Ast.typerep -> evalenv

val addTypeDecl : evalenv ->
       Ast.Ast.userty -> Ast.Ast.constraintbody list -> evalenv

val lookupTypeDeclByData : evalenv -> string -> Ast.Ast.userty option

val lookupType : evalenv -> Ast.Ast.var -> Ast.Ast.typerep option

val lookupTypeConstraints : evalenv -> string -> typeconstraint option

val addConstraintGlobalEnv : evalenv ->
       Ast.Ast.var -> Constraint.Constraint.cexp -> evalenv

val addConstraintListGlobalEnv : evalenv ->
       Ast.Ast.var -> Constraint.Constraint.cexp list -> evalenv

val lookupConstraintsEnv : evalenv -> Ast.Ast.var -> Constraint.Constraint.cexp list

val lookupValueEnv : evalenv -> Ast.Ast.var -> Ast.Ast.exp option

val bindValueGlobalEnv : evalenv ->
       Ast.Ast.var -> Ast.Ast.exp -> evalenv

val bindValueLocalEnv : evalenv ->
       Ast.Ast.var -> Ast.Ast.exp -> evalenv

val lookupRelationGlobalEnv : evalenv -> Ast.Ast.var -> Ast.Ast.relation option

val addConstraint : evalenv ->
       string -> Ast.Ast.constraintbody list -> evalenv