3b5e50c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added universe constraint checker and --typeintype command line option

3b5e50cEdwin Brady15 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -27,7 +27,7 @@ Executable idris

27 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,

28 Core.ProofShell, Core.ProofState, Core.CoreParser,

29 Core.ShellParser, Core.Unify, Core.Elaborate,

30− Core.CaseTree,

30+ Core.CaseTree, Core.Constraints,

32 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

33 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

lib/prelude/list.idr+6−5

@@ -38,11 +38,6 @@ filter pred (x :: xs) with (pred x, filter pred xs) {

38 filter pred (x :: xs) | (False, fxs) = fxs;

39}

41−merge : Ord a => List a -> List a -> List a;

42−merge xs [] = xs;

43−merge [] ys = ys;

44−merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))

45− else (y :: merge (x :: xs) ys);

47sort : Ord a => List a -> List a;

42sort : Ord a => List a -> List a;

48sort [] = [];

43sort [] = [];

@@ -55,5 +50,11 @@ sort xs = let s = split xs in

56 split : List a -> (List a, List a);

51 split : List a -> (List a, List a);

57 split xs = splitrec xs xs id;

52 split xs = splitrec xs xs id;

53+

54+ merge : Ord a => List a -> List a -> List a;

55+ merge xs [] = xs;

56+ merge [] ys = ys;

57+ merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))

58+ else (y :: merge (x :: xs) ys);

58}

59}

samples/interp.idr+2−2

@@ -24,8 +24,8 @@ using (G : Vect Ty n) {

24 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

25 | Op : (Int -> Int -> interpTy c) ->

26 Expr G TyInt -> Expr G TyInt -> Expr G c

27− | Op' : (interpTy a -> interpTy b -> interpTy c) ->

27+ | Op' : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

28− Expr G a -> Expr G b -> Expr G c

28+ Expr G c

29 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

src/Core/Constraints.hs+24−85

@@ -1,5 +1,3 @@

1−{-# LANGUAGE FlexibleContexts #-}

2−

3module Core.Constraints(ucheck) where

1module Core.Constraints(ucheck) where

5import Core.TT

3import Core.TT

@@ -14,13 +12,11 @@ import Data.Maybe

14import qualified Data.Map as M

12import qualified Data.Map as M

17−ucheck :: Int -> [(UConstraint, FC)] -> TC ()

15+ucheck :: [(UConstraint, FC)] -> TC ()

18−ucheck num cs = case solve (mkNode num cs) of

16+ucheck cs = acyclic rels (map fst (M.toList rels))

19− Left _ -> tfail UniverseError

17+ where lhs (ULT l _) = l

20− Right _ -> return ()

18+ lhs (ULE l _) = l

21−

22−mkNode :: Int -> [(UConstraint, FC)] -> Node

23−mkNode num cs = relNode num (M.toList (mkRels cs M.empty))

19+ rels = mkRels cs M.empty

25type Relations = M.Map UExp [(UConstraint, FC)]

21type Relations = M.Map UExp [(UConstraint, FC)]

@@ -33,80 +29,23 @@ mkRels ((c, f) : cs) acc

33 where lhs (ULT l _) = l

29 where lhs (ULT l _) = l

34 lhs (ULE l _) = l

30 lhs (ULE l _) = l

36−relNode :: Int -> [(UExp, [(UConstraint, FC)])] -> Node

32+acyclic :: Relations -> [UExp] -> TC ()

37−relNode num [] = CI 0 $ map Le (map (expNode . UVar) [0..num])

33+acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

38−relNode num ((c, cons) : cs) = relNode num cs

34+ where

39−

35+ checkCycle :: FC -> Relations -> [UExp] -> Int -> [UExp] -> TC ()

40−data Child = Lt Node | Le Node

36+ checkCycle fc r path inc [] = return ()

41− deriving Show

37+ checkCycle fc r path inc (c : cs)

42−

38+ = do check fc path inc c

43−data Node = CI Int [Child]

39+ -- Remove c from r since we know there's no cycles now

44− | CV String [Child]

40+ let r' = M.insert c [] r

45− deriving Show

41+ checkCycle fc r' path inc cs

46−

42+

47−expNode :: UExp -> Node

43+ check fc path inc cv

48−expNode (UVar i) = CV (show (UVar i)) []

44+ | inc > 0 && cv `elem` path = Error $ At fc UniverseError

49−expNode (UVal i) = CI i []

45+ | otherwise = case M.lookup cv r of

50−

46+ Nothing -> return ()

51−test :: Node

47+ Just cs -> mapM_ (next (cv:path) inc) cs

52−test = CI 0 $ [Lt x, Lt y, Le z] ++ map Le ints

48+

53− where

49+ next path inc (ULT l r, fc) = check fc path (inc + 1) r

54− x = CV "x" []

50+ next path inc (ULE l r, fc) = check fc path inc r

55− y = CV "y" [Lt z]

56− z = CV "z" [Lt x]

57− ints = [ -- CI 3 [Lt y]

58− ]

59−

60−add :: Node -> Node -> Node

61−add i node = undefined

62−

63−test2 :: Node

64−test2 = CI 0 $ [ Le v84, Le q25 ] ++ map Le [g,e85,v29,f90,j45,g86,n45,v84,q25,y48,q45,h45,g90]

65− where

66− g = CV "g" [Le y48]

67− e85 = CV "e85" [Le n45, Le q45, Le h45]

68− v29 = CV "v29" [Lt g90]

69− f90 = CV "f90" [Lt g90]

70− j45 = CV "j45" [Lt f90]

71− g86 = CV "g86" [Lt f90]

72− n45 = CV "n45" []

73− v84 = CV "v84" []

74− q25 = CV "q25" []

75− y48 = CV "y48" []

76− q45 = CV "q45" []

77− h45 = CV "h45" []

78− g90 = CV "g90" []

79−

80−cyclic :: Node

81−cyclic = CI 0 $ map Le [a,b,c]

82− where

83− a = CV "a" [Lt b]

84− b = CV "b" [Lt c]

85− c = CV "c" [Lt a]

86−

87−-- onChild :: Int -> Child -> m ()

88−onChild i (Lt n) = solveFrom (i+1) n

89−onChild i (Le n) = solveFrom i n

90−

91−solveFrom ::

92− ( Applicative m

93− , MonadState (M.Map String Int, [String]) m

94− , MonadError String m

95− ) => Int -> Node -> m ()

96−solveFrom num (CI i chs ) = do

97− let numi = max num i

98− mapM_ (onChild numi) chs

99−solveFrom num (CV nm chs) = do

100− nms <- snd <$> get

101− if nm `elem` nms

102− then throwError $ "cycle: " ++ intercalate ", " nms

103− else do

104− modify $ second (nm:) -- add this node for cycle detection

105− i <- M.lookup nm . fst <$> get

106− let numi = max num (fromMaybe 0 i)

107− modify $ first (M.insert nm numi)

108− mapM_ (onChild numi) chs

109− modify $ second (drop 1) -- remove the node

110

111−solve :: Node -> Either String (M.Map String Int)

112−solve n = fst <$> execStateT (solveFrom 0 n) (M.empty, [])

src/Idris/AbsSyntax.hs+13−2

@@ -17,11 +17,12 @@ import qualified Epic.Epic as E

18data IOption = IOption { opt_logLevel :: Int,

19 opt_typecase :: Bool,

20+ opt_typeintype :: Bool,

20 opt_showimp :: Bool

21 opt_showimp :: Bool

21 }

22 }

22 deriving (Show, Eq)

23 deriving (Show, Eq)

24−defaultOpts = IOption 0 False False

25+defaultOpts = IOption 0 False False False

26-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

27-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

27-- without typechecking).

28-- without typechecking).

@@ -154,6 +155,16 @@ logLevel :: Idris Int

154logLevel = do i <- get

155logLevel = do i <- get

155 return (opt_logLevel (idris_options i))

156 return (opt_logLevel (idris_options i))

156

157

158+typeInType :: Idris Bool

159+typeInType = do i <- get

160+ return (opt_typeintype (idris_options i))

161+

162+setTypeInType :: Bool -> Idris ()

163+setTypeInType t = do i <- get

164+ let opts = idris_options i

165+ let opt' = opts { opt_typeintype = t }

166+ put (i { idris_options = opt' })

167+

157impShow :: Idris Bool

168impShow :: Idris Bool

158impShow = do i <- get

169impShow = do i <- get

159 return (opt_showimp (idris_options i))

170 return (opt_showimp (idris_options i))

@@ -835,7 +846,7 @@ implicitise syn ist tm

835addImpl :: IState -> PTerm -> PTerm

846addImpl :: IState -> PTerm -> PTerm

836addImpl ist ptm = ai [] ptm

847addImpl ist ptm = ai [] ptm

837 where

848 where

838− ai env (PRef fc f) = aiFn ist fc f []

849+ ai env (PRef fc f) = aiFn ist fc f []

839 ai env (PEq fc l r) = let l' = ai env l

850 ai env (PEq fc l r) = let l' = ai env l

840 r' = ai env r in

851 r' = ai env r in

841 PEq fc l' r'

852 PEq fc l' r'

src/Idris/REPL.hs+17−2

@@ -17,6 +17,7 @@ import Paths_idris

17import Core.Evaluate

18import Core.ProofShell

19import Core.TT

20+import Core.Constraints

21import System.Console.Readline

22import System.Console.Readline

22import System.FilePath

23import System.FilePath

@@ -42,6 +43,15 @@ repl orig mods

42 Just mods -> repl orig mods

43 Just mods -> repl orig mods

43 Nothing -> return ()

44 Nothing -> return ()

46+iucheck :: Idris ()

47+iucheck = do tit <- typeInType

48+ when (not tit) $

49+ do ist <- get

50+ idrisCatch (tclift $ ucheck (idris_constraints ist))

51+ (\e -> do let msg = report e

52+ setErrLine (getErrLine msg)

53+ iputStrLn msg)

54+

45mkPrompt [] = "Idris"

55mkPrompt [] = "Idris"

46mkPrompt [x] = "*" ++ dropExtension x

56mkPrompt [x] = "*" ++ dropExtension x

47mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

57mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

@@ -84,6 +94,7 @@ edit f orig

84 clearErr

94 clearErr

85 put (orig { idris_options = idris_options i })

95 put (orig { idris_options = idris_options i })

86 loadModule f

96 loadModule f

97+ iucheck

87 return ()

98 return ()

88 where getEditor env | Just ed <- lookup "EDITOR" env = ed

99 where getEditor env | Just ed <- lookup "EDITOR" env = ed

89 | Just ed <- lookup "VISUAL" env = ed

100 | Just ed <- lookup "VISUAL" env = ed

@@ -137,10 +148,14 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t

137 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

148 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

138 showImp imp (delab ist ty))

149 showImp imp (delab ist ty))

139process Universes = do i <- get

150process Universes = do i <- get

140− let cs = nub $ idris_constraints i

151+ let cs = idris_constraints i

141-- iputStrLn $ showSep "\n" (map show cs)

152-- iputStrLn $ showSep "\n" (map show cs)

142 lift $ print (map fst cs)

153 lift $ print (map fst cs)

143− iputStrLn $ "(" ++ show (length cs) ++ " constraints)"

154+ let n = length cs

155+ iputStrLn $ "(" ++ show n ++ " constraints)"

156+ case ucheck cs of

157+ Error e -> iputStrLn $ pshow i e

158+ OK _ -> iputStrLn "Universes OK"

144process (Defn n) = do ctxt <- getContext

159process (Defn n) = do ctxt <- getContext

145 lift $ print (lookupDef Nothing n ctxt)

160 lift $ print (lookupDef Nothing n ctxt)

146process (Spec t) = do (tm, ty) <- elabVal toplevel False t

161process (Spec t) = do (tm, ty) <- elabVal toplevel False t

src/Main.hs+6

@@ -15,6 +15,7 @@ import Core.TT

15import Core.Typecheck

16import Core.ProofShell

17import Core.Evaluate

18+import Core.Constraints

19import Idris.AbsSyntax

20import Idris.AbsSyntax

20import Idris.Parser

21import Idris.Parser

@@ -22,6 +23,7 @@ import Idris.REPL

22import Idris.ElabDecls

23import Idris.ElabDecls

23import Idris.Primitives

24import Idris.Primitives

24import Idris.Imports

25import Idris.Imports

26+import Idris.Error

25import Paths_idris

27import Paths_idris

27-- Main program reads command line options, parses the main program, and gets

29-- Main program reads command line options, parses the main program, and gets

@@ -34,6 +36,7 @@ data Opt = Filename String

34 | OLogging Int

36 | OLogging Int

35 | Output String

37 | Output String

36 | TypeCase

38 | TypeCase

39+ | TypeInType

37 deriving Eq

40 deriving Eq

39main = do xs <- getArgs

42main = do xs <- getArgs

@@ -52,6 +55,7 @@ runIdris opts =

52 when runrepl $ iputStrLn banner

55 when runrepl $ iputStrLn banner

53 ist <- get

56 ist <- get

54 mods <- mapM loadModule inputs

57 mods <- mapM loadModule inputs

58+ iucheck

55 ok <- noErrors

59 ok <- noErrors

56 when ok $ case output of

60 when ok $ case output of

57 [] -> return ()

61 [] -> return ()

@@ -60,6 +64,7 @@ runIdris opts =

60 where

64 where

61 makeOption (OLogging i) = setLogLevel i

65 makeOption (OLogging i) = setLogLevel i

62 makeOption TypeCase = setTypeCase True

66 makeOption TypeCase = setTypeCase True

67+ makeOption TypeInType = setTypeInType True

63 makeOption _ = return ()

68 makeOption _ = return ()

65getFile :: Opt -> Maybe String

70getFile :: Opt -> Maybe String

@@ -83,6 +88,7 @@ parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

83parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

88parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

84parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

89parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

85parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

90parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

91+parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

86parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

92parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

88{-

94{-