TypedLogic

TypedLogic.idr

module TypedLogic

import Data.SortedMap

data LType : Type where
  FreshType : LType
  Atom : String -> LType
  DisjUnion : LType -> LType -> LType
  Relation : (Vect n LType) -> LType

total confirmEq : Eq a => Vect n a -> Vect m a -> Bool
confirmEq [] [] = True
confirmEq (x::xs) (y::ys) = x == y && (confirmEq xs ys)
confirmEq _ _ = False

instance Eq LType where
  FreshType == FreshType = True
  (Atom s) == (Atom t) = s == t
  (DisjUnion x y) == (DisjUnion x' y') = x == y && x' == y'
  (Relation ts) == (Relation us) = confirmEq ts us
  _ == _ = False

-- -----------
-- atom : Atom

-- x_1..x_i : t_1..t_i, s : Atom
-- ----------
-- s(x_1..x_i) : Relation t_1..t_i

-- A compile time proof representing type unification between t, u resulting in r.
typeUnify : LType -> LType -> Maybe LType
typeUnify (Atom s) (Atom s') =
  case s == s' of
    False => Nothing
    True  => Just (Atom s)
typeUnify FreshType t = Just t
typeUnify t FreshType = Just t
typeUnify (Relation ts) (Relation us) =
  if confirmEq ts us then Just (Relation ts) else Nothing

typeUnify _ _ = Nothing
data Term : LType -> Type where
  AnAtom : (s: String) -> Term (Atom s)
  Var : Term FreshType
  Functor : String -> (ts: Vect n LType) -> Term (Relation ts)
  Unify : { auto p: typeUnify t u = Just r } -> Term t -> Term u -> Term r
  -- Conj : Term _ -> Term t -> Term t
  -- Disj : Term t -> Term u -> Term (DisjUnion t u)

-- data Predicates : LType -> Type where
--  And : Term t -> Predicates u -> Predicates [
--  Conj : Term -> Predicates
-- data Clause : LType -> Type where
  -- MkClause : (body: