Transfer: added support for disjunctive patterns.

2 files changed, 47 insertions, 0 deletions

diff --git a/transfer/README b/transfer/README
new file mode 100644
index 000000000..ed31ae3f9
--- /dev/null
+++ b/transfer/README
@@ -0,0 +1,23 @@
+Some features of the Transfer language:
+
+* Purely functional
+* Dependent types
+* Eager evaluation
+* Generalized algebraic datatypes
+* Metavariables
+* Records with subtyping
+* Overloading by explicit dictionary passing
+* Pattern matching by case expressions
+
+Additional features in the front-end language:
+
+* Disjunctive patterns
+* do-notation
+* Hidden arguments (not implemented yet)
+* Automatic derivation of some operations on user-defined GADTs:
+  - Compositional maps and folds
+  - Equality
+  - Ordering
+  - Showing
+* Pattern equations
+* Operator syntax for common functions, most are overloaded
diff --git a/transfer/examples/disjpatt.tr b/transfer/examples/disjpatt.tr
new file mode 100644
index 000000000..740e08a7b
--- /dev/null
+++ b/transfer/examples/disjpatt.tr
@@ -0,0 +1,24 @@
+data Cat : Type where
+    VarOrWild : Cat
+    Exp : Cat
+    Ident : Cat
+
+data Tree : Cat -> Type where
+    EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp
+    EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp
+    EVar : Tree Ident -> Tree Exp
+    EType : Tree Exp
+    EStr : String -> Tree Exp
+    EInt : Integer -> Tree Exp
+    VVar : Tree Ident -> Tree VarOrWild
+    VWild : Tree VarOrWild
+    Ident : String -> Tree Ident
+
+
+f e = case e of
+       EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e
+       Ident i -> Ident i
+       _ -> catchAll
+
+
+g (Ident x || EAbs (VWild || VVar _) t e) = x e
\ No newline at end of file