From ebafddcfc9eee598b0bf305fd55733f6fa5be26d Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 27 Mar 2020 14:26:25 +0000 Subject: [PATCH] Look for scrutinee type in case We can work out what it should be since each case is supposed to have the same type, so we can look ahead to the alternatives. This way, we don't have to rely on the scrutinee alone to calculate the type of the case block. (Idris 1 does this too but I've only just encountered the need for it in Idris 2 now!) --- docs/typedd/typedd.rst | 5 ++++ src/TTImp/Elab/Case.idr | 42 ++++++++++++++++++++++++++++++++-- tests/idris2/basic030/expected | 8 +++++-- tests/ttimp/qtt002/expected | 4 ++-- 4 files changed, 53 insertions(+), 6 deletions(-) diff --git a/docs/typedd/typedd.rst b/docs/typedd/typedd.rst index fa853a2..6f94bdf 100644 --- a/docs/typedd/typedd.rst +++ b/docs/typedd/typedd.rst @@ -11,6 +11,11 @@ code is also [going to be] part of the test suite (see `tests/typedd-book `_ in the Idris 2 source). +If you are new to Idris, and learning from the book, we recommend working +through the first 3-4 chapters with Idris 1, to avoid the need to worry about +the changes described here. After that, refer to this document for any +necessary changes. + Chapter 1 --------- diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 4ea77fa..8587051 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -311,9 +311,12 @@ checkCase : {vars : _} -> FC -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause -> Maybe (Glued vars) -> Core (Term vars, Glued vars) -checkCase rig elabinfo nest env fc scr scrty_exp alts exp +checkCase rig elabinfo nest env fc scr scrty_in alts exp = delayElab fc rig env exp $ - do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp + do scrty_exp <- case scrty_in of + Implicit _ _ => guessScrType alts + _ => pure scrty_in + (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp (Just (gType fc)) logTerm 10 "Expected scrutinee type" scrtyv -- Try checking at the given multiplicity; if that doesn't work, @@ -347,3 +350,38 @@ checkCase rig elabinfo nest env fc scr scrty_exp alts exp checkConcrete (NApp _ (NMeta n i _) _) = throw (GenericMsg (getFC scr) "Can't infer type for case scrutinee") checkConcrete _ = pure () + + applyTo : Defs -> RawImp -> NF [] -> Core RawImp + applyTo defs ty (NBind fc _ (Pi _ Explicit _) sc) + = applyTo defs (IApp fc ty (Implicit fc False)) + !(sc defs (toClosure defaultOpts [] (Erased fc False))) + applyTo defs ty (NBind _ x (Pi _ _ _) sc) + = applyTo defs (IImplicitApp fc ty (Just x) (Implicit fc False)) + !(sc defs (toClosure defaultOpts [] (Erased fc False))) + applyTo defs ty _ = pure ty + + -- Get the name and type of the family the scrutinee is in + getRetTy : Defs -> NF [] -> Core (Maybe (Name, NF [])) + getRetTy defs (NBind fc _ (Pi _ _ _) sc) + = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc False))) + getRetTy defs (NTCon _ n _ arity _) + = do Just ty <- lookupTyExact n (gamma defs) + | Nothing => pure Nothing + pure (Just (n, !(nf defs [] ty))) + getRetTy _ _ = pure Nothing + + -- Guess a scrutinee type by looking at the alternatives, so that we + -- have a hint for building the case type + guessScrType : List ImpClause -> Core RawImp + guessScrType [] = pure $ Implicit fc False + guessScrType (PatClause _ x _ :: xs) + = case getFn x of + IVar _ n => + do defs <- get Ctxt + [(n', (_, ty))] <- lookupTyName n (gamma defs) + | _ => guessScrType xs + Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty) + | _ => guessScrType xs + applyTo defs (IVar fc tyn) tyty + _ => guessScrType xs + guessScrType (_ :: xs) = guessScrType xs diff --git a/tests/idris2/basic030/expected b/tests/idris2/basic030/expected index d14fac1..5dbeaac 100644 --- a/tests/idris2/basic030/expected +++ b/tests/idris2/basic030/expected @@ -1,3 +1,7 @@ 1/1: Building arity (arity.idr) -arity.idr:5:16--5:22:While processing right hand side of foo at arity.idr:4:1--7:1: -Constructor Main.MkN is not fully applied +arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1: +When unifying (1 {arg:169} : Nat) -> MyN and MyN +Mismatch between: + (1 {arg:169} : Nat) -> MyN +and + MyN diff --git a/tests/ttimp/qtt002/expected b/tests/ttimp/qtt002/expected index 703017c..597b530 100644 --- a/tests/ttimp/qtt002/expected +++ b/tests/ttimp/qtt002/expected @@ -1,6 +1,6 @@ Processing as TTImp Written TTC Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:19} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:19}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:19})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:19}))) m)) a)))))))))) -Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:48} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:48}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:48})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:48})) m)) a))))))))) -Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:78} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:78}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:78})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:78}) a) ((Main.Vect ((Main.plus (Main.S {k:78})) m)) a)))))))))) +Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:49} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:49}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:49})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:49})) m)) a))))))))) +Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:80} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:80}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:80})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:80}) a) ((Main.Vect ((Main.plus (Main.S {k:80})) m)) a)))))))))) Yaffle> Bye for now!