# HG changeset patch # User Adam Chlipala # Date 1334581648 14400 # Node ID 1b3f82b09bb083f759c0cd961b21a8ce240c1297 # Parent 355dc023fbb873652334a59b03e08e41e61d3599 Fix monoization of recursive variants diff -r 355dc023fbb8 -r 1b3f82b09bb0 src/monoize.sml --- a/src/monoize.sml Wed Apr 11 03:05:26 2012 +0400 +++ b/src/monoize.sml Mon Apr 16 09:07:28 2012 -0400 @@ -52,7 +52,7 @@ val nextPvar = ref 0 val pvars = ref (RM.empty : (int * (string * int * L'.typ) list) RM.map) -val pvarDefs = ref ([] : L'.decl list) +val pvarDefs = ref ([] : (string * int * (string * int * L'.typ option) list) list) val pvarOldDefs = ref ([] : (int * (string * int * L.con option) list) list) fun choosePvar () = @@ -74,7 +74,7 @@ SM.insert (fs', x, n))) ([], SM.empty) (r, fs) in pvars := RM.insert (!pvars, r', (n, fs)); - pvarDefs := (L'.DDatatype [("$poly" ^ Int.toString n, n, map (fn (x, n, t) => (x, n, SOME t)) fs)], loc) + pvarDefs := ("$poly" ^ Int.toString n, n, map (fn (x, n, t) => (x, n, SOME t)) fs) :: !pvarDefs; pvarOldDefs := (n, r) :: !pvarOldDefs; (n, fs) @@ -532,12 +532,11 @@ fun makeDecl n fm = let val (x, xncs) = - case ListUtil.search (fn (L'.DDatatype [(x, i', xncs)], _) => + case ListUtil.search (fn (x, i', xncs) => if i' = i then SOME (x, xncs) else - NONE - | _ => NONE) (!pvarDefs) of + NONE) (!pvarDefs) of NONE => let val (x, _, xncs) = Env.lookupDatatype env i @@ -4361,7 +4360,11 @@ cs)], loc)) env (!pvarOldDefs), Fm.enter fm, - ds' @ Fm.decls fm @ !pvarDefs @ ds))) + case ds' of + [(L'.DDatatype dts, loc)] => + (L'.DDatatype (dts @ !pvarDefs), loc) :: Fm.decls fm @ ds + | _ => + ds' @ Fm.decls fm @ (L'.DDatatype (!pvarDefs), loc) :: ds))) (env, Fm.empty mname, []) file in pvars := RM.empty;