mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-19 03:47:30 +03:00
Conversion checking of case blocks
This is a little bit of a hack, but is for the situation where a case block arises from the same bit of source but with a different name, which would happen when elaborating interfaces with cases in a method signature. If it's the same function with the same scrutinee, it's convertible. Fixes #191
This commit is contained in:
parent
6267231649
commit
3fe5c78f86
@ -43,7 +43,7 @@ mutual
|
|||||||
export
|
export
|
||||||
Show (CaseTree vars) where
|
Show (CaseTree vars) where
|
||||||
show (Case {name} idx prf ty alts)
|
show (Case {name} idx prf ty alts)
|
||||||
= "case " ++ show name ++ " : " ++ show ty ++ " of { " ++
|
= "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++
|
||||||
showSep " | " (assert_total (map show alts)) ++ " }"
|
showSep " | " (assert_total (map show alts)) ++ " }"
|
||||||
show (STerm tm) = show tm
|
show (STerm tm) = show tm
|
||||||
show (Unmatched msg) = "Error: " ++ show msg
|
show (Unmatched msg) = "Error: " ++ show msg
|
||||||
|
@ -16,6 +16,12 @@ public export
|
|||||||
data FC = MkFC FileName FilePos FilePos
|
data FC = MkFC FileName FilePos FilePos
|
||||||
| EmptyFC
|
| EmptyFC
|
||||||
|
|
||||||
|
export
|
||||||
|
Eq FC where
|
||||||
|
(==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
|
||||||
|
(==) EmptyFC EmptyFC = True
|
||||||
|
(==) _ _ = False
|
||||||
|
|
||||||
export
|
export
|
||||||
file : FC -> FileName
|
file : FC -> FileName
|
||||||
file (MkFC fn _ _) = fn
|
file (MkFC fn _ _) = fn
|
||||||
|
@ -178,3 +178,14 @@ nameEq (Resolved x) (Resolved y) with (decEq x y)
|
|||||||
nameEq (Resolved x) (Resolved y) | (No contra) = Nothing
|
nameEq (Resolved x) (Resolved y) | (No contra) = Nothing
|
||||||
nameEq _ _ = Nothing
|
nameEq _ _ = Nothing
|
||||||
|
|
||||||
|
export
|
||||||
|
namesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
|
||||||
|
namesEq [] [] = Just Refl
|
||||||
|
namesEq (x :: xs) (y :: ys)
|
||||||
|
= do p <- nameEq x y
|
||||||
|
ps <- namesEq xs ys
|
||||||
|
rewrite p
|
||||||
|
rewrite ps
|
||||||
|
Just Refl
|
||||||
|
namesEq _ _ = Nothing
|
||||||
|
|
||||||
|
@ -645,6 +645,53 @@ mutual
|
|||||||
= pure $ !(convGen q defs env x y) && !(allConv q defs env xs ys)
|
= pure $ !(convGen q defs env x y) && !(allConv q defs env xs ys)
|
||||||
allConv q defs env _ _ = pure False
|
allConv q defs env _ _ = pure False
|
||||||
|
|
||||||
|
-- If two names are standing for case blocks, check the blocks originate
|
||||||
|
-- from the same place, and have the same scrutinee
|
||||||
|
chkConvCaseBlock : FC -> Ref QVar Int -> Defs -> Env Term vars ->
|
||||||
|
NHead vars -> List (Closure vars) ->
|
||||||
|
NHead vars -> List (Closure vars) -> Core Bool
|
||||||
|
chkConvCaseBlock fc q defs env (NRef _ n) nargs (NRef _ n') nargs'
|
||||||
|
= do NS _ (CaseBlock _ _) <- full (gamma defs) n
|
||||||
|
| _ => pure False
|
||||||
|
NS _ (CaseBlock _ _) <- full (gamma defs) n'
|
||||||
|
| _ => pure False
|
||||||
|
-- both case operators. Due to the way they're elaborated, two
|
||||||
|
-- blocks might be arise from the same source but have different
|
||||||
|
-- names. So we consider them the same if the scrutinees convert,
|
||||||
|
-- and the functions are defined at the same location. This is a
|
||||||
|
-- bit of a hack - and relies on the location being stored in the
|
||||||
|
-- term accurately - but otherwise it's a quick way to find out!
|
||||||
|
Just def <- lookupCtxtExact n (gamma defs)
|
||||||
|
| _ => pure False
|
||||||
|
Just def' <- lookupCtxtExact n' (gamma defs)
|
||||||
|
| _ => pure False
|
||||||
|
let PMDef _ _ tree _ _ = definition def
|
||||||
|
| _ => pure False
|
||||||
|
let PMDef _ _ tree' _ _ = definition def'
|
||||||
|
| _ => pure False
|
||||||
|
let Just scpos = findArgPos tree
|
||||||
|
| Nothing => pure False
|
||||||
|
let Just scpos' = findArgPos tree'
|
||||||
|
| Nothing => pure False
|
||||||
|
let Just sc = getScrutinee scpos nargs
|
||||||
|
| Nothing => pure False
|
||||||
|
let Just sc' = getScrutinee scpos' nargs'
|
||||||
|
| Nothing => pure False
|
||||||
|
convGen q defs env sc sc'
|
||||||
|
pure (location def == location def')
|
||||||
|
where
|
||||||
|
-- Need to find the position of the scrutinee to see if they are the
|
||||||
|
-- same
|
||||||
|
findArgPos : CaseTree as -> Maybe Nat
|
||||||
|
findArgPos (Case idx p _ _) = Just idx
|
||||||
|
findArgPos _ = Nothing
|
||||||
|
|
||||||
|
getScrutinee : Nat -> List (Closure vs) -> Maybe (Closure vs)
|
||||||
|
getScrutinee Z (x :: xs) = Just x
|
||||||
|
getScrutinee (S k) (x :: xs) = getScrutinee k xs
|
||||||
|
getScrutinee _ _ = Nothing
|
||||||
|
chkConvCaseBlock _ _ _ _ _ _ _ _ = pure False
|
||||||
|
|
||||||
chkConvHead : Ref QVar Int -> Defs -> Env Term vars ->
|
chkConvHead : Ref QVar Int -> Defs -> Env Term vars ->
|
||||||
NHead vars -> NHead vars -> Core Bool
|
NHead vars -> NHead vars -> Core Bool
|
||||||
chkConvHead q defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
|
chkConvHead q defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
|
||||||
@ -703,10 +750,10 @@ mutual
|
|||||||
(Local fc Nothing _ First)))
|
(Local fc Nothing _ First)))
|
||||||
convGen q defs env etax tmy
|
convGen q defs env etax tmy
|
||||||
|
|
||||||
convGen q defs env (NApp _ val args) (NApp _ val' args')
|
convGen q defs env (NApp fc val args) (NApp _ val' args')
|
||||||
= if !(chkConvHead q defs env val val')
|
= if !(chkConvHead q defs env val val')
|
||||||
then allConv q defs env args args'
|
then allConv q defs env args args'
|
||||||
else pure False
|
else chkConvCaseBlock fc q defs env val args val' args'
|
||||||
|
|
||||||
convGen q defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
|
convGen q defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
|
||||||
= if tag == tag'
|
= if tag == tag'
|
||||||
|
@ -53,7 +53,7 @@ idrisTests
|
|||||||
"lazy001",
|
"lazy001",
|
||||||
-- QTT and linearity related
|
-- QTT and linearity related
|
||||||
"linear001", "linear002", "linear003", "linear004", "linear005",
|
"linear001", "linear002", "linear003", "linear004", "linear005",
|
||||||
"linear006", "linear007",
|
"linear006", "linear007", "linear008",
|
||||||
-- Parameters blocks
|
-- Parameters blocks
|
||||||
"params001",
|
"params001",
|
||||||
-- Performance: things which have been slow in the past, or which
|
-- Performance: things which have been slow in the past, or which
|
||||||
|
Loading…
Reference in New Issue
Block a user