diff --git a/TODO.md b/TODO.md index e875f5e..384dfce 100644 --- a/TODO.md +++ b/TODO.md @@ -15,3 +15,8 @@ - [ ] type at point - [ ] repl - [ ] LSP +- [ ] don't match forced constructors + - maybe do this in codegen if there is only one case. +- [ ] magic nat (codegen as number with appropriate pattern matching) +- [ ] magic tuple? (codegen as array) +- [ ] magic newtype? (drop in codegen) diff --git a/newt/typeclass.newt b/newt/typeclass.newt new file mode 100644 index 0000000..0b08c4d --- /dev/null +++ b/newt/typeclass.newt @@ -0,0 +1,29 @@ +module TypeClass + +-- experiment on one option for typeclass (we don't have record yet) + +-- we need a bit more than this, but +data Monad : (U -> U) -> U where + MkMonad : { M : U -> U } -> + (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> + Monad M + +data Maybe : U -> U where + Just : {A : U} -> A -> Maybe A + Nothing : {A : U} -> Maybe A + + +-- NEXT trying to get this to work. An equivalence is not found in pattern +-- matching + +-- [instance] +MaybeMonad : Monad Maybe +-- Agda case lambda might be nice.. +-- The {Maybe} isn't solved in type for the case +MaybeMonad = MkMonad {Maybe} (\ {A} ma amb => + case ma of + Nothing => Nothing + -- It doesn't discover pat$5 is A during pattern matching + -- oh, but var 0 value is var5 + Just a => amb a) + diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index e55007c..a97b578 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -120,12 +120,33 @@ parameters (ctx: Context) unifySpine l True (xs :< x) (ys :< y) = [| unify l x y <+> (unifySpine l True xs ys) |] unifySpine l True _ _ = error emptyFC "meta spine length mismatch" + lookupVar : Nat -> Maybe Val + lookupVar k = let l = length ctx.env in + if k > l + then Nothing + else case getAt ((l `minus` k) `minus` 1) ctx.env of + Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v + Just v => Just v + Nothing => Nothing + + -- hoping to apply what we got via pattern matching + unlet : Val -> M Val + unlet t@(VVar fc k sp) = case lookupVar k of + Just tt@(VVar fc' k' sp') => do + debug "lookup \{show k} is \{show tt}" + if k' == k then pure t else vappSpine (VVar fc' k' sp') sp + Just t => vappSpine t sp + Nothing => do + debug "lookup \{show k} is Nothing in env \{show ctx.env}" + pure t + unlet x = pure x + unify l t u = do debug "Unify \{show ctx.lvl}" debug " \{show l} \{show t}" debug " =?= \{show u}" - t' <- forceMeta t - u' <- forceMeta u + t' <- forceMeta t >>= unlet + u' <- forceMeta u >>= unlet debug "forced \{show t'}" debug " =?= \{show u'}" debug "env \{show ctx.env}" @@ -146,11 +167,7 @@ parameters (ctx: Context) -- else error ctx.fc "unify error: vvar mismatch \{show k} \{show k'} \{show ctx.env}" -- attempt at building constraints - -- and using them - (VVar fc k sp, u) => case lookupVar k of - Just v => unify l v u - Nothing => pure $ MkResult[(k, u)] - + (VVar fc k sp, u) => pure $ MkResult[(k, u)] (t, VVar fc k sp) => pure $ MkResult[(k, t)] (VRef fc k def sp, VRef fc' k' def' sp' ) => @@ -487,6 +504,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of -- We've got a beta redex or need to do something... -- Maybe we can let the scrutinee and jump into the middle? (sc, scty) <- infer ctx rsc + scty <- forceMeta scty + debug "SCTM/TY \{pprint (names ctx) sc} \{show scty}" let scnm = fresh "sc" -- FIXME FC diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 74cf643..6607857 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -48,7 +48,8 @@ piArity _ = Z arityForName : FC -> Name -> M Nat arityForName fc nm = case lookup nm !get of - Nothing => error fc "Name \{show nm} not in scope" + -- let the magic hole through for now (will generate bad JS) + Nothing => if nm == "?" then pure 0 else error fc "Name \{show nm} not in scope" (Just (MkEntry name type Axiom)) => pure 0 (Just (MkEntry name type (TCon strs))) => pure 0 -- FIXME (Just (MkEntry name type (DCon k str))) => pure k diff --git a/tests/black/typeclass.newt b/tests/black/typeclass.newt new file mode 100644 index 0000000..0b08c4d --- /dev/null +++ b/tests/black/typeclass.newt @@ -0,0 +1,29 @@ +module TypeClass + +-- experiment on one option for typeclass (we don't have record yet) + +-- we need a bit more than this, but +data Monad : (U -> U) -> U where + MkMonad : { M : U -> U } -> + (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) -> + Monad M + +data Maybe : U -> U where + Just : {A : U} -> A -> Maybe A + Nothing : {A : U} -> Maybe A + + +-- NEXT trying to get this to work. An equivalence is not found in pattern +-- matching + +-- [instance] +MaybeMonad : Monad Maybe +-- Agda case lambda might be nice.. +-- The {Maybe} isn't solved in type for the case +MaybeMonad = MkMonad {Maybe} (\ {A} ma amb => + case ma of + Nothing => Nothing + -- It doesn't discover pat$5 is A during pattern matching + -- oh, but var 0 value is var5 + Just a => amb a) +