From 95a4baf12d425a1ee22d8a93f1fb74ae506828a0 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 26 Oct 2024 21:39:25 -0700 Subject: [PATCH] _+_ works with an Add typeclass now. - add test case - fix some issues with eval - filter out non-candidates for auto search --- TODO.md | 9 +++++---- src/Lib/Elab.idr | 3 ++- src/Lib/Eval.idr | 3 ++- src/Lib/ProcessDecl.idr | 20 ++++++++++++++++++-- tests/black/Auto2.newt | 38 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 tests/black/Auto2.newt diff --git a/TODO.md b/TODO.md index 624aa84..a5bc41a 100644 --- a/TODO.md +++ b/TODO.md @@ -8,10 +8,10 @@ - [x] day1 - [x] day2 - some "real world" examples -- [ ] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet -- [ ] unsolved meta errors repeat (need to freeze or only report at end) +- [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet +- [x] unsolved meta errors repeat (need to freeze or only report at end) - [x] Sanitize JS idents, e.g. `_+_` -- [ ] Generate some programs that do stuff +- [x] Generate some programs that do stuff - [x] import - [ ] consider making meta application implicit in term, so its more readable when printed - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people @@ -37,6 +37,7 @@ - [x] ~~SKIP list syntax~~ - Agda doesn't have it, clashes with pair syntax - [ ] autos / typeclass resolution + - [x] very primitive version in place, not higher order, search at end - We need special handling in unification to make this possible for typeclasses on `U -> U`, we could still do `Eq` or `Show` with the current unification - options - keep as implicit and do auto if the type constructor is flagged auto @@ -44,7 +45,7 @@ - have separate type of implict with `{{}}` - `TypeClass.newt` is the exercise for this - [ ] do blocks (needs typeclass, overloaded functions, or constrain to IO) -- [ ] some solution for `+` problem (classes? ambiguity?) +- [x] some solution for `+` problem (classes? ambiguity?) - [x] show compiler failure in the editor (exit code != 0) - [x] write output to file - uses `-o` option diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 4f3a4fe..cefd340 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -67,11 +67,12 @@ tryEval k sp = v => pure $ Just v _ => pure Nothing --- Lennart needed more forcing for recursive nat, +-- Force far enough to compare types forceType : Val -> M Val forceType (VMeta fc ix sp) = case !(lookupMeta ix) of (Unsolved x k xs _ _) => pure (VMeta fc ix sp) (Solved k t) => vappSpine t sp >>= forceType +forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp forceType x = pure x public export diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index dd427b1..97871e5 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -88,7 +88,8 @@ evalSpine env mode (Ref fc nm (Fn tm)) sp = do v => pure v evalSpine env mode tm sp = vappSpine !(eval env mode tm) ([<] <>< sp) -eval env mode (Ref _ x (Fn tm)) = eval env mode tm +-- This is too aggressive... +-- eval env mode (Ref _ x (Fn tm)) = eval env mode tm eval env mode (Ref fc x def) = pure $ VRef fc x def [<] eval env mode (App _ t u) = evalSpine env mode t [!(eval env mode u)] eval env mode (U fc) = pure (VU fc) diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 5487a63..78f74b3 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -12,12 +12,27 @@ import Lib.Eval import Lib.Types import Lib.Util +-- Check that the arguments are not explicit and the type constructor in codomain matches +-- Later we will build a table of codomain type, and maybe make the user tag the candidates +-- like Idris does with %hint +isCandidate : Val -> Tm -> Bool +isCandidate ty (Pi fc nm Explicit t u) = False +isCandidate ty (Pi fc nm icit t u) = isCandidate ty u +isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm' +isCandidate ty (App fc t u) = isCandidate ty t +isCandidate _ _ = False + + -- go : List Binder -> Tm -> (Tm, List Binder) + -- go ts (Pi fc nm icit t u) = go (MkBind fc nm icit t :: ts) u + -- go ts tm = (tm, reverse ts) + -- This is a crude first pass -- TODO consider ctx findMatches : Val -> List TopEntry -> M (List Tm) findMatches ty [] = pure [] findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do + let True = isCandidate ty type | False => findMatches ty xs top <- get let ctx = mkCtx top.metas (getFC ty) -- FIXME we're restoring state, but the INFO logs have already been emitted @@ -26,6 +41,7 @@ findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do catchError {e=Error} (do -- TODO sort out the FC here let fc = getFC ty + debug "TRY \{name} : \{pprint [] type} for \{show ty}" tm <- check (mkCtx top.metas fc) (RVar fc name) ty debug "Found \{pprint [] tm} for \{show ty}" (tm ::) <$> findMatches ty xs) @@ -121,6 +137,7 @@ processDecl (Def fc nm clauses) = do [tm] <- findMatches ty top.defs | res => error fc "Failed to solve \{show ty}, matches: \{show $ map (pprint []) res}" val <- eval ctx.env CBN tm + debug "solution \{pprint [] tm} evaled to \{show val}" let sp = makeSpine ctx.lvl ctx.bds solve ctx ctx.lvl k sp val pure () @@ -130,8 +147,7 @@ processDecl (Def fc nm clauses) = do putStrLn "NF \{pprint[] tm'}" mc <- readIORef top.metas - -- for_ (take mlen mc.metas) $ \case - for_ (mc.metas) $ \case + for_ (take mlen mc.metas) $ \case (Solved k x) => pure () (Unsolved (l,c) k ctx ty User) => do -- TODO print here instead of during Elab diff --git a/tests/black/Auto2.newt b/tests/black/Auto2.newt new file mode 100644 index 0000000..1dc63de --- /dev/null +++ b/tests/black/Auto2.newt @@ -0,0 +1,38 @@ +module Auto2 + +ptype World +pfunc log : {A : U} -> A -> World := "(_, a) => console.log(a)" + +ptype Int +pfunc i_plus : Int -> Int -> Int := "(x,y) => x + y" + +data Nat : U where + Z : Nat + S : Nat -> Nat + +plus : Nat -> Nat -> Nat +plus Z x = x +plus (S k) x = S (plus k x) + +-- a type class +data Add : U -> U where + MkAdd : {A : U} -> (A -> A -> A) -> Add A + +infixl 8 _+_ +_+_ : {A : U} -> {{myadd : Add A}} -> A -> A -> A +_+_ {_} {{MkAdd adder}} x y = adder x y + +-- Two instances +addInt : Add Int +addInt = MkAdd i_plus + +addNat : Add Nat +addNat = MkAdd plus + +-- sequencing hack +infixl 2 _>>_ +_>>_ : {a b : U} -> a -> b -> b +a >> b = b + +main : World -> World +main _ = log (40 + 2) >> log (Z + Z)