use string for module names
This commit is contained in:
@@ -132,8 +132,8 @@ fcCol fc = fc.bnds.startCol
|
||||
class HasFC a where
|
||||
getFC : a -> FC
|
||||
|
||||
primNS : List String
|
||||
primNS = ("Prim" :: Nil)
|
||||
primNS : String
|
||||
primNS = "Prim"
|
||||
|
||||
emptyFC : FC
|
||||
emptyFC = MkFC "" (MkBounds 0 0 0 0)
|
||||
@@ -141,10 +141,9 @@ emptyFC = MkFC "" (MkBounds 0 0 0 0)
|
||||
emptyFC' : String → FC
|
||||
emptyFC' fn = MkFC fn (MkBounds 0 0 0 0)
|
||||
|
||||
-- Error of a parse
|
||||
|
||||
-- Using a String instead of List String for the module shaved about 16% of compile time...
|
||||
data QName : U where
|
||||
QN : List String -> String -> QName
|
||||
QN : String -> String -> QName
|
||||
|
||||
.baseName : QName → String
|
||||
(QN _ name).baseName = name
|
||||
@@ -154,8 +153,8 @@ instance Eq QName where
|
||||
QN ns n == QN ns' n' = if n == n' then ns == ns' else False
|
||||
|
||||
instance Show QName where
|
||||
show (QN Nil n) = n
|
||||
show (QN ns n) = joinBy "." ns ++ "." ++ n
|
||||
show (QN "" n) = n
|
||||
show (QN ns n) = ns ++ "." ++ n
|
||||
|
||||
instance Ord QName where
|
||||
compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
|
||||
|
||||
@@ -157,7 +157,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
|
||||
applySucc Nil = pure $ CLam "x" $ CPrimOp "+" (CLit $ LInt 1) (CBnd 0)
|
||||
applySucc (t :: Nil) = pure $ CPrimOp "+" (CLit $ LInt 1) t
|
||||
applySucc _ = error emptyFC "overapplied Succ \{show tm}"
|
||||
compileTerm (UU _) = pure $ CRef (QN Nil "U")
|
||||
compileTerm (UU _) = pure $ CRef (QN "" "U")
|
||||
compileTerm (Pi _ nm icit rig t u) = do
|
||||
t' <- compileTerm t
|
||||
u' <- compileTerm u
|
||||
|
||||
@@ -1549,7 +1549,7 @@ infer ctx tm@(RUpdateRec fc _ _) = do
|
||||
infer ctx (RVar fc nm) = go 0 ctx.types
|
||||
where
|
||||
entryNS : TopEntry → String
|
||||
entryNS (MkEntry fc (QN ns _) _ _ _) = joinBy "." ns
|
||||
entryNS (MkEntry fc (QN ns _) _ _ _) = ns
|
||||
|
||||
go : Int -> List (String × Val) -> M (Tm × Val)
|
||||
go i Nil = do
|
||||
|
||||
@@ -100,9 +100,9 @@ checkAlreadyDef fc nm = do
|
||||
Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
|
||||
|
||||
|
||||
processDecl : List String -> Decl -> M Unit
|
||||
processDecl : String -> Decl -> M Unit
|
||||
|
||||
processTypeSig : List String → FC → List Name → Raw → M Unit
|
||||
processTypeSig : String → FC → List Name → Raw → M Unit
|
||||
processTypeSig ns fc names tm = do
|
||||
log 1 $ \ _ => "-----"
|
||||
top <- getTop
|
||||
@@ -112,7 +112,7 @@ processTypeSig ns fc names tm = do
|
||||
ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
|
||||
|
||||
|
||||
processPrimType : List Name → FC → Name → Maybe Raw → M Unit
|
||||
processPrimType : String → FC → Name → Maybe Raw → M Unit
|
||||
processPrimType ns fc nm ty = do
|
||||
top <- getTop
|
||||
ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc)
|
||||
@@ -120,7 +120,7 @@ processPrimType ns fc nm ty = do
|
||||
setDef (QN ns nm) fc ty' (PrimTCon arity) Nil
|
||||
|
||||
|
||||
processPrimFn : List String → FC → String → List String → Raw → String → M Unit
|
||||
processPrimFn : String → FC → String → List String → Raw → String → M Unit
|
||||
processPrimFn ns fc nm used ty src = do
|
||||
top <- getTop
|
||||
ty <- check (mkCtx fc) ty (VU fc)
|
||||
@@ -153,7 +153,7 @@ complexity (Lit _ _) = 0
|
||||
complexity (Case _ sc (CaseCons _ _ t :: Nil)) = 1 + complexity sc + complexity t
|
||||
complexity _ = 100
|
||||
|
||||
processDef : List String → FC → String → List (Raw × Maybe Raw) → M Unit
|
||||
processDef : String → FC → String → List (Raw × Maybe Raw) → M Unit
|
||||
processDef ns fc nm clauses = do
|
||||
log 1 $ \ _ => "-----"
|
||||
log 1 $ \ _ => "Def \{show nm}"
|
||||
@@ -194,7 +194,7 @@ processDef ns fc nm clauses = do
|
||||
then setFlag (QN ns nm) fc Inline
|
||||
else pure MkUnit
|
||||
|
||||
processCheck : List String → FC → Raw → Raw → M Unit
|
||||
processCheck : String → FC → Raw → Raw → M Unit
|
||||
processCheck ns fc tm ty = do
|
||||
log 1 $ \ _ => "----- DCheck"
|
||||
top <- getTop
|
||||
@@ -209,7 +209,7 @@ processCheck ns fc tm ty = do
|
||||
putStrLn " NF \{render 90 $ pprint Nil norm}"
|
||||
|
||||
|
||||
processClass : List String → FC → (FC × String) → Telescope → List Decl → M Unit
|
||||
processClass : String → FC → (FC × String) → Telescope → List Decl → M Unit
|
||||
processClass ns classFC (nameFC, nm) tele decls = do
|
||||
-- REVIEW maybe we can leverage Record for this
|
||||
-- a couple of catches, we don't want the dotted accessors and
|
||||
@@ -257,7 +257,7 @@ processClass ns classFC (nameFC, nm) tele decls = do
|
||||
mkApp : Raw → BindInfo × Raw → Raw
|
||||
mkApp acc (BI fc nm icit _, _) = RApp fc acc (RVar fc nm) icit
|
||||
|
||||
processInstance : List String → FC → Raw → Maybe (List Decl) → M Unit
|
||||
processInstance : String → FC → Raw → Maybe (List Decl) → M Unit
|
||||
processInstance ns instfc ty decls = do
|
||||
log 1 $ \ _ => "-----"
|
||||
log 1 $ \ _ => "Instance \{render 90 $ pretty ty}"
|
||||
@@ -372,7 +372,7 @@ processInstance ns instfc ty decls = do
|
||||
apply x (y :: xs) = error instfc "expected pi type \{show x}"
|
||||
|
||||
-- desugars to Data and processes it
|
||||
processShortData : List String → FC → Raw → List Raw → M Unit
|
||||
processShortData : String → FC → Raw → List Raw → M Unit
|
||||
processShortData ns fc lhs sigs = do
|
||||
(nameFC, nm,args) <- getArgs lhs Nil
|
||||
let ty = foldr mkPi (RU fc) args
|
||||
@@ -431,7 +431,7 @@ populateConInfo entries =
|
||||
isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ (Many :: Nil) hn) _) = a == b
|
||||
isSucc _ = False
|
||||
|
||||
processData : List String → FC → FC × String → Raw → List Decl → M Unit
|
||||
processData : String → FC → FC × String → Raw → List Decl → M Unit
|
||||
processData ns fc (nameFC, nm) ty cons = do
|
||||
log 1 $ \ _ => "-----"
|
||||
log 1 $ \ _ => "Data \{nm}"
|
||||
@@ -487,7 +487,7 @@ processData ns fc (nameFC, nm) ty cons = do
|
||||
checkDeclType _ = error fc "data type doesn't return U"
|
||||
|
||||
|
||||
processRecord : List String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit
|
||||
processRecord : String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit
|
||||
processRecord ns recordFC (nameFC, nm) tele cname decls = do
|
||||
log 1 $ \ _ => "-----"
|
||||
log 1 $ \ _ => "Record"
|
||||
|
||||
@@ -23,10 +23,11 @@ addPrimitives = do
|
||||
top <- getTop
|
||||
let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors
|
||||
let modules = updateMap primNS mod top.modules
|
||||
-- TODO - do we clear this? Try just modules := modules, but wait until this refactor is done.
|
||||
modifyTop [ modules := modules
|
||||
; imported := primNS :: Nil
|
||||
; hints := emptyMap
|
||||
; ns := Nil
|
||||
; ns := ""
|
||||
; defs := emptyMap
|
||||
]
|
||||
pure mod
|
||||
@@ -62,17 +63,17 @@ importHints (entry :: entries) = do
|
||||
-- HACK this is returning src to help render errors..
|
||||
-- Maybe return module, put src and errors in module, add error for import with error, callers can sort out what they want to do?
|
||||
-- The issue here is command line newt wants to report all errors (we can print that though?) LSP wants something more subtle
|
||||
processModule : FC → FileSource → List String → (stack : List String) → M ModContext
|
||||
processModule : FC → FileSource → List String → String → M ModContext
|
||||
processModule importFC repo stk modns = do
|
||||
top <- getTop
|
||||
let name = joinBy "." modns
|
||||
|
||||
let (Nothing) = lookupMap' modns top.modules
|
||||
| Just mod => pure mod
|
||||
|
||||
let (False) = modns == primNS
|
||||
| _ => addPrimitives
|
||||
|
||||
let fn = joinBy "/" modns ++ ".newt"
|
||||
let parts = split modns "."
|
||||
let fn = joinBy "/" parts ++ ".newt"
|
||||
-- TODO now we can pass in the module name...
|
||||
(fn,src) <- repo.getFile importFC fn
|
||||
let (Right toks) = tokenise fn src
|
||||
@@ -82,21 +83,18 @@ processModule importFC repo stk modns = do
|
||||
| Left (err, toks) => throwError err
|
||||
|
||||
log 1 $ \ _ => "scan imports for module \{modName}"
|
||||
let (True) = modns == split modName "."
|
||||
let (True) = modns == modName
|
||||
| _ => throwError $ E nameFC "module name \{show modName} doesn't match file name \{show fn}"
|
||||
|
||||
let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks
|
||||
| Left (err, toks) => throwError err
|
||||
|
||||
let importNames = map importToName imports
|
||||
|
||||
imported <- for imports $ \case
|
||||
MkImport fc (nameFC, name') => do
|
||||
let imp = split name' "."
|
||||
when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}"
|
||||
processModule nameFC repo (name :: stk) imp
|
||||
pure $ imp
|
||||
processModule nameFC repo (name :: stk) primNS
|
||||
when (elem name' stk) $ \ _ => error nameFC "import loop \{modns} → \{name'}"
|
||||
processModule nameFC repo (modns :: stk) name'
|
||||
pure $ name'
|
||||
processModule nameFC repo (modns :: stk) primNS
|
||||
let imported = snoc imported primNS
|
||||
|
||||
putStrLn "module \{modName}"
|
||||
@@ -107,6 +105,7 @@ processModule importFC repo stk modns = do
|
||||
|
||||
top <- getTop
|
||||
let freshMC = MC emptyMap Nil 0 CheckAll
|
||||
-- NOW Print and drop errors here
|
||||
-- set imported, mod, freshMC, ops before processing
|
||||
modifyTop [ imported := imported
|
||||
; hints := emptyMap
|
||||
@@ -125,7 +124,7 @@ processModule importFC repo stk modns = do
|
||||
-- update modules with result, leave the rest of context in case this is top file
|
||||
top <- getTop
|
||||
|
||||
let mod = MkModCtx src top.defs top.metaCtx top.ops importNames top.errors
|
||||
let mod = MkModCtx src top.defs top.metaCtx top.ops imported top.errors
|
||||
|
||||
let modules = updateMap modns mod top.modules
|
||||
modifyTop [modules := modules]
|
||||
@@ -134,11 +133,11 @@ processModule importFC repo stk modns = do
|
||||
-- FIXME module context should hold errors, to report in replay
|
||||
pure mod
|
||||
where
|
||||
tryProcessDecl : String → List String → Decl → M Unit
|
||||
tryProcessDecl : String → String → Decl → M Unit
|
||||
tryProcessDecl src ns decl = do
|
||||
(Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
|
||||
addError err
|
||||
|
||||
-- TODO clear dependents too.
|
||||
invalidateModule : List String -> M Unit
|
||||
-- NOW TODO clear dependents too.
|
||||
invalidateModule : String -> M Unit
|
||||
invalidateModule modname = modifyTop [modules $= deleteMap modname]
|
||||
|
||||
@@ -36,7 +36,8 @@ replQN = do
|
||||
ident <- uident
|
||||
rest <- many $ token Projection
|
||||
let name = joinBy "" (ident :: rest)
|
||||
pure $ uncurry QN $ unsnoc $ split1 name "."
|
||||
let (ns,nm) = unsnoc $ split1 name "."
|
||||
pure $ QN (joinBy "." ns) nm
|
||||
|
||||
data ArgType = ArgNone | ArgString | ArgIdent | ArgOptInt | ArgQName
|
||||
|
||||
|
||||
@@ -65,7 +65,7 @@ rewriteTailCalls nms tm = case tm of
|
||||
|
||||
-- the name of our trampoline
|
||||
bouncer : QName
|
||||
bouncer = QN Nil "bouncer"
|
||||
bouncer = QN "" "bouncer"
|
||||
|
||||
doOptimize : List (QName × CExp) → M (List (QName × CExp))
|
||||
doOptimize fns = do
|
||||
|
||||
@@ -34,7 +34,7 @@ lookupRaw raw top =
|
||||
Just entry => Just entry
|
||||
Nothing => go top.imported
|
||||
where
|
||||
go : List (List String) → Maybe TopEntry
|
||||
go : List String → Maybe TopEntry
|
||||
go Nil = Nothing
|
||||
go (ns :: nss) = case lookupMap' ns top.modules of
|
||||
Nothing => go nss
|
||||
@@ -47,7 +47,7 @@ instance Show TopContext where
|
||||
show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.defs}]"
|
||||
|
||||
emptyTop : TopContext
|
||||
emptyTop = MkTop emptyMap Nil emptyMap Nil emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap
|
||||
emptyTop = MkTop emptyMap Nil emptyMap "" emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap
|
||||
|
||||
|
||||
setFlag : QName → FC → EFlag → M Unit
|
||||
|
||||
@@ -402,7 +402,7 @@ record ModContext where
|
||||
modMetaCtx : MetaContext
|
||||
-- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import
|
||||
ctxOps : Operators
|
||||
modDeps : List (List String)
|
||||
modDeps : List String
|
||||
modErrors : List Error
|
||||
|
||||
-- Top level context.
|
||||
@@ -421,15 +421,13 @@ HintTable = SortedMap QName (List (QName × Tm))
|
||||
|
||||
record TopContext where
|
||||
constructor MkTop
|
||||
-- maybe we use a String instead of List String for the left of QN
|
||||
-- I'm putting a dummy entry in
|
||||
modules : SortedMap (List String) ModContext
|
||||
imported : List (List String)
|
||||
modules : SortedMap String ModContext
|
||||
imported : List String
|
||||
-- TCon name → function name × type
|
||||
hints : HintTable
|
||||
|
||||
-- current module
|
||||
ns : List String
|
||||
ns : String
|
||||
defs : SortedMap QName TopEntry
|
||||
metaCtx : MetaContext
|
||||
|
||||
|
||||
Reference in New Issue
Block a user