mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 14:06:26 +03:00
Merge pull request #136 from clayrat/sourcedir
Add 'sourcedir' option to IPKG
This commit is contained in:
Edwin Brady
GitHub
commit
dab2bb36c1
@ -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) = "<external def with arity " ++ show arity ++ ">"
|
||||
show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
|
||||
show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
|
||||
" " ++ show cs ++">"
|
||||
show (Builtin {arity} _) = "<builtin with arith " ++ show 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
|
||||
@ -734,9 +734,9 @@ 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
|
||||
empty)
|
||||
|
||||
@ -757,7 +757,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
|
||||
@ -799,7 +799,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
|
||||
@ -812,7 +812,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
|
||||
@ -824,14 +824,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
|
||||
@ -941,7 +941,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
|
||||
@ -949,7 +949,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
|
||||
@ -961,15 +961,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))
|
||||
@ -1000,7 +1000,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
|
||||
|
||||
@ -1147,7 +1147,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
|
||||
@ -1179,14 +1179,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
|
||||
@ -1200,7 +1200,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]"))
|
||||
@ -1225,7 +1225,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]"))
|
||||
@ -1427,7 +1427,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
|
||||
@ -1460,10 +1460,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))
|
||||
@ -1480,7 +1480,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
|
||||
@ -1536,7 +1536,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
|
||||
@ -1637,6 +1637,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
|
||||
@ -1754,7 +1760,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
|
||||
@ -1770,7 +1776,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))
|
||||
|
||||
@ -1784,7 +1790,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
|
||||
@ -1854,7 +1860,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 ()
|
||||
|
||||
@ -1917,7 +1923,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
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -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,31 +93,35 @@ 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
|
||||
wdrop = dropDir wsplit fsplit fsplit
|
||||
in
|
||||
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
|
||||
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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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,57 @@ 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
|
||||
-- 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))
|
||||
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 +220,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} ->
|
||||
|
||||
@ -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"
|
||||
|
||||
@ -28,7 +28,7 @@ usage = "Usage: yaffle <input file> [--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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user