ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Added universe constraint checker and --typeintype command line option

Browse Source
This commit is contained in:
Edwin Brady 2011-12-01 15:13:25 +00:00
parent b2f6cc3877
commit 3b5e50c1f9
7 changed files with 68 additions and 96 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
idris.cabal
View File

@ -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,

11
lib/prelude/list.idr
View File

@ -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);
}

4
samples/interp.idr
View File

@ -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;

107
src/Core/Constraints.hs
View File

@ -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
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
data Child = Lt Node | Le Node
deriving Show
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
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
solve :: Node -> Either String (M.Map String Int)
solve n = fst <$> execStateT (solveFrom 0 n) (M.empty, [])

15
src/Idris/AbsSyntax.hs
View File

@ -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'

19
src/Idris/REPL.hs
View File

@ -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

6
src/Main.hs
View File

@ -15,6 +15,7 @@ import Core.TT
import Core.Typecheck
import Core.ProofShell
import Core.Evaluate
import Core.Constraints
import Idris.AbsSyntax
import Idris.Parser
@ -22,6 +23,7 @@ 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)
{-