edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-23 20:22:34 +03:00
Code Issues Projects Releases Wiki Activity

Use a data type for dotting reason

Browse Source 
Then we can more safely match on it
This commit is contained in:
Edwin Brady 2020-01-24 16:16:31 +00:00
parent 118ea787c3
commit a26581f454
13 changed files with 90 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libs/base/Language/Reflection/TTImp.idr
View File

@ -12,6 +12,14 @@ mutual
public export
data UseSide = UseLeft | UseRight
public export
data DotReason = NonLinearVar
| VarApplied
| NotConstructor
| ErasedArg
| UserDotted
| UnknownDot
public export
data TTImp : Type where
IVar : FC -> Name -> TTImp
@ -44,7 +52,7 @@ mutual
IAs : FC -> UseSide -> Name -> TTImp -> TTImp
-- A 'dot' pattern, i.e. one which must also have the given value
-- by unification
IMustUnify : FC -> (reason : String) -> TTImp -> TTImp
IMustUnify : FC -> DotReason -> TTImp -> TTImp
-- Laziness annotations
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type

21
src/Core/Core.idr
View File

@ -25,6 +25,23 @@ data CaseError = DifferingArgNumbers
| NotFullyApplied Name
| UnknownType
public export
data DotReason = NonLinearVar
| VarApplied
| NotConstructor
| ErasedArg
| UserDotted
| UnknownDot
export
Show DotReason where
show NonLinearVar = "Non linear pattern variable"
show VarApplied = "Variable applied to arguments"
show NotConstructor = "Not a constructor application or primitive"
show ErasedArg = "Erased argument"
show UserDotted = "User dotted"
show UnknownDot = "Unknown reason"
-- All possible errors, carrying a location
public export
data Error
@ -71,7 +88,7 @@ data Error
| NotRewriteRule FC (Env Term vars) (Term vars)
| CaseCompile FC Name CaseError
| MatchTooSpecific FC (Env Term vars) (Term vars)
| BadDotPattern FC (Env Term vars) String (Term vars) (Term vars)
| BadDotPattern FC (Env Term vars) DotReason (Term vars) (Term vars)
| BadImplicit FC String
| BadRunElab FC (Env Term vars) (Term vars)
| GenericMsg FC String
@ -218,7 +235,7 @@ Show Error where
= show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"
show (BadDotPattern fc env reason x y)
= show fc ++ ":Can't match on " ++ show x ++
(if reason /= "" then " (" ++ reason ++ ")" else "") ++
" (" ++ show reason ++ ")" ++
" - it elaborates to " ++ show y
show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
show (BadRunElab fc env script) = show fc ++ ":Bad elaborator script " ++ show script

2
src/Core/Unify.idr
View File

@ -1272,7 +1272,7 @@ checkDots
ust <- get UST
put UST (record { dotConstraints = [] } ust)
where
checkConstraint : (Name, String, Constraint) -> Core ()
checkConstraint : (Name, DotReason, Constraint) -> Core ()
checkConstraint (n, reason, MkConstraint fc env x y)
= do logTermNF 10 "Dot" env y
logTermNF 10 " =" env x

4
src/Core/UnifyState.idr
View File

@ -73,7 +73,7 @@ record UState where
-- user defined hole names, which don't need
-- to have been solved
constraints : IntMap Constraint -- map for finding constraints by ID
dotConstraints : List (Name, String, Constraint) -- dot pattern constraints
dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints
nextName : Int
nextConstraint : Int
delayedElab : List (Int, Core ClosedTerm)
@ -271,7 +271,7 @@ addConstraint constr
export
addDot : {auto u : Ref UST UState} ->
FC -> Env Term vars -> Name -> Term vars -> String -> Term vars ->
FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->
Core ()
addDot fc env dotarg x reason y
= do ust <- get UST

2
src/Idris/Desugar.idr
View File

@ -222,7 +222,7 @@ mutual
desugar side ps (PAs fc vname pattern)
= pure $ IAs fc UseRight vname !(desugar side ps pattern)
desugar side ps (PDotted fc x)
= pure $ IMustUnify fc "User dotted" !(desugar side ps x)
= pure $ IMustUnify fc UserDotted !(desugar side ps x)
desugar side ps (PImplicit fc) = pure $ Implicit fc True
desugar side ps (PInfer fc) = pure $ Implicit fc False
desugar side ps (PDoBlock fc block)

2
src/Idris/Error.idr
View File

@ -208,7 +208,7 @@ perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
" in " ++ show n
perror (BadDotPattern _ env reason x y)
= pure $ "Can't match on " ++ !(pshow env x) ++
(if reason /= "" then " (" ++ reason ++ ")" else "")
" (" ++ show reason ++ ")"
perror (MatchTooSpecific _ env tm)
= pure $ "Can't match on " ++ !(pshow env tm) ++
" as it has a polymorphic type"

25
src/TTImp/Elab/Ambiguity.idr
View File

@ -24,18 +24,20 @@ expandAmbigName : {auto c : Ref Ctxt Defs} ->
expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp
= do est <- get EST
if n `elem` lhsPatVars est
then pure $ IMustUnify fc "Non linear pattern variable" orig
then pure $ IMustUnify fc NonLinearVar orig
else pure $ orig
expandAmbigName mode nest env orig args (IVar fc x) exp
= case lookup x (names nest) of
Just _ => pure orig
Just _ => do log 10 $ "Nested " ++ show x
pure orig
Nothing => do
defs <- get Ctxt
case defined x env of
Just _ =>
if isNil args || notLHS mode
then pure $ orig
else pure $ IMustUnify fc "Name applied to arguments" orig
then do log 10 $ "Defined in env " ++ show x
pure $ orig
else pure $ IMustUnify fc VarApplied orig
Nothing =>
do est <- get EST
fi <- fromIntegerName
@ -44,8 +46,11 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
let prims = mapMaybe id [fi, si, ci]
let primApp = isPrimName prims x
case !(lookupCtxtName x (gamma defs)) of
[] => pure orig
[nalt] => pure $ mkAlt primApp est nalt
[] => do log 10 $ "Failed to find " ++ show orig
pure orig
[nalt] =>
do log 10 $ "Only one " ++ show (fst nalt)
pure $ mkAlt primApp est nalt
nalts => pure $ IAlternative fc (uniqType fi si ci x args)
(map (mkAlt primApp est) nalts)
where
@ -84,11 +89,11 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
wrapDot prim est (InLHS _) n' [arg] _ tm
= if n' == Resolved (defining est) || prim
then tm
else IMustUnify fc "Not a constructor application or primitive" tm
else IMustUnify fc NotConstructor tm
wrapDot prim est (InLHS _) n' _ _ tm
= if n' == Resolved (defining est)
then tm
else IMustUnify fc "Not a constructor application or primitive" tm
else IMustUnify fc NotConstructor tm
wrapDot _ _ _ _ _ _ tm = tm
@ -111,7 +116,9 @@ expandAmbigName mode nest env orig args (IApp fc f a) exp
expandAmbigName mode nest env orig args (IImplicitApp fc f n a) exp
= expandAmbigName mode nest env orig
((fc, Just n, a) :: args) f exp
expandAmbigName elabmode nest env orig args tm exp = pure orig
expandAmbigName elabmode nest env orig args tm exp
= do log 10 $ "No ambiguity " ++ show orig
pure orig
stripDelay : NF vars -> NF vars
stripDelay (NDelayed fc r t) = stripDelay t

5
src/TTImp/Elab/App.idr
View File

@ -283,7 +283,7 @@ mutual
Implicit _ _ => tm
IAs _ _ _ (IBindVar _ _) => tm
IAs _ _ _ (Implicit _ _) => tm
_ => IMustUnify (getFC tm) "Erased argument" tm
_ => IMustUnify (getFC tm) ErasedArg tm
dotErased _ _ _ r tm = pure $ tm
-- Check the rest of an application given the argument type and the
@ -534,7 +534,8 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
etynf <- normaliseHoles defs env ety
pure (Just !(toFullNames etynf)))
exp
pure ("Checking application of " ++ show !(getFullName n) ++
pure ("Checking application of " ++ show !(getFullName n) ++
" (" ++ show n ++ ")" ++
" to " ++ show expargs ++ "\n\tFunction type " ++
(show !(toFullNames fnty)) ++ "\n\tExpected app type "
++ show exptyt))

3
src/TTImp/Elab/Check.idr
View File

@ -347,11 +347,12 @@ record ElabInfo where
constructor MkElabInfo
elabMode : ElabMode
implicitMode : BindMode
topLevel : Bool
bindingVars : Bool
export
initElabInfo : ElabMode -> ElabInfo
initElabInfo m = MkElabInfo m NONE False
initElabInfo m = MkElabInfo m NONE False True
export
tryError : {vars : _} ->

2
src/TTImp/Elab/Dot.idr
View File

@ -25,7 +25,7 @@ checkDot : {vars : _} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> String -> RawImp -> Maybe (Glued vars) ->
FC -> DotReason -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkDot rig elabinfo nest env fc reason tm Nothing
= throw (GenericMsg fc ("Dot pattern not valid here (unknown type) "

2
src/TTImp/ProcessDef.idr
View File

@ -76,7 +76,7 @@ impossibleErrOK defs (CantSolveEq fc env l r)
logTerm 10 " ...and" !(normalise defs env r)
impossibleOK defs !(nf defs env l)
!(nf defs env r)
impossibleErrOK defs (BadDotPattern _ _ "Erased argument" _ _) = pure True
impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
impossibleErrOK defs (CyclicMeta _ _) = pure True
impossibleErrOK defs (AllFailed errs)
= anyM (impossibleErrOK defs) (map snd errs)

33
src/TTImp/Reflect.idr
View File

@ -38,7 +38,7 @@ Reify UseSide where
= pure UseLeft
reify defs (NDCon _ (NS _ (UN "UseRight")) _ _ _)
= pure UseRight
reify deva val = cantReify val "UseSide"
reify defs val = cantReify val "UseSide"
export
Reflect UseSide where
@ -47,6 +47,37 @@ Reflect UseSide where
reflect fc defs env UseRight
= getCon fc defs (reflectionttimp "UseRight")
export
Reify DotReason where
reify defs (NDCon _ (NS _ (UN "NonLinearVar")) _ _ _)
= pure NonLinearVar
reify defs (NDCon _ (NS _ (UN "VarApplied")) _ _ _)
= pure VarApplied
reify defs (NDCon _ (NS _ (UN "NotConstructor")) _ _ _)
= pure NotConstructor
reify defs (NDCon _ (NS _ (UN "ErasedArg")) _ _ _)
= pure ErasedArg
reify defs (NDCon _ (NS _ (UN "UserDotted")) _ _ _)
= pure UserDotted
reify defs (NDCon _ (NS _ (UN "UnknownDot")) _ _ _)
= pure UnknownDot
reify defs val = cantReify val "DotReason"
export
Reflect DotReason where
reflect fc defs env NonLinearVar
= getCon fc defs (reflectionttimp "NonLinearVar")
reflect fc defs env VarApplied
= getCon fc defs (reflectionttimp "VarApplied")
reflect fc defs env NotConstructor
= getCon fc defs (reflectionttimp "NotConstructor")
reflect fc defs env ErasedArg
= getCon fc defs (reflectionttimp "ErasedArg")
reflect fc defs env UserDotted
= getCon fc defs (reflectionttimp "UserDotted")
reflect fc defs env UnknownDot
= getCon fc defs (reflectionttimp "UnknownDot")
mutual
export
Reify RawImp where

4
src/TTImp/TTImp.idr
View File

@ -75,7 +75,7 @@ mutual
IAs : FC -> UseSide -> Name -> RawImp -> RawImp
-- A 'dot' pattern, i.e. one which must also have the given value
-- by unification
IMustUnify : FC -> (reason : String) -> RawImp -> RawImp
IMustUnify : FC -> DotReason -> RawImp -> RawImp
-- Laziness annotations
IDelayed : FC -> LazyReason -> RawImp -> RawImp -- the type
@ -683,7 +683,7 @@ mutual
pure (IAs fc side y pattern)
17 => do fc <- fromBuf b
pattern <- fromBuf b
pure (IMustUnify fc "" pattern)
pure (IMustUnify fc UnknownDot pattern)
18 => do fc <- fromBuf b; r <- fromBuf b
y <- fromBuf b