summaryrefslogtreecommitdiff
path: root/src/expl.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 16:28:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 16:28:55 -0400
commit16d3d1c3a6d1e78faab91076c20b76fdcb90edb9 (patch)
treeef54b557b346fa95b4322478bf5fbec431944f18 /src/expl.sml
parentd668886a45158cf3a292fdef3fa81498efd77652 (diff)
Case through explify
Diffstat (limited to 'src/expl.sml')
-rw-r--r--src/expl.sml15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/expl.sml b/src/expl.sml
index 183dbc31..52dbee63 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -59,6 +59,19 @@ datatype con' =
withtype con = con' located
+datatype patCon =
+ PConVar of int
+ | PConProj of int * string list * string
+
+datatype pat' =
+ PWild
+ | PVar of string
+ | PPrim of Prim.t
+ | PCon of patCon * pat option
+ | PRecord of (string * pat) list
+
+withtype pat = pat' located
+
datatype exp' =
EPrim of Prim.t
| ERel of int
@@ -74,6 +87,8 @@ datatype exp' =
| ECut of exp * con * { field : con, rest : con }
| EFold of kind
+ | ECase of exp * (pat * exp) list * con
+
| EWrite of exp
withtype exp = exp' located