comparison src/reduce_local.sml @ 721:9864b64b1700

Classes as optional arguments to Basis.tag
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 14:19:15 -0400
parents f152f215a02c
children 8688e01ae469
comparison
equal deleted inserted replaced
720:acb8537f58f0 721:9864b64b1700
70 | ENamed _ => all 70 | ENamed _ => all
71 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc) 71 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
72 | EFfi _ => all 72 | EFfi _ => all
73 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) 73 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
74 74
75 | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
76 (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
77 t), _), e) =>
78 (ECon (dk, pc, [t], SOME (exp env e)), loc)
79
75 | EApp (e1, e2) => 80 | EApp (e1, e2) =>
76 let 81 let
77 val e1 = exp env e1 82 val e1 = exp env e1
78 val e2 = exp env e2 83 val e2 = exp env e2
79 in 84 in
81 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b 86 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
82 | _ => (EApp (e1, e2), loc) 87 | _ => (EApp (e1, e2), loc)
83 end 88 end
84 89
85 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) 90 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
91
92 | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
93 (ECon (dk, pc, [t], NONE), loc)
86 94
87 | ECApp (e, c) => (ECApp (exp env e, c), loc) 95 | ECApp (e, c) => (ECApp (exp env e, c), loc)
88 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) 96 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
89 97
90 | EKApp (e, k) => (EKApp (exp env e, k), loc) 98 | EKApp (e, k) => (EKApp (exp env e, k), loc)