diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 904f89e..df1d98e 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -455,6 +455,12 @@ unify env mode t u = do xb' <- b' $$ fresh _<+>_ <$> unify env mode a a' <*> unify (fresh :: env) mode xb xb' + -- TODO adds about 2kb, maybe add one more func for unifyPi? + -- or rearrange to split on first arg and then case on second (might be a good experiment) + unifyRest (VLit fc l) (VLit _ k) = if l == k + then pure neutral + else error fc "unify failed \{show l} =?= \{show k}" + unifyRest (VU _) (VU _) = pure neutral -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 06fcf42..bfb14cb 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -54,9 +54,9 @@ Tm : U data Literal = LString String | LInt Int | LChar Char instance Show Literal where - show (LString str) = show str + show (LString str) = quoteString str show (LInt i) = show i - show (LChar c) = show c + show (LChar c) = "'\{show c}'" -- FIXME single quote data CaseAlt : U where CaseDefault : Tm -> CaseAlt diff --git a/tests/UnifyLit.newt b/tests/UnifyLit.newt new file mode 100644 index 0000000..15a0a88 --- /dev/null +++ b/tests/UnifyLit.newt @@ -0,0 +1,12 @@ +module UnifyLit + +import Prelude + +test : 'x' ≡ 'x' +test = Refl + +test2 : "foo" ≡ "foo" +test2 = Refl + +test3 : 1 ≡ 1 +test3 = Refl