idris 0.9.17 → 0.9.17.1

raw patch · 34 files changed

+570/−98 lines, 34 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• idris.cabal +17/−1
• libs/contrib/Data/Graph.idr +8/−0
• libs/contrib/Data/Polyhedra.idr +9/−0
• libs/effects/Effect/File.idr +4/−3
• src/Idris/AbsSyntax.hs +6/−3
• src/Idris/AbsSyntaxTree.hs +2/−2
• src/Idris/Core/Binary.hs +16/−1
• src/Idris/Core/Constraints.hs +209/−57
• src/Idris/Core/Evaluate.hs +3/−4
• src/Idris/Core/TT.hs +12/−8
• src/Idris/Core/Typecheck.hs +35/−7
• src/Idris/Elab/Data.hs +13/−4
• src/Idris/ElabTerm.hs +2/−1
• src/Idris/IBC.hs +1/−1
• src/Idris/Parser.hs +46/−1
• src/Idris/REPL.hs +4/−2
• test/error001/expected +9/−1
• test/proof005/DefaultArgSubstitutionSuccess.idr +44/−0
• test/proof005/expected +0/−0
• test/proof005/run +3/−0
• test/proof006/DefaultArgSubstitutionSyntax.idr +49/−0
• test/proof006/expected +0/−0
• test/proof006/run +3/−0
• test/proof007/DefaultArgUnknownName.idr +10/−0
• test/proof007/expected +4/−0
• test/proof007/run +3/−0
• test/proof009/expected +26/−0
• test/proof009/input +6/−0
• test/proof009/proof009.idr +9/−0
• test/proof009/run +3/−0
• test/quasiquote001/expected +2/−2
• test/reg061/Capture.idr +9/−0
• test/reg061/expected +0/−0
• test/reg061/run +3/−0

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.17+Version:        0.9.17.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -301,6 +301,9 @@                        test/reg060/run                        test/reg060/*.idr                        test/reg060/expected+                       test/reg061/run+                       test/reg061/*.idr+                       test/reg061/expected                         test/basic001/run                        test/basic001/*.idr@@ -513,9 +516,22 @@                        test/proof004/run                        test/proof004/*.idr                        test/proof004/expected+                       test/proof005/run+                       test/proof005/*.idr+                       test/proof005/expected+                       test/proof006/run+                       test/proof006/*.idr+                       test/proof006/expected+                       test/proof007/run+                       test/proof007/*.idr+                       test/proof007/expected                        test/proof008/run                        test/proof008/*.idr                        test/proof008/expected+                       test/proof009/run+                       test/proof009/*.idr+                       test/proof009/expected+                       test/proof009/input                         test/quasiquote001/run                        test/quasiquote001/*.idr

@@ -0,0 +1,8 @@+module Data.Graph++import Data.Vect++data Edge e = MkEdge e e++data Graph : Nat −> Nat −> Type −> Type −> Type where+  MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k

@@ -0,0 +1,9 @@+module Data.Polyhedra++import Data.Vect+import Data.Graph++data Face f = MkFace (Vect n f)++data Polyhedron : Nat -> Nat -> Nat -> Type -> Type where+  MkPolyhedron : Vect k v -> Vect m (Edge v) -> Vect n (Face v) -> Polyhedron k m n v

@@ -117,9 +117,10 @@ ||| @ m The file mode. open : (fname : String)        -> (m : Mode)-       -> { [FILE_IO ()] ==> [FILE_IO (if result-                                          then OpenFile m-                                          else ())] } Eff Bool+       -> { [FILE_IO ()] ==> {result}+            [FILE_IO (if result+                        then OpenFile m+                        else ())] } Eff Bool open f m = call $ Open f m  

@@ -543,10 +543,13 @@ addConstraints fc (v, cs)     = do i <- getIState          let ctxt = tt_ctxt i-         let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,-                            next_tvar = v }-         let ics = zip cs (repeat fc) ++ idris_constraints i+         let ctxt' = ctxt { next_tvar = v }+         let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)          putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }+  where+    insertAll [] c = c+    insertAll ((c, fc) : cs) ics +       = insertAll cs $ S.insert (ConstraintFC c fc) ics  addDeferred = addDeferred' Ref addDeferredTyCon = addDeferred' (TCon 0 0)

@@ -157,7 +157,7 @@ -- | The global state used in the Idris monad data IState = IState {     tt_ctxt :: Context, -- ^ All the currently defined names and their terms-    idris_constraints :: [(UConstraint, FC)],+    idris_constraints :: S.Set ConstraintFC,       -- ^ A list of universe constraints and their corresponding source locations     idris_infixes :: [FixDecl], -- ^ Currently defined infix operators     idris_implicits :: Ctxt [PArg],@@ -309,7 +309,7 @@  -- | The initial state for the compiler idrisInit :: IState-idrisInit = IState initContext [] []+idrisInit = IState initContext S.empty []                    emptyContext emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext                    emptyContext emptyContext emptyContext emptyContext

@@ -546,7 +546,22 @@                            return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))                    _ -> error "Corrupted binary data for NameType" +-- record concrete levels only, for now+instance Binary UExp where+    put x = case x of+                 UVar t -> do putWord8 0+                              put ((-1) :: Int) -- TMP HACK!+                 UVal t -> do putWord8 1 +                              put t +    get = do i <- getWord8+             case i of+                 0 -> do x1 <- get+                         return (UVar x1)+                 1 -> do x1 <- get+                         return (UVal x1)+                 _ -> error "Corrupted binary data for UExp"+ instance {- (Binary n) => -} Binary (TT Name) where         put x           = {-# SCC "putTT" #-}@@ -600,7 +615,7 @@                            x2 <- getWord8                            return (Proj x1 ((fromEnum x2)-1))                    6 -> return Erased-                   7 -> do x1 <- get+                   7 -> do x1 <- get                             return (TType x1)                    8 -> return Impossible                    9 -> do x1 <- get

@@ -1,71 +1,223 @@ -- | Check universe constraints.-module Idris.Core.Constraints(ucheck) where+module Idris.Core.Constraints ( ucheck ) where -import Idris.Core.TT-import Idris.Core.Typecheck+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), +                       ConstraintFC(..), Err'(..) )  import Control.Applicative-import Control.Arrow-import Control.Monad.RWS-import Control.Monad.State-import qualified Data.Set as S-import Data.List-import Data.Maybe+import Control.Monad.State.Strict+import Data.List ( partition ) import qualified Data.Map.Strict as M+import qualified Data.Set as S -import Debug.Trace  -- | Check that a list of universe constraints can be satisfied.-ucheck :: [(UConstraint, FC)] -> TC ()-ucheck cs = acyclic rels (map fst (M.toList rels))-  where lhs (ULT l _) = l-        lhs (ULE l _) = l-        cs' = S.toList (S.fromList cs)-        rels = mkRels cs' M.empty+ucheck :: S.Set ConstraintFC -> TC ()+ucheck = void . solve 10 . S.filter (not . ignore)+    where+        -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with+        ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True+        ignore (ConstraintFC (ULE a b) _) = a == b+        ignore _ = False -type Relations = M.Map UExp [(UConstraint, FC)]+newtype Var = Var Int+    deriving (Eq, Ord, Show) -mkRels :: [(UConstraint, FC)] -> Relations -> Relations-mkRels [] acc = acc-mkRels ((c, f) : cs) acc-    | not (ignore c)-       = case M.lookup (lhs c) acc of-              Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)-              Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)-    | otherwise = mkRels cs acc-  where lhs (ULT l _) = l-        lhs (ULE l _) = l-        ignore (ULE l r) = l == r-        ignore _ = False+data Domain = Domain Int Int+    deriving (Eq, Ord, Show) +data SolverState =+    SolverState+        { queue       :: Queue+        , domainStore :: M.Map Var ( Domain+                                   , S.Set ConstraintFC        -- constraints that effected this variable+                                   )+        , cons_lhs    :: M.Map Var (S.Set ConstraintFC)+        , cons_rhs    :: M.Map Var (S.Set ConstraintFC)+        } -acyclic :: Relations -> [UExp] -> TC ()-acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs-  where-    checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()-    checkCycle fc r path inc [] = return ()-    checkCycle fc r path inc (c : cs)-        = do check fc r 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 Queue = Queue [ConstraintFC] (S.Set UConstraint) -    check fc r path inc (UVar x) | x < 0 = return ()-    check fc r path inc cv-        | inc > 0 && cv `elem` map fst path-            = Error $ At fc UniverseError-                -- FIXME: Make informative-                -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))-                -- Issue #1725 on the issue tracker.-                -- https://github.com/idris-lang/Idris-dev/issues/1725-        -- if we reach a cycle but we're at the same universe level, it's-        -- fine, because they must all be equal, so stop.-        | inc == 0 && cv `elem` map fst path-            = return ()-        | otherwise-             = case M.lookup cv r of-                    Nothing -> return ()-                    Just cs -> mapM_ (next r ((cv, fc):path) inc) cs -    next r path inc (ULT l x, fc) = check fc r path (inc + 1) x-    next r path inc (ULE l x, fc) = check fc r path inc x+solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)+solve maxUniverseLevel ucs =+    evalStateT (propagate >> extractSolution) initSolverState++    where+        inpConstraints = S.toAscList ucs++        -- | initial solver state.+        --   the queue contains all constraints, the domain store contains the initial domains.+        initSolverState :: SolverState+        initSolverState =+            let+                (initUnaryQueue, initQueue) = partition (\ c -> length (varsIn (uconstraint c)) == 1) inpConstraints+            in+                SolverState+                    { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map uconstraint (initUnaryQueue ++ initQueue)))+                    , domainStore = M.fromList+                        [ (v, (Domain 0 maxUniverseLevel, S.empty))+                        | v <- ordNub [ v+                                      | ConstraintFC c _ <- inpConstraints+                                      , v <- varsIn c+                                      ]+                        ]+                    , cons_lhs = constraintsLHS+                    , cons_rhs = constraintsRHS+                    }++        lhs (ULT (UVar x) _) = Just (Var x)+        lhs (ULE (UVar x) _) = Just (Var x)+        lhs _ = Nothing++        rhs (ULT _ (UVar x)) = Just (Var x)+        rhs (ULE _ (UVar x)) = Just (Var x)+        rhs _ = Nothing++        -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)+        constraintsLHS :: M.Map Var (S.Set ConstraintFC)+        constraintsLHS = M.fromListWith S.union+            [ (v, S.singleton (ConstraintFC c fc))+            | (ConstraintFC c fc) <- inpConstraints+            , let vars = varsIn c+            , length vars > 1               -- do not register unary constraints+            , v <- vars+            , lhs c == Just v+            ]++        -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)+        constraintsRHS :: M.Map Var (S.Set ConstraintFC)+        constraintsRHS = M.fromListWith S.union+            [ (v, S.singleton (ConstraintFC c fc))+            | (ConstraintFC c fc) <- inpConstraints+            , let vars = varsIn c+            , length vars > 1               -- do not register unary constraints+            , v <- vars+            , rhs c == Just v+            ]++        -- | this is where the actual work is done.+        --   dequeue the first constraint,+        --   filter domains,+        --   update domains (possibly resulting in a domain wipe out),+        --   until the queue is empty.+        propagate :: StateT SolverState TC ()+        propagate = do+            mcons <- nextConstraint+            case mcons of+                Nothing -> return ()+                Just (ConstraintFC cons fc) -> do+                    case cons of+                        ULE a b -> do+                            Domain lowerA upperA <- domainOf a+                            Domain lowerB upperB <- domainOf b+                            when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB+                            when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA+                        ULT a b -> do+                            Domain lowerA upperA <- domainOf a+                            Domain lowerB upperB <- domainOf b+                            let upperB_pred = pred upperB+                            let lowerA_succ = succ lowerA+                            when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred+                            when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ+                    propagate++        -- | extract a solution from the state.+        extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)+        extractSolution = M.map (extractValue . fst) <$> gets domainStore++        extractValue :: Domain -> Int+        extractValue (Domain x _) = x++        -- | dequeue the first constraint.+        nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)+        nextConstraint = do+            Queue list set <- gets queue+            case list of+                [] -> return Nothing+                (q:qs) -> do+                    modify $ \ st -> st { queue = Queue qs (S.delete (uconstraint q) set) }+                    return (Just q)++        -- | look up the domain of a variable from the state.+        --   for convenience, this function also accepts UVal's and returns a singleton domain for them.+        domainOf :: MonadState SolverState m => UExp -> m Domain+        domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)+        domainOf (UVal val) = return (Domain val val)++        updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()+        updateUpperBoundOf suspect (UVar var) upper = do+            doms <- gets domainStore+            let (oldDom@(Domain lower _), suspects) = doms M.! Var var+            let newDom = Domain lower upper+            when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines+                $ "Universe inconsistency."+                : ("Working on: " ++ show (UVar var))+                : ("Old domain: " ++ show oldDom)+                : ("New domain: " ++ show newDom)+                : "Involved constraints: "+                : map (("\t"++) . show) (suspect : S.toList suspects)+            modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }+            addToQueueRHS (uconstraint suspect) (Var var)+        updateUpperBoundOf _ UVal{} _ = return ()++        updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()+        updateLowerBoundOf suspect (UVar var) lower = do+            doms <- gets domainStore+            let (oldDom@(Domain _ upper), suspects) = doms M.! Var var+            let newDom = Domain lower upper+            when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines+                $ "Universe inconsistency."+                : ("Working on: " ++ show (UVar var))+                : ("Old domain: " ++ show oldDom)+                : ("New domain: " ++ show newDom)+                : "Involved constraints: "+                : map (("\t"++) . show) (suspect : S.toList suspects)+            modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }+            addToQueueLHS (uconstraint suspect) (Var var)+        updateLowerBoundOf _ UVal{} _ = return ()++        -- | add all constraints (with the given var on the lhs) to the queue+        addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()+        addToQueueLHS thisCons var = do+            clhs <- gets cons_lhs+            case M.lookup var clhs of+                Nothing -> return ()+                Just cs -> do+                    Queue list set <- gets queue+                    let set' = S.insert thisCons set+                    let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]+                    if null newCons+                        then return ()+                        else modify $ \ st -> st { queue = Queue (list ++ newCons)+                                                                 (S.union set (S.fromList (map uconstraint newCons))) }++        -- | add all constraints (with the given var on the rhs) to the queue+        addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()+        addToQueueRHS thisCons var = do+            crhs <- gets cons_rhs+            case M.lookup var crhs of+                Nothing -> return ()+                Just cs -> do+                    Queue list set <- gets queue+                    let set' = S.insert thisCons set+                    let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]+                    if null newCons+                        then return ()+                        else modify $ \ st -> st { queue = Queue (list ++ newCons)+                                                                 (insertAll (map uconstraint newCons) set) }++        insertAll [] s = s+        insertAll (x : xs) s = insertAll xs (S.insert x s)++        -- | check if a domain is wiped out.+        wipeOut :: Domain -> Bool+        wipeOut (Domain l u) = l > u++ordNub :: Ord a => [a] -> [a]+ordNub = S.toList . S.fromList++-- | variables in a constraint+varsIn :: UConstraint -> [Var]+varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]+varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]

@@ -5,7 +5,7 @@                 rt_simplify, simplify, specialise, hnf, convEq, convEq',                 Def(..), CaseInfo(..), CaseDefs(..),                 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),-                Context, initContext, ctxtAlist, uconstraints, next_tvar,+                Context, initContext, ctxtAlist, next_tvar,                 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,                 addDatatype, addCasedef, simplifyCasedef, addOperator,                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,@@ -786,16 +786,15 @@ -- | Contexts used for global definitions and for proof state. They contain -- universe constraints and existing definitions. data Context = MkContext {-                  uconstraints    :: [UConstraint],                   next_tvar       :: Int,                   definitions     :: Ctxt (Def, Accessibility, Totality, MetaInformation)                 } deriving Show  -- | The initial empty context-initContext = MkContext [] 0 emptyContext+initContext = MkContext 0 emptyContext  mapDefCtxt :: (Def -> Def) -> Context -> Context-mapDefCtxt f (MkContext c t defs) = MkContext c t (mapCtxt f' defs)+mapDefCtxt f (MkContext t defs) = MkContext t (mapCtxt f' defs)    where f' (d, a, t, m) = f' (f d, a, t, m)  -- | Get the definitions from a context

@@ -782,14 +782,6 @@ instance Sized UExp where   size _ = 1 --- We assume that universe levels have been checked, so anything external--- can just have the same universe variable and we won't get any new--- cycles.--instance Binary UExp where-    put x = return ()-    get = return (UVar (-1))- instance Show UExp where     show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]                   | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)@@ -801,6 +793,16 @@                  | ULE UExp UExp -- ^ Less than or equal to   deriving (Eq, Ord) +data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,+                                   ufc :: FC }+  deriving Show++instance Eq ConstraintFC where+    x == y = uconstraint x == uconstraint y  ++instance Ord ConstraintFC where+    compare x y = compare (uconstraint x) (uconstraint y)+ instance Show UConstraint where     show (ULT x y) = show x ++ " < " ++ show y     show (ULE x y) = show x ++ " <= " ++ show y@@ -1191,6 +1193,8 @@           Just $ RBind n' b' sc'   where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)                                                    (safeForgetEnv env v)+        safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t) +                                                      (safeForgetEnv env v)         safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)                                   Just $ fmap (\_ -> ty') b  safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

@@ -86,15 +86,38 @@       | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt             = return (P nt n' ty, ty)       | otherwise = do lift $ tfail $ NoSuchVariable n+  chk u env ap@(RApp f RType) | not holes+    -- special case to reduce constraintss+      = do (fv, fty) <- chk u env f+           let fty' = case uniqueBinders (map fst env) (finalise fty) of+                        ty@(Bind x (Pi i s k) t) -> ty+                        _ -> uniqueBinders (map fst env)+                                 $ case hnf ctxt env fty of+                                     ty@(Bind x (Pi i s k) t) -> ty+                                     _ -> normalise ctxt env fty+           case fty' of+             Bind x (Pi i (TType v') k) t ->+               do (v, cs) <- get+                  put (v+1, ULT (UVar v) v' : cs)+                  let apty = simplify initContext env+                                 (Bind x (Let (TType v') (TType (UVar v))) t)+                  return (App fv (TType (UVar v)), apty)+             Bind x (Pi i s k) t ->+                 do (av, aty) <- chk u env RType +                    convertsC ctxt env aty s+                    let apty = simplify initContext env+                                        (Bind x (Let aty av) t)+                    return (App fv av, apty)+             t -> lift $ tfail $ NonFunctionType fv fty   chk u env ap@(RApp f a)       = do (fv, fty) <- chk u env f-           (av, aty) <- chk u env a            let fty' = case uniqueBinders (map fst env) (finalise fty) of                         ty@(Bind x (Pi i s k) t) -> ty                         _ -> uniqueBinders (map fst env)                                  $ case hnf ctxt env fty of                                      ty@(Bind x (Pi i s k) t) -> ty                                      _ -> normalise ctxt env fty+           (av, aty) <- chk u env a            case fty' of              Bind x (Pi i s k) t ->                  do convertsC ctxt env aty s@@ -135,17 +158,22 @@           constType TheWorld = Constant WorldType           constType Forgot  = Erased           constType _       = TType (UVal 0)-  chk u env (RForce t) = do (_, ty) <- chk u env t-                            return (Erased, ty)+  chk u env (RForce t) +      = do (_, ty) <- chk u env t+           return (Erased, ty)   chk u env (RBind n (Pi i s k) t)       = do (sv, st) <- chk u env s-           (kv, kt) <- chk u env k-           (tv, tt) <- chk st ((n, Pi i sv kv) : env) t            (v, cs) <- get+           (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent+           put (v+1, cs)+           let maxu = UVar v+           (tv, tt) <- chk st ((n, Pi i sv kv) : env) t            case (normalise ctxt env st, normalise ctxt env tt) of                 (TType su, TType tu) -> do-                    when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)-                    let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u+                    when (not holes) $ do (v, cs) <- get+                                          put (v, ULE su maxu : +                                                  ULE tu maxu : cs)+                    let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u                     return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')                               (pToV n tv), k')                 (un, un') ->

@@ -64,7 +64,7 @@     = do let codata = Codata `elem` opts          iLOG (show fc)          undef <- isUndefined fc n-         (cty, _, t, inacc) <- buildType info syn fc [] n t_in+         (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in          -- if n is defined already, make sure it is just a type declaration          -- with the same type we've just elaborated, and no constructors          -- yet@@ -76,7 +76,7 @@          let unique = case getRetTy cty of                            UType UniqueType -> True                            _ -> False-         cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons+         cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons          ttag <- getName          i <- getIState          let as = map (const (Left (Msg ""))) (getArgTys cty)@@ -210,16 +210,18 @@                      }  elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->-           Type -> -- for kind checking+           Type -> -- for unique kind checking+           Type -> -- data type's kind            (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->            Idris (Name, Type)-elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)+elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)     = do checkUndefined fc n          logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in          (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)          ctxt <- getContext          let cty' = normalise ctxt [] cty          checkUniqueKind ckind expkind+         addDataConstraint ckind dkind           -- Check that the constructor type is, in fact, a part of the family being defined          tyIs n cty'@@ -279,6 +281,13 @@         = tclift $ tfail (At fc (UniqueKindError UniqueType n))     checkUniqueKind (UType AllTypes) _ = return ()     checkUniqueKind _ _ = return ()++    -- Constructor's kind must be <= expected kind+    addDataConstraint (TType con) (TType exp) +       = do ctxt <- getContext+            let v = next_tvar ctxt+            addConstraints fc (v, [ULT con exp])+    addDataConstraint _ _ = return ()  type EliminatorState = StateT (Map.Map String Int) Idris 

@@ -1734,7 +1734,8 @@         bname _ = Nothing     runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs     runT Intros = do g <- goal-                     attack; intro (bname g)+                     attack; +                     intro (bname g)                      try' (runT Intros)                           (return ()) True       where

@@ -37,7 +37,7 @@ import Util.Zlib (decompressEither)  ibcVersion :: Word8-ibcVersion = 100+ibcVersion = 101  data IBCFile = IBCFile { ver :: Word8,                          sourcefile :: FilePath,

@@ -59,6 +59,7 @@ import Data.Monoid import Data.Char import Data.Ord+import Data.Generics.Uniplate.Data (descendM) import qualified Data.Map as M import qualified Data.HashSet as HS import qualified Data.Text as T@@ -276,7 +277,7 @@          when (length ns /= length (nub ns))             $ unexpected "repeated variable in syntax rule"          lchar '='-         tm <- typeExpr (allowImp syn)+         tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]          terminator          return (Rule (mkSimple syms) tm sty)   where@@ -297,7 +298,51 @@        where ts = dropWhile isSpace . dropWhileEnd isSpace $ s     mkSimple' (e : es) = e : mkSimple' es     mkSimple' [] = []+    +    -- Prevent syntax variable capture by making all binders under syntax unique+    -- (the ol' Common Lisp GENSYM approach)+    uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm+    uniquifyBinders userNames = fixBind []+      where+        fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm+        fixBind rens (PRef fc n) | Just n' <- lookup n rens =+          return $ PRef fc n'+        fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =+          return $ PPatvar fc n'+        fixBind rens (PLam fc n ty body)+          | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)+          | otherwise =+            do ty' <- fixBind rens ty+               n' <- gensym n+               body' <- fixBind ((n,n'):rens) body+               return $ PLam fc n' ty' body'+        fixBind rens (PPi plic n argTy body)+          | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)+          | otherwise =+            do ty' <- fixBind rens argTy+               n' <- gensym n+               body' <- fixBind ((n,n'):rens) body+               return $ (PPi plic n' ty' body')+        fixBind rens (PLet fc n ty val body)+          | n `elem` userNames = liftM3 (PLet fc n)+                                        (fixBind rens ty)+                                        (fixBind rens val)+                                        (fixBind rens body)+          | otherwise =+            do ty' <- fixBind rens ty+               val' <- fixBind rens val+               n' <- gensym n+               body' <- fixBind ((n,n'):rens) body+               return $ (PLet fc n' ty' val' body')+        fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =+          return $ PMatchApp fc n'+        fixBind rens x = descendM (fixBind rens) x +        gensym :: Name -> IdrisParser Name+        gensym n = do ist <- get+                      let idx = idris_name ist+                      put ist { idris_name = idx + 1 }+                      return $ sMN idx (show n)  {- | Parses a syntax symbol (either binding variable, keyword or expression) 

@@ -87,6 +87,7 @@ import Data.Maybe import Data.List hiding (group) import Data.Char+import qualified Data.Set as S import Data.Version import Data.Word (Word) import Data.Either (partitionEithers)@@ -945,9 +946,10 @@ process fn Universes                      = do i <- getIState                           let cs = idris_constraints i+                          let cslist = S.toAscList cs  --                        iputStrLn $ showSep "\n" (map show cs)-                          iputStrLn $ show (map fst cs)-                          let n = length cs+                          iputStrLn $ show (map uconstraint cslist)+                          let n = length cslist                           iputStrLn $ "(" ++ show n ++ " constraints)"                           case ucheck cs of                             Error e -> iPrintError $ pshow i e

@@ -1,1 +1,9 @@-test002.idr:5:6:Universe inconsistency+test002.idr:1:6:Universe inconsistency.+Working on: z+Old domain: Domain 6 6+New domain: Domain 6 5+Involved constraints: +	ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}+	ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}+	ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}+

@@ -0,0 +1,44 @@+module DefaultArgSubstitutionSuccess++DecProofType : {a:Type} -> Dec a -> Type+DecProofType {a} (Yes _)  = a+DecProofType {a} (No _)   = a -> Void++decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec+decProof (Yes x)  = x+decProof (No x)   = x++DecType : {a:Type} -> Dec a -> Type+DecType {a} _ = a+++argsAreSame : (n:Nat) -> (m:Nat)+              -> { default (decProof (decEq m n)) same : (m=n) } -> ()+argsAreSame _ _ = ()+++argsAreDiff : (n:Nat) -> (m:Nat)+              -> { default (decProof (decEq m n)) same : (m=n) -> Void } -> ()+argsAreDiff _ _ = ()+++data SameNats : Type where+  same : (n:Nat) -> (m:Nat) ->+         { default (decProof (decEq m n)) same : (m=n) } -> SameNats++data DiffNats : Type where+  diff : (n:Nat) -> (m:Nat) ->+         { default (decProof (decEq m n)) same : (m=n) -> Void } -> DiffNats+++zArgsAreSame : ()+zArgsAreSame = argsAreSame Z Z++zszArgsAreDiff : ()+zszArgsAreDiff = argsAreDiff Z (S Z)++sameNatZs : SameNats+sameNatZs = same Z Z++diffNatsZSZ : DiffNats+diffNatsZSZ = diff Z (S Z)

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --check $@ DefaultArgSubstitutionSuccess.idr+rm -f *.ibc

@@ -0,0 +1,49 @@+module DefaultArgSubstitutionSyntax++DecProofType : {a:Type} -> Dec a -> Type+DecProofType {a} (Yes _)  = a+DecProofType {a} (No _)   = a -> Void++decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec+decProof (Yes x)  = x+decProof (No x)   = x++DecType : {a:Type} -> Dec a -> Type+DecType {a} _ = a+++syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret] +  = { default (decProof dec) prfname : DecType dec } -> ret++syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret] +  = { default (decProof dec) prfname : DecType dec -> Void } -> ret+++argsAreSame : (n:Nat) -> (m:Nat)+              -> {{ same : accept (decEq n m) }} -> ()+argsAreSame _ _ = ()+++argsAreDiff : (n:Nat) -> (m:Nat)+              -> {{ diff : reject (decEq m n) }} -> ()+argsAreDiff _ _ = ()+++data SameNats : Type where+  same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats++data DiffNats : Type where+  diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats+++zArgsAreSame : ()+zArgsAreSame = argsAreSame Z Z++zszArgsAreDiff : ()+zszArgsAreDiff = argsAreDiff Z (S Z)++sameNatZs : SameNats+sameNatZs = same Z Z++diffNatsZSZ : DiffNats+diffNatsZSZ = diff Z (S Z)

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --check $@ DefaultArgSubstitutionSyntax.idr+rm -f *.ibc

@@ -0,0 +1,10 @@+module DefaultArgUnknownName++-- FIXME: What is the expected behaviour here? Should the type declaration+-- not compile?+funWithBadDefArg : { default sadgjhsag arg : () } -> ()+funWithBadDefArg = ()++test : ()+test = funWithBadDefArg+

@@ -0,0 +1,4 @@+DefaultArgUnknownName.idr:9:6:+When elaborating right hand side of test:+When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:+        No such variable sadgjhsag

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr+rm -f *.ibc

@@ -0,0 +1,26 @@+Type checking ./proof009.idr+++----------                 Goal:                  ----------+{hole0} : Int -> Int -> Int+-Main.arhs> ----------              Other goals:              ----------+{hole0}+----------              Assumptions:              ----------+ x : Int+----------                 Goal:                  ----------+{hole1} : Int -> Int+-Main.arhs> ----------              Other goals:              ----------+{hole1},{hole0}+----------              Assumptions:              ----------+ x : Int+ y : Int+----------                 Goal:                  ----------+{hole2} : Int+-Main.arhs> arhs: No more goals.+-Main.arhs> Proof completed!+Main.arhs = proof+  intro x+  intros+  trivial++

@@ -0,0 +1,6 @@+:p arhs+intro x+intros+trivial+qed+:q

@@ -0,0 +1,9 @@+afn : Int -> Int -> Int+afn x y = ?arhs++-- plus_comm_rhs_1 : y = plus y 0+-- +-- plus_comm : (x, y : Nat) -> plus x y = plus y x+-- plus_comm Z y = plus_comm_rhs_1+-- plus_comm (S k) y = ?plus_comm_rhs_2+

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris $@ --quiet proof009.idr < input+rm -f *.ibc

@@ -1,5 +1,5 @@ (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))))) ---------------(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))) ---------------(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24))))

@@ -0,0 +1,9 @@+module Capture++-- Test for variable capture in syntax++syntax delay  [x] = \z => case z of { () => x }+syntax delay' [z] = delay z++capture : a -> () -> a+capture x = delay' x

@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris $@ Capture.idr --check+rm -f *.ibc