From 54ac7237441fce3800536ef6166512da38278aed Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 24 Oct 2019 20:33:28 +0300 Subject: [PATCH 1/2] add sourcedir option --- src/Core/Context.idr | 178 ++++++++++++++++++++------------------- src/Core/Core.idr | 83 +++++++++--------- src/Core/Directory.idr | 56 ++++++------ src/Core/Options.idr | 6 +- src/Idris/ModTree.idr | 28 +++--- src/Idris/Package.idr | 82 +++++++++++------- src/Idris/ProcessIdr.idr | 30 +++---- src/Yaffle/Main.idr | 6 +- 8 files changed, 254 insertions(+), 215 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 52f0f78..eab50ff 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -34,7 +34,7 @@ data Def : Type where -- find size changes in termination checking Def -- Ordinary function definition ExternDef : (arity : Nat) -> Def - ForeignDef : (arity : Nat) -> + ForeignDef : (arity : Nat) -> List String -> -- supported calling conventions, -- e.g "C:printf,libc,stdlib.h", "scheme:display", ... Def @@ -53,7 +53,7 @@ data Def : Type where BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def -- Constraints are integer references into the current map of -- constraints in the UnifyState (see Core.UnifyState) - Guess : (guess : ClosedTerm) -> + Guess : (guess : ClosedTerm) -> (envbind : Nat) -> -- Number of things in the environment when -- we guessed the term (constraints : List Int) -> Def @@ -65,15 +65,15 @@ data Def : Type where export Show Def where show None = "undefined" - show (PMDef _ args ct rt pats) + show (PMDef _ args ct rt pats) = show args ++ "; " ++ show ct show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a - show (TCon t a ps ds ms cons) - = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ - " constructors: " ++ show cons ++ + show (TCon t a ps ds ms cons) + = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ + " constructors: " ++ show cons ++ " mutual with: " ++ show ms show (ExternDef arity) = "" - show (ForeignDef a cs) = "" show (Builtin {arity} _) = "" show (Hole _ p) = "Hole" ++ if p then " [impl]" else "" @@ -104,7 +104,7 @@ public export data TotalReq = Total | CoveringOnly | PartialOK public export -data DefFlag +data DefFlag = Inline | Invertible -- assume safe to cancel arguments in unification | Overloadable -- allow ad-hoc overloads @@ -174,7 +174,7 @@ record GlobalDef where refersToM : Maybe (NameMap Bool) invertible : Bool -- for an ordinary definition, is it invertible in unification noCycles : Bool -- for metavariables, whether they can be cyclic (this - -- would only be allowed when using a metavariable as a + -- would only be allowed when using a metavariable as a -- placeholder for a yet to be elaborated arguments, but -- not for implicits because that'd indicate failing the -- occurs check) @@ -211,7 +211,7 @@ record Context where -- Map from strings to all the possible names in all namespaces possibles : StringMap (List (Name, Int)) -- Reference to the actual content, indexed by Int - content : Ref Arr (IOArray ContextEntry) + content : Ref Arr (IOArray ContextEntry) -- Branching depth, in a backtracking elaborator. 0 is top level; at lower -- levels we need to stage updates rather than add directly to the -- 'content' store @@ -252,7 +252,7 @@ export initCtxt : Core Context initCtxt = initCtxtS initSize -addPossible : Name -> Int -> +addPossible : Name -> Int -> StringMap (List (Name, Int)) -> StringMap (List (Name, Int)) addPossible n i ps = case userNameRoot n of @@ -284,7 +284,7 @@ getPosition : Name -> Context -> Core (Int, Context) getPosition (Resolved idx) ctxt = pure (idx, ctxt) getPosition n ctxt = case lookup n (resolvedAs ctxt) of - Just idx => + Just idx => do pure (idx, ctxt) Nothing => newEntry n ctxt @@ -322,7 +322,7 @@ addEntry n entry ctxt_in returnDef : Bool -> Int -> GlobalDef -> Maybe (Int, GlobalDef) returnDef False idx def = Just (idx, def) -returnDef True idx def +returnDef True idx def = case definition def of PMDef True _ _ _ _ => Just (idx, def) _ => Nothing @@ -331,7 +331,7 @@ export lookupCtxtExactI : Name -> Context -> Core (Maybe (Int, GlobalDef)) lookupCtxtExactI (Resolved idx) ctxt = case lookup idx (staging ctxt) of - Just val => + Just val => pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx val) Nothing => do let a = content ctxt @@ -348,7 +348,7 @@ export lookupCtxtExact : Name -> Context -> Core (Maybe GlobalDef) lookupCtxtExact (Resolved idx) ctxt = case lookup idx (staging ctxt) of - Just res => + Just res => do def <- decode ctxt idx res case returnDef (inlineOnly ctxt) idx def of Nothing => pure Nothing @@ -378,7 +378,7 @@ lookupCtxtName n ctxt do let Just ps = lookup r (possibles ctxt) | Nothing => pure [] ps' <- the (Core (List (Maybe (Name, Int, GlobalDef)))) $ - traverse (\ (n, i) => + traverse (\ (n, i) => do Just res <- lookupCtxtExact (Resolved i) ctxt | pure Nothing pure (Just (n, i, res))) ps @@ -388,8 +388,8 @@ lookupCtxtName n ctxt matches (NS ns _) (NS cns _, _, _) = ns `isPrefixOf` cns matches (NS _ _) _ = True -- no in library name, so root doesn't match matches _ _ = True -- no prefix, so root must match, so good - - getMatches : List (Maybe (Name, Int, GlobalDef)) -> + + getMatches : List (Maybe (Name, Int, GlobalDef)) -> Core (List (Name, Int, GlobalDef)) getMatches [] = pure [] getMatches (Nothing :: rs) = getMatches rs @@ -423,9 +423,9 @@ commitCtxt ctxt commitStaged rest arr export -newDef : FC -> Name -> RigCount -> List Name -> +newDef : FC -> Name -> RigCount -> List Name -> ClosedTerm -> Visibility -> Def -> GlobalDef -newDef fc n rig vars ty vis def +newDef fc n rig vars ty vis def = MkGlobalDef fc n ty [] rig vars vis unchecked [] empty False False False def Nothing [] @@ -452,20 +452,20 @@ HasNames Name where export HasNames (Term vars) where - full gam (Ref fc x (Resolved i)) + full gam (Ref fc x (Resolved i)) = do Just gdef <- lookupCtxtExact (Resolved i) gam | Nothing => do coreLift $ putStrLn $ "Missing name! " ++ show i pure (Ref fc x (Resolved i)) pure (Ref fc x (fullname gdef)) - full gam (Meta fc x y xs) + full gam (Meta fc x y xs) = pure (Meta fc x y !(traverse (full gam) xs)) - full gam (Bind fc x b scope) + full gam (Bind fc x b scope) = pure (Bind fc x !(traverse (full gam) b) !(full gam scope)) - full gam (App fc fn arg) + full gam (App fc fn arg) = pure (App fc !(full gam fn) !(full gam arg)) full gam (As fc p tm) = pure (As fc !(full gam p) !(full gam tm)) - full gam (TDelayed fc x y) + full gam (TDelayed fc x y) = pure (TDelayed fc x !(full gam y)) full gam (TDelay fc x t y) = pure (TDelay fc x !(full gam t) !(full gam y)) @@ -473,22 +473,22 @@ HasNames (Term vars) where = pure (TForce fc !(full gam y)) full gam tm = pure tm - resolved gam (Ref fc x n) - = do let Just i = getNameID n gam + resolved gam (Ref fc x n) + = do let Just i = getNameID n gam | Nothing => pure (Ref fc x n) pure (Ref fc x (Resolved i)) - resolved gam (Meta fc x y xs) + resolved gam (Meta fc x y xs) = do xs' <- traverse (resolved gam) xs let Just i = getNameID x gam | Nothing => pure (Meta fc x y xs') pure (Meta fc x i xs') - resolved gam (Bind fc x b scope) + resolved gam (Bind fc x b scope) = pure (Bind fc x !(traverse (resolved gam) b) !(resolved gam scope)) - resolved gam (App fc fn arg) + resolved gam (App fc fn arg) = pure (App fc !(resolved gam fn) !(resolved gam arg)) resolved gam (As fc p tm) = pure (As fc !(resolved gam p) !(resolved gam tm)) - resolved gam (TDelayed fc x y) + resolved gam (TDelayed fc x y) = pure (TDelayed fc x !(resolved gam y)) resolved gam (TDelay fc x t y) = pure (TDelay fc x !(resolved gam t) !(resolved gam y)) @@ -527,7 +527,7 @@ mutual resolved gam (ConCase n t args sc) = do sc' <- resolved gam sc - let Just i = getNameID n gam + let Just i = getNameID n gam | Nothing => pure (ConCase n t args sc') pure $ ConCase (Resolved i) t args sc' resolved gam (DelayCase ty arg sc) @@ -549,39 +549,39 @@ HasNames (Env Term vars) where export HasNames Def where - full gam (PMDef r args ct rt pats) + full gam (PMDef r args ct rt pats) = pure $ PMDef r args !(full gam ct) !(full gam rt) !(traverse fullNamesPat pats) where fullNamesPat : (vs ** (Env Term vs, Term vs, Term vs)) -> Core (vs ** (Env Term vs, Term vs, Term vs)) fullNamesPat (_ ** (env, lhs, rhs)) - = pure $ (_ ** (!(full gam env), - !(full gam lhs), !(full gam rhs))) + = pure $ (_ ** (!(full gam env), + !(full gam lhs), !(full gam rhs))) full gam (TCon t a ps ds ms cs) = pure $ TCon t a ps ds !(traverse (full gam) ms) !(traverse (full gam) cs) full gam (BySearch c d def) = pure $ BySearch c d !(full gam def) - full gam (Guess tm b cs) + full gam (Guess tm b cs) = pure $ Guess !(full gam tm) b cs full gam t = pure t - - resolved gam (PMDef r args ct rt pats) + + resolved gam (PMDef r args ct rt pats) = pure $ PMDef r args !(resolved gam ct) !(resolved gam rt) !(traverse resolvedNamesPat pats) where resolvedNamesPat : (vs ** (Env Term vs, Term vs, Term vs)) -> Core (vs ** (Env Term vs, Term vs, Term vs)) resolvedNamesPat (_ ** (env, lhs, rhs)) - = pure $ (_ ** (!(resolved gam env), - !(resolved gam lhs), !(resolved gam rhs))) + = pure $ (_ ** (!(resolved gam env), + !(resolved gam lhs), !(resolved gam rhs))) resolved gam (TCon t a ps ds ms cs) = pure $ TCon t a ps ds !(traverse (resolved gam) ms) !(traverse (resolved gam) cs) resolved gam (BySearch c d def) = pure $ BySearch c d !(resolved gam def) - resolved gam (Guess tm b cs) + resolved gam (Guess tm b cs) = pure $ Guess !(resolved gam tm) b cs resolved gam t = pure t @@ -592,7 +592,7 @@ HasNames (NameMap a) where insertAll : NameMap a -> List (Name, a) -> Core (NameMap a) insertAll ms [] = pure ms insertAll ms ((k, v) :: ns) - = insertAll (insert !(full gam k) v ms) ns + = insertAll (insert !(full gam k) v ms) ns resolved gam nmap = insertAll empty (toList nmap) @@ -600,7 +600,7 @@ HasNames (NameMap a) where insertAll : NameMap a -> List (Name, a) -> Core (NameMap a) insertAll ms [] = pure ms insertAll ms ((k, v) :: ns) - = insertAll (insert !(resolved gam k) v ms) ns + = insertAll (insert !(resolved gam k) v ms) ns export HasNames PartialReason where @@ -653,8 +653,8 @@ HasNames a => HasNames (Maybe a) where export HasNames GlobalDef where - full gam def - = do + full gam def + = do -- ts <- full gam (type def) -- d <- full gam (definition def) -- coreLift $ printLn (fullname def, ts) @@ -669,7 +669,7 @@ HasNames GlobalDef where = pure $ record { type = !(resolved gam (type def)), definition = !(resolved gam (definition def)), totality = !(resolved gam (totality def)), - refersToM = !(resolved gam (refersToM def)), + refersToM = !(resolved gam (refersToM def)), sizeChange = !(traverse (resolved gam) (sizeChange def)) } def @@ -684,15 +684,15 @@ record Defs where toSave : NameMap () nextTag : Int typeHints : NameMap (List (Name, Bool)) - -- ^ a mapping from type names to hints (and a flag setting whether it's + -- ^ a mapping from type names to hints (and a flag setting whether it's -- a "direct" hint). Direct hints are searched first (as part of a group) -- the indirect hints. Indirect hints, in practice, are used to find -- instances of parent interfaces, and we don't search these until we've -- tried to find a direct result via a constructor or a top level hint. autoHints : NameMap Bool -- ^ global search hints. A mapping from the hint name, to whether it is - -- a "default hint". A default hint is used only if all other attempts - -- to search fail (this flag is really only intended as a mechanism + -- a "default hint". A default hint is used only if all other attempts + -- to search fail (this flag is really only intended as a mechanism -- for defaulting of literals) openHints : NameMap () -- ^ currently open global hints; just for the rest of this module (not exported) @@ -712,7 +712,7 @@ record Defs where -- twice unnecessarily (this is a record of all the things we've -- called 'readFromTTC' with, in practice) cgdirectives : List (CG, String) - -- ^ Code generator directives, which are free form text and thus to + -- ^ Code generator directives, which are free form text and thus to -- be interpreted however the specific code generator requires toCompile : List Name -- ^ Names which need to be compiled to run time case trees @@ -732,11 +732,11 @@ clearDefs defs export initDefs : Core Defs -initDefs +initDefs = do gam <- initCtxt - pure (MkDefs gam [] ["Main"] [] defaults empty 100 + pure (MkDefs gam [] ["Main"] [] defaults empty 100 empty empty empty [] [] [] 5381 [] [] [] [] [] empty) - + -- Reset the context, except for the options export clearCtxt : {auto c : Ref Ctxt Defs} -> @@ -753,7 +753,7 @@ addHash x put Ctxt (record { ifaceHash = hashWithSalt (ifaceHash defs) x } defs) export -initHash : {auto c : Ref Ctxt Defs} -> +initHash : {auto c : Ref Ctxt Defs} -> Core () initHash = do defs <- get Ctxt @@ -795,7 +795,7 @@ getUserHoles _ => pure False export -addDef : {auto c : Ref Ctxt Defs} -> +addDef : {auto c : Ref Ctxt Defs} -> Name -> GlobalDef -> Core Int addDef n def = do defs <- get Ctxt @@ -808,7 +808,7 @@ addDef n def pure idx export -addContextEntry : {auto c : Ref Ctxt Defs} -> +addContextEntry : {auto c : Ref Ctxt Defs} -> Name -> Binary -> Core Int addContextEntry n def = do defs <- get Ctxt @@ -820,14 +820,14 @@ export addBuiltin : {auto x : Ref Ctxt Defs} -> Name -> ClosedTerm -> Totality -> PrimFn arity -> Core () -addBuiltin n ty tot op - = do addDef n (MkGlobalDef emptyFC n ty [] RigW [] Public tot +addBuiltin n ty tot op + = do addDef n (MkGlobalDef emptyFC n ty [] RigW [] Public tot [Inline] empty False False True (Builtin op) - Nothing []) + Nothing []) pure () export -updateDef : {auto c : Ref Ctxt Defs} -> +updateDef : {auto c : Ref Ctxt Defs} -> Name -> (Def -> Maybe Def) -> Core () updateDef n fdef = do defs <- get Ctxt @@ -937,7 +937,7 @@ addToSave n -- Specific lookup functions export -lookupExactBy : (GlobalDef -> a) -> Name -> Context -> +lookupExactBy : (GlobalDef -> a) -> Name -> Context -> Core (Maybe a) lookupExactBy fn n gam = do Just gdef <- lookupCtxtExact n gam @@ -945,7 +945,7 @@ lookupExactBy fn n gam pure (Just (fn gdef)) export -lookupNameBy : (GlobalDef -> a) -> Name -> Context -> +lookupNameBy : (GlobalDef -> a) -> Name -> Context -> Core (List (Name, Int, a)) lookupNameBy fn n gam = do gdef <- lookupCtxtName n gam @@ -957,15 +957,15 @@ lookupDefExact = lookupExactBy definition export lookupDefName : Name -> Context -> Core (List (Name, Int, Def)) -lookupDefName = lookupNameBy definition +lookupDefName = lookupNameBy definition export lookupTyExact : Name -> Context -> Core (Maybe ClosedTerm) -lookupTyExact = lookupExactBy type +lookupTyExact = lookupExactBy type export lookupTyName : Name -> Context -> Core (List (Name, Int, ClosedTerm)) -lookupTyName = lookupNameBy type +lookupTyName = lookupNameBy type export lookupDefTyExact : Name -> Context -> Core (Maybe (Def, ClosedTerm)) @@ -996,7 +996,7 @@ reducibleInAny nss n vis = any (\ns => reducibleIn ns n vis) nss export toFullNames : {auto c : Ref Ctxt Defs} -> HasNames a => a -> Core a -toFullNames t +toFullNames t = do defs <- get Ctxt full (gamma defs) t @@ -1143,7 +1143,7 @@ public export record SearchData where constructor MkSearchData detArgs : List Nat -- determining argument positions - hintGroups : List (Bool, List Name) + hintGroups : List (Bool, List Name) -- names of functions to use as hints, and whether ambiguity is allowed {- In proof search, for every group of names * If exactly one succeeds, use it @@ -1175,14 +1175,14 @@ getSearchData fc defaults target (toList (autoHints defs))) in pure (MkSearchData [] [(False, defns)]) else let opens = map fst (toList (openHints defs)) - autos = map fst (filter (not . isDefault) + autos = map fst (filter (not . isDefault) (toList (autoHints defs))) - tyhs = map fst (filter direct hs) + tyhs = map fst (filter direct hs) chasers = map fst (filter (not . direct) hs) in pure (MkSearchData dets (filter (isCons . snd) - [(False, opens), - (False, autos), - (False, tyhs), + [(False, opens), + (False, autos), + (False, tyhs), (True, chasers)])) where isDefault : (Name, Bool) -> Bool @@ -1196,7 +1196,7 @@ setMutWith : {auto c : Ref Ctxt Defs} -> FC -> Name -> List Name -> Core () setMutWith fc tn tns = do defs <- get Ctxt - Just g <- lookupCtxtExact tn (gamma defs) + Just g <- lookupCtxtExact tn (gamma defs) | _ => throw (UndefinedName fc tn) let TCon t a ps dets _ cons = definition g | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setMutWith]")) @@ -1221,7 +1221,7 @@ setDetermining : {auto c : Ref Ctxt Defs} -> FC -> Name -> List Name -> Core () setDetermining fc tyn args = do defs <- get Ctxt - Just g <- lookupCtxtExact tyn (gamma defs) + Just g <- lookupCtxtExact tyn (gamma defs) | _ => throw (UndefinedName fc tyn) let TCon t a ps _ cons ms = definition g | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]")) @@ -1423,7 +1423,7 @@ getPs acc tyn (Bind _ x (Pi _ _ ty) sc) shrink (Just tm) = shrinkTerm tm (DropCons SubRefl) getPs acc tyn tm = case getFnArgs tm of - (Ref _ _ n, args) => + (Ref _ _ n, args) => if n == tyn then Just (updateParams acc args) else acc @@ -1456,10 +1456,10 @@ export addData : {auto c : Ref Ctxt Defs} -> List Name -> Visibility -> Int -> DataDef -> Core Int addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons) - = do defs <- get Ctxt - tag <- getNextTypeTag - let tydef = newDef dfc tyn RigW vars tycon vis - (TCon tag arity + = do defs <- get Ctxt + tag <- getNextTypeTag + let tydef = newDef dfc tyn RigW vars tycon vis + (TCon tag arity (paramPos (Resolved tidx) (map type datacons)) (allDet arity) [] (map name datacons)) @@ -1476,7 +1476,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons) conVisibility Export = Private conVisibility x = x - addDataConstructors : (tag : Int) -> List Constructor -> + addDataConstructors : (tag : Int) -> List Constructor -> Context -> Core Context addDataConstructors tag [] gam = pure gam addDataConstructors tag (MkCon fc n a ty :: cs) gam @@ -1532,7 +1532,7 @@ isVisible : {auto c : Ref Ctxt Defs} -> (nspace : List String) -> Core Bool isVisible nspace = do defs <- get Ctxt - pure (any visible (allParents (currentNS defs) ++ + pure (any visible (allParents (currentNS defs) ++ nestedNS defs ++ visibleNS (gamma defs))) where @@ -1633,6 +1633,12 @@ setBuildDir dir = do defs <- get Ctxt put Ctxt (record { options->dirs->build_dir = dir } defs) +export +setSourceDir : {auto c : Ref Ctxt Defs} -> Maybe String -> Core () +setSourceDir mdir + = do defs <- get Ctxt + put Ctxt (record { options->dirs->source_dir = mdir } defs) + export setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core () setWorkingDir dir @@ -1750,7 +1756,7 @@ addNameDirective fc n ns export isPairType : {auto c : Ref Ctxt Defs} -> Name -> Core Bool -isPairType n +isPairType n = do defs <- get Ctxt case pairnames (options defs) of Nothing => pure False @@ -1766,7 +1772,7 @@ fstName export sndName : {auto c : Ref Ctxt Defs} -> Core (Maybe Name) -sndName +sndName = do defs <- get Ctxt pure $ maybe Nothing (Just . sndName) (pairnames (options defs)) @@ -1780,7 +1786,7 @@ getRewrite export isEqualTy : {auto c : Ref Ctxt Defs} -> Name -> Core Bool -isEqualTy n +isEqualTy n = do defs <- get Ctxt case rewritenames (options defs) of Nothing => pure False @@ -1850,7 +1856,7 @@ logTerm lvl msg tm = do opts <- getSession if logLevel opts >= lvl then do tm' <- toFullNames tm - coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg + coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg ++ ": " ++ show tm' else pure () @@ -1887,7 +1893,7 @@ logTimeWhen p str act let time = t' - t assert_total $ -- We're not dividing by 0 coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++ - show (time `div` nano) ++ "." ++ + show (time `div` nano) ++ "." ++ addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++ "s" pure res diff --git a/src/Core/Core.idr b/src/Core/Core.idr index f94cc42..a8f10f5 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -25,7 +25,7 @@ data CaseError = DifferingArgNumbers -- All possible errors, carrying a location public export -data Error +data Error = Fatal Error -- flag as unrecoverable (so don't postpone awaiting further info) | CantConvert FC (Env Term vars) (Term vars) (Term vars) | CantSolveEq FC (Env Term vars) (Term vars) (Term vars) @@ -35,7 +35,7 @@ data Error | ValidCase FC (Env Term vars) (Either (Term vars) Error) | UndefinedName FC Name | InvisibleName FC Name (Maybe (List String)) - | BadTypeConType FC Name + | BadTypeConType FC Name | BadDataConType FC Name Name | NotCovering FC Name Covering | NotTotal FC Name PartialReason @@ -67,7 +67,7 @@ data Error | NotFunctionType FC (Env Term vars) (Term vars) | RewriteNoChange FC (Env Term vars) (Term vars) (Term vars) | NotRewriteRule FC (Env Term vars) (Term vars) - | CaseCompile FC Name CaseError + | CaseCompile FC Name CaseError | MatchTooSpecific FC (Env Term vars) (Term vars) | BadDotPattern FC (Env Term vars) String (Term vars) (Term vars) | BadImplicit FC String @@ -98,29 +98,29 @@ Show TTCErrorMsg where export Show Error where show (Fatal err) = show err - show (CantConvert fc env x y) + show (CantConvert fc env x y) = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y - show (CantSolveEq fc env x y) + show (CantSolveEq fc env x y) = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal" show (PatternVariableUnifies fc env n x) = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x - show (CyclicMeta fc n) + show (CyclicMeta fc n) = show fc ++ ":Cycle detected in metavariable solution " ++ show n show (WhenUnifying fc _ x y err) = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err show (ValidCase fc _ prob) - = show fc ++ ":" ++ + = show fc ++ ":" ++ case prob of Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks" Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err) show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x - show (InvisibleName fc x (Just ns)) + show (InvisibleName fc x (Just ns)) = show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++ showSep "." (reverse ns) ++ " is not explicitly imported" show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private" - show (BadTypeConType fc n) + show (BadTypeConType fc n) = show fc ++ ":Return type of " ++ show n ++ " must be Type" - show (BadDataConType fc n fam) + show (BadDataConType fc n fam) = show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam show (NotCovering fc n cov) = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++ @@ -128,7 +128,7 @@ Show Error where IsCovering => "Oh yes it is (Internal error!)" MissingCases cs => "Missing cases:\n\t" ++ showSep "\n\t" (map show cs) - NonCoveringCall ns => "Calls non covering function" + NonCoveringCall ns => "Calls non covering function" ++ (case ns of [fn] => " " ++ show fn _ => "s: " ++ showSep ", " (map show ns)) @@ -151,7 +151,7 @@ Show Error where showRel Rig1 = "relevant" showRel RigW = "non-linear" show (BorrowPartial fc env t arg) - = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++ + = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++ " so must be fully applied" show (BorrowPartialType fc env t) = show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type" @@ -164,25 +164,25 @@ Show Error where = show fc ++ ":Can't infer type of record to update" show (NotRecordField fc fld Nothing) = show fc ++ ":" ++ fld ++ " is not part of a record type" - show (NotRecordField fc fld (Just ty)) - = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld + show (NotRecordField fc fld (Just ty)) + = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld show (NotRecordType fc ty) = show fc ++ ":" ++ show ty ++ " is not a record type" - show (IncompatibleFieldUpdate fc flds) - = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates" - show (InvalidImplicits fc env ns tm) - = show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm - show (TryWithImplicits fc env imps) - = show fc ++ ":Need to bind implicits " + show (IncompatibleFieldUpdate fc flds) + = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates" + show (InvalidImplicits fc env ns tm) + = show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm + show (TryWithImplicits fc env imps) + = show fc ++ ":Need to bind implicits " ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps) ++ "\n(The front end should probably have done this for you. Please report!)" show (BadUnboundImplicit fc env n ty) - = show fc ++ ":Can't bind name " ++ nameRoot n ++ + = show fc ++ ":Can't bind name " ++ nameRoot n ++ " with type " ++ show ty - show (CantSolveGoal fc env g) + show (CantSolveGoal fc env g) = show fc ++ ":Can't solve goal " ++ assert_total (show g) show (DeterminingArg fc n i env g) - = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++ + = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++ " since argument " ++ show n ++ " can't be inferred" show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs show (CantInferArgType fc env n h ty) @@ -201,19 +201,19 @@ Show Error where = show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty show (NotRewriteRule fc env rule) = show fc ++ ":" ++ show rule ++ " is not a rewrite rule type" - show (CaseCompile fc n DifferingArgNumbers) + show (CaseCompile fc n DifferingArgNumbers) = show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments" - show (CaseCompile fc n DifferingTypes) + show (CaseCompile fc n DifferingTypes) = show fc ++ ":Patterns for " ++ show n ++ " require matching on different types" - show (CaseCompile fc n UnknownType) + show (CaseCompile fc n UnknownType) = show fc ++ ":Can't infer type to match in " ++ show n show (CaseCompile fc n (MatchErased (_ ** (env, tm)))) - = show fc ++ ":Attempt to match on erased argument " ++ show tm ++ + = show fc ++ ":Attempt to match on erased argument " ++ show tm ++ " in " ++ show n show (MatchTooSpecific fc env tm) = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type" show (BadDotPattern fc env reason x y) - = show fc ++ ":Can't match on " ++ show x ++ + = show fc ++ ":Can't match on " ++ show x ++ (if reason /= "" then " (" ++ reason ++ ")" else "") ++ " - it elaborates to " ++ show y show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here" @@ -222,7 +222,7 @@ Show Error where show (TTCError msg) = "Error in TTC file: " ++ show msg show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err show (ParseFail fc err) = "Parse error (" ++ show err ++ ")" - show (ModuleNotFound fc ns) + show (ModuleNotFound fc ns) = show fc ++ ":" ++ showSep "." (reverse ns) ++ " not found" show (CyclicImports ns) = "Module imports form a cycle: " ++ showSep " -> " (map showMod ns) @@ -315,7 +315,7 @@ record Core t where runCore : IO (Either Error t) export -coreRun : Core a -> +coreRun : Core a -> (Error -> IO b) -> (a -> IO b) -> IO b coreRun (MkCore act) err ok = either err ok !act @@ -342,7 +342,7 @@ coreLift op = MkCore (do op' <- op {- Monad, Applicative, Traversable are specialised by hand for Core. In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't specialise interfaces under 'case' expressions, and this has a significant -impact on both compile time and run time. +impact on both compile time and run time. Of course it would be a good idea to fix this in Idris, but it's not an urgent thing on the road to self hosting, and we can make sure this isn't a problem @@ -356,8 +356,8 @@ map f (MkCore a) = MkCore (map (map f) a) -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b -(>>=) (MkCore act) f - = MkCore (act >>= +(>>=) (MkCore act) f + = MkCore (act >>= (\x => case x of Left err => pure (Left err) Right val => runCore (f val))) @@ -378,7 +378,7 @@ when False f = pure () export Catchable Core Error where - catch (MkCore prog) h + catch (MkCore prog) h = MkCore ( do p' <- prog case p' of Left e => let MkCore he = h e in he @@ -388,13 +388,18 @@ Catchable Core Error where -- Traversable (specialised) traverse' : (a -> Core b) -> List a -> List b -> Core (List b) traverse' f [] acc = pure (reverse acc) -traverse' f (x :: xs) acc - = traverse' f xs (!(f x) :: acc) +traverse' f (x :: xs) acc + = traverse' f xs (!(f x) :: acc) export traverse : (a -> Core b) -> List a -> Core (List b) traverse f xs = traverse' f xs [] +export +traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b) +traverseOpt f Nothing = pure Nothing +traverseOpt f (Just x) = map Just (f x) + export traverse_ : (a -> Core b) -> List a -> Core () traverse_ f [] = pure () @@ -443,11 +448,11 @@ data Ref : label -> Type -> Type where export newRef : (x : label) -> t -> Core (Ref x t) -newRef x val +newRef x val = do ref <- coreLift (newIORef val) pure (MkRef ref) -export %inline +export %inline get : (x : label) -> {auto ref : Ref x a} -> Core a get x {ref = MkRef io} = coreLift (readIORef io) @@ -463,6 +468,6 @@ cond ((x, y) :: xs) def = if x then y else cond xs def export condC : List (Core Bool, Core a) -> Core a -> Core a condC [] def = def -condC ((x, y) :: xs) def +condC ((x, y) :: xs) def = if !x then y else condC xs def diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 767cc5e..69e8918 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -28,14 +28,14 @@ fullPath : String -> List String fullPath fp = filter (/="") $ split (==sep) fp dropExtension : String -> String -dropExtension fname +dropExtension fname = case span (/= '.') (reverse fname) of (all, "") => -- no extension reverse all - (ext, root) => + (ext, root) => -- assert that root can't be empty reverse (assert_total (strTail root)) - + -- Return the name of the first file available in the list firstAvailable : List String -> Core (Maybe String) firstAvailable [] = pure Nothing @@ -50,7 +50,7 @@ readDataFile : {auto c : Ref Ctxt Defs} -> String -> Core String readDataFile fname = do d <- getDirs - let fs = map (\p => p ++ cast sep ++ fname) (data_dirs d) + let fs = map (\p => p ++ dirSep ++ fname) (data_dirs d) Just f <- firstAvailable fs | Nothing => throw (InternalError ("Can't find data file " ++ fname)) Right d <- coreLift $ readFile f @@ -58,30 +58,30 @@ readDataFile fname pure d -- Look for a library file required by a code generator. Look in the --- library directories, and in the lib/ subdirectoriy of all the 'extra import' +-- library directories, and in the lib/ subdirectoriy of all the 'extra import' -- directories export findLibraryFile : {auto c : Ref Ctxt Defs} -> String -> Core String findLibraryFile fname = do d <- getDirs - let fs = map (\p => p ++ cast sep ++ fname) - (lib_dirs d ++ map (\x => x ++ cast sep ++ "lib") + let fs = map (\p => p ++ dirSep ++ fname) + (lib_dirs d ++ map (\x => x ++ dirSep ++ "lib") (extra_dirs d)) Just f <- firstAvailable fs | Nothing => throw (InternalError ("Can't find library " ++ fname)) pure f --- Given a namespace, return the full path to the checked module, +-- Given a namespace, return the full path to the checked module, -- looking first in the build directory then in the extra_dirs export nsToPath : {auto c : Ref Ctxt Defs} -> FC -> List String -> Core (Either Error String) nsToPath loc ns = do d <- getDirs - let fnameBase = showSep (cast sep) (reverse ns) - let fs = map (\p => p ++ cast sep ++ fnameBase ++ ".ttc") - ((build_dir d ++ cast sep ++ "ttc") :: extra_dirs d) + let fnameBase = showSep dirSep (reverse ns) + let fs = map (\p => p ++ dirSep ++ fnameBase ++ ".ttc") + ((build_dir d ++ dirSep ++ "ttc") :: extra_dirs d) Just f <- firstAvailable fs | Nothing => pure (Left (ModuleNotFound loc ns)) pure (Right f) @@ -93,21 +93,25 @@ nsToSource : {auto c : Ref Ctxt Defs} -> FC -> List String -> Core String nsToSource loc ns = do d <- getDirs - let fnameBase = showSep (cast sep) (reverse ns) + let fnameOrig = showSep dirSep (reverse ns) + let fnameBase = maybe fnameOrig (\srcdir => srcdir ++ dirSep ++ fnameOrig) (source_dir d) let fs = map (\ext => fnameBase ++ ext) [".yaff", ".idr", ".lidr"] Just f <- firstAvailable fs | Nothing => throw (ModuleNotFound loc ns) pure f --- Given a filename in the working directory, return the correct +-- Given a filename in the working directory + source directory, return the correct -- namespace for it export -pathToNS : String -> String -> List String -pathToNS wdir fname +pathToNS : String -> Maybe String -> String -> List String +pathToNS wdir sdir fname = let wsplit = splitSep wdir - fsplit = splitSep fname in - dropWdir wsplit fsplit fsplit + ssplit = maybe [] splitSep sdir + fsplit = splitSep fname + sdrop = dropWdir ssplit fsplit fsplit + in + dropWdir wsplit sdrop sdrop where dropWdir : List String -> List String -> List String -> List String dropWdir wdir orig [] = [] @@ -117,7 +121,7 @@ pathToNS wdir fname else x :: dropWdir wdir orig xs splitSep : String -> List String - splitSep fname + splitSep fname = case span (/=sep) fname of (end, "") => [dropExtension end] (mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod] @@ -139,7 +143,7 @@ mkdirs (d :: ds) changeDir ".." pure (Right ()) --- Given a namespace (i.e. a module name), make the build directory for the +-- Given a namespace (i.e. a module name), make the build directory for the -- corresponding ttc file export makeBuildDirectory : {auto c : Ref Ctxt Defs} -> @@ -150,28 +154,28 @@ makeBuildDirectory ns let ndirs = case ns of [] => [] (n :: ns) => ns -- first item is file name - let fname = showSep (cast sep) (reverse ndirs) + let fname = showSep dirSep (reverse ndirs) Right _ <- coreLift $ mkdirs (build_dir d :: "ttc" :: reverse ndirs) - | Left err => throw (FileErr (bdir ++ cast sep ++ fname) err) + | Left err => throw (FileErr (bdir ++ dirSep ++ fname) err) pure () -- Given a source file, return the name of the ttc file to generate export -getTTCFileName : {auto c : Ref Ctxt Defs} -> +getTTCFileName : {auto c : Ref Ctxt Defs} -> String -> String -> Core String getTTCFileName inp ext = do ns <- getNS d <- getDirs -- Get its namespace from the file relative to the working directory -- and generate the ttc file from that - let ns = pathToNS (working_dir d) inp - let fname = showSep (cast sep) (reverse ns) ++ ext + let ns = pathToNS (working_dir d) (source_dir d) inp + let fname = showSep dirSep (reverse ns) ++ ext let bdir = build_dir d - pure $ bdir ++ cast sep ++ "ttc" ++ cast sep ++ fname + pure $ bdir ++ dirSep ++ "ttc" ++ dirSep ++ fname -- Given a root executable name, return the name in the build directory export getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String getExecFileName efile = do d <- getDirs - pure $ build_dir d ++ cast sep ++ efile + pure $ build_dir d ++ dirSep ++ efile diff --git a/src/Core/Options.idr b/src/Core/Options.idr index ee07f63..8c4c096 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -8,6 +8,7 @@ public export record Dirs where constructor MkDirs working_dir : String + source_dir : Maybe String -- source directory, relative to working directory build_dir : String -- build directory, relative to working directory dir_prefix : String -- installation prefix, for finding data files (e.g. run time support) extra_dirs : List String -- places to look for import files @@ -16,8 +17,9 @@ record Dirs where public export toString : Dirs -> String -toString (MkDirs wdir bdir dfix edirs ldirs ddirs) = +toString (MkDirs wdir sdir bdir dfix edirs ldirs ddirs) = unlines [ "+ Working Directory :: " ++ show wdir + , "+ Source Directory :: " ++ show sdir , "+ Build Directory :: " ++ show bdir , "+ Installation Prefix :: " ++ show dfix , "+ Extra Directories :: " ++ show edirs @@ -109,7 +111,7 @@ record Options where extensions : List LangExt defaultDirs : Dirs -defaultDirs = MkDirs "." "build" "/usr/local" ["."] ["."] [] +defaultDirs = MkDirs "." Nothing "build" "/usr/local" ["."] ["."] [] defaultPPrint : PPrinter defaultPPrint = MkPPOpts False True False diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index c4abe07..6102990 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -25,6 +25,9 @@ record ModTree where sourceFile : Maybe String deps : List ModTree +Show ModTree where + show t = show (sourceFile t) ++ " " ++ show (nspace t) ++ "<-" ++ show (deps t) + -- A module file to build, and its list of dependencies -- From this we can work out if the source file needs rebuilding, assuming -- things are build in dependency order. A source file needs rebuilding @@ -32,7 +35,7 @@ record ModTree where -- + Its corresponding ttc is older than the source file -- + Any of the import ttcs are *newer* than the corresponding ttc -- (If so: also any imported ttc's fingerprint is different from the one --- stored in the source file's ttc) +-- stored in the source file's ttc) public export record BuildMod where constructor MkBuildMod @@ -60,7 +63,7 @@ readHeader loc mod -- Stop at the first :, that's definitely not part of the header, to -- save lexing the whole file unnecessarily isColon : TokenData Token -> Bool - isColon t + isColon t = case tok t of Symbol ":" => True _ => False @@ -69,14 +72,14 @@ data AllMods : Type where mkModTree : {auto c : Ref Ctxt Defs} -> {auto a : Ref AllMods (List (List String, ModTree))} -> - FC -> + FC -> (done : List (List String)) -> -- if 'mod' is here we have a cycle (mod : List String) -> Core ModTree mkModTree loc done mod = if mod `elem` done then throw (CyclicImports (done ++ [mod])) - else + else -- Read imports from source file. If the source file isn't -- available, it's not our responsibility catch (do all <- get AllMods @@ -92,7 +95,7 @@ mkModTree loc done mod pure mt Just m => pure m) -- Couldn't find source, assume it's in a package directory - (\err => + (\err => case err of CyclicImports _ => throw err _ => pure (MkModTree mod Nothing [])) @@ -105,7 +108,7 @@ mkBuildMods acc mod maybe req -- only build ones where we can find the source code (\sf => if sf `elem` map buildFile req then req - else MkBuildMod sf (nspace mod) + else MkBuildMod sf (nspace mod) (map nspace (deps mod)) :: req) (sourceFile mod) where @@ -117,13 +120,12 @@ mkBuildMods acc mod -- built for that main file, in the order they need to be built getBuildMods : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> - FC -> (mainFile : String) -> + FC -> (mainFile : String) -> Core (List BuildMod) getBuildMods loc fname = do a <- newRef AllMods [] d <- getDirs - - t <- mkModTree {a} loc [] (pathToNS (working_dir d) fname) + t <- mkModTree {a} loc [] (pathToNS (working_dir d) (source_dir d) fname) pure (reverse (mkBuildMods [] t)) fnameModified : String -> Core Integer @@ -139,7 +141,7 @@ fnameModified fname buildMod : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - FC -> Nat -> Nat -> BuildMod -> + FC -> Nat -> Nat -> BuildMod -> Core (List Error) -- Build from source if any of the dependencies, or the associated source -- file, have a modification time which is newer than the module's ttc @@ -193,7 +195,7 @@ buildMod loc num len mod buildMods : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - FC -> Nat -> Nat -> List BuildMod -> + FC -> Nat -> Nat -> List BuildMod -> Core (List Error) buildMods fc num len [] = pure [] buildMods fc num len (m :: ms) @@ -207,7 +209,7 @@ buildDeps : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> {auto o : Ref ROpts REPLOpts} -> - (mainFile : String) -> + (mainFile : String) -> Core (List Error) buildDeps fname = do mods <- getBuildMods toplevelFC fname @@ -233,7 +235,7 @@ export buildAll : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - (allFiles : List String) -> + (allFiles : List String) -> Core (List Error) buildAll allFiles = do mods <- traverse (getBuildMods toplevelFC) allFiles diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 74982e0..a8e980c 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -44,6 +44,7 @@ record PkgDesc where mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL) executable : Maybe String -- name of executable options : Maybe (FC, String) + sourcedir : Maybe String prebuild : Maybe (FC, String) -- Script to run before building postbuild : Maybe (FC, String) -- Script to run after building preinstall : Maybe (FC, String) -- Script to run after building, before installing @@ -65,7 +66,7 @@ Show PkgDesc where maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++ maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++ maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++ - maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++ + maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++ maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++ maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++ maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) @@ -75,7 +76,7 @@ initPkgDesc pname = MkPkgDesc pname "0" "Anonymous" Nothing Nothing Nothing Nothing Nothing Nothing Nothing [] [] - Nothing Nothing Nothing Nothing Nothing Nothing Nothing + Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing data DescField : Type where PVersion : FC -> String -> DescField @@ -92,6 +93,7 @@ data DescField : Type where PMainMod : FC -> List String -> DescField PExec : String -> DescField POpts : FC -> String -> DescField + PSourceDir : FC -> String -> DescField PPrebuild : FC -> String -> DescField PPostbuild : FC -> String -> DescField PPreinstall : FC -> String -> DescField @@ -110,6 +112,7 @@ field fname <|> strField PBugTracker "bugtracker" <|> strField POpts "options" <|> strField POpts "opts" + <|> strField PSourceDir "sourcedir" <|> strField PPrebuild "prebuild" <|> strField PPostbuild "postbuild" <|> strField PPreinstall "preinstall" @@ -154,37 +157,55 @@ parsePkgDesc fname fields <- many (field fname) pure (name, fields) -addField : {auto c : Ref Ctxt Defs} -> - DescField -> PkgDesc -> Core PkgDesc -addField (PVersion fc n) pkg = pure (record { version = n } pkg) -addField (PAuthors fc a) pkg = pure (record { authors = a } pkg) -addField (PMaintainers fc a) pkg = pure (record { maintainers = Just a } pkg) -addField (PLicense fc a) pkg = pure (record { license = Just a } pkg) -addField (PBrief fc a) pkg = pure (record { brief = Just a } pkg) -addField (PReadMe fc a) pkg = pure (record { readme = Just a } pkg) -addField (PHomePage fc a) pkg = pure (record { homepage = Just a } pkg) -addField (PSourceLoc fc a) pkg = pure (record { sourceloc = Just a } pkg) -addField (PBugTracker fc a) pkg = pure (record { bugtracker = Just a } pkg) +data ParsedMods : Type where -addField (PDepends ds) pkg = pure (record { depends = ds } pkg) -addField (PModules ms) pkg - = pure (record { modules = !(traverse toSource ms) } pkg) - where - toSource : (FC, List String) -> Core (List String, String) - toSource (loc, ns) = pure (ns, !(nsToSource loc ns)) -addField (PMainMod loc n) pkg - = pure (record { mainmod = Just (n, !(nsToSource loc n)) } pkg) -addField (PExec e) pkg = pure (record { executable = Just e } pkg) -addField (POpts fc e) pkg = pure (record { options = Just (fc, e) } pkg) -addField (PPrebuild fc e) pkg = pure (record { prebuild = Just (fc, e) } pkg) -addField (PPostbuild fc e) pkg = pure (record { postbuild = Just (fc, e) } pkg) -addField (PPreinstall fc e) pkg = pure (record { preinstall = Just (fc, e) } pkg) -addField (PPostinstall fc e) pkg = pure (record { postinstall = Just (fc, e) } pkg) +data MainMod : Type where + +addField : {auto c : Ref Ctxt Defs} -> + {auto p : Ref ParsedMods (List (FC, List String))} -> + {auto m : Ref MainMod (Maybe (FC, List String))} -> + DescField -> PkgDesc -> Core PkgDesc +addField (PVersion fc n) pkg = pure $ record { version = n } pkg +addField (PAuthors fc a) pkg = pure $ record { authors = a } pkg +addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg +addField (PLicense fc a) pkg = pure $ record { license = Just a } pkg +addField (PBrief fc a) pkg = pure $ record { brief = Just a } pkg +addField (PReadMe fc a) pkg = pure $ record { readme = Just a } pkg +addField (PHomePage fc a) pkg = pure $ record { homepage = Just a } pkg +addField (PSourceLoc fc a) pkg = pure $ record { sourceloc = Just a } pkg +addField (PBugTracker fc a) pkg = pure $ record { bugtracker = Just a } pkg +addField (PDepends ds) pkg = pure $ record { depends = ds } pkg +addField (PModules ms) pkg = do put ParsedMods ms + pure pkg +addField (PMainMod loc n) pkg = do put MainMod (Just (loc, n)) + pure pkg +addField (PExec e) pkg = pure $ record { executable = Just e } pkg +addField (POpts fc e) pkg = pure $ record { options = Just (fc, e) } pkg +addField (PSourceDir fc a) pkg = pure $ record { sourcedir = Just a } pkg +addField (PPrebuild fc e) pkg = pure $ record { prebuild = Just (fc, e) } pkg +addField (PPostbuild fc e) pkg = pure $ record { postbuild = Just (fc, e) } pkg +addField (PPreinstall fc e) pkg = pure $ record { preinstall = Just (fc, e) } pkg +addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg addFields : {auto c : Ref Ctxt Defs} -> List DescField -> PkgDesc -> Core PkgDesc -addFields [] desc = pure desc -addFields (x :: xs) desc = addFields xs !(addField x desc) +addFields xs desc = do p <- newRef ParsedMods [] + m <- newRef MainMod Nothing + added <- go {p} {m} xs desc + setSourceDir (sourcedir added) + ms <- get ParsedMods + mmod <- get MainMod + pure $ record { modules = !(traverse toSource ms) + , mainmod = !(traverseOpt toSource mmod) + } added + where + toSource : (FC, List String) -> Core (List String, String) + toSource (loc, ns) = pure (ns, !(nsToSource loc ns)) + go : {auto p : Ref ParsedMods (List (FC, List String))} -> + {auto m : Ref MainMod (Maybe (FC, List String))} -> + List DescField -> PkgDesc -> Core PkgDesc + go [] dsc = pure dsc + go (x :: xs) dsc = go xs !(addField x dsc) runScript : Maybe (FC, String) -> Core () runScript Nothing = pure () @@ -197,8 +218,7 @@ addDeps : {auto c : Ref Ctxt Defs} -> PkgDesc -> Core () addDeps pkg = do defs <- get Ctxt - traverse addPkgDir (depends pkg) - pure () + traverse_ addPkgDir (depends pkg) processOptions : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index e7d575f..4d71fed 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -28,7 +28,7 @@ processDecl : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> PDecl -> Core (Maybe Error) processDecl decl - = catch (do impdecls <- desugarDecl [] decl + = catch (do impdecls <- desugarDecl [] decl traverse (Check.processDecl [] (MkNested []) []) impdecls pure Nothing) (\err => do giveUpConstraints -- or we'll keep trying... @@ -41,7 +41,7 @@ processDecls : {auto c : Ref Ctxt Defs} -> List PDecl -> Core (List Error) processDecls decls = do xs <- traverse processDecl decls - Nothing <- checkDelayedHoles + Nothing <- checkDelayedHoles | Just err => pure (case mapMaybe id xs of [] => [err] errs => errs) @@ -61,7 +61,7 @@ readModule top loc vis reexp imp as = do Right fname <- nsToPath loc imp | Left err => throw err Just (syn, hash, more) <- logTime ("Reading " ++ show imp) $ - readFromTTC {extra = SyntaxInfo} + readFromTTC {extra = SyntaxInfo} loc vis fname imp as | Nothing => when vis (setVisible imp) -- already loaded, just set visibility addImported (imp, reexp, as) @@ -72,7 +72,7 @@ readModule top loc vis reexp imp as modNS <- getNS when vis $ setVisible imp - traverse_ (\ mimp => + traverse_ (\ mimp => do let m = fst mimp let reexp = fst (snd mimp) let as = snd (snd mimp) @@ -95,7 +95,7 @@ readHash imp h <- readIFaceHash fname -- If the import is a 'public' import, then it forms part of -- our own interface so add its hash to our hash - when (reexport imp) $ + when (reexport imp) $ do log 5 $ "Reexporting " ++ show (path imp) ++ " hash " ++ show h addHash h pure (nameAs imp, h) @@ -109,7 +109,7 @@ readPrelude : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> Core () -readPrelude = do readImport prelude +readPrelude = do readImport prelude setNS ["Main"] -- Import a TTC for use as the main file (e.g. at the REPL) @@ -119,7 +119,7 @@ readAsMain : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> (fname : String) -> Core () readAsMain fname - = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo} + = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo} toplevelFC True fname [] [] | Nothing => throw (InternalError "Already loaded") replNS <- getNS @@ -127,7 +127,7 @@ readAsMain fname extendAs replNS replNS syn ustm <- get UST - traverse (\ mimp => + traverse (\ mimp => do let m = fst mimp let as = snd (snd mimp) fname <- nsToPath emptyFC m @@ -144,7 +144,7 @@ readAsMain fname setNestedNS replNestedNS addPrelude : List Import -> List Import -addPrelude imps +addPrelude imps = if not (["Prelude"] `elem` map path imps) then prelude :: imps else imps @@ -177,7 +177,7 @@ processMod : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> (srcf : String) -> (ttcf : String) -> (msg : String) -> - Module -> + Module -> (sourcecode : String) -> Core (Maybe (List Error)) processMod srcf ttcf msg mod sourcecode @@ -185,8 +185,8 @@ processMod srcf ttcf msg mod sourcecode when (ns /= ["Main"]) $ do let MkFC fname _ _ = headerloc mod d <- getDirs - when (pathToNS (working_dir d) fname /= ns) $ - throw (GenericMsg (headerloc mod) + when (pathToNS (working_dir d) (source_dir d) fname /= ns) $ + throw (GenericMsg (headerloc mod) ("Module name " ++ showSep "." (reverse ns) ++ " does not match file name " ++ fname)) -- Add an implicit prelude import @@ -214,7 +214,7 @@ processMod srcf ttcf msg mod sourcecode -- for the REPL do setNS ns pure Nothing - else + else do iputStrLn msg -- read imports here -- Note: We should only import .ttc - assumption is that there's @@ -242,7 +242,7 @@ process : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - String -> FileName -> + String -> FileName -> Core (List Error) process buildmsg file = do Right res <- coreLift (readFile file) @@ -265,7 +265,7 @@ process buildmsg file then do defs <- get Ctxt d <- getDirs - makeBuildDirectory (pathToNS (working_dir d) file) + makeBuildDirectory (pathToNS (working_dir d) (source_dir d) file) logTime ("Writing TTC for " ++ file) $ writeToTTC !(get Syn) fn mfn <- getTTCFileName file ".ttm" diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index dd0133c..a7d1929 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -28,7 +28,7 @@ usage = "Usage: yaffle [--timing]" processArgs : List String -> Core Bool processArgs [] = pure False processArgs ["--timing"] = pure True -processArgs _ +processArgs _ = coreLift $ do putStrLn usage exitWith (ExitFailure 1) @@ -39,7 +39,7 @@ HasNames () where export yaffleMain : String -> List String -> Core () yaffleMain fname args - = do defs <- initDefs + = do defs <- initDefs c <- newRef Ctxt defs m <- newRef MD initMetadata u <- newRef UST initUState @@ -54,7 +54,7 @@ yaffleMain fname args _ => do coreLift $ putStrLn "Processing as TTImp" ok <- processTTImpFile fname when ok $ - do makeBuildDirectory (pathToNS (working_dir d) fname) + do makeBuildDirectory (pathToNS (working_dir d) (source_dir d) fname) writeToTTC () !(getTTCFileName fname ".ttc") coreLift $ putStrLn "Written TTC" ust <- get UST From fcb337b3dc567dd3a4941a2d5d26315a50263d36 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 24 Oct 2019 20:45:16 +0300 Subject: [PATCH 2/2] fix dir order & add comment --- src/Core/Directory.idr | 14 +++++++------- src/Idris/Package.idr | 2 ++ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 69e8918..3e85a8f 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -109,16 +109,16 @@ pathToNS wdir sdir fname = let wsplit = splitSep wdir ssplit = maybe [] splitSep sdir fsplit = splitSep fname - sdrop = dropWdir ssplit fsplit fsplit + wdrop = dropDir wsplit fsplit fsplit in - dropWdir wsplit sdrop sdrop + dropDir ssplit wdrop wdrop where - dropWdir : List String -> List String -> List String -> List String - dropWdir wdir orig [] = [] - dropWdir wdir orig (x :: xs) - = if wdir == xs + dropDir : List String -> List String -> List String -> List String + dropDir dir orig [] = [] + dropDir dir orig (x :: xs) + = if dir == xs then [x] - else x :: dropWdir wdir orig xs + else x :: dropDir dir orig xs splitSep : String -> List String splitSep fname diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index a8e980c..2fef378 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -175,6 +175,8 @@ addField (PHomePage fc a) pkg = pure $ record { homepage = Just a } pkg addField (PSourceLoc fc a) pkg = pure $ record { sourceloc = Just a } pkg addField (PBugTracker fc a) pkg = pure $ record { bugtracker = Just a } pkg addField (PDepends ds) pkg = pure $ record { depends = ds } pkg +-- we can't resolve source files for modules without knowing the source directory, +-- so we save them for the second pass addField (PModules ms) pkg = do put ParsedMods ms pure pkg addField (PMainMod loc n) pkg = do put MainMod (Just (loc, n))