dcc09e0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix metavariable naming in namespaces

commitdcc09e00b2d65708858c42d051411a8bbca621cd authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 1 Jan 2012, 18:59 (15 years ago) parent16708a9

9 files changed+92−9

compare with master

unifiedsplit

lib/prelude/nat.idr+1−1 src/Core/TT.hs+1 src/Idris/ElabTerm.hs+5−3 src/Idris/Parser.hs+4−3 src/Idris/Prover.hs+2−2 tutorial/examples/theorems.idr+38 tutorial/examples/views.idr+39 tutorial/provisional.tex+1 tutorial/theorems.tex+1

lib/prelude/nat.idr+1−1

@@ -51,7 +51,7 @@ plusnO : (m : Nat) -> m + O = m;

5151plusnO O = refl;

5252plusnO (S k) = eqRespS (plusnO k);

5353

54−plusn_Sm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m);

54+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);

5555plusn_Sm O m = refl;

5656plusn_Sm (S j) m = eqRespS (plusn_Sm _ _);

5757

src/Core/TT.hs+1

@@ -415,6 +415,7 @@ uniqueName :: Name -> [Name] -> Name

415415uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

416416 | otherwise = n

417417

418+nextName (NS x s) = NS (nextName x) s

418419nextName (MN i n) = MN (i+1) n

419420nextName (UN x) = let (num', nm') = span isDigit (reverse x)

420421 nm = reverse nm'

src/Idris/ElabTerm.hs+5−3

@@ -208,10 +208,12 @@ elab ist info pattern tcgen fn tm

208208 solve

209209 elab' ina Placeholder = do (h : hs) <- get_holes

210210 movelast h

211− elab' ina (PMetavar n) = let n' = case namespace info of

212− Just xs@(_:_) -> NS n xs

213− _ -> n in

211+ elab' ina (PMetavar n) = let n' = mkN n in

214212 do attack; defer n'; solve

213+ where mkN n@(NS _ _) = n

214+ mkN n = case namespace info of

215+ Just xs@(_:_) -> NS n xs

216+ _ -> n

215217 elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

216218 elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts

217219 elab' ina (PElabError e) = fail e

src/Idris/Parser.hs+4−3

@@ -340,6 +340,7 @@ pNamespace syn =

340340 return [PNamespace n (concat ds)]

341341

342342expandNS :: SyntaxInfo -> Name -> Name

343+expandNS syn n@(NS _ _) = n

343344expandNS syn n = case syn_namespace syn of

344345 [] -> n

345346 xs -> NS n xs

@@ -796,9 +797,9 @@ pRHS syn n = do lchar '='; pExpr syn

796797 <|> do symbol "?="; rhs <- pExpr syn;

797798 return (PLet (UN "value") Placeholder rhs (PMetavar n'))

798799 <|> do reserved "impossible"; return PImpossible

799− where n' = case n of

800− UN x -> UN (x++"_lemma_1")

801− x -> x

800+ where mkN (UN x) = UN (x++"_lemma_1")

801+ mkN (NS x n) = NS (mkN x) n

802+ n' = mkN n

802803

803804pClause :: SyntaxInfo -> IParser PClause

804805pClause syn

src/Idris/Prover.hs+2−2

@@ -55,8 +55,8 @@ dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no mo

5555dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)

5656 = do let OK ty = goalAtFocus ps

5757 let OK env = envAtFocus ps

58− putStrLn $ "Other goals: " ++ show hs ++ "\n"

59− putStr $ showPs (reverse env)

58+-- putStrLn $ "Other goals: " ++ show hs ++ "\n"

59+ putStr $ "\n" ++ showPs (reverse env)

6060 putStrLn $ "---------------------------------- (" ++ show nm

6161 ++ ") --------"

6262 putStrLn $ show h ++ " : " ++ showG ty ++ "\n"

tutorial/examples/theorems.idrnew file+38

@@ -0,0 +1,38 @@

2+fiveIsFive : 5 = 5;

3+fiveIsFive = refl;

5+twoPlusTwo : 2 + 2 = 4;

6+twoPlusTwo = refl;

8+plusReduces : (n:Nat) -> plus O n = n;

9+plusReduces n = refl;

10+

11+plusReducesO : (n:Nat) -> n = plus n O;

12+plusReducesO O = refl;

13+plusReducesO (S k) = eqRespS (plusReducesO k);

14+

15+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m);

16+plusReducesS O m = refl;

17+plusReducesS (S k) m = eqRespS (plusReducesS k m);

18+

19+plusReducesO' : (n:Nat) -> n = plus n O;

20+plusReducesO' O = ?plusredO_O;

21+plusReducesO' (S k) = let ih = plusReducesO' k in

22+ ?plusredO_S;

23+

24+

25+---------- Proofs ----------

26+

27+plusredO_S = proof {

28+ intro;

29+ intro;

30+ rewrite ih;

31+ trivial;

32+};

33+

34+plusredO_O = proof {

35+ compute;

36+ trivial;

37+};

38+

tutorial/examples/views.idrnew file+39

@@ -0,0 +1,39 @@

1+module views;

3+data Parity : Nat -> Set where

4+ even : Parity (n + n)

5+ | odd : Parity (S (n + n));

7+parity : (n:Nat) -> Parity n;

8+parity O = even {n=O};

9+parity (S O) = odd {n=O};

10+parity (S (S k)) with parity k {

11+ parity (S (S (j + j))) | even ?= even {n=S j};

12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j};

13+}

14+

15+

16+natToBin : Nat -> List Bool;

17+natToBin O = Nil;

18+natToBin k with parity k {

19+ natToBin (j + j) | even = False :: natToBin j;

20+ natToBin (S (j + j)) | odd = True :: natToBin j;

21+}

22+

23+

24+---------- Proofs ----------

25+

26+views.parity_lemma_2 = proof {

27+ intro;

28+ intro;

29+ rewrite plusn_Sm j j;

30+ trivial;

31+};

32+

33+views.parity_lemma_1 = proof {

34+ intro j;

35+ intro;

36+ rewrite plusn_Sm j j;

37+ trivial;

38+};

39+

tutorial/provisional.texnew file+1

@@ -0,0 +1 @@

1+\section{Provisional Definitions}

tutorial/theorems.texnew file+1

@@ -0,0 +1 @@

1+\section{Theorem Proving}