{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.IR where

open import SemanticExplanation.Base
open import Agda.Builtin.Reflection using (Name ; Visibility ; Relevance ; Quantity)

data AtomSurface : Set where
  unarySuffix : String → AtomSurface
  binaryVerb  : String → AtomSurface
  equalityPhrase : String → AtomSurface

data ExprSurface : Set where
  constantWord : String → ExprSurface
  unaryForm : String → String → ExprSurface
  binaryForm : String → String → String → ExprSurface

data ExprIR (scope : Nat) : Set where
  bound      : Fin scope → ExprIR scope
  application : String → ExprSurface → List (ExprIR scope) → ExprIR scope

record Binder (scope : Nat) : Set where
  constructor binder
  field
    hint       : String
    entityWord : String
    indices    : List (ExprIR scope)
    ruleId     : String
    visibility : Visibility
    relevance  : Relevance
    quantity   : Quantity

data PropIR (scope : Nat) : Set where
  atom   : String → AtomSurface → List (ExprIR scope) → PropIR scope
  equal  : String → String → ExprIR scope → ExprIR scope → PropIR scope
  imply  : PropIR scope → PropIR scope → PropIR scope
  forallP : Binder scope → PropIR (suc scope) → PropIR scope

data ProvenanceEntry : Set where
  ruleUsed      : String → ProvenanceEntry
  aliasUnfolded : Name → ProvenanceEntry
  binderOmitted : String → ProvenanceEntry
  argumentOmitted : String → Nat → ProvenanceEntry

record Translation (scope : Nat) : Set where
  constructor translated
  field
    proposition : PropIR scope
    provenance  : List ProvenanceEntry