mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-23 06:57:15 +03:00
Deal with shadowing better in patterns
Variable names in patterns should override global names, as long as they are not applied to anything. If the global name is desired (e.g. if it is the result of a dependency elsewhere, either use a _ or give the qualified version of the name)
This commit is contained in:
parent
4ff3b25441
commit
f26b42f8ce
@ -1,5 +1,5 @@
|
||||
Name: idris
|
||||
Version: 0.9.4
|
||||
Version: 0.9.4.2
|
||||
License: BSD3
|
||||
License-file: LICENSE
|
||||
Author: Edwin Brady
|
||||
@ -45,7 +45,7 @@ Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h
|
||||
rts/libtest.c
|
||||
Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
|
||||
lib/control/monad/*.idr lib/language/*.idr
|
||||
tutorial/examples/*.idr
|
||||
tutorial/examples/*.idr lib/base.ipkg
|
||||
rts/*.c rts/*.h rts/Makefile
|
||||
|
||||
source-repository head
|
||||
@ -74,7 +74,7 @@ Executable idris
|
||||
|
||||
IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
|
||||
IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
|
||||
IRTS.Compiler,
|
||||
IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,
|
||||
|
||||
Paths_idris
|
||||
|
||||
|
@ -705,13 +705,24 @@ addImpl' inpat env ist ptm = ai env ptm
|
||||
|
||||
aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
|
||||
aiFn inpat True ist fc f []
|
||||
= case lookupCtxt Nothing f (idris_implicits ist) of
|
||||
[] -> Right $ PRef fc f
|
||||
alts -> if (any (all imp) alts)
|
||||
= case lookupDef Nothing f (tt_ctxt ist) of
|
||||
[] -> Right $ PPatvar fc f
|
||||
alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
|
||||
-- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
|
||||
if (not (vname f) || tcname f
|
||||
|| any constructor alts || any allImp ialts)
|
||||
then aiFn inpat False ist fc f [] -- use it as a constructor
|
||||
else Right $ PRef fc f
|
||||
else Right $ PPatvar fc f
|
||||
where imp (PExp _ _ _) = False
|
||||
imp _ = True
|
||||
allImp [] = False
|
||||
allImp xs = all imp xs
|
||||
constructor (TyDecl (DCon _ _) _) = True
|
||||
constructor _ = False
|
||||
|
||||
vname (UN n) = True -- non qualified
|
||||
vname _ = False
|
||||
|
||||
aiFn inpat expat ist fc f as
|
||||
| f `elem` primNames = Right $ PApp fc (PRef fc f) as
|
||||
aiFn inpat expat ist fc f as
|
||||
|
@ -342,6 +342,7 @@ updateNs ns t = mapPT updateRef t
|
||||
|
||||
data PTerm = PQuote Raw
|
||||
| PRef FC Name
|
||||
| PPatvar FC Name
|
||||
| PLam Name PTerm PTerm
|
||||
| PPi Plicity Name PTerm PTerm
|
||||
| PLet Name PTerm PTerm PTerm
|
||||
@ -650,6 +651,7 @@ prettyImp impl = prettySe 10
|
||||
text "![" $$ pretty r <> text "]"
|
||||
else
|
||||
text "![" <> pretty r <> text "]"
|
||||
prettySe p (PPatvar fc n) = pretty n
|
||||
prettySe p (PRef fc n) =
|
||||
if impl then
|
||||
pretty n
|
||||
@ -825,6 +827,7 @@ prettyImp impl = prettySe 10
|
||||
showImp :: Bool -> PTerm -> String
|
||||
showImp impl tm = se 10 tm where
|
||||
se p (PQuote r) = "![" ++ show r ++ "]"
|
||||
se p (PPatvar fc n) = show n
|
||||
se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
|
||||
else showbasic n
|
||||
where showbasic n@(UN _) = show n
|
||||
|
@ -153,6 +153,7 @@ elab ist info pattern tcgen fn tm
|
||||
= trySeq as
|
||||
where trySeq [] = fail "All alternatives fail to elaborate"
|
||||
trySeq (x : xs) = try (elab' ina x) (trySeq xs)
|
||||
elab' ina (PPatvar fc n) | pattern = patvar n
|
||||
elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
|
||||
= do ctxt <- get_context
|
||||
let iscon = isConName Nothing n ctxt
|
||||
|
@ -1087,6 +1087,9 @@ instance Binary PTerm where
|
||||
PTactics x1 -> do putWord8 25
|
||||
put x1
|
||||
PImpossible -> putWord8 27
|
||||
PPatvar x1 x2 -> do putWord8 28
|
||||
put x1
|
||||
put x2
|
||||
get
|
||||
= do i <- getWord8
|
||||
case i of
|
||||
@ -1164,6 +1167,9 @@ instance Binary PTerm where
|
||||
25 -> do x1 <- get
|
||||
return (PTactics x1)
|
||||
27 -> return PImpossible
|
||||
28 -> do x1 <- get
|
||||
x2 <- get
|
||||
return (PPatvar x1 x2)
|
||||
_ -> error "Corrupted binary data for PTerm"
|
||||
|
||||
instance (Binary t) => Binary (PTactic' t) where
|
||||
|
@ -1,4 +1,4 @@
|
||||
#!/bin/bash
|
||||
idris test014.idr -o test014
|
||||
./test014
|
||||
rm -f test014 test014.ibc
|
||||
rm -f test014 resimp.ibc test014.ibc
|
||||
|
3
test/test015/expected
Normal file
3
test/test015/expected
Normal file
@ -0,0 +1,3 @@
|
||||
00101010
|
||||
01011001
|
||||
010000011
|
28
test/test015/parity.idr
Normal file
28
test/test015/parity.idr
Normal file
@ -0,0 +1,28 @@
|
||||
module parity
|
||||
|
||||
data Parity : Nat -> Set where
|
||||
even : Parity (n + n)
|
||||
odd : Parity (S (n + n))
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity O = even {n=O}
|
||||
parity (S O) = odd {n=O}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | even ?= even {n=S j}
|
||||
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
|
||||
|
||||
|
||||
parity_lemma_2 = proof {
|
||||
intro;
|
||||
intro;
|
||||
rewrite sym (plusSuccRightSucc j j);
|
||||
trivial;
|
||||
}
|
||||
|
||||
parity_lemma_1 = proof {
|
||||
intro j;
|
||||
intro;
|
||||
rewrite sym (plusSuccRightSucc j j);
|
||||
trivial;
|
||||
}
|
||||
|
4
test/test015/run
Executable file
4
test/test015/run
Executable file
@ -0,0 +1,4 @@
|
||||
#!/bin/bash
|
||||
idris test015.idr -o test015
|
||||
./test015
|
||||
rm -f test015 parity.ibc test015.ibc
|
141
test/test015/test015.idr
Normal file
141
test/test015/test015.idr
Normal file
@ -0,0 +1,141 @@
|
||||
module main
|
||||
|
||||
import parity
|
||||
import system
|
||||
|
||||
data Bit : Nat -> Set where
|
||||
b0 : Bit 0
|
||||
b1 : Bit 1
|
||||
|
||||
instance Show (Bit n) where
|
||||
show b0 = "0"
|
||||
show b1 = "1"
|
||||
|
||||
infixl 5 #
|
||||
|
||||
data Binary : (width : Nat) -> (value : Nat) -> Set where
|
||||
zero : Binary O O
|
||||
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
|
||||
|
||||
instance Show (Binary w k) where
|
||||
show zero = ""
|
||||
show (bin # bit) = show bin ++ show bit
|
||||
|
||||
pad : Binary w n -> Binary (S w) n
|
||||
pad zero = zero # b0
|
||||
pad (num # x) = pad num # x
|
||||
|
||||
natToBin : (width : Nat) -> (n : Nat) ->
|
||||
Maybe (Binary width n)
|
||||
natToBin O (S k) = Nothing
|
||||
natToBin O O = Just zero
|
||||
natToBin (S k) O = do x <- natToBin k O
|
||||
Just (pad x)
|
||||
natToBin (S w) (S k) with (parity k)
|
||||
natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j
|
||||
let value = jbin # b1
|
||||
?ntbEven
|
||||
natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)
|
||||
let value = jbin # b0
|
||||
?ntbOdd
|
||||
|
||||
testBin : Maybe (Binary 8 42)
|
||||
testBin = natToBin _ _
|
||||
|
||||
pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
|
||||
term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
|
||||
|
||||
addBit : Bit x -> Bit y -> Bit c ->
|
||||
(bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
|
||||
addBit b0 b0 b0 = bitpair b0 b0
|
||||
addBit b0 b0 b1 = bitpair b0 b1
|
||||
addBit b0 b1 b0 = bitpair b0 b1
|
||||
addBit b0 b1 b1 = bitpair b1 b0
|
||||
addBit b1 b0 b0 = bitpair b0 b1
|
||||
addBit b1 b0 b1 = bitpair b1 b0
|
||||
addBit b1 b1 b0 = bitpair b1 b0
|
||||
addBit b1 b1 b1 = bitpair b1 b1
|
||||
|
||||
adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
|
||||
adc zero zero carry ?= zero # carry
|
||||
adc (numx # bx) (numy # by) carry
|
||||
?= let (bitpair carry0 lsb) = addBit bx by carry in
|
||||
adc numx numy carry0 # lsb
|
||||
|
||||
readNum : IO Nat
|
||||
readNum = do putStr "Enter a number:"
|
||||
i <- getLine
|
||||
let n : Int = cast i
|
||||
return (fromInteger n)
|
||||
|
||||
main : IO ()
|
||||
main = do let Just bin1 = natToBin 8 42
|
||||
print bin1
|
||||
let Just bin2 = natToBin 8 89
|
||||
print bin2
|
||||
print (adc bin1 bin2 b0)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
---------- Proofs ----------
|
||||
|
||||
main.ntbOdd = proof {
|
||||
intro w,j;
|
||||
rewrite sym (plusZeroRightNeutral j);
|
||||
rewrite plusSuccRightSucc j j;
|
||||
intros;
|
||||
refine Just;
|
||||
trivial;
|
||||
}
|
||||
|
||||
main.ntbEven = proof {
|
||||
compute;
|
||||
intro w,j;
|
||||
rewrite sym (plusZeroRightNeutral j);
|
||||
intros;
|
||||
refine Just;
|
||||
trivial;
|
||||
}
|
||||
|
||||
-- There is almost certainly an easier proof. I don't care, for now :)
|
||||
|
||||
main.adc_lemma_2 = proof {
|
||||
intro c,w,v,bit0,num0;
|
||||
intro b0,v1,bit1,num1,b1;
|
||||
intro bc,x,x1,bx,bx1;
|
||||
rewrite sym (plusZeroRightNeutral x);
|
||||
rewrite sym (plusZeroRightNeutral v1);
|
||||
rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));
|
||||
rewrite sym (plusZeroRightNeutral v);
|
||||
intros;
|
||||
rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
|
||||
rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);
|
||||
rewrite (plusAssociative bit0 (plus v v) bit1);
|
||||
rewrite plusCommutative bit1 (plus v v);
|
||||
rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
|
||||
rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
|
||||
rewrite sym b;
|
||||
rewrite plusAssociative x1 (plus x x) (plus v v);
|
||||
rewrite plusAssociative x x (plus v v);
|
||||
rewrite sym (plusAssociative x v v);
|
||||
rewrite plusCommutative v (plus x v);
|
||||
rewrite sym (plusAssociative x v (plus x v));
|
||||
rewrite (plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1));
|
||||
rewrite sym (plusAssociative (plus (plus x v) (plus x v)) v1 v1);
|
||||
rewrite (plusAssociative (plus x v) (plus x v) v1);
|
||||
rewrite (plusCommutative v1 (plus x v));
|
||||
rewrite sym (plusAssociative (plus x v) v1 (plus x v));
|
||||
rewrite (plusAssociative (plus (plus x v) v1) (plus x v) v1);
|
||||
trivial;
|
||||
}
|
||||
|
||||
main.adc_lemma_1 = proof {
|
||||
intros;
|
||||
rewrite sym (plusZeroRightNeutral c) ;
|
||||
trivial;
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user