Move transfer into the GF repo.

15 files changed, 332 insertions, 0 deletions

diff --git a/transfer/Makefile b/transfer/Makefile
new file mode 100644
index 000000000..5c2e68362
--- /dev/null
+++ b/transfer/Makefile
@@ -0,0 +1,50 @@
+SRCDIR=../src
+
+GHC=ghc
+GHCFLAGS=-i$(SRCDIR)
+
+
+.PHONY: all bnfc bnfctest doc docclean clean bnfcclean distclean
+
+all:
+	$(GHC) $(GHCFLAGS) --make -o run_core run_core.hs
+	$(GHC) $(GHCFLAGS) --make -o compile_to_core compile_to_core.hs
+
+bnfc: bnfcclean
+	cd $(SRCDIR) && bnfc -gadt -d -p Transfer Transfer/Core/Core.cf
+	perl -i -pe 's/^import Transfer.Core.ErrM/import Transfer.ErrM/' $(SRCDIR)/Transfer/Core/*.{hs,x,y}
+	-rm -f $(SRCDIR)/Transfer/Core/ErrM.hs
+	cd $(SRCDIR) && alex -g Transfer/Core/Lex.x
+	cd $(SRCDIR) && happy -gca Transfer/Core/Par.y
+	cd $(SRCDIR) && bnfc -gadt -d -p Transfer Transfer/Syntax/Syntax.cf
+	perl -i -pe 's/^import Transfer.Syntax.ErrM/import Transfer.ErrM/' $(SRCDIR)/Transfer/Syntax/*.{hs,x,y}
+	-rm -f $(SRCDIR)/Transfer/Syntax/ErrM.hs
+	cd $(SRCDIR) && alex -g Transfer/Syntax/Lex.x
+	cd $(SRCDIR) && happy -gca Transfer/Syntax/Par.y
+
+bnfctest:
+	ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Core/Test.hs -o test_core
+	ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Syntax/Test.hs -o test_syntax
+	ghc $(GHCFLAGS) --make $(SRCDIR)/Transfer/Syntax/ResolveLayout.hs -o test_layout
+
+doc:
+	(cd $(SRCDIR)/Transfer/Core/; latex Doc.tex; dvips Doc.dvi -o Doc.ps)
+	(cd $(SRCDIR)/Transfer/Syntax/; latex Doc.tex; dvips Doc.dvi -o Doc.ps)
+
+docclean:
+	-rm -f $(SRCDIR)/Transfer/Core/*.{log,aux,dvi,ps}
+	-rm -f $(SRCDIR)/Transfer/Syntax/*.{log,aux,dvi,ps}
+
+clean:
+	-rm -f *.o *.hi
+	find $(SRCDIR)/Transfer -name '*.o' -o -name '*.hi' | xargs rm -f
+	-rm -f run_core	
+	-rm -f compile_to_core
+	-rm -f test_core test_syntax test_layout
+
+bnfcclean: 
+	-rm -f $(SRCDIR)/Transfer/Core/{Doc,Lex,Par,Layout,Skel,Print,Test,Abs}.*
+	-rm -f $(SRCDIR)/Transfer/Syntax/{Doc,Lex,Par,Layout,Skel,Print,Test,Abs}.*
+
+distclean: clean bnfcclean
+
diff --git a/transfer/TODO b/transfer/TODO
new file mode 100644
index 000000000..2fb8f6260
--- /dev/null
+++ b/transfer/TODO
@@ -0,0 +1,57 @@
+* Improve front-end language
+
+- Tuple syntax in expressions, types and patterns. Implemented with records.
+
+- List syntax in expressions, types and patterns. Implemented with List.
+
+- operators for primitive string operations: 
+
+- list operators: ++, :
+
+- overloaded operators?
+
+- implicit arguments?
+
+- layout syntax?
+
+- composOp generation
+
+- show generation
+
+- eq generation
+
+- better module system
+
+- Disjunctive patterns
+
+- Negated patterns?
+
+- Fix BNFC layout resolver to not insert double ; (instead of removing them)
+
+* Improve interpreter
+
+- More efficient handling of constructor application
+
+* Improve interpreter API
+
+- Allow passing terms as some structured type.
+
+* Improve the core language
+
+* Improve compilation
+
+- Eta-expand constructor applications and use the core feature for them.
+
+* Add primitive operations to core
+
+- primitive operations on strings:
+
+- add floating-point numbers with primitive oeprations?
+
+* Implement module system in interpreter
+
+* Add type checker for core
+
+* Add friendly type checker for front-end language
+
+* Add termination checker
diff --git a/transfer/compile_to_core.hs b/transfer/compile_to_core.hs
new file mode 100644
index 000000000..1f9ea746b
--- /dev/null
+++ b/transfer/compile_to_core.hs
@@ -0,0 +1,52 @@
+module Main where
+
+import Transfer.Syntax.Lex
+import Transfer.Syntax.Par
+import Transfer.Syntax.Print
+import Transfer.Syntax.Abs
+import Transfer.Syntax.Layout
+
+import Transfer.ErrM
+import Transfer.SyntaxToCore
+
+import Transfer.PathUtil
+
+import System.Environment
+import System.Exit
+import System.IO
+
+import Debug.Trace
+
+myLLexer = resolveLayout True . myLexer
+
+compile :: Monad m => [Decl] -> m String
+compile m = return (printTree $ declsToCore m)
+
+loadModule :: FilePath -> IO [Decl]
+loadModule f = 
+    do
+    s <- readFile f
+    Module is ds <- case pModule (myLLexer s) of
+                     Bad e    -> die $ "Parse error in " ++ f ++ ": " ++ e
+                     Ok  m    -> return m 
+    let dir = directoryOf f
+        deps = [ replaceFilename f i ++ ".tr" | Import (Ident i) <- is ]
+    dss <- mapM loadModule deps
+    return $ concat (ds:dss)
+
+die :: String -> IO a
+die s = do
+        hPutStrLn stderr s
+        exitFailure
+
+coreFile :: FilePath -> FilePath
+coreFile f = replaceFilenameSuffix f "trc"
+
+compileFile :: FilePath -> IO String
+compileFile f = loadModule f >>= compile
+
+main :: IO ()
+main = do args <- getArgs
+          case args of
+            [f] -> compileFile f >>= writeFile (coreFile f)
+            _   -> die "Usage: compile_to_core <file>"
diff --git a/transfer/examples/array.tr b/transfer/examples/array.tr
new file mode 100644
index 000000000..7dcf6d443
--- /dev/null
+++ b/transfer/examples/array.tr
@@ -0,0 +1,10 @@
+import nat ;
+
+data Array : Type -> Nat -> Type where {
+   Empty : (A:Type) -> Array A Zero ;
+   Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n) ;
+ } ;
+
+mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n ;
+mapA A B _ f (Empty _) = Empty B ;
+mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs) ;
diff --git a/transfer/examples/bool.tr b/transfer/examples/bool.tr
new file mode 100644
index 000000000..291434a9f
--- /dev/null
+++ b/transfer/examples/bool.tr
@@ -0,0 +1,8 @@
+data Bool : Type where { True : Bool; False : Bool; } ;
+
+depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B ;
+depif _ _ True x _ = x ;
+depif _ _ False _ y = y ;
+
+not : Bool -> Bool ;
+not b = if b then False else True ;
diff --git a/transfer/examples/exp.tr b/transfer/examples/exp.tr
new file mode 100644
index 000000000..b7202fedf
--- /dev/null
+++ b/transfer/examples/exp.tr
@@ -0,0 +1,31 @@
+data Stm : Type where {} ;
+data Exp : Type where {} ;
+data Var : Type where {} ;
+data Typ : Type where {} ;
+
+data ListStm : Type where {} ;
+
+data Tree : Type -> Type where {
+  SDecl   : Tree Typ -> Tree Var -> Tree Stm ;
+  SAss    : Tree Var -> Tree Exp -> Tree Stm ;
+  SBlock  : Tree ListStm -> Tree Stm ;
+  EAdd    : Tree Exp -> Tree Exp -> Tree Exp ;
+  EStm    : Tree Stm -> Tree Exp ;
+  EVar    : Tree Var -> Tree Exp ;
+  EInt    : Integer -> Tree Exp ;
+  V       : String -> Tree Var ;
+  TInt    : Tree Typ ;
+  TFloat  : Tree Typ ;
+
+  NilStm  : Tree ListStm ;
+  ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm ;
+ } ;
+
+derive composOp Tree ;
+
+rename : (String -> String) -> (C : Type) -> Tree C -> Tree C;
+rename f C t = case t of {
+		   V x -> V (f x) ;
+		   _ -> composOp_Tree C (rename f) t;
+                 } ;
+
diff --git a/transfer/examples/fib.tr b/transfer/examples/fib.tr
new file mode 100644
index 000000000..91bb69ed7
--- /dev/null
+++ b/transfer/examples/fib.tr
@@ -0,0 +1,11 @@
+import nat ;
+
+fib : Int -> Int ;
+fib 0 = 1 ;
+fib 1 = 1 ;
+fib n = fib (n-1) + fib (n-2) ;
+
+fibNat : Nat -> Nat ;
+fibNat Zero = Succ Zero ;
+fibNat (Succ Zero) = Succ Zero ;
+fibNat (Succ (Succ n)) = plus (fibNat (Succ n)) (fibNat n) ;
\ No newline at end of file
diff --git a/transfer/examples/layout.tr b/transfer/examples/layout.tr
new file mode 100644
index 000000000..15f0aac3a
--- /dev/null
+++ b/transfer/examples/layout.tr
@@ -0,0 +1,5 @@
+x : Apa
+x = let x : T = y 
+     in case y of
+         f -> q
+         _ -> a
diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr
new file mode 100644
index 000000000..f31278f54
--- /dev/null
+++ b/transfer/examples/list.tr
@@ -0,0 +1,17 @@
+import nat ;
+
+data List : (_:Type) -> Type where 
+	{ Nil : (A:Type) -> List A ;
+          Cons : (A:Type) -> A -> List A -> List A ; } ;
+
+size : (A:Type) -> List A -> Nat ;
+size _ (Nil _) = Zero ;
+size A (Cons _ x xs) = Succ (size A xs) ;
+
+map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B ;
+map _ B _ (Nil _) = Nil B ;
+map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs) ;
+
+append : (A:Type) -> (xs:List A) -> List A -> List A ;
+append _ (Nil _) ys = ys ;
+append A (Cons _ x xs) ys = Cons A x (append A xs ys) ;
diff --git a/transfer/examples/nat.tr b/transfer/examples/nat.tr
new file mode 100644
index 000000000..f67dc55ce
--- /dev/null
+++ b/transfer/examples/nat.tr
@@ -0,0 +1,23 @@
+data Nat : Type where { 
+	Zero : Nat ;
+  	Succ : (n:Nat) -> Nat ;
+ } ;
+
+plus : Nat -> Nat -> Nat ;
+plus Zero y = y ;
+plus (Succ x) y = Succ (plus x y) ;
+
+pred : Nat -> Nat ;
+pred Zero = Zero ;
+pred (Succ n) = n ;
+
+natToInt : Nat -> Int ;
+natToInt Zero = 0 ;
+natToInt (Succ n) = 1 + natToInt n ;
+
+plus : Nat -> Nat -> Nat ;
+plus Zero y = y ;
+plus (Succ x) y = Succ (plus x y) ;
+
+intToNat : Int -> Nat ;
+intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) ;
diff --git a/transfer/examples/pair.tr b/transfer/examples/pair.tr
new file mode 100644
index 000000000..07182e301
--- /dev/null
+++ b/transfer/examples/pair.tr
@@ -0,0 +1,11 @@
+Pair : Type -> Type -> Type ;
+Pair A B = { p1 : A; p2 : B } ;
+
+pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B ;
+pair _ _ x y = { p1 = x; p2 = y } ;
+
+fst : (A:Type) -> (B:Type) -> Pair A B -> A ;
+fst _ _ p = case p of { (Pair _ _ x _) -> x } ;
+
+snd : (A:Type) -> (B:Type) -> Pair A B -> B ;
+snd _ _ p = case p of { (Pair _ _ x _) -> x } ;
diff --git a/transfer/examples/prelude.tr b/transfer/examples/prelude.tr
new file mode 100644
index 000000000..a7e7443a1
--- /dev/null
+++ b/transfer/examples/prelude.tr
@@ -0,0 +1,5 @@
+const : (A:Type) -> (B:Type) -> A -> B -> A ;
+const _ _ x _ = x ;
+
+id : (A:Type) -> A -> A ;
+id A x = x ;
\ No newline at end of file
diff --git a/transfer/examples/prim.tr b/transfer/examples/prim.tr
new file mode 100644
index 000000000..fe0d32eac
--- /dev/null
+++ b/transfer/examples/prim.tr
@@ -0,0 +1,23 @@
+--
+-- Primitives
+--
+
+
+String : Type ;
+
+Int : Type ;
+
+prim_add_Int : (_:Int) -> (_:Int) -> Int ;
+prim_sub_Int : (_:Int) -> (_:Int) -> Int ;
+prim_mul_Int : (_:Int) -> (_:Int) -> Int ;
+prim_div_Int : (_:Int) -> (_:Int) -> Int ;
+prim_mod_Int : (_:Int) -> (_:Int) -> Int ;
+
+prim_neg_Int : (_:Int) -> Int ;
+
+prim_lt_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_le_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_gt_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_ge_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_eq_Int : (_:Int) -> (_:Int) -> Bool ;
+prim_ne_Int : (_:Int) -> (_:Int) -> Bool ;
diff --git a/transfer/examples/test.tr b/transfer/examples/test.tr
new file mode 100644
index 000000000..50aa638b4
--- /dev/null
+++ b/transfer/examples/test.tr
@@ -0,0 +1,3 @@
+import nat ;
+
+main = natToInt (intToNat 100) ;
\ No newline at end of file
diff --git a/transfer/run_core.hs b/transfer/run_core.hs
new file mode 100644
index 000000000..1d0457acd
--- /dev/null
+++ b/transfer/run_core.hs
@@ -0,0 +1,26 @@
+import Transfer.InterpreterAPI
+
+import Data.List (partition, isPrefixOf)
+import System.Environment (getArgs)
+
+interpretLoop :: Env -> IO ()
+interpretLoop env = do    
+                    line <- getLine
+                    r <- evaluateString env line
+                    putStrLn r
+                    interpretLoop env
+
+runMain :: Env -> IO ()
+runMain env = do
+              r <- evaluateString env "main"
+              putStrLn r
+
+main :: IO ()
+main = do args <- getArgs
+          let (flags,files) = partition ("-" `isPrefixOf`) args
+          env <- case files of
+            [f] -> loadFile f
+            _   -> fail "Usage: run_core [-i] <file>"
+          if "-i" `elem` flags 
+            then interpretLoop env
+            else runMain env