comparison src/elab_util.sml @ 2201:1091227f535a

Unnest properly in presence of kind polymorphism
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Dec 2015 13:41:35 -0500
parents 22117edf8fd3
children
comparison
equal deleted inserted replaced
2200:fc1c89627178 2201:1091227f535a
113 S.Return () 113 S.Return ()
114 else 114 else
115 S.Continue (k, ())) k () of 115 S.Continue (k, ())) k () of
116 S.Return _ => true 116 S.Return _ => true
117 | S.Continue _ => false 117 | S.Continue _ => false
118
119 fun foldB {kind, bind} ctx st k =
120 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
121 bind = bind} ctx k st of
122 S.Continue (_, st) => st
123 | S.Return _ => raise Fail "ElabUtil.Kind.foldB: Impossible"
118 124
119 end 125 end
120 126
121 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con) 127 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)
122 128