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

sha256=e5d2278c99128621110cd015dafcbcae9792bbf2c8bb09d7b02c57d50fa28075

sha512=e08ecf720d35b6ee72f37d780cc3da22f61e22314ffd093ff3314fb89684b863b5c96c97375d48bcb4ba2838ec8f61a495105c989f292c5dbcd095e14f52bdba

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