mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-23 09:52:55 -06:00
fixed a deep bug in TypeCheck due to swap of arguments; print empty record as <> instead of {} to distinguish from empty record type
This commit is contained in:
@@ -256,7 +256,7 @@ inferLType gr g trm = case trm of
|
|||||||
-- for record fields, which may be typed
|
-- for record fields, which may be typed
|
||||||
inferM (mty, t) = do
|
inferM (mty, t) = do
|
||||||
(t', ty') <- case mty of
|
(t', ty') <- case mty of
|
||||||
Just ty -> checkLType gr g ty t
|
Just ty -> checkLType gr g t ty
|
||||||
_ -> inferLType gr g t
|
_ -> inferLType gr g t
|
||||||
return (Just ty',t')
|
return (Just ty',t')
|
||||||
|
|
||||||
@@ -431,6 +431,7 @@ checkLType gr g trm typ0 = do
|
|||||||
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
|
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
|
||||||
-- ext t = t ** ...
|
-- ext t = t ** ...
|
||||||
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
|
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
|
||||||
|
|
||||||
RecType rr -> do
|
RecType rr -> do
|
||||||
(r',ty,s') <- checks [
|
(r',ty,s') <- checks [
|
||||||
do (r',ty) <- inferLType gr g r
|
do (r',ty) <- inferLType gr g r
|
||||||
@@ -439,6 +440,7 @@ checkLType gr g trm typ0 = do
|
|||||||
do (s',ty) <- inferLType gr g s
|
do (s',ty) <- inferLType gr g s
|
||||||
return (s',ty,r)
|
return (s',ty,r)
|
||||||
]
|
]
|
||||||
|
|
||||||
case ty of
|
case ty of
|
||||||
RecType rr1 -> do
|
RecType rr1 -> do
|
||||||
let (rr0,rr2) = recParts rr rr1
|
let (rr0,rr2) = recParts rr rr1
|
||||||
@@ -451,7 +453,7 @@ checkLType gr g trm typ0 = do
|
|||||||
ExtR ty ex -> do
|
ExtR ty ex -> do
|
||||||
r' <- justCheck g r ty
|
r' <- justCheck g r ty
|
||||||
s' <- justCheck g s ex
|
s' <- justCheck g s ex
|
||||||
return $ (ExtR r' s', typ) --- is this all?
|
return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
|
||||||
|
|
||||||
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
|
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
|
||||||
|
|
||||||
|
|||||||
@@ -176,6 +176,7 @@ ppTerm q d (EInt n) = integer n
|
|||||||
ppTerm q d (EFloat f) = double f
|
ppTerm q d (EFloat f) = double f
|
||||||
ppTerm q d (Meta _) = char '?'
|
ppTerm q d (Meta _) = char '?'
|
||||||
ppTerm q d (Empty) = text "[]"
|
ppTerm q d (Empty) = text "[]"
|
||||||
|
ppTerm q d (R []) = text "<>" -- to distinguish from {} empty RecType
|
||||||
ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+>
|
ppTerm q d (R xs) = braces (fsep (punctuate semi [ppLabel l <+>
|
||||||
fsep [case mb_t of {Just t -> colon <+> ppTerm q 0 t; Nothing -> empty},
|
fsep [case mb_t of {Just t -> colon <+> ppTerm q 0 t; Nothing -> empty},
|
||||||
equals <+> ppTerm q 0 e] | (l,(mb_t,e)) <- xs]))
|
equals <+> ppTerm q 0 e] | (l,(mb_t,e)) <- xs]))
|
||||||
|
|||||||
Reference in New Issue
Block a user