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=b0bce9cc7126672feda5a02d5ef0c1131ba54db57654f80c0768c2f8d043cef9

sha512=92cc22f81522435e190039324767b6f69fa0b7d9dbfc3fb5561919823136fe492244dae993caf98633828e0090b67f306eec6270b86a1b2ff8630642130a3081

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