constructors === id (#693)
This commit is contained in:
parent
04e2dbfcaa
commit
5a0d671f95
|
@ -1897,14 +1897,8 @@ normalizeWithM ctx e0 = loop (denote e0)
|
||||||
Constructors t -> do
|
Constructors t -> do
|
||||||
t' <- loop t
|
t' <- loop t
|
||||||
case t' of
|
case t' of
|
||||||
Union kts -> pure (RecordLit kvs)
|
u@(Union _) -> pure u
|
||||||
where
|
_ -> pure $ Constructors t'
|
||||||
kvs = Dhall.Map.mapWithKey adapt kts
|
|
||||||
|
|
||||||
adapt k t_ = Lam k t_ (UnionLit k (Var (V k 0)) rest)
|
|
||||||
where
|
|
||||||
rest = Dhall.Map.delete k kts
|
|
||||||
_ -> pure (Constructors t')
|
|
||||||
Field r x -> do
|
Field r x -> do
|
||||||
r' <- loop r
|
r' <- loop r
|
||||||
case r' of
|
case r' of
|
||||||
|
|
|
@ -771,13 +771,10 @@ typeWithA tpa = loop
|
||||||
loop ctx e@(Constructors t ) = do
|
loop ctx e@(Constructors t ) = do
|
||||||
_ <- loop ctx t
|
_ <- loop ctx t
|
||||||
|
|
||||||
kts <- case Dhall.Core.normalize t of
|
case Dhall.Core.normalize t of
|
||||||
Union kts -> return kts
|
u@(Union _) -> loop ctx u
|
||||||
t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))
|
t' -> Left (TypeError ctx e (ConstructorsRequiresAUnionType t t'))
|
||||||
|
|
||||||
let adapt k t_ = Pi k t_ (Union kts)
|
|
||||||
|
|
||||||
return (Record (Dhall.Map.mapWithKey adapt kts))
|
|
||||||
loop ctx e@(Field r x ) = do
|
loop ctx e@(Field r x ) = do
|
||||||
t <- fmap Dhall.Core.normalize (loop ctx r)
|
t <- fmap Dhall.Core.normalize (loop ctx r)
|
||||||
|
|
||||||
|
|
|
@ -1 +1 @@
|
||||||
./issue553A.dhall sha256:6fb582c043889dd5a4c97176f8a58d2633252b5374cb71e288b93bc3757f9643
|
./issue553A.dhall sha256:e2d014696fb7d773727ae5aa42dc20bbd2447ea82bcb5971ccbb7763906edace
|
||||||
|
|
|
@ -1,6 +1 @@
|
||||||
{ Empty =
|
< Empty : {} | Person : { name : Text, age : Natural } >
|
||||||
λ(Empty : {}) → < Empty = Empty | Person : { age : Natural, name : Text } >
|
|
||||||
, Person =
|
|
||||||
λ(Person : { age : Natural, name : Text })
|
|
||||||
→ < Person = Person | Empty : {} >
|
|
||||||
}
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user