diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-08-08 17:55:51 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-08 17:55:51 -0400 |
commit | b9b67597324deb6e6dfc8ef33c60c110abc2af7b (patch) | |
tree | 2ff5f7417692c2590916a6eeb55aa38bbb47516f /src/core_env.sml | |
parent | e2a9136ed7123cb8e5cac4a20cbce5467643ecd6 (diff) |
Specialization of single-parameter datatypes
Diffstat (limited to 'src/core_env.sml')
-rw-r--r-- | src/core_env.sml | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/core_env.sml b/src/core_env.sml index 5b7cfa2e..d59e3d3d 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -51,6 +51,19 @@ val liftConInCon = val lift = liftConInCon 0 +val subConInCon = + U.Con.mapB {kind = fn k => k, + con = fn (xn, rep) => fn c => + case c of + CRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => CRel (xn' - 1) + | LESS => c) + | _ => c, + bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) @@ -175,4 +188,13 @@ fun declBinds env (d, loc) = | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env +fun patBinds env (p, loc) = + case p of + PWild => env + | PVar (x, t) => pushERel env x t + | PPrim _ => env + | PCon (_, _, _, NONE) => env + | PCon (_, _, _, SOME p) => patBinds env p + | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps + end |