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

module SemanticExplanation.Base where

open import Agda.Builtin.Bool public using (Bool ; true ; false)
open import Agda.Builtin.List public using (List ; [] ; _∷_)
open import Agda.Builtin.Maybe public using (Maybe ; just ; nothing)
open import Agda.Builtin.Nat public using (Nat ; zero ; suc)
open import Agda.Builtin.String public
  using (String ; primShowNat ; primStringAppend ; primStringEquality)
open import Agda.Builtin.Unit public using (⊤ ; tt)
open import Agda.Primitive public using (Level ; lzero ; lsuc ; _⊔_)

infixr  _++_

_++_ : String → String → String
_++_ = primStringAppend

infixr  _++L_

_++L_ : ∀ {a} {A : Set a} → List A → List A → List A
[] ++L ys = ys
(x ∷ xs) ++L ys = x ∷ (xs ++L ys)

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

length : ∀ {a} {A : Set a} → List A → Nat
length [] = zero
length (_ ∷ xs) = suc (length xs)

_==N_ : Nat → Nat → Bool
zero ==N zero = true
zero ==N suc _ = false
suc _ ==N zero = false
suc n ==N suc m = n ==N m

_==S_ : String → String → Bool
_==S_ = primStringEquality

if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

data Fin : Nat → Set where
  fzero : ∀ {n} → Fin (suc n)
  fsuc : ∀ {n} → Fin n → Fin (suc n)

lookupFin : ∀ {a n} {A : Set a} → List A → Fin n → Maybe A
lookupFin [] i = nothing
lookupFin (x ∷ xs) fzero = just x
lookupFin (x ∷ xs) (fsuc i) = lookupFin xs i

lookupNat : ∀ {a} {A : Set a} → List A → Nat → Maybe A
lookupNat [] n = nothing
lookupNat (x ∷ xs) zero = just x
lookupNat (x ∷ xs) (suc n) = lookupNat xs n

memberString : String → List String → Bool
memberString x [] = false
memberString x (y ∷ ys) with x ==S y
... | true = true
... | false = memberString x ys

freshHint : String → List String → String
freshHint "" used = "x" ++ primShowNat (length used)
freshHint hint used with memberString hint used
... | false = hint
... | true = hint ++ primShowNat (length used)