package electrod

You can search for identifiers within the package.

in-package search v0.2.0

Formal analysis for the Electrod formal pivot language

Install

dune-project

Dependency

sha256=545020556bdc1517867791ccbbf4a00623d911663daa26e6d57dc66e7652f269

sha512=2921be5e844e408f1d3208c7d9b310d3ef3b050d37ab0b449b9fd9722be54167eacc08b957b595cab58dedb28c43f327238a30a360ac0ae45d724bd1d8bd664c

Sourcemodule E = Elo

Sourceval convert_arity : int option -> int

Sourceval get_var : Var.t -> Var.t Containers.List.t -> int

Sourceval new_env : Ast.var list -> Var.t list -> Var.t list

val convert_fml : 
  Var.t Containers.List.t ->
  (Ast.var, Ast.ident) Gen_goal.fml ->
  E.fml

val convert_block : 
  Var.t Containers.List.t ->
  (Ast.var, Ast.ident) Gen_goal.block ->
  E.fml Containers.List.t

Sourceval convert_quant : Gen_goal.quant -> E.quant

Sourceval convert_comp_op : Gen_goal.comp_op -> E.comp_op

Sourceval convert_icomp_op : Gen_goal.icomp_op -> E.icomp_op

Sourceval convert_lunop : Gen_goal.lunop -> E.lunop

Sourceval convert_lbinop : Gen_goal.lbinop -> E.lbinop

val convert_exp : 
  Var.t Containers.List.t ->
  (Ast.var, Ast.ident) Gen_goal.exp ->
  E.exp

val convert_sim_bindings : 
  Var.t Containers.List.t ->
  (Ast.var, Ast.ident) Gen_goal.sim_binding list ->
  (Gen_goal.disj * int * E.exp) list

Sourceval convert_runop : Gen_goal.runop -> E.runop

Sourceval convert_rbinop : Gen_goal.rbinop -> E.rbinop

val convert_iexp : 
  Var.t Containers.List.t ->
  (Ast.var, Ast.ident) Gen_goal.iexp ->
  E.iexp

Sourceval convert_ibinop : Gen_goal.ibinop -> E.ibinop

Sourceval convert_goal : (Ast.var, Ast.ident) Gen_goal.t -> E.goal

Sourceval convert : Ast.t -> E.t