sidekick/src/base/proof-trace/proof_ser.bare

type ID i32
type Lit ID

type Clause {
  lits: []Lit
}

type Step_input {
  c: Clause
}

# clause, RUP with previous steps
type Step_rup {
  res: Clause
  hyps: []ID
}

# TODO: remove?
# lit <-> expr
type Step_bridge_lit_expr {
  lit: Lit
  expr: ID
}

# prove congruence closure lemma `\/_{e\in eqns} e`
type Step_cc {
  eqns: []ID
}

# prove t=u using some previous steps and unit equations,
# and add clause (t=u) with given ID
type Step_preprocess {
  t: ID
  u: ID
  using: []ID
}

type Step_clause_rw {
  c: ID
  res: Clause
  using: []ID
}

type Step_unsat {
  c: ID
}

# rewrite `c` with the unit clause `rw_with` of the form `t=u`  *)
type Step_proof_p1 {
  rw_with: ID
  c: ID
}

# resolve `c` with the unit clause `unit` of the form `|- t`  *)
type Step_proof_r1 {
  unit: ID
  c: ID
}

# resolve `c1` with `c2` on pivot `pivot` *)
type Step_proof_res {
  pivot: ID
  c1: ID
  c2: ID
}

type Step_bool_tauto {
  lits: []Lit
}

type Step_bool_c {
  rule: string
  exprs: []ID
}

type Step_true {
  true_: ID
}

type Fun_decl {
  f: string
}

# define c := rhs
type Expr_def {
  c: ID
  rhs: ID
}

type Expr_bool {
  b: bool
}

type Expr_if {
  cond: ID
  then_: ID
  else_: ID
}

type Expr_not {
  f: ID
}

type Expr_eq {
  lhs: ID
  rhs: ID
}

type Expr_app {
  f: ID
  args: []ID
}

type Expr_isa {
  c: ID
  arg: ID
}

type Step_view
  ( Step_input
  | Step_unsat
  | Step_rup
  | Step_bridge_lit_expr
  | Step_cc
  | Step_preprocess
  | Step_clause_rw
  | Step_bool_tauto
  | Step_bool_c
  | Step_proof_p1
  | Step_proof_r1
  | Step_proof_res
  | Step_true
  | Fun_decl
  | Expr_def
  | Expr_bool
  | Expr_if
  | Expr_not
  | Expr_isa
  | Expr_eq
  | Expr_app
  )

type Step {
  id: ID
  view: Step_view
}