From beb7b1a623380008b7ed667e4f2c859300b7de57 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 28 Sep 2024 20:53:22 -0700 Subject: [PATCH] 1 + 1 = 2 --- .gitignore | 3 +++ TODO.md | 2 +- newt-vscode/LICENSE | 24 +++++++++++++++++++++++ newt/order.newt | 9 ++++++++- src/Lib/Elab.idr | 13 ++++++++++++- src/Lib/Eval.idr | 40 ++++++++++++++++++--------------------- tests/black/caseeval.newt | 18 ++++++++++++++++++ 7 files changed, 84 insertions(+), 25 deletions(-) create mode 100644 newt-vscode/LICENSE create mode 100644 tests/black/caseeval.newt diff --git a/.gitignore b/.gitignore index 5444303..eaf0eed 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,6 @@ build/ *.*~ATTIC \#* *~ +*.log +*.agda +*.agdai diff --git a/TODO.md b/TODO.md index b6647d7..e972ea3 100644 --- a/TODO.md +++ b/TODO.md @@ -6,7 +6,7 @@ I may be done with `U` - I keep typing `Type`. - [ ] 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 leave that implicit for efficiency. I think it would also make printing more readable. -- [ ] eval for case (see order.newt) +- [x] eval for case (see order.newt) - [ ] dynamic pattern unification (add test case first) - [x] switch from commit/mustWork to checking progress - [x] type constructors are no longer generated? And seem to have 0 arity. diff --git a/newt-vscode/LICENSE b/newt-vscode/LICENSE new file mode 100644 index 0000000..fdddb29 --- /dev/null +++ b/newt-vscode/LICENSE @@ -0,0 +1,24 @@ +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. + +In jurisdictions that recognize copyright laws, the author or authors +of this software dedicate any and all copyright interest in the +software to the public domain. We make this dedication for the benefit +of the public at large and to the detriment of our heirs and +successors. We intend this dedication to be an overt act of +relinquishment in perpetuity of all present and future rights to this +software under copyright law. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. + +For more information, please refer to diff --git a/newt/order.newt b/newt/order.newt index 2a5fc5f..0216b36 100644 --- a/newt/order.newt +++ b/newt/order.newt @@ -14,6 +14,7 @@ data Pair : U -> U -> U where infix 1 _,_ foo : Pair Nat Nat +-- vscode plugin issue: Without the space the info is rendered on Z... foo = (Z , S Z) -- So I was going to force a (a + b, a) =?= (3,0) unification problem @@ -24,6 +25,12 @@ data Eq : {A : U} -> A -> A -> U where -- but hold up here. This doesn't solve either. -- Oh, because I can't reduce case. -- And the FC is useless. +-- these go into caseeval.newt test two : Eq (plus Z (S (S Z))) (S (S Z)) -two = Refl {Nat} {S (S Z)} +two = Refl +two' : Eq (plus (S Z) (S Z)) (S (S Z)) +two' = Refl {Nat} {S (S Z)} + +three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z)) +three = Refl {Nat} {S (S (S Z))} diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index a87c9cf..db0fd26 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -192,11 +192,22 @@ parameters (ctx: Context) (VVar fc k sp, u) => pure $ MkResult[(k, u)] (t, VVar fc k sp) => pure $ MkResult[(k, t)] + -- REVIEW - consider separate value for DCon/TCon (VRef fc k def sp, VRef fc' k' def' sp' ) => if k == k' then do debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}" unifySpine l (k == k') sp sp' - else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" + else case lookup k !(get) of + Just (MkEntry name ty (Fn tm)) => do + vtm <- eval [] CBN tm + v <- vappSpine vtm sp + unify l v u' + _ => case lookup k' !(get) of + Just (MkEntry name ty (Fn tm)) => do + vtm <- eval [] CBN tm + v <- vappSpine vtm sp' + unify l t' v + _ => error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}" (VU _, VU _) => pure neutral -- Lennart.newt cursed type references itself diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index c430172..2bb6641 100644 --- a/src/Lib/Eval.idr +++ b/src/Lib/Eval.idr @@ -9,6 +9,7 @@ import Control.Monad.Error.Interface import Data.IORef import Data.Fin import Data.List +import Data.SnocList import Data.Vect import Data.SortedMap @@ -43,23 +44,19 @@ vappSpine : Val -> SnocList Val -> M Val vappSpine t [<] = pure t vappSpine t (xs :< x) = vapp !(vappSpine t xs) x --- So we need: --- - a Neutral case statement --- - split out data / type constructors from VRef application --- - should we sort out what the case tree really looks like first? - --- Technically I don't need this now, as a neutral would be fine. - -evalAlt : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) --- FIXME spine length? Should this be VRef or do we specialize? -evalAlt env mode (VRef _ nm y sp) ((CaseCons name args t) :: xs) = +evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) +evalCase env mode sc@(VRef _ nm y sp) (cc@(CaseCons name nms t) :: xs) = if nm == name - -- Here we bind the args and push on. Do we have enough? Too many? - then ?evalAlt_success - -- here we need to know if we've got a mismatched constructor or some function app - else ?evalAlt_what -evalAlt env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u) -evalAlt env mode sc _ = pure Nothing -- stuck + then go env sp nms + else evalCase env mode sc xs + where + go : Env -> SnocList Val -> List String -> M (Maybe Val) + go env (args :< arg) (nm :: nms) = go (arg :: env) args nms + go env args [] = Just <$> vappSpine !(eval env mode t) args + go env [<] rest = pure Nothing + +evalCase env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u) +evalCase env mode sc _ = pure Nothing bind : Val -> Env -> Env bind v env = v :: env @@ -71,9 +68,6 @@ bind v env = v :: env -- - Applications headed by top-level variables are lazy. -- - Any other function application is call-by-value during evaluation. --- Do we want a def in here instead? We'll need DCon/TCon eventually --- I need to be aggressive about reduction, I guess. I'll figure it out --- later, maybe need lazy glued values. -- TODO - probably want to figure out gluing and handle constructors eval env mode (Ref _ x (Fn tm)) = eval env mode tm eval env mode (Ref fc x def) = pure $ VRef fc x def [<] @@ -94,9 +88,11 @@ eval env mode (Bnd fc i) = case getAt i env of Nothing => error' "Bad deBruin index \{show i}" eval env mode (Lit fc lit) = pure $ VLit fc lit --- We need a neutral and some code to run the case tree - -eval env mode tm@(Case fc sc alts) = pure $ VCase fc !(eval env mode sc) alts +eval env mode tm@(Case fc sc alts) = + case !(evalCase env mode !(eval env mode sc) alts) of + Just v => pure v + Nothing => pure $ fromMaybe (VCase fc !(eval env mode sc) alts) + !(evalCase env mode !(eval env mode sc) alts) export quote : (lvl : Nat) -> Val -> M Tm diff --git a/tests/black/caseeval.newt b/tests/black/caseeval.newt new file mode 100644 index 0000000..a47596f --- /dev/null +++ b/tests/black/caseeval.newt @@ -0,0 +1,18 @@ +module CaseEval + +data Nat : U where + Z : Nat + S : Nat -> Nat + +plus : Nat -> Nat -> Nat +plus Z y = y +plus (S x) y = S (plus x y) + +data Eq : {A : U} -> A -> A -> U where + Refl : {A : U} -> {x : A} -> Eq x x + +two : Eq (plus (S Z) (S Z)) (S (S Z)) +two = Refl + +three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z)) +three = Refl {Nat} {S (S (S Z))}