Permalink
Browse files

Added universe constraint checker and --typeintype command line option

  • Loading branch information...
1 parent b2f6cc3 commit 3b5e50c1f948d88de26a2404f00c0821d9ebba28 Edwin Brady committed Dec 1, 2011
Showing with 69 additions and 97 deletions.
  1. +1 −1 idris.cabal
  2. +6 −5 lib/prelude/list.idr
  3. +2 −2 samples/interp.idr
  4. +24 −85 src/Core/Constraints.hs
  5. +13 −2 src/Idris/AbsSyntax.hs
  6. +17 −2 src/Idris/REPL.hs
  7. +6 −0 src/Main.hs
View
@@ -27,7 +27,7 @@ Executable idris
Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
Core.ProofShell, Core.ProofState, Core.CoreParser,
Core.ShellParser, Core.Unify, Core.Elaborate,
- Core.CaseTree,
+ Core.CaseTree, Core.Constraints,
Idris.AbsSyntax, Idris.Parser, Idris.REPL,
Idris.REPLParser, Idris.ElabDecls, Idris.Error,
View
@@ -38,11 +38,6 @@ filter pred (x :: xs) with (pred x, filter pred xs) {
filter pred (x :: xs) | (False, fxs) = fxs;
}
-merge : Ord a => List a -> List a -> List a;
-merge xs [] = xs;
-merge [] ys = ys;
-merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
- else (y :: merge (x :: xs) ys);
sort : Ord a => List a -> List a;
sort [] = [];
@@ -55,5 +50,11 @@ sort xs = let s = split xs in
split : List a -> (List a, List a);
split xs = splitrec xs xs id;
+
+ merge : Ord a => List a -> List a -> List a;
+ merge xs [] = xs;
+ merge [] ys = ys;
+ merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))
+ else (y :: merge (x :: xs) ys);
}
View
@@ -24,8 +24,8 @@ using (G : Vect Ty n) {
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (Int -> Int -> interpTy c) ->
Expr G TyInt -> Expr G TyInt -> Expr G c
- | Op' : (interpTy a -> interpTy b -> interpTy c) ->
- Expr G a -> Expr G b -> Expr G c
+ | Op' : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
+ Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
| Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
View
@@ -1,5 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-
module Core.Constraints(ucheck) where
import Core.TT
@@ -14,13 +12,11 @@ import Data.Maybe
import qualified Data.Map as M
-ucheck :: Int -> [(UConstraint, FC)] -> TC ()
-ucheck num cs = case solve (mkNode num cs) of
- Left _ -> tfail UniverseError
- Right _ -> return ()
-
-mkNode :: Int -> [(UConstraint, FC)] -> Node
-mkNode num cs = relNode num (M.toList (mkRels cs M.empty))
+ucheck :: [(UConstraint, FC)] -> TC ()
+ucheck cs = acyclic rels (map fst (M.toList rels))
+ where lhs (ULT l _) = l
+ lhs (ULE l _) = l
+ rels = mkRels cs M.empty
type Relations = M.Map UExp [(UConstraint, FC)]
@@ -33,80 +29,23 @@ mkRels ((c, f) : cs) acc
where lhs (ULT l _) = l
lhs (ULE l _) = l
-relNode :: Int -> [(UExp, [(UConstraint, FC)])] -> Node
-relNode num [] = CI 0 $ map Le (map (expNode . UVar) [0..num])
-relNode num ((c, cons) : cs) = relNode num cs
-
-data Child = Lt Node | Le Node
- deriving Show
-
-data Node = CI Int [Child]
- | CV String [Child]
- deriving Show
-
-expNode :: UExp -> Node
-expNode (UVar i) = CV (show (UVar i)) []
-expNode (UVal i) = CI i []
-
-test :: Node
-test = CI 0 $ [Lt x, Lt y, Le z] ++ map Le ints
- where
- x = CV "x" []
- y = CV "y" [Lt z]
- z = CV "z" [Lt x]
- ints = [ -- CI 3 [Lt y]
- ]
-
-add :: Node -> Node -> Node
-add i node = undefined
-
-test2 :: Node
-test2 = CI 0 $ [ Le v84, Le q25 ] ++ map Le [g,e85,v29,f90,j45,g86,n45,v84,q25,y48,q45,h45,g90]
- where
- g = CV "g" [Le y48]
- e85 = CV "e85" [Le n45, Le q45, Le h45]
- v29 = CV "v29" [Lt g90]
- f90 = CV "f90" [Lt g90]
- j45 = CV "j45" [Lt f90]
- g86 = CV "g86" [Lt f90]
- n45 = CV "n45" []
- v84 = CV "v84" []
- q25 = CV "q25" []
- y48 = CV "y48" []
- q45 = CV "q45" []
- h45 = CV "h45" []
- g90 = CV "g90" []
-
-cyclic :: Node
-cyclic = CI 0 $ map Le [a,b,c]
- where
- a = CV "a" [Lt b]
- b = CV "b" [Lt c]
- c = CV "c" [Lt a]
-
--- onChild :: Int -> Child -> m ()
-onChild i (Lt n) = solveFrom (i+1) n
-onChild i (Le n) = solveFrom i n
-
-solveFrom ::
- ( Applicative m
- , MonadState (M.Map String Int, [String]) m
- , MonadError String m
- ) => Int -> Node -> m ()
-solveFrom num (CI i chs ) = do
- let numi = max num i
- mapM_ (onChild numi) chs
-solveFrom num (CV nm chs) = do
- nms <- snd <$> get
- if nm `elem` nms
- then throwError $ "cycle: " ++ intercalate ", " nms
- else do
- modify $ second (nm:) -- add this node for cycle detection
- i <- M.lookup nm . fst <$> get
- let numi = max num (fromMaybe 0 i)
- modify $ first (M.insert nm numi)
- mapM_ (onChild numi) chs
- modify $ second (drop 1) -- remove the node
+acyclic :: Relations -> [UExp] -> TC ()
+acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
+ where
+ checkCycle :: FC -> Relations -> [UExp] -> Int -> [UExp] -> TC ()
+ checkCycle fc r path inc [] = return ()
+ checkCycle fc r path inc (c : cs)
+ = do check fc path inc c
+ -- Remove c from r since we know there's no cycles now
+ let r' = M.insert c [] r
+ checkCycle fc r' path inc cs
+
+ check fc path inc cv
+ | inc > 0 && cv `elem` path = Error $ At fc UniverseError
+ | otherwise = case M.lookup cv r of
+ Nothing -> return ()
+ Just cs -> mapM_ (next (cv:path) inc) cs
+
+ next path inc (ULT l r, fc) = check fc path (inc + 1) r
+ next path inc (ULE l r, fc) = check fc path inc r
-solve :: Node -> Either String (M.Map String Int)
-solve n = fst <$> execStateT (solveFrom 0 n) (M.empty, [])
View
@@ -17,11 +17,12 @@ import qualified Epic.Epic as E
data IOption = IOption { opt_logLevel :: Int,
opt_typecase :: Bool,
+ opt_typeintype :: Bool,
opt_showimp :: Bool
}
deriving (Show, Eq)
-defaultOpts = IOption 0 False False
+defaultOpts = IOption 0 False False False
-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
-- without typechecking).
@@ -154,6 +155,16 @@ logLevel :: Idris Int
logLevel = do i <- get
return (opt_logLevel (idris_options i))
+typeInType :: Idris Bool
+typeInType = do i <- get
+ return (opt_typeintype (idris_options i))
+
+setTypeInType :: Bool -> Idris ()
+setTypeInType t = do i <- get
+ let opts = idris_options i
+ let opt' = opts { opt_typeintype = t }
+ put (i { idris_options = opt' })
+
impShow :: Idris Bool
impShow = do i <- get
return (opt_showimp (idris_options i))
@@ -835,7 +846,7 @@ implicitise syn ist tm
addImpl :: IState -> PTerm -> PTerm
addImpl ist ptm = ai [] ptm
where
- ai env (PRef fc f) = aiFn ist fc f []
+ ai env (PRef fc f) = aiFn ist fc f []
ai env (PEq fc l r) = let l' = ai env l
r' = ai env r in
PEq fc l' r'
View
@@ -17,6 +17,7 @@ import Paths_idris
import Core.Evaluate
import Core.ProofShell
import Core.TT
+import Core.Constraints
import System.Console.Readline
import System.FilePath
@@ -42,6 +43,15 @@ repl orig mods
Just mods -> repl orig mods
Nothing -> return ()
+iucheck :: Idris ()
+iucheck = do tit <- typeInType
+ when (not tit) $
+ do ist <- get
+ idrisCatch (tclift $ ucheck (idris_constraints ist))
+ (\e -> do let msg = report e
+ setErrLine (getErrLine msg)
+ iputStrLn msg)
+
mkPrompt [] = "Idris"
mkPrompt [x] = "*" ++ dropExtension x
mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
@@ -84,6 +94,7 @@ edit f orig
clearErr
put (orig { idris_options = idris_options i })
loadModule f
+ iucheck
return ()
where getEditor env | Just ed <- lookup "EDITOR" env = ed
| Just ed <- lookup "VISUAL" env = ed
@@ -137,10 +148,14 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t
iputStrLn (showImp imp (delab ist tm) ++ " : " ++
showImp imp (delab ist ty))
process Universes = do i <- get
- let cs = nub $ idris_constraints i
+ let cs = idris_constraints i
-- iputStrLn $ showSep "\n" (map show cs)
lift $ print (map fst cs)
- iputStrLn $ "(" ++ show (length cs) ++ " constraints)"
+ let n = length cs
+ iputStrLn $ "(" ++ show n ++ " constraints)"
+ case ucheck cs of
+ Error e -> iputStrLn $ pshow i e
+ OK _ -> iputStrLn "Universes OK"
process (Defn n) = do ctxt <- getContext
lift $ print (lookupDef Nothing n ctxt)
process (Spec t) = do (tm, ty) <- elabVal toplevel False t
View
@@ -15,13 +15,15 @@ import Core.TT
import Core.Typecheck
import Core.ProofShell
import Core.Evaluate
+import Core.Constraints
import Idris.AbsSyntax
import Idris.Parser
import Idris.REPL
import Idris.ElabDecls
import Idris.Primitives
import Idris.Imports
+import Idris.Error
import Paths_idris
-- Main program reads command line options, parses the main program, and gets
@@ -34,6 +36,7 @@ data Opt = Filename String
| OLogging Int
| Output String
| TypeCase
+ | TypeInType
deriving Eq
main = do xs <- getArgs
@@ -52,6 +55,7 @@ runIdris opts =
when runrepl $ iputStrLn banner
ist <- get
mods <- mapM loadModule inputs
+ iucheck
ok <- noErrors
when ok $ case output of
[] -> return ()
@@ -60,6 +64,7 @@ runIdris opts =
where
makeOption (OLogging i) = setLogLevel i
makeOption TypeCase = setTypeCase True
+ makeOption TypeInType = setTypeInType True
makeOption _ = return ()
getFile :: Opt -> Maybe String
@@ -83,6 +88,7 @@ parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
+parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
{-

0 comments on commit 3b5e50c

Please sign in to comment.