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))