From b9b67597324deb6e6dfc8ef33c60c110abc2af7b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 8 Aug 2008 17:55:51 -0400 Subject: Specialization of single-parameter datatypes --- src/core_env.sml | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/core_env.sml') 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 -- cgit v1.2.3