Move old implementation of FCU and start one with new syntax

src/Language/Lambda/FCU/Discharge.hs

@@ -2,19 +2,21 @@
 
 module Language.Lambda.FCU.Discharge where
 
-import Language.Lambda.FCU.Terms (Id, Term (..))
+import Language.Lambda.FCU.PPTerm ()
+import qualified Language.Lambda.FCU.FCUSyntax.Abs as Raw
 
 -- | Discharge a term by replacing all terms t in s with variables z.
-discharge :: [(Term, Id)] -> Term -> Term
+discharge :: [(Raw.Term, Raw.Id)] -> Raw.Term -> Raw.Term
 discharge th t = case lookup t th of
-  Just y -> O y
+  Just y -> Raw.OTerm y
   Nothing -> case t of
-    (x :.: t1) -> x :.: discharge th t1
-    (t1 :@ t2) -> discharge th t1 :@ discharge th t2
+    Raw.AbsTerm x t1 -> Raw.AbsTerm x (discharge th t1)
+    Raw.AppTerm t1 t2 -> Raw.AppTerm (discharge th t1) (discharge th t2)
     t -> t
 
--- >>> discharge [("Cons" :@ "x" :@ "y", "z")] ("Cons" :@ "x" :@ "y")
+-- >>> discharge [("Cons :@ x :@ y", "z")] "Cons :@ x :@ y"
 -- z
 
--- >>> discharge [("Fst" :@ "x", "z")] ("Cons" :@ ("Fst" :@ "x") :@ "w")
--- (Cons z) (w)
+
+-- >>> discharge [("Fst :@ x", "z")] "Cons :@ ( Fst :@ x ) :@ w"
+-- (Cons (z w))

src/Language/Lambda/FCU/Covers.hs → src/Language/Lambda/FCU/FCUImplSW/Covers.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Language.Lambda.FCU.Covers
+module Language.Lambda.FCU.FCUImplSW.Covers
   ( findCover,
     coverExists,
     CoverTest (..),
@@ -10,8 +10,8 @@ module Language.Lambda.FCU.Covers
 where
 
 import Data.Maybe (isJust)
-import Language.Lambda.FCU.RTerms (RTerm (..), toRTerm, toTerm)
-import Language.Lambda.FCU.Terms (Term (..))
+import Language.Lambda.FCU.FCUImplSW.RTerms (RTerm (..), toRTerm, toTerm)
+import Language.Lambda.FCU.FCUImplSW.Terms (Term (..))
 
 findCover :: [RTerm] -> RTerm -> Maybe RTerm
 findCover params r =

src/Language/Lambda/FCU/FCUImplSW/Discharge.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Language.Lambda.FCU.FCUImplSW.Discharge where
+
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..))
+
+-- | Discharge a term by replacing all terms t in s with variables z.
+discharge :: [(Term, Id)] -> Term -> Term
+discharge th t = case lookup t th of
+  Just y -> O y
+  Nothing -> case t of
+    (x :.: t1) -> x :.: discharge th t1
+    (t1 :@ t2) -> discharge th t1 :@ discharge th t2
+    t -> t
+
+-- >>> discharge [("Cons" :@ "x" :@ "y", "z")] ("Cons" :@ "x" :@ "y")
+-- z
+
+-- >>> discharge [("Fst" :@ "x", "z")] ("Cons" :@ ("Fst" :@ "x") :@ "w")
+-- (Cons z) (w)

src/Language/Lambda/FCU/Prune.hs → src/Language/Lambda/FCU/FCUImplSW/Prune.hs

@@ -1,13 +1,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.Prune where
+module Language.Lambda.FCU.FCUImplSW.Prune where
 
 import Data.List (elemIndex)
-import Language.Lambda.FCU.Covers (coverExists)
-import Language.Lambda.FCU.RTerms (RTerm (..), toRTerm)
-import Language.Lambda.FCU.Strip (strip)
-import Language.Lambda.FCU.Substitutions (Substitutions (..), devar, mkvars)
-import Language.Lambda.FCU.Terms (Id, Term (..), newMetaVarId, subset)
+import Language.Lambda.FCU.FCUImplSW.Covers (coverExists)
+import Language.Lambda.FCU.FCUImplSW.RTerms (RTerm (..), toRTerm)
+import Language.Lambda.FCU.FCUImplSW.Strip (strip)
+import Language.Lambda.FCU.FCUImplSW.Substitutions (Substitutions (..), devar, mkvars)
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..), newMetaVarId, subset)
 
 abst :: ([Id], Term) -> Term
 abst ([], t) = t

src/Language/Lambda/FCU/RTerms.hs → src/Language/Lambda/FCU/FCUImplSW/RTerms.hs

@@ -1,8 +1,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.RTerms (RTerm (..), toRTerm, toTerm, isRTerm) where
+module Language.Lambda.FCU.FCUImplSW.RTerms (RTerm (..), toRTerm, toTerm, isRTerm) where
 
-import Language.Lambda.FCU.Terms (Id, Term (..))
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..))
 
 data RTerm = RO Id | RConstructor Id | RApp RTerm RTerm
   deriving (Eq, Show)

src/Language/Lambda/FCU/Restrictions.hs → src/Language/Lambda/FCU/FCUImplSW/Restrictions.hs

@@ -1,10 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.Restrictions where
+module Language.Lambda.FCU.FCUImplSW.Restrictions where
 
-import Language.Lambda.FCU.RTerms (RTerm (..), isRTerm)
-import Language.Lambda.FCU.Substitutions (Substitutions)
-import Language.Lambda.FCU.Terms (Id, Term (..))
+import Language.Lambda.FCU.FCUImplSW.RTerms (RTerm (..), isRTerm)
+import Language.Lambda.FCU.FCUImplSW.Substitutions (Substitutions)
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..))
 
 -- >>> argumentRestriction ["X" :@ "a" :@ "b" :@ "c", "X" :@ "a" :@ "b" :@ "c"]
 -- False

src/Language/Lambda/FCU/FCUImplSW/Strip.hs

@@ -0,0 +1,31 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Language.Lambda.FCU.FCUImplSW.Strip where
+
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..))
+
+-- | Strip a term into a head and a list of arguments.
+strip :: Term -> (Term, [Term])
+strip (t1 :@ t2) =
+  let (h, rest) = strip t1
+   in (h, rest ++ [t2])
+strip t = (t, [])
+
+--- >>> strip ("X" :@ "y" :@ "z")
+-- (X,[y,z])
+
+--- >>> strip ("Cons" :@ "x" :@ ("y" :@ ("z" :.: "z")))
+-- (Cons,[x,y λz . (z)])
+
+-- | Combine a head term with arguments to reconstruct the original term
+unstrip :: (Term, [Term]) -> Term
+unstrip (head, args) = foldl (:@) head args
+
+-- >>> unstrip ("X", ["y", "z"])
+-- (W "X" :@ O "y") :@ O "z"
+
+-- >>> ("X" :@ "y" :@ "z")
+-- (W "X" :@ O "y") :@ O "z"
+
+-- >>> unstrip ("Cons", ["x", "y" :@ ("z" :.: "z")])
+-- (Constructor "Cons" :@ O "x") :@ (O "y" :@ ("z" :.: O "z"))

src/Language/Lambda/FCU/Substitutions.hs → src/Language/Lambda/FCU/FCUImplSW/Substitutions.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.Substitutions
+module Language.Lambda.FCU.FCUImplSW.Substitutions
   ( Substitutions (..),
     ppSubstitutions,
     devar,
@@ -11,7 +11,7 @@ module Language.Lambda.FCU.Substitutions
   )
 where
 
-import Language.Lambda.FCU.Terms (Id, Term (..))
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..))
 
 newtype Substitutions
   = Substitutions [(Id, Term)]

src/Language/Lambda/FCU/Terms.hs → src/Language/Lambda/FCU/FCUImplSW/Terms.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.Terms where
+module Language.Lambda.FCU.FCUImplSW.Terms where
 
 import Data.Char (isUpper)
 import Data.List (elemIndex)
@@ -50,7 +50,7 @@ ppTerm (f :@ x) = case f of
 -- >>> "Cons" :: Term
 -- Cons
 -- >>> "x" :.: ("Cons" :@ "x" :@ "y") :: Term
--- λx . ((Cons x) y)
+-- λx . ((Cons x) (y))
 
 isMeta :: Term -> Bool
 isMeta (W _) = True

src/Language/Lambda/FCU/Unification.hs → src/Language/Lambda/FCU/FCUImplSW/Unification.hs

@@ -1,17 +1,17 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Language.Lambda.FCU.Unification
+module Language.Lambda.FCU.FCUImplSW.Unification
   ( unify,
   )
 where
 
-import Language.Lambda.FCU.Discharge (discharge)
-import Language.Lambda.FCU.Prune (abst, eqsel, hnf, prune)
-import Language.Lambda.FCU.RTerms (RTerm (..), toRTerm)
-import Language.Lambda.FCU.Restrictions (argumentRestriction, globalRestriction, localRestriction)
-import Language.Lambda.FCU.Strip (strip, unstrip)
-import Language.Lambda.FCU.Substitutions (devar, mkvars, rename)
-import Language.Lambda.FCU.Terms (Id, Term (..), newMetaVarId, permutate, subset)
+import Language.Lambda.FCU.FCUImplSW.Discharge (discharge)
+import Language.Lambda.FCU.FCUImplSW.Prune (abst, eqsel, hnf, prune)
+import Language.Lambda.FCU.FCUImplSW.RTerms (RTerm (..), toRTerm)
+import Language.Lambda.FCU.FCUImplSW.Restrictions (argumentRestriction, globalRestriction, localRestriction)
+import Language.Lambda.FCU.FCUImplSW.Strip (strip, unstrip)
+import Language.Lambda.FCU.FCUImplSW.Substitutions (devar, mkvars, rename)
+import Language.Lambda.FCU.FCUImplSW.Terms (Id, Term (..), newMetaVarId, permutate, subset)
 
 ----- Unification ----- bvs (th (s,t)) = Q, (theta, S)
 unify :: [(Char, Id)] -> ([(Id, Term)], (Term, Term)) -> [(Id, Term)]

src/Language/Lambda/FCU/FCUSyntax/Abs.hs

@@ -1,7 +1,10 @@
 -- Haskell data types for the abstract syntax.
 -- Generated by the BNF converter.
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Language.Lambda.FCU.FCUSyntax.Abs where
+import Data.String (IsString (fromString))
 
 newtype Id = Id String
   deriving (Eq, Ord, Show, Read)
@@ -18,5 +21,8 @@ data Term
     | CTerm ConstructorId
     | AppTerm Term Term
     | AbsTerm Id Term
-  deriving (Eq, Ord, Show, Read)
+  deriving (Eq, Ord, Read)
 
+instance IsString Id where
+    fromString :: String -> Id
+    fromString = Id

src/Language/Lambda/FCU/PPTerm.hs

@@ -0,0 +1,36 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Language.Lambda.FCU.PPTerm where
+
+import Data.String
+import qualified Language.Lambda.FCU.FCUSyntax.ErrM as Raw
+import qualified Language.Lambda.FCU.FCUSyntax.Abs as Raw
+import qualified Language.Lambda.FCU.FCUSyntax.Par as Raw
+
+
+showRaw :: Raw.Term -> String
+showRaw term = case term of
+    Raw.WTerm (Raw.MetavarId x) -> x
+    Raw.OTerm (Raw.Id x) -> x
+    Raw.CTerm (Raw.ConstructorId x) -> x
+    Raw.AppTerm t1 t2 -> addParens $ showRaw t1 ++ " " ++ showRaw t2
+    Raw.AbsTerm (Raw.Id x) t -> "λ" ++ x ++ " . " ++ showRaw t
+  where
+    addParens s = "(" ++ s ++ ")"
+
+instance Show Raw.Term where
+    show :: Raw.Term -> String
+    show = showRaw
+
+instance IsString Raw.Term where
+    fromString :: String -> Raw.Term
+    fromString s = case Raw.pTerm . Raw.myLexer $ s of
+        Raw.Ok term -> term
+        Raw.Bad err -> error $ "Parse error: " ++ err
+
+-- >>> Raw.AppTerm (Raw.AppTerm (Raw.CTerm (Raw.ConstructorId "Cons")) (Raw.OTerm (Raw.Id "x"))) (Raw.OTerm (Raw.Id "y"))
+-- ((Cons x) y)
+
+
+-- >>> "X" :: Raw.Term
+-- X

src/Language/Lambda/FCU/Parse.hs

@@ -6,7 +6,7 @@ import qualified Language.Lambda.FCU.FCUSyntax.Lex as Raw
 import qualified Language.Lambda.FCU.FCUSyntax.Layout as Raw
 import qualified Language.Lambda.FCU.FCUSyntax.Print as Raw
 import qualified Language.Lambda.FCU.FCUSyntax.ErrM as Raw
-import Language.Lambda.FCU.Terms
+import Language.Lambda.FCU.FCUImplSW.Terms ( Term(..) ) 
 import qualified Control.Applicative as Raw
 
 
@@ -25,5 +25,5 @@ convertTerm term = case term of
     Raw.AppTerm t1 t2 -> convertTerm t1 :@ convertTerm t2
     Raw.AbsTerm (Raw.Id x) t -> x :.: convertTerm t
 
--- >>> parseTerm "xy :@ y"
--- Right xy y
+-- >>> parseTerm "( f :@ a ) :@ ( x :.: y )"
+-- Right (f a) (λx . (y))

src/Language/Lambda/FCU/Strip.hs

@@ -2,30 +2,33 @@
 
 module Language.Lambda.FCU.Strip where
 
-import Language.Lambda.FCU.Terms (Id, Term (..))
+import Language.Lambda.FCU.PPTerm ()
+import qualified Language.Lambda.FCU.FCUSyntax.Abs as Raw
 
 -- | Strip a term into a head and a list of arguments.
-strip :: Term -> (Term, [Term])
-strip (t1 :@ t2) =
+strip :: Raw.Term -> (Raw.Term, [Raw.Term])
+strip (Raw.AppTerm t1 t2) =
   let (h, rest) = strip t1
    in (h, rest ++ [t2])
 strip t = (t, [])
 
---- >>> strip ("X" :@ "y" :@ "z")
--- (X,[y,z])
+--- >>> strip ("X :@ y :@ z")
+-- (X,[(y z)])
 
---- >>> strip ("Cons" :@ "x" :@ ("y" :@ ("z" :.: "z")))
--- (Cons,[x,y λz . (z)])
+--- >>> strip ("Cons :@ x :@ ( y :@ ( z :.: z ) )")
+-- (Cons,[(x (y λz . z))])
 
 -- | Combine a head term with arguments to reconstruct the original term
-unstrip :: (Term, [Term]) -> Term
-unstrip (head, args) = foldl (:@) head args
+unstrip :: (Raw.Term, [Raw.Term]) -> Raw.Term
+unstrip (head, args) = case args of
+    [] -> head
+    _ -> Raw.AppTerm head (foldl1 Raw.AppTerm args)
 
 -- >>> unstrip ("X", ["y", "z"])
--- (W "X" :@ O "y") :@ O "z"
+-- (X (y z))
 
--- >>> ("X" :@ "y" :@ "z")
--- (W "X" :@ O "y") :@ O "z"
+-- >>> "X :@ y :@ z" :: Raw.Term
+-- (X (y z))
 
--- >>> unstrip ("Cons", ["x", "y" :@ ("z" :.: "z")])
--- (Constructor "Cons" :@ O "x") :@ (O "y" :@ ("z" :.: O "z"))
+-- >>> unstrip ("Cons", ["x", "y :@ ( z :.: z )"])
+-- (Cons (x (y λz . z)))