module Nehemiah.Syntax.Term where
open import Nehemiah.Syntax.Type
open import Data.Integer
import Parametric.Syntax.Term Base as Term
data Const : Term.Structure where
intlit-const : (n : ℤ) → Const ∅ int
add-const : Const (int • int • ∅) int
minus-const : Const (int • ∅) (int)
empty-const : Const ∅ (bag)
insert-const : Const (int • bag • ∅) (bag)
union-const : Const (bag • bag • ∅) (bag)
negate-const : Const (bag • ∅) (bag)
flatmap-const : Const ((int ⇒ bag) • bag • ∅) (bag)
sum-const : Const (bag • ∅) (int)
open Term.Structure Const public
pattern intlit n = const (intlit-const n) ∅
pattern add s t = const add-const (s • t • ∅)
pattern minus t = const minus-const (t • ∅)
pattern empty = const empty-const ∅
pattern insert s t = const insert-const (s • t • ∅)
pattern union s t = const union-const (s • t • ∅)
pattern negate t = const negate-const (t • ∅)
pattern flatmap s t = const flatmap-const (s • t • ∅)
pattern sum t = const sum-const (t • ∅)