Define first-order terms.

1 files changed, 171 insertions, 0 deletions

diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
new file mode 100644
index 0000000..c8da5d9
--- /dev/null
+++ b/src/Soat/FirstOrder/Term.idr
@@ -0,0 +1,171 @@
+module Soat.FirstOrder.Term
+
+import Control.Relation
+
+import Soat.Data.Product
+import Soat.FirstOrder.Algebra
+import Soat.FirstOrder.Signature
+import Soat.Relation
+
+%default total
+%hide Control.Relation.Equivalence
+
+public export
+data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
+  Done : (i : x t) -> Term sig x t
+  Call : (op : Op sig t) -> (ts : Term sig x ^ op.arity) -> Term sig x t
+
+Environment : {a : Type} -> (x, y : a -> Type) -> Type
+Environment {a} x y = (t : a) -> x t -> y t
+
+record SetoidEnvironment {a : Type} (x, y : ISetoid a) where
+  f    : Environment {a} x.U y.U
+  cong : (t : a) -> {u, v : x.U t} -> x.rel t u v -> y.rel t (f t u) (f t v)
+
+public export
+bindTerm : {auto a : RawAlgebra sig}
+  -> Environment x a.U -> {t : _} -> Term sig x t -> a.U t
+
+public export
+bindTerms : {auto a : RawAlgebra sig}
+  -> Environment x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts
+
+bindTerm         env (Done i)     = env _ i
+bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
+
+bindTerms env []        = []
+bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
+
+public export
+bindTermsIsMap : {auto a : RawAlgebra sig}
+  -> (env : Environment x a.U) -> {ts : _} -> (tms : Term sig x ^ ts)
+  -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
+bindTermsIsMap env []        = Refl
+bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
+
+namespace Rel
+  public export
+  data (~=~) : forall x . (0 r : IRel x) -> IRel (Term sig x)
+    where
+    Done' : {0 x : sig.T -> Type} -> {0 r : IRel x}
+      -> {t : sig.T} -> {i, j : x t}
+      -> r t i j
+      -> (~=~) {sig = sig} {x = x} r t (Done i) (Done j)
+    Call' : {0 x : sig.T -> Type} -> {0 r : IRel x}
+      -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig x ^ op.arity}
+      -> Pointwise ((~=~) {sig = sig} {x = x} r) tms tms'
+      -> (~=~) {sig = sig} {x = x} r t (Call op tms) (Call op tms')
+
+  tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+    -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
+
+  tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+    -> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
+
+  tmRelRefl refl (Done i)     = Done' reflexive
+  tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
+
+  tmsRelRefl refl []        = []
+  tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
+
+  tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+    -> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
+
+  tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+    -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
+    -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
+
+  tmRelSym sym (Done' i)     = Done' (symmetric i)
+  tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)
+
+  tmsRelSym sym []        = []
+  tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
+
+  tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+    -> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
+    -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
+
+  tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+    -> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
+    -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
+    -> Pointwise ((~=~) rel) tms tms''
+
+  tmRelTrans trans (Done' i)     (Done' j)     = Done' (transitive i j)
+  tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')
+
+  tmsRelTrans trans []        []          = []
+  tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
+
+  export
+  tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
+    -> IEquivalence _ ((~=~) {sig = sig} {x = V} rel)
+  tmRelEq eq t = MkEquivalence
+    (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
+    (MkSymmetric $ tmRelSym (\t => (eq t).sym))
+    (MkTransitive $ tmRelTrans (\t => (eq t).trans))
+
+public export
+Free : (0 V : sig.T -> Type) -> RawAlgebra sig
+Free v = MakeRawAlgebra (Term sig v) Call
+
+public export
+FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.rel)
+FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
+
+public export
+FreeAlgebra : ISetoid sig.T -> Algebra sig
+FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
+
+public export 0
+bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
+  -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.rel t tm tm'
+  -> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm')
+
+public export 0
+bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
+  -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.rel) tms tms'
+  -> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms')
+
+bindTermCong         env (Done' i)     = env.cong _ i
+bindTermCong {a = a} env (Call' op ts) = a.algebra.semCong op (bindTermsCong env ts)
+
+bindTermsCong env                                    []        = []
+bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) =
+  bindTermCong env t :: bindTermsCong env ts
+
+public export
+bindHomo : (a : Algebra sig) -> (env : SetoidEnvironment v a.setoid)
+  -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.f)
+bindHomo a env = MkIsHomomorphism
+  (\t, eq => bindTermCong env eq)
+  (\op, tms =>
+      a.algebra.semCong op $
+      map (\t => (a.algebra.equivalence t).equalImpliesEq) $
+      equalImpliesPwEq $
+      bindTermsIsMap {a = a.raw} env.f tms)
+
+public export
+bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a
+bind env = MkHomomorphism _ (bindHomo _ env)
+
+public export 0
+bindUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+  -> (f : Homomorphism (FreeAlgebra v) a)
+  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
+  -> {t : sig.T} -> (tm : Term sig v.U t)
+  -> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm)
+
+public export 0
+bindsUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+  -> (f : Homomorphism (FreeAlgebra v) a)
+  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
+  -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
+  -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.f tms)
+
+bindUnique env f fDone (Done i)     = fDone i
+bindUnique env f fDone (Call op ts) = (a.algebra.equivalence _).transitive
+  (f.homo.semHomo op ts)
+  (a.algebra.semCong op $ bindsUnique env f fDone ts)
+
+bindsUnique env f fDone []        = []
+bindsUnique env f fDone (t :: ts) = bindUnique env f fDone t :: bindsUnique env f fDone ts