Mercurial > urweb
diff src/elab_util.sml @ 329:eec65c11d3e2
foldTR2
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 13 Sep 2008 10:30:45 -0400 |
| parents | 42dfb0d61cf0 |
| children | 9601c717d2f3 |
line wrap: on
line diff
--- a/src/elab_util.sml Thu Sep 11 19:59:31 2008 -0400 +++ b/src/elab_util.sml Sat Sep 13 10:30:45 2008 -0400 @@ -96,7 +96,7 @@ datatype binder = Rel of string * Elab.kind - | Named of string * Elab.kind + | Named of string * int * Elab.kind fun mapfoldB {kind = fk, con = fc, bind} = let @@ -240,7 +240,7 @@ datatype binder = RelC of string * Elab.kind - | NamedC of string * Elab.kind + | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con @@ -392,7 +392,7 @@ datatype binder = RelC of string * Elab.kind - | NamedC of string * Elab.kind + | NamedC of string * int * Elab.kind | Str of string * Elab.sgn | Sgn of string * Elab.sgn @@ -479,14 +479,14 @@ SgnConst sgis => S.map2 (ListUtil.mapfoldB (fn (ctx, si) => (case #1 si of - SgiConAbs (x, _, k) => - bind (ctx, NamedC (x, k)) - | SgiCon (x, _, k, _) => - bind (ctx, NamedC (x, k)) + SgiConAbs (x, n, k) => + bind (ctx, NamedC (x, n, k)) + | SgiCon (x, n, k, _) => + bind (ctx, NamedC (x, n, k)) | SgiDatatype (x, n, _, xncs) => - bind (ctx, NamedC (x, (KType, loc))) - | SgiDatatypeImp (x, _, _, _, _, _, _) => - bind (ctx, NamedC (x, (KType, loc))) + bind (ctx, NamedC (x, n, (KType, loc))) + | SgiDatatypeImp (x, n, _, _, _, _, _) => + bind (ctx, NamedC (x, n, (KType, loc))) | SgiVal _ => ctx | SgiStr (x, _, sgn) => bind (ctx, Str (x, sgn)) @@ -494,10 +494,10 @@ bind (ctx, Sgn (x, sgn)) | SgiConstraint _ => ctx | SgiTable _ => ctx - | SgiClassAbs (x, _) => - bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) - | SgiClass (x, _, _) => - bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))), + | SgiClassAbs (x, n) => + bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) + | SgiClass (x, n, _) => + bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))), sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -542,7 +542,7 @@ datatype binder = RelC of string * Elab.kind - | NamedC of string * Elab.kind + | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con | Str of string * Elab.sgn @@ -594,11 +594,11 @@ StrConst ds => S.map2 (ListUtil.mapfoldB (fn (ctx, d) => (case #1 d of - DCon (x, _, k, _) => - bind (ctx, NamedC (x, k)) + DCon (x, n, k, _) => + bind (ctx, NamedC (x, n, k)) | DDatatype (x, n, xs, xncs) => let - val ctx = bind (ctx, NamedC (x, (KType, loc))) + val ctx = bind (ctx, NamedC (x, n, (KType, loc))) in foldl (fn ((x, _, co), ctx) => let @@ -621,7 +621,7 @@ ctx xncs end | DDatatypeImp (x, n, m, ms, x', _, _) => - bind (ctx, NamedC (x, (KType, loc))) + bind (ctx, NamedC (x, n, (KType, loc))) | DVal (x, _, c, _) => bind (ctx, NamedE (x, c)) | DValRec vis => @@ -637,8 +637,8 @@ | DTable (tn, x, n, c) => bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc), c), loc))) - | DClass (x, _, _) => - bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))) + | DClass (x, n, _) => + bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) | DDatabase _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc))