From 9e7e27ed0347219db948aadb5cc9e3e0bf6f25f5 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 13 Apr 2019 13:33:45 +0100 Subject: [PATCH] Fill in holes for reading/writing TTC Tricky bit is the 'NameRefs'. When we load a file back in, we load a mapping from resolved ids in the file to their full names, and immediately resolve them in the current context so that we have the correct ids after loading. --- src/Core/Binary.idr | 224 ++++++++++++++---------- src/Core/Context.idr | 183 ++++++++++++++++++-- src/Core/Hash.idr | 152 +++++++++++----- src/Core/Options.idr | 2 +- src/Core/TT.idr | 11 +- src/Core/TTC.idr | 352 +++++++++++++++++++++++++++++++++++++- src/Core/UnifyState.idr | 30 +++- src/Data/IOArray.idr | 26 +++ src/TTImp/ProcessData.idr | 4 +- src/TTImp/ProcessType.idr | 2 +- src/Utils/Binary.idr | 92 ++++++---- 11 files changed, 880 insertions(+), 198 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 96de527..7ff0df1 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -8,6 +8,8 @@ import Core.TT import Core.TTC import Core.UnifyState +import Data.IntMap + -- Reading and writing 'Defs' from/to a binary file -- In order to be saved, a name must have been flagged using 'toSave'. -- (Otherwise we'd save out everything, not just the things in the current @@ -39,113 +41,153 @@ record TTCFile extra where version : Int ifaceHash : Int importHashes : List (List String, Int) + nameMap : NameRefs -- All the names referenced in the file + -- This is a mapping from the index used in the file + -- to the actual name holes : List (Int, (FC, Name)) guesses : List (Int, (FC, Name)) - constraints : Context Constraint - context : Defs + constraints : List (Int, Constraint) + context : List GlobalDef + imported : List (List String, Bool, List String) + currentNS : List String extraData : extra +asName : List String -> Maybe (List String) -> Name -> Name +asName mod (Just ns) (NS oldns n) + = if mod == oldns + then NS ns n -- TODO: What about if there are nested namespaces in a module? + else NS oldns n +asName _ _ n = n + +readNameMap : NameRefs -> Ref Bin Binary -> Core NameRefs +readNameMap r b + = do ns <- fromBuf r b + coreLift $ fromList ns + +-- For every name we're going to read from the file, work out what it's +-- new resolved name is going to be in the context and update the name +-- map accordingly +-- Also update namespace if we've done "import ... as ..." +updateEntries : {auto c : Ref Ctxt Defs} -> + Context GlobalDef -> + List String -> Maybe (List String) -> + Int -> Int -> NameRefs -> Core (Context GlobalDef) +updateEntries ctxt mod as pos end r + = if pos >= end + then pure ctxt + else do Just (n, Nothing) <- coreLift $ readArray r pos + | _ => updateEntries ctxt mod as (pos+1) end r + let n' = asName mod as n + (idx, ctxt') <- getPosition n' ctxt + coreLift $ writeArray r pos (n', Just idx) + updateEntries ctxt' mod as (pos+1) end r + +writeNameMap : Ref Bin Binary -> NameRefs -> Core () +writeNameMap b r + = do ns <- coreLift $ toList r + toBuf b ns + -- NOTE: TTC files are only compatible if the version number is the same, -- *and* the 'annot/extra' type are the same, or there are no holes/constraints -TTC extra => TTC (TTCFile extra) where - toBuf b file +writeTTCFile : TTC extra => Ref Bin Binary -> TTCFile extra -> Core () +writeTTCFile b file = do toBuf b "TTC" toBuf b (version file) toBuf b (ifaceHash file) toBuf b (importHashes file) + writeNameMap b (nameMap file) toBuf b (holes file) toBuf b (guesses file) toBuf b (constraints file) toBuf b (context file) + toBuf b (imported file) + toBuf b (currentNS file) toBuf b (extraData file) - fromBuf b - = do hdr <- fromBuf b +readTTCFile : TTC extra => + {auto c : Ref Ctxt Defs} -> + List String -> Maybe (List String) -> + NameRefs -> Ref Bin Binary -> Core (TTCFile extra) +readTTCFile modns as r b + = do hdr <- fromBuf r b when (hdr /= "TTC") $ corrupt "TTC header" - ver <- fromBuf b + ver <- fromBuf r b checkTTCVersion ver ttcVersion - ifaceHash <- fromBuf b - importHashes <- fromBuf b - holes <- fromBuf b - guesses <- fromBuf b - constraints <- fromBuf b - defs <- fromBuf b - ex <- fromBuf b - pure (MkTTCFile ver ifaceHash importHashes - holes guesses constraints defs ex) + ifaceHash <- fromBuf r b + importHashes <- fromBuf r b + -- Read in name map, update 'r' + r <- readNameMap r b + defs <- get Ctxt + gam' <- updateEntries (gamma defs) modns as 0 (max r) r + setCtxt gam' + holes <- fromBuf r b + guesses <- fromBuf r b + constraints <- fromBuf r b + defs <- fromBuf r b + imp <- fromBuf r b + cns <- fromBuf r b + ex <- fromBuf r b + pure (MkTTCFile ver ifaceHash importHashes r + holes guesses constraints defs imp cns ex) -{- --- Update the various fields in Defs affected by the name's flags -processFlags : Name -> List DefFlag -> Defs -> Defs -processFlags n [] defs = defs -processFlags n (GlobalHint t :: fs) defs - = processFlags n fs (record { autoHints $= ((t, n) ::) } defs) -processFlags n (TypeHint ty d :: fs) defs - = processFlags n fs (addToTypeHints ty n d defs) -processFlags n (Inline :: fs) defs = processFlags n fs defs -processFlags n (TCInline :: fs) defs = processFlags n fs defs -processFlags n (Invertible :: fs) defs = processFlags n fs defs -processFlags n (Overloadable :: fs) defs = processFlags n fs defs -processFlags n (SetTotal t :: fs) defs = processFlags n fs defs - --- For every name (from 'toSave' in defs), add its definition and any --- information from its flags to the new set of Defs that we'll write out --- as Binary. -mkSaveDefs : List Name -> Defs -> Defs -> Defs -mkSaveDefs [] acc _ = acc -mkSaveDefs (n :: ns) acc defs - = case lookupGlobalExact n (gamma defs) of - Nothing => mkSaveDefs ns acc defs -- 'n' really should exist though! - Just gdef => - let gdef' = record { type $= normaliseHoles defs [] } gdef - gam' = addCtxt n gdef' (gamma acc) - defs' = processFlags n (flags gdef) defs in - mkSaveDefs ns (record { gamma = gam' } acc) defs' +-- Pull out the list of GlobalDefs that we want to save +getSaveDefs : List Name -> List GlobalDef -> Defs -> Core (List GlobalDef) +getSaveDefs [] acc _ = pure acc +getSaveDefs (n :: ns) acc defs + = do Just gdef <- lookupCtxtExact n (gamma defs) + | Nothing => getSaveDefs ns acc defs -- 'n' really should exist though! + getSaveDefs ns (gdef :: acc) defs -- Write out the things in the context which have been defined in the -- current source file export -writeToTTC : (TTC annot annot, TTC annot extra) => +writeToTTC : TTC extra => {auto c : Ref Ctxt Defs} -> - {auto u : Ref UST (UState annot)} -> - extra -> - (fname : String) -> - Core annot () + {auto u : Ref UST UState} -> + extra -> (fname : String) -> Core () writeToTTC extradata fname = do buf <- initBinary defs <- get Ctxt ust <- get UST - let defs' = mkSaveDefs (getSave defs) - (record { options = options defs, - imported = imported defs, - currentNS = currentNS defs, - hiddenNames = hiddenNames defs, - cgdirectives = cgdirectives defs - } initCtxt) - defs + gdefs <- getSaveDefs (getSave defs) [] defs log 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs) - toBuf buf (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs) - (holes ust) (constraints ust) defs' + r <- getNameRefs (gamma defs) + writeTTCFile buf + (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs) + r + (toList (holes ust)) + (toList (guesses ust)) + (toList (constraints ust)) + gdefs + (imported defs) + (currentNS defs) extradata) Right ok <- coreLift $ writeToFile fname !(get Bin) | Left err => throw (InternalError (fname ++ ": " ++ show err)) pure () +addGlobalDef : {auto c : Ref Ctxt Defs} -> + (modns : List String) -> (importAs : Maybe (List String)) -> + GlobalDef -> Core () +addGlobalDef modns as def + = do let n = fullname def + addDef (asName modns as n) def + pure () + -- Add definitions from a binary file to the current context -- Returns the "extra" section of the file (user defined data), the interface --- has and the list of additional TTCs that need importing +-- hash and the list of additional TTCs that need importing -- (we need to return these, rather than do it here, because after loading -- the data that's when we process the extra data...) export -readFromTTC : (TTC annot annot, TTC annot extra) => +readFromTTC : TTC extra => {auto c : Ref Ctxt Defs} -> - {auto u : Ref UST (UState annot)} -> - annot -> - Bool -> + {auto u : Ref UST UState} -> + FC -> Bool -> (fname : String) -> -- file containing the module (modNS : List String) -> -- module namespace (importAs : List String) -> -- namespace to import as - Core annot (Maybe (extra, Int, List (List String, Bool, List String))) + Core (Maybe (extra, Int, List (List String, Bool, List String))) readFromTTC loc reexp fname modNS importAs = do defs <- get Ctxt -- If it's already in the context, don't load it again @@ -156,42 +198,39 @@ readFromTTC loc reexp fname modNS importAs Right buf <- coreLift $ readFromFile fname | Left err => throw (InternalError (fname ++ ": " ++ show err)) bin <- newRef Bin buf -- for reading the file into - sh <- initShare -- for recording string sharing - ttc <- fromBuf sh bin - -- Rename everything in the ttc's context according to the namespace - -- it was imported as - -- [TODO] - let renamed = context ttc - - -- Extend the current context with the updated definitions from the ttc - extendAs loc reexp modNS importAs renamed - setNS (currentNS (context ttc)) + r <- initNameRefs 1 -- this will be updated when we read the name + -- map from the file + let as = if importAs == modNS + then Nothing + else Just importAs + ttc <- readTTCFile modNS as r bin + traverse (addGlobalDef modNS as) (context ttc) + setNS (currentNS ttc) -- Finally, update the unification state with the holes from the -- ttc ust <- get UST - put UST (record { holes = holes ttc, - constraints = constraints ttc } ust) - pure (Just (extraData ttc, ifaceHash ttc, imported (context ttc))) - -} + put UST (record { holes = fromList (holes ttc), + constraints = fromList (constraints ttc) } ust) + pure (Just (extraData ttc, ifaceHash ttc, imported ttc)) -getImportHashes : Ref Bin Binary -> +getImportHashes : NameRefs -> Ref Bin Binary -> Core (List (List String, Int)) -getImportHashes b - = do hdr <- fromBuf {a = String} b +getImportHashes r b + = do hdr <- fromBuf r {a = String} b when (hdr /= "TTC") $ corrupt "TTC header" - ver <- fromBuf {a = Int} b + ver <- fromBuf r {a = Int} b checkTTCVersion ver ttcVersion - ifaceHash <- fromBuf {a = Int} b - fromBuf b + ifaceHash <- fromBuf r {a = Int} b + fromBuf r b -getHash : Ref Bin Binary -> Core Int -getHash b - = do hdr <- fromBuf {a = String} b +getHash : NameRefs -> Ref Bin Binary -> Core Int +getHash r b + = do hdr <- fromBuf r {a = String} b when (hdr /= "TTC") $ corrupt "TTC header" - ver <- fromBuf {a = Int} b + ver <- fromBuf r {a = Int} b checkTTCVersion ver ttcVersion - fromBuf b + fromBuf r b export readIFaceHash : (fname : String) -> -- file containing the module @@ -200,8 +239,8 @@ readIFaceHash fname = do Right buf <- coreLift $ readFromFile fname | Left err => pure 0 b <- newRef Bin buf - - catch (getHash b) + r <- initNameRefs 1 + catch (getHash r b) (\err => pure 0) export @@ -211,6 +250,7 @@ readImportHashes fname = do Right buf <- coreLift $ readFromFile fname | Left err => pure [] b <- newRef Bin buf - catch (getImportHashes b) + r <- initNameRefs 1 + catch (getImportHashes r b) (\err => pure []) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 9ca92a9..1b0e1bb 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -4,6 +4,7 @@ import public Core.Core import public Core.Name import Core.Options import public Core.TT +import Core.TTC import Utils.Binary import Data.IOArray @@ -32,10 +33,21 @@ record Context a where -- visible visibleNS : List (List String) +-- Make an array which is a mapping from IDs to the names they represent +-- (the reverse of 'resolvedAs') which we use when serialising to record which +-- name each ID refers to. Then when we read references in terms, we'll know +-- which name it really is and can update appropriately for the new context. export -TTC a => TTC (Context a) where - toBuf = ?tocontext - fromBuf = ?fromcontext +getNameRefs : Context a -> Core NameRefs +getNameRefs gam + = do arr <- coreLift $ newArray (nextEntry gam) + traverse (addToMap arr) (toList (resolvedAs gam)) + pure arr + where + addToMap : NameRefs -> (Name, Int) -> Core () + addToMap arr (n, i) + = coreLift $ writeArray arr i (n, Nothing) + initSize : Int initSize = 10000 @@ -67,6 +79,7 @@ addPossible n i ps -- Get the position of the next entry in the context array, growing the -- array if it's out of bounds. -- Updates the context with the mapping from name to index +export getPosition : Name -> Context a -> Core (Int, Context a) getPosition (Resolved idx) ctxt = pure (idx, ctxt) getPosition n ctxt @@ -182,6 +195,33 @@ Show Def where show (Hole inv) = "Hole" show (Guess tm cs) = "Guess " ++ show tm ++ " when " ++ show cs +export +TTC Def where + toBuf b None = tag 0 + toBuf b (Fn x) = do tag 1; toBuf b x + toBuf b (DCon t arity) = do tag 2; toBuf b t; toBuf b arity + toBuf b (TCon t arity parampos detpos datacons) + = do tag 3; toBuf b t; toBuf b arity; toBuf b parampos + toBuf b detpos; toBuf b datacons + toBuf b (Hole invertible) = do tag 4; toBuf b invertible + toBuf b (Guess guess constraints) = do tag 5; toBuf b guess; toBuf b constraints + + fromBuf r b + = case !getTag of + 0 => pure None + 1 => do x <- fromBuf r b + pure (Fn x) + 2 => do t <- fromBuf r b; a <- fromBuf r b + pure (DCon t a) + 3 => do t <- fromBuf r b; a <- fromBuf r b + ps <- fromBuf r b; dets <- fromBuf r b; cs <- fromBuf r b + pure (TCon t a ps dets cs) + 4 => do i <- fromBuf r b; + pure (Hole i) + 5 => do g <- fromBuf r b; cs <- fromBuf r b + pure (Guess g cs) + _ => corrupt "Def" + public export record Constructor where constructor MkCon @@ -195,18 +235,108 @@ data DataDef : Type where MkData : (tycon : Constructor) -> (datacons : List Constructor) -> DataDef +public export +data TotalReq = Total | CoveringOnly | PartialOK + +public export +data DefFlag + = TypeHint Name Bool -- True == direct hint + | GlobalHint Bool -- True == always search (not a default hint) + | Inline + | Invertible -- assume safe to cancel arguments in unification + | Overloadable -- allow ad-hoc overloads + | TCInline -- always inline before totality checking + -- (in practice, this means it's reduced in 'normaliseHoles') + -- This means the function gets inlined when calculating the size + -- change graph, but otherwise not. It's only safe if the function + -- being inlined is terminating no matter what, and is really a bit + -- of a hack to make sure interface dictionaries are properly inlined + -- (otherwise they look potentially non terminating) so use with + -- care! + | SetTotal TotalReq + +export +Eq TotalReq where + (==) Total Total = True + (==) CoveringOnly CoveringOnly = True + (==) PartialOK PartialOK = True + (==) _ _ = False + +export +Eq DefFlag where + (==) (TypeHint ty x) (TypeHint ty' y) = ty == ty' && x == y + (==) (GlobalHint x) (GlobalHint y) = x == y + (==) Inline Inline = True + (==) Invertible Invertible = True + (==) Overloadable Overloadable = True + (==) TCInline TCInline = True + (==) (SetTotal x) (SetTotal y) = x == y + (==) _ _ = False + +TTC TotalReq where + toBuf b Total = tag 0 + toBuf b CoveringOnly = tag 1 + toBuf b PartialOK = tag 2 + + fromBuf s b + = case !getTag of + 0 => pure Total + 1 => pure CoveringOnly + 2 => pure PartialOK + _ => corrupt "TotalReq" + +TTC DefFlag where + toBuf b (TypeHint x y) = do tag 0; toBuf b x; toBuf b y + toBuf b (GlobalHint t) = do tag 1; toBuf b t + toBuf b Inline = tag 2 + toBuf b Invertible = tag 3 + toBuf b Overloadable = tag 4 + toBuf b TCInline = tag 5 + toBuf b (SetTotal x) = do tag 6; toBuf b x + + fromBuf s b + = case !getTag of + 0 => do x <- fromBuf s b; y <- fromBuf s b; pure (TypeHint x y) + 1 => do t <- fromBuf s b; pure (GlobalHint t) + 2 => pure Inline + 3 => pure Invertible + 4 => pure Overloadable + 5 => pure TCInline + 6 => do x <- fromBuf s b; pure (SetTotal x) + _ => corrupt "DefFlag" + public export record GlobalDef where constructor MkGlobalDef location : FC + fullname : Name -- original unresolved name type : ClosedTerm multiplicity : RigCount visibility : Visibility + flags : List DefFlag definition : Def export -newDef : FC -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef -newDef fc rig ty vis def = MkGlobalDef fc ty rig vis def +TTC GlobalDef where + toBuf b gdef + = do toBuf b (location gdef) + toBuf b (fullname gdef) + toBuf b (type gdef) + toBuf b (multiplicity gdef) + toBuf b (visibility gdef) + toBuf b (flags gdef) + toBuf b (definition gdef) + + fromBuf r b + = do loc <- fromBuf r b; name <- fromBuf r b + ty <- fromBuf r b; mul <- fromBuf r b + vis <- fromBuf r b; fl <- fromBuf r b + def <- fromBuf r b + pure (MkGlobalDef loc name ty mul vis fl def) + +export +newDef : FC -> Name -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef +newDef fc n rig ty vis def = MkGlobalDef fc n ty rig vis [] def public export record Defs where @@ -214,9 +344,17 @@ record Defs where gamma : Context GlobalDef currentNS : List String -- namespace for current definitions options : Options --- toSave : SortedSet + toSave : NameMap () nextTag : Int ifaceHash : Int + -- interface hashes of imported modules + importHashes : List (List String, Int) + -- imported modules, whether to rexport, as namespace + imported : List (List String, Bool, List String) + -- all imported filenames/namespaces, just to avoid loading something + -- twice unnecessarily (this is a record of all the things we've + -- called 'readFromTTC' with, in practice) + allImported : List (String, List String) export clearDefs : Defs -> Core Defs @@ -228,12 +366,11 @@ export initDefs : Core Defs initDefs = do gam <- initCtxt - pure (MkDefs gam ["Main"] defaults 100 5381) + pure (MkDefs gam ["Main"] defaults empty 100 5381 [] [] []) export -TTC Defs where - toBuf = ?todefs - fromBuf = ?fromdefs +getSave : Defs -> List Name +getSave = map Basics.fst . toList . toSave -- Label for context references export @@ -248,6 +385,28 @@ addDef n def put Ctxt (record { gamma = gam' } defs) pure idx +export +setCtxt : {auto c : Ref Ctxt Defs} -> Context GlobalDef -> Core () +setCtxt gam + = do defs <- get Ctxt + put Ctxt (record { gamma = gam } defs) + +-- Set the default namespace for new definitions +export +setNS : {auto c : Ref Ctxt Defs} -> + List String -> Core () +setNS ns + = do defs <- get Ctxt + put Ctxt (record { currentNS = ns } defs) + +-- Get the default namespace for new definitions +export +getNS : {auto c : Ref Ctxt Defs} -> + Core (List String) +getNS + = do defs <- get Ctxt + pure (currentNS defs) + getNextTypeTag : {auto c : Ref Ctxt Defs} -> Core Int getNextTypeTag @@ -264,7 +423,7 @@ addData : {auto c : Ref Ctxt Defs} -> addData vis (MkData (MkCon dfc tyn arity tycon) datacons) = do defs <- get Ctxt tag <- getNextTypeTag - let tydef = newDef dfc RigW tycon vis + let tydef = newDef dfc tyn RigW tycon vis (TCon tag arity (paramPos tyn (map type datacons)) (allDet arity) @@ -286,7 +445,7 @@ addData vis (MkData (MkCon dfc tyn arity tycon) datacons) Context GlobalDef -> Core (Context GlobalDef) addDataConstructors tag [] gam = pure gam addDataConstructors tag (MkCon fc n a ty :: cs) gam - = do let condef = newDef fc RigW ty (conVisibility vis) (DCon tag a) + = do let condef = newDef fc n RigW ty (conVisibility vis) (DCon tag a) (idx, gam') <- addCtxt n condef gam addDataConstructors (tag + 1) cs gam' diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr index a9d91ff..0c0721e 100644 --- a/src/Core/Hash.idr +++ b/src/Core/Hash.idr @@ -3,7 +3,7 @@ module Core.Hash import Core.TT import Data.List -%default total +%default covering -- This is so that we can store a hash of the interface in ttc files, to avoid -- the need for reloading modules when no interfaces have changed in imports. @@ -18,10 +18,20 @@ interface Hashable a where hash = hashWithSalt 5381 hashWithSalt h i = h * 33 + hash i +infixl 5 `hashWithSalt` + export Hashable Int where hash = id +export +Hashable Integer where + hash = fromInteger + +export +Hashable Nat where + hash = cast + export Hashable Char where hash = cast @@ -31,6 +41,11 @@ Hashable a => Hashable (List a) where hashWithSalt h [] = abs h hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs +export +Hashable a => Hashable (Maybe a) where + hashWithSalt h Nothing = abs h + hashWithSalt h (Just x) = hashWithSalt h x + export Hashable String where hashWithSalt h str = hashChars h 0 (cast (length str)) str @@ -46,47 +61,104 @@ Hashable String where export Hashable Name where hashWithSalt h (MN s _) = hashWithSalt h s + hashWithSalt h (Resolved i) = i hashWithSalt h n = hashWithSalt h (show n) -count : RigCount -> String -count Rig0 = "0" -count Rig1 = "1" -count RigW = "w" - -plicity : PiInfo -> String -plicity Implicit = "{}" -plicity Explicit = "()" -plicity AutoImplicit = "{a}" - --- I suppose this'll do for now... TODO: Write a proper one! --- Converting to a string (and indeed, however we do the hash function...) --- we need to ignore machine generated names because they'll have different --- numbers depending on implementations of functions, and that doesn't affect --- the exported interface. -hshow : Term vars -> String --- hshow (Local {x} _ _) = nameRoot x --- hshow (Ref _ n) = nameRoot n --- hshow (Bind x (Lam c p ty) sc) --- = "\\" ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc --- hshow (Bind x (Let c val ty) sc) --- = "let " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "." --- ++ hshow sc --- hshow (Bind x (Pi c p ty) sc) --- = "pi." ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc --- hshow (Bind x (PVar c ty) sc) --- = "pvar." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc --- hshow (Bind x (PLet c val ty) sc) --- = "plet " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "." --- ++ hshow sc --- hshow (Bind x (PVTy c ty) sc) --- = "pty." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc --- hshow (App f a) = "(" ++ hshow f ++ " " ++ hshow a ++ ")" --- hshow (PrimVal x) = show x --- hshow TType = "#" --- hshow Erased = "_" +export +Hashable RigCount where + hashWithSalt h Rig0 = hashWithSalt h 0 + hashWithSalt h Rig1 = hashWithSalt h 1 + hashWithSalt h RigW = hashWithSalt h 2 export -Hashable (Term vars) where - hashWithSalt h tm - = hashWithSalt h (hshow tm) +Hashable PiInfo where + hashWithSalt h Implicit = hashWithSalt h 0 + hashWithSalt h Explicit = hashWithSalt h 1 + hashWithSalt h AutoImplicit = hashWithSalt h 2 + +export +Hashable ty => Hashable (Binder ty) where + hashWithSalt h (Lam c p ty) + = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty + hashWithSalt h (Let c val ty) + = h `hashWithSalt` 1 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty + hashWithSalt h (Pi c p ty) + = h `hashWithSalt` 2 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty + hashWithSalt h (PVar c ty) + = h `hashWithSalt` 3 `hashWithSalt` c `hashWithSalt` ty + hashWithSalt h (PVTy c ty) + = h `hashWithSalt` 4 `hashWithSalt` c `hashWithSalt` ty + +Hashable (Var vars) where + hashWithSalt h (MkVar {i} _) = hashWithSalt h i + +mutual + export + Hashable (Term vars) where + hashWithSalt h (Local fc x idx y) + = h `hashWithSalt` 0 `hashWithSalt` idx + hashWithSalt h (Ref fc x name) + = h `hashWithSalt` 1 `hashWithSalt` name + hashWithSalt h (Meta fc x y xs) + = h `hashWithSalt` 2 `hashWithSalt` y `hashWithSalt` xs + hashWithSalt h (Bind fc x b scope) + = h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope + hashWithSalt h (App fc fn p arg) + = h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg + hashWithSalt h (Case fc cs ty tree alts) + = h `hashWithSalt` 5 `hashWithSalt` cs `hashWithSalt` ty + `hashWithSalt` tree `hashWithSalt` alts + hashWithSalt h (TDelayed fc x y) + = h `hashWithSalt` 6 `hashWithSalt` y + hashWithSalt h (TDelay fc x y) + = h `hashWithSalt` 7 `hashWithSalt` y + hashWithSalt h (TForce fc x) + = h `hashWithSalt` 8 `hashWithSalt` x + hashWithSalt h (PrimVal fc c) + = h `hashWithSalt` 9 `hashWithSalt` (show c) + hashWithSalt h (Erased fc) + = hashWithSalt h 10 + hashWithSalt h (TType fc) + = hashWithSalt h 11 + + export + Hashable (Pat vars) where + hashWithSalt h (PAs fc idx x y) + = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` y + hashWithSalt h (PCon fc x tag arity xs) + = h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs + hashWithSalt h (PLoc fc idx x) + = h `hashWithSalt` 2 `hashWithSalt` idx + hashWithSalt h (PUnmatchable fc x) + = h `hashWithSalt` 3 `hashWithSalt` x + + export + Hashable (PatAlt vars) where + hashWithSalt h (CBind c n ty p) + = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` n + `hashWithSalt` p + hashWithSalt h (CPats xs x) + = h `hashWithSalt` 1 `hashWithSalt` xs `hashWithSalt` x + + export + Hashable (CaseTree vars) where + hashWithSalt h (Switch idx x scTy xs) + = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs + hashWithSalt h (STerm x) + = h `hashWithSalt` 1 `hashWithSalt` x + hashWithSalt h (Unmatched msg) + = h `hashWithSalt` 2 + hashWithSalt h Impossible + = h `hashWithSalt` 3 + + export + Hashable (CaseAlt vars) where + hashWithSalt h (ConCase x tag args y) + = h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args + `hashWithSalt` y + hashWithSalt h (ConstCase x y) + = h `hashWithSalt` 1 `hashWithSalt` (show x) `hashWithSalt` y + hashWithSalt h (DefaultCase x) + = h `hashWithSalt` 2 `hashWithSalt` x + diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 9a8387a..4d2b5c5 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -41,7 +41,7 @@ TTC CG where toBuf b Chicken = tag 1 toBuf b Racket = tag 2 - fromBuf b + fromBuf r b = case !getTag of 0 => pure Chez 1 => pure Chicken diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 7a2c5af..ce80637 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -237,7 +237,7 @@ data IsVar : Name -> Nat -> List Name -> Type where public export data Var : List Name -> Type where - MkVar : {i : Nat} -> IsVar n i vars -> Var vars + MkVar : {i : Nat} -> {n : _} -> IsVar n i vars -> Var vars export sameVar : {i, j : _} -> IsVar n i xs -> IsVar m j xs -> Bool @@ -300,10 +300,12 @@ mutual public export data Pat : List Name -> Type where - PAs : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars + PAs : {name : _} -> + FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars PCon : FC -> Name -> (tag : Int) -> (arity : Nat) -> List (Pat vars) -> Pat vars - PLoc : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars + PLoc : {name : _} -> + FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars PUnmatchable : FC -> Term vars -> Pat vars public export @@ -314,7 +316,8 @@ mutual public export data CaseTree : List Name -> Type where - Switch : (idx : Nat) -> IsVar name idx vars -> + Switch : {name : _} -> + (idx : Nat) -> IsVar name idx vars -> (scTy : Term vars) -> List (CaseAlt vars) -> CaseTree vars STerm : Term vars -> CaseTree vars diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index b1f0d14..223d305 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -1,18 +1,362 @@ module Core.TTC import Core.Core +import Core.Env import Core.FC import Core.TT import Utils.Binary +%default covering + export TTC FC where - toBuf = ?tofc - fromBuf = ?fromfc + toBuf b (MkFC file startPos endPos) + = do toBuf b file; toBuf b startPos; toBuf b endPos + fromBuf r b + = do f <- fromBuf r b; s <- fromBuf r b; e <- fromBuf r b + pure (MkFC f s e) export TTC Name where - toBuf = ?toName - fromBuf = ?fromName + toBuf b (NS xs x) = do tag 0; toBuf b xs; toBuf b x + toBuf b (UN x) = do tag 1; toBuf b x + toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y + toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y + toBuf b (Nested x y) = do tag 4; toBuf b x; toBuf b y + toBuf b (Resolved x) = do tag 5; toBuf b x + + fromBuf r b + = case !getTag of + 0 => do xs <- fromBuf r b + x <- fromBuf r b + pure (NS xs x) + 1 => do x <- fromBuf r b + pure (UN x) + 2 => do x <- fromBuf r b + y <- fromBuf r b + pure (MN x y) + 3 => do x <- fromBuf r b + y <- fromBuf r b + pure (PV x y) + 4 => do x <- fromBuf r b + y <- fromBuf r b + pure (Nested x y) + 5 => do x <- fromBuf r b + Just (n, Just idx) <- coreLift $ readArray r x + | Just (n, Nothing) => pure n + | Nothing => corrupt "Name index" + pure (Resolved idx) + _ => corrupt "Name" + +export +TTC RigCount where + toBuf b Rig0 = tag 0 + toBuf b Rig1 = tag 1 + toBuf b RigW = tag 2 + + fromBuf r b + = case !getTag of + 0 => pure Rig0 + 1 => pure Rig1 + 2 => pure RigW + _ => corrupt "RigCount" + +export +TTC PiInfo where + toBuf b Implicit = tag 0 + toBuf b Explicit = tag 1 + toBuf b AutoImplicit = tag 2 + + fromBuf r b + = case !getTag of + 0 => pure Implicit + 1 => pure Explicit + 2 => pure AutoImplicit + _ => corrupt "PiInfo" + +export +TTC ty => TTC (Binder ty) where + toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty + toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val; toBuf b ty + toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty + toBuf b (PVar c ty) = do tag 3; toBuf b c; toBuf b ty + toBuf b (PVTy c ty) = do tag 4; toBuf b c; toBuf b ty + + fromBuf r b + = case !getTag of + 0 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Lam c x y) + 1 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Let c x y) + 2 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Pi c x y) + 3 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVar c x) + 4 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVTy c x) + _ => corrupt "Binder" + +export +TTC Visibility where + toBuf b Private = tag 0 + toBuf b Export = tag 1 + toBuf b Public = tag 2 + + fromBuf s b + = case !getTag of + 0 => pure Private + 1 => pure Export + 2 => pure Public + _ => corrupt "Visibility" + +export +TTC Constant where + toBuf b (I x) = do tag 0; toBuf b x + toBuf b (BI x) = do tag 1; toBuf b x + toBuf b (Str x) = do tag 2; toBuf b x + toBuf b (Ch x) = do tag 3; toBuf b x + toBuf b (Db x) = do tag 4; toBuf b x + + toBuf b WorldVal = tag 5 + toBuf b IntType = tag 6 + toBuf b IntegerType = tag 7 + toBuf b StringType = tag 8 + toBuf b CharType = tag 9 + toBuf b DoubleType = tag 10 + toBuf b WorldType = tag 11 + + fromBuf r b + = case !getTag of + 0 => do x <- fromBuf r b; pure (I x) + 1 => do x <- fromBuf r b; pure (BI x) + 2 => do x <- fromBuf r b; pure (Str x) + 3 => do x <- fromBuf r b; pure (Ch x) + 4 => do x <- fromBuf r b; pure (Db x) + 5 => pure WorldVal + 6 => pure IntType + 7 => pure IntegerType + 8 => pure StringType + 9 => pure CharType + 10 => pure DoubleType + 11 => pure WorldType + _ => corrupt "Constant" + +export +TTC LazyReason where + toBuf b LInf = tag 0 + toBuf b LLazy = tag 1 + + fromBuf r b + = case !getTag of + 0 => pure LInf + 1 => pure LLazy + _ => corrupt "LazyReason" + +export +TTC NameType where + toBuf b Bound = tag 0 + toBuf b Func = tag 1 + toBuf b (DataCon t arity) = do tag 2; toBuf b t; toBuf b arity + toBuf b (TyCon t arity) = do tag 3; toBuf b t; toBuf b arity + + fromBuf r b + = case !getTag of + 0 => pure Bound + 1 => pure Func + 2 => do x <- fromBuf r b; y <- fromBuf r b; pure (DataCon x y) + 3 => do x <- fromBuf r b; y <- fromBuf r b; pure (TyCon x y) + _ => corrupt "NameType" + +export +TTC AppInfo where + toBuf b (MkAppInfo an p) + = do toBuf b an; toBuf b p + fromBuf r b + = do an <- fromBuf r b; p <- fromBuf r b + pure (MkAppInfo an p) + +-- Assumption is that it was type safe when we wrote it out, so believe_me +-- to rebuild proofs is fine. +-- We're just making up the implicit arguments - this is only fine at run +-- time because those arguments get erased! +-- (Indeed, we're expecting the whole IsVar proof to be erased because +-- we have the idx...) +mkPrf : (idx : Nat) -> IsVar n idx ns +mkPrf {n} {ns} Z = believe_me (First {n} {ns = n :: ns}) +mkPrf {n} {ns} (S k) = believe_me (Later {m=n} (mkPrf {n} {ns} k)) + +export +TTC (Var vars) where + toBuf b (MkVar {i} {n} v) = do toBuf b n; toBuf b i + fromBuf r b + = do n <- fromBuf r b + i <- fromBuf r b + pure (MkVar {n} (mkPrf i)) + +mutual + export + TTC (Term vars) where + toBuf b (Local {name} fc c idx y) + = do tag 0; + toBuf b fc; toBuf b name + toBuf b c; toBuf b idx + toBuf b (Ref fc nt name) + = do tag 1; + toBuf b fc; toBuf b nt; toBuf b name + toBuf b (Meta fc n i xs) + = do tag 2; + toBuf b fc; toBuf b n; toBuf b i; toBuf b xs + toBuf b (Bind fc x bnd scope) + = do tag 3; + toBuf b fc; toBuf b bnd; toBuf b scope + toBuf b (App fc fn p arg) + = do tag 4; + toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg + toBuf b (Case fc cs ty tree alts) + = do tag 5; + toBuf b fc; toBuf b cs; toBuf b ty; toBuf b tree; toBuf b alts + toBuf b (TDelayed fc r tm) + = do tag 6; + toBuf b fc; toBuf b r; toBuf b tm + toBuf b (TDelay fc r tm) + = do tag 7; + toBuf b fc; toBuf b r; toBuf b tm + toBuf b (TForce fc tm) + = do tag 8; + toBuf b fc; toBuf b tm + toBuf b (PrimVal fc c) + = do tag 9; + toBuf b fc; toBuf b c + toBuf b (Erased fc) + = do tag 10; + toBuf b fc + toBuf b (TType fc) + = do tag 11; + toBuf b fc + + fromBuf r b + = case !getTag of + 0 => do fc <- fromBuf r b; name <- fromBuf r b + c <- fromBuf r b; idx <- fromBuf r b + pure (Local {name} fc c idx (mkPrf idx)) + 1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b + pure (Ref fc nt name) + 2 => do fc <- fromBuf r b; n <- fromBuf r b; i <- fromBuf r b + xs <- fromBuf r b + pure (Meta fc n i xs) + 3 => do fc <- fromBuf r b; x <- fromBuf r b + bnd <- fromBuf r b; scope <- fromBuf r b + pure (Bind fc x bnd scope) + 4 => do fc <- fromBuf r b; fn <- fromBuf r b + p <- fromBuf r b; arg <- fromBuf r b + pure (App fc fn p arg) + 5 => do fc <- fromBuf r b; cs <- fromBuf r b + ty <- fromBuf r b; tree <- fromBuf r b + alts <- fromBuf r b + pure (Case fc cs ty tree alts) + 6 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b + pure (TDelayed fc lr tm) + 7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b + pure (TDelay fc lr tm) + 8 => do fc <- fromBuf r b; tm <- fromBuf r b + pure (TForce fc tm) + 9 => do fc <- fromBuf r b; c <- fromBuf r b + pure (PrimVal fc c) + 10 => do fc <- fromBuf r b; pure (Erased fc) + 11 => do fc <- fromBuf r b; pure (TType fc) + _ => corrupt "Term" + + export + TTC (Pat vars) where + toBuf b (PAs {name} fc idx x y) + = do tag 0; toBuf b fc; toBuf b name; toBuf b idx; toBuf b y + toBuf b (PCon fc x t arity xs) + = do tag 1; toBuf b fc; toBuf b t; toBuf b arity; toBuf b xs + toBuf b (PLoc {name} fc idx x) + = do tag 2; toBuf b fc; toBuf b name; toBuf b idx + toBuf b (PUnmatchable fc x) + = do tag 3; toBuf b fc; toBuf b x + + fromBuf r b + = case !getTag of + 0 => do fc <- fromBuf r b; name <- fromBuf r b; + idx <- fromBuf r b; y <- fromBuf r b + pure (PAs {name} fc idx (mkPrf idx) y) + 1 => do fc <- fromBuf r b; x <- fromBuf r b + t <- fromBuf r b; arity <- fromBuf r b + xs <- fromBuf r b + pure (PCon fc x t arity xs) + 2 => do fc <- fromBuf r b; name <- fromBuf r b + idx <- fromBuf r b + pure (PLoc {name} fc idx (mkPrf idx)) + 3 => do fc <- fromBuf r b; x <- fromBuf r b + pure (PUnmatchable fc x) + _ => corrupt "Pat" + + export + TTC (PatAlt vars) where + toBuf b (CBind c x ty alt) + = do tag 0; toBuf b c; toBuf b x; toBuf b ty; toBuf b alt + toBuf b (CPats xs tm) + = do tag 1; toBuf b xs; toBuf b tm + + fromBuf r b + = case !getTag of + 0 => do c <- fromBuf r b; x <- fromBuf r b + ty <- fromBuf r b; alt <- fromBuf r b + pure (CBind c x ty alt) + 1 => do xs <- fromBuf r b; tm <- fromBuf r b + pure (CPats xs tm) + _ => corrupt "PatAlt" + + export + TTC (CaseTree vars) where + toBuf b (Switch {name} idx x scTy xs) + = do tag 0; toBuf b name; toBuf b idx; toBuf b scTy; toBuf b xs + toBuf b (STerm x) + = do tag 1; toBuf b x + toBuf b (Unmatched msg) + = do tag 2; toBuf b msg + toBuf b Impossible = tag 3 + + fromBuf r b + = case !getTag of + 0 => do name <- fromBuf r b; idx <- fromBuf r b + scTy <- fromBuf r b; xs <- fromBuf r b + pure (Switch {name} idx (mkPrf idx) scTy xs) + 1 => do x <- fromBuf r b + pure (STerm x) + 2 => do msg <- fromBuf r b + pure (Unmatched msg) + 3 => pure Impossible + _ => corrupt "CaseTree" + + export + TTC (CaseAlt vars) where + toBuf b (ConCase x t args y) + = do tag 0; toBuf b x; toBuf b t; toBuf b args; toBuf b y + toBuf b (ConstCase x y) + = do tag 1; toBuf b x; toBuf b y + toBuf b (DefaultCase x) + = do tag 2; toBuf b x + + fromBuf r b + = case !getTag of + 0 => do x <- fromBuf r b; t <- fromBuf r b + args <- fromBuf r b; y <- fromBuf r b + pure (ConCase x t args y) + 1 => do x <- fromBuf r b; y <- fromBuf r b + pure (ConstCase x y) + 2 => do x <- fromBuf r b + pure (DefaultCase x) + _ => corrupt "CaseAlt" + +export +TTC (Env Term vars) where + toBuf b [] = pure () + toBuf b ((::) bnd env) + = do toBuf b bnd; toBuf b env + + -- Length has to correspond to length of 'vars' + fromBuf s {vars = []} b = pure Nil + fromBuf s {vars = x :: xs} b + = do bnd <- fromBuf s b + env <- fromBuf s b + pure (bnd :: env) diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index a2a7e90..d6e02d6 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -16,14 +16,16 @@ public export data Constraint : Type where -- An unsolved constraint, noting two terms which need to be convertible -- in a particular environment - MkConstraint : FC -> + MkConstraint : {vars : _} -> + FC -> (env : Env Term vars) -> (x : Term vars) -> (y : Term vars) -> Constraint -- An unsolved sequence of constraints, arising from arguments in an -- application where solving later constraints relies on solving earlier -- ones - MkSeqConstraint : FC -> + MkSeqConstraint : {vars : _} -> + FC -> (env : Env Term vars) -> (xs : List (Term vars)) -> (ys : List (Term vars)) -> @@ -33,8 +35,24 @@ data Constraint : Type where export TTC Constraint where - toBuf = ?toconstraint - fromBuf = ?fromconstraint + toBuf b (MkConstraint {vars} fc env x y) + = do tag 0; toBuf b vars; toBuf b fc; toBuf b env; toBuf b x; toBuf b y + toBuf b (MkSeqConstraint {vars} fc env xs ys) + = do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys + toBuf b Resolved = tag 2 + + fromBuf r b + = case !getTag of + 0 => do vars <- fromBuf r b + fc <- fromBuf r b; env <- fromBuf r b + x <- fromBuf r b; y <- fromBuf r b + pure (MkConstraint {vars} fc env x y) + 1 => do vars <- fromBuf r b + fc <- fromBuf r b; env <- fromBuf r b + xs <- fromBuf r b; ys <- fromBuf r b + pure (MkSeqConstraint {vars} fc env xs ys) + 2 => pure Resolved + _ => corrupt "Constraint" public export record UState where @@ -157,7 +175,7 @@ newMeta : {auto c : Ref Ctxt Defs} -> Env Term vars -> Name -> Term vars -> Core (Term vars) newMeta {vars} fc rig env n ty = do let hty = abstractEnvType fc env ty - let hole = newDef fc rig hty Public (Hole False) + let hole = newDef fc n rig hty Public (Hole False) idx <- addDef n hole addHoleName fc n idx pure (Meta fc n idx envArgs) @@ -187,8 +205,8 @@ newConstant : {auto u : Ref UST UState} -> newConstant fc rig env tm ty constrs = do let def = mkConstant fc env tm let defty = abstractEnvType fc env ty - let guess = newDef fc rig defty Public (Guess def constrs) cn <- genName "p" + let guess = newDef fc cn rig defty Public (Guess def constrs) idx <- addDef cn guess addGuessName fc cn idx pure (applyTo fc (Ref fc Func (Resolved idx)) env) diff --git a/src/Data/IOArray.idr b/src/Data/IOArray.idr index d12c25c..96d5a28 100644 --- a/src/Data/IOArray.idr +++ b/src/Data/IOArray.idr @@ -94,3 +94,29 @@ newArrayCopy newsize arr unsafeWriteArray new pos el assert_total (copyFrom old new (pos - 1)) +export +toList : IOArray elem -> IO (List (Maybe elem)) +toList arr = iter 0 (max arr) [] + where + iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem)) + iter pos end acc + = if pos >= end + then pure (reverse acc) + else do el <- readArray arr pos + assert_total (iter (pos + 1) end (el :: acc)) + +export +fromList : List (Maybe elem) -> IO (IOArray elem) +fromList ns + = do arr <- newArray (cast (length ns)) + addToArray 0 ns arr + pure arr + where + addToArray : Int -> List (Maybe elem) -> IOArray elem -> IO () + addToArray loc [] arr = pure () + addToArray loc (Nothing :: ns) arr + = assert_total (addToArray (loc + 1) ns arr) + addToArray loc (Just el :: ns) arr + = do unsafeWriteArray (content arr) loc (Just el) + assert_total (addToArray (loc + 1) ns arr) + diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 4be18a4..9970872 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -76,7 +76,7 @@ processData env fc vis (MkImpLater dfc n_in ty_raw) -- Add the type constructor as a placeholder while checking -- data constructors - tidx <- addDef n (newDef fc Rig1 fullty vis + tidx <- addDef n (newDef fc n Rig1 fullty vis (TCon 0 arity [] [] [])) pure () processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw) @@ -105,7 +105,7 @@ processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw) -- Add the type constructor as a placeholder while checking -- data constructors - tidx <- addDef n (newDef fc Rig1 fullty vis + tidx <- addDef n (newDef fc n Rig1 fullty vis (TCon 0 arity [] [] [])) -- Constructors are private if the data type as a whole is diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 432a870..d3367d6 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -26,7 +26,7 @@ processType env fc rig vis opts (MkImpTy tfc n_in ty_raw) -- TODO: Check name visibility let def = None -- TODO: External definitions - addDef n (newDef fc rig (abstractEnvType tfc env ty) vis def) + addDef n (newDef fc n rig (abstractEnvType tfc env ty) vis def) -- TODO: Interface hash and saving pure () diff --git a/src/Utils/Binary.idr b/src/Utils/Binary.idr index 88b4fbf..a262f39 100644 --- a/src/Utils/Binary.idr +++ b/src/Utils/Binary.idr @@ -1,10 +1,14 @@ module Utils.Binary import Core.Core +import Core.Name + import Data.Buffer +import public Data.IOArray import Data.List import Data.Vect + -- Serialising data as binary. Provides an interface TTC which allows -- reading and writing to chunks of memory, "Binary", which can be written -- to and read from files. @@ -15,9 +19,9 @@ import Data.Vect export data Bin : Type where --- A label for storing shared strings +-- A label for storing resolved name ids export -data Share : Type where +data ResID : Type where -- A component of the serialised data. record Chunk where @@ -122,13 +126,23 @@ readFromFile fname b <- readBufferFromFile h b max pure (Right (MkBin [] (MkChunk b 0 max max) [])) +-- A mapping from the resolved name ids encountered in a TTC file to the +-- name they represent, and (if known) the new resolved id it'll be after +-- reading +-- (We need this because files will be used in different contexts and resolved +-- name ids are not going to be unique, so we need to recalculate them when +-- loading from TTC) +public export +NameRefs : Type +NameRefs = IOArray (Name, Maybe Int) + public export interface TTC a where -- TTC = TT intermediate code/interface file -- Add binary data representing the value to the given buffer toBuf : Ref Bin Binary -> a -> Core () -- Return the data representing a thing of type 'a' from the given buffer. -- Throws if the data can't be parsed as an 'a' - fromBuf : Ref Bin Binary -> Core a + fromBuf : NameRefs -> Ref Bin Binary -> Core a -- Create a new list of chunks, initialised with one 64k chunk export @@ -138,6 +152,11 @@ initBinary | Nothing => throw (InternalError "Buffer creation failed") newRef Bin (MkBin [] (newChunk buf) []) +export +initNameRefs : Int -> Core NameRefs +initNameRefs num + = coreLift $ newArray num + export corrupt : String -> Core a corrupt ty = throw (TTCError (Corrupt ty)) @@ -161,7 +180,7 @@ TTC Bits8 where (MkChunk newbuf 1 (size newbuf) 1) rest) - fromBuf b + fromBuf s b = do MkBin done chunk rest <- get Bin if toRead chunk >= 1 then @@ -181,8 +200,9 @@ tag : {auto b : Ref Bin Binary} -> Bits8 -> Core () tag {b} val = toBuf b val export -getTag : {auto b : Ref Bin Binary} -> Core Bits8 -getTag {b} = fromBuf b +getTag : {auto r : NameRefs} -> + {auto b : Ref Bin Binary} -> Core Bits8 +getTag {r} {b} = fromBuf r b -- Some useful types from the prelude @@ -201,7 +221,7 @@ TTC Int where put Bin (MkBin (chunk :: done) (MkChunk newbuf 4 (size newbuf) 4) rest) - fromBuf b + fromBuf r b = do MkBin done chunk rest <- get Bin if toRead chunk >= 4 then @@ -234,8 +254,8 @@ TTC String where (MkChunk newbuf req (size newbuf) req) rest) - fromBuf b - = do len <- fromBuf {a = Int} b + fromBuf r b + = do len <- fromBuf {a = Int} r b MkBin done chunk rest <- get Bin if toRead chunk >= len then @@ -255,7 +275,7 @@ export TTC Bool where toBuf b False = tag 0 toBuf b True = tag 1 - fromBuf b + fromBuf r b = case !getTag of 0 => pure False 1 => pure True @@ -264,8 +284,8 @@ TTC Bool where export TTC Char where toBuf b c = toBuf b (cast {to=Int} c) - fromBuf b - = do i <- fromBuf b + fromBuf r b + = do i <- fromBuf r b pure (cast {from=Int} i) export @@ -283,7 +303,7 @@ TTC Double where put Bin (MkBin (chunk :: done) (MkChunk newbuf 8 (size newbuf) 8) rest) - fromBuf b + fromBuf r b = do MkBin done chunk rest <- get Bin if toRead chunk >= 8 then @@ -303,15 +323,15 @@ export toBuf b (x, y) = do toBuf b x toBuf b y - fromBuf b - = do x <- fromBuf b - y <- fromBuf b + fromBuf r b + = do x <- fromBuf r b + y <- fromBuf r b pure (x, y) export TTC () where toBuf b () = pure () - fromBuf b = pure () + fromBuf r b = pure () export (TTC a, {y : a} -> TTC (p y)) => TTC (DPair a p) where @@ -319,9 +339,9 @@ export = do toBuf b vs toBuf b tm - fromBuf b - = do x <- fromBuf b - p <- fromBuf b + fromBuf r b + = do x <- fromBuf r b + p <- fromBuf r b pure (x ** p) export @@ -332,10 +352,10 @@ TTC a => TTC (Maybe a) where = do tag 1 toBuf b val - fromBuf b + fromBuf r b = case !getTag of 0 => pure Nothing - 1 => do val <- fromBuf b + 1 => do val <- fromBuf r b pure (Just val) _ => corrupt "Maybe" @@ -348,11 +368,11 @@ export = do tag 1 toBuf b val - fromBuf b + fromBuf r b = case !getTag of - 0 => do val <- fromBuf b + 0 => do val <- fromBuf r b pure (Left val) - 1 => do val <- fromBuf b + 1 => do val <- fromBuf r b pure (Right val) _ => corrupt "Either" @@ -362,14 +382,14 @@ TTC a => TTC (List a) where = do toBuf b (cast {to=Int} (length xs)) traverse (toBuf b) xs pure () - fromBuf b - = do len <- fromBuf b {a = Int} + fromBuf r b + = do len <- fromBuf r b {a = Int} readElems [] (cast len) where readElems : List a -> Nat -> Core (List a) readElems xs Z = pure (reverse xs) readElems xs (S k) - = do val <- fromBuf b + = do val <- fromBuf r b readElems (val :: xs) k export @@ -380,13 +400,13 @@ TTC a => TTC (Vect n a) where writeAll [] = pure () writeAll (x :: xs) = do toBuf b x; writeAll xs - fromBuf {n} b = rewrite sym (plusZeroRightNeutral n) in readElems [] n + fromBuf {n} r b = rewrite sym (plusZeroRightNeutral n) in readElems [] n where readElems : Vect done a -> (todo : Nat) -> Core (Vect (todo + done) a) readElems {done} xs Z = pure (reverse xs) readElems {done} xs (S k) - = do val <- fromBuf b + = do val <- fromBuf r b rewrite (plusSuccRightSucc k done) readElems (val :: xs) k @@ -414,18 +434,18 @@ TTC Integer where toBuf b (toLimbs (-val)) else do toBuf b (the Bits8 1) toBuf b (toLimbs val) - fromBuf b - = do val <- fromBuf b {a = Bits8} + fromBuf r b + = do val <- fromBuf r b {a = Bits8} case val of - 0 => do val <- fromBuf b + 0 => do val <- fromBuf r b pure (-(fromLimbs val)) - 1 => do val <- fromBuf b + 1 => do val <- fromBuf r b pure (fromLimbs val) _ => corrupt "Integer" export TTC Nat where toBuf b val = toBuf b (cast {to=Integer} val) - fromBuf b - = do val <- fromBuf b + fromBuf r b + = do val <- fromBuf r b pure (fromInteger val)