From 2f324fc9e868e0775e1401833b74af15652c6732 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 12 Apr 2009 14:19:15 -0400 Subject: Classes as optional arguments to Basis.tag --- src/reduce_local.sml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/reduce_local.sml') diff --git a/src/reduce_local.sml b/src/reduce_local.sml index cf602406..265cb2a4 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -72,6 +72,11 @@ fun exp env (all as (e, loc)) = | EFfi _ => all | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) + | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _, + (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _), + t), _), e) => + (ECon (dk, pc, [t], SOME (exp env e)), loc) + | EApp (e1, e2) => let val e1 = exp env e1 @@ -84,6 +89,9 @@ fun exp env (all as (e, loc)) = | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) + | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) => + (ECon (dk, pc, [t], NONE), loc) + | ECApp (e, c) => (ECApp (exp env e, c), loc) | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) -- cgit v1.2.3