mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-30 12:14:17 +03:00
The Prelude type checks!
This commit is contained in:
Edwin Brady
parent
2374f23320
commit
772b098de0
89
libs/prelude/Builtin.idr
Normal file
89
libs/prelude/Builtin.idr
Normal file
@ -0,0 +1,89 @@
|
||||
module Builtin
|
||||
|
||||
-- The most primitive data types; things which are used by desugaring
|
||||
|
||||
-- Totality assertions
|
||||
|
||||
%inline
|
||||
public export
|
||||
assert_total : {0 a : _} -> a -> a
|
||||
assert_total x = x
|
||||
|
||||
%inline
|
||||
public export
|
||||
assert_smaller : {0 a, b : _} -> (x : a) -> (y : b) -> b
|
||||
assert_smaller x y = y
|
||||
|
||||
-- Unit type and pairs
|
||||
|
||||
public export
|
||||
data Unit = MkUnit
|
||||
|
||||
public export
|
||||
data Pair : Type -> Type -> Type where
|
||||
MkPair : {0 a, b : Type} -> (1 x : a) -> (1 y : b) -> Pair a b
|
||||
|
||||
public export
|
||||
fst : {0 a, b : Type} -> (a, b) -> a
|
||||
fst (x, y) = x
|
||||
|
||||
public export
|
||||
snd : {0 a, b : Type} -> (a, b) -> b
|
||||
snd (x, y) = y
|
||||
|
||||
-- This directive tells auto implicit search what to use to look inside pairs
|
||||
%pair Pair fst snd
|
||||
|
||||
namespace DPair
|
||||
public export
|
||||
data DPair : (a : Type) -> (a -> Type) -> Type where
|
||||
MkDPair : {0 a : Type} -> {0 p : a -> Type} ->
|
||||
(1 x : a) -> (1 y : p x)-> DPair a p
|
||||
|
||||
public export
|
||||
fst : DPair a p -> a
|
||||
fst (MkDPair x y) = x
|
||||
|
||||
public export
|
||||
snd : (x : DPair a p) -> p (fst x)
|
||||
snd (MkDPair x y) = y
|
||||
|
||||
-- The empty type
|
||||
|
||||
public export
|
||||
data Void : Type where
|
||||
|
||||
-- Equality
|
||||
|
||||
public export
|
||||
data Equal : forall a, b . a -> b -> Type where
|
||||
Refl : {0 x : a} -> Equal x x
|
||||
|
||||
%name Equal prf
|
||||
|
||||
%inline
|
||||
public export
|
||||
rewrite__impl : {0 x, y : a} -> (0 p : _) ->
|
||||
(0 rule : x = y) -> (1 val : p y) -> p x
|
||||
rewrite__impl p Refl prf = prf
|
||||
|
||||
%rewrite Equal rewrite__impl
|
||||
|
||||
%inline
|
||||
public export
|
||||
replace : forall x, y, p . (0 rule : x = y) -> p x -> p y
|
||||
replace Refl prf = prf
|
||||
|
||||
%inline
|
||||
public export
|
||||
sym : (0 rule : x = y) -> y = x
|
||||
sym Refl = Refl
|
||||
|
||||
%inline
|
||||
public export
|
||||
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
|
||||
trans Refl Refl = Refl
|
||||
|
||||
public export
|
||||
believe_me : a -> b
|
||||
believe_me = prim__believe_me _ _
|
||||
1156
libs/prelude/Prelude.idr
Normal file
1156
libs/prelude/Prelude.idr
Normal file
File diff suppressed because it is too large
Load Diff
81
libs/prelude/PrimIO.idr
Normal file
81
libs/prelude/PrimIO.idr
Normal file
@ -0,0 +1,81 @@
|
||||
module PrimIO
|
||||
|
||||
import Builtin
|
||||
|
||||
public export
|
||||
data IORes : Type -> Type where
|
||||
MkIORes : (result : a) -> (1 x : %World) -> IORes a
|
||||
|
||||
export
|
||||
data IO : Type -> Type where
|
||||
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
|
||||
|
||||
export
|
||||
io_pure : a -> IO a
|
||||
io_pure x = MkIO (\w => MkIORes x w)
|
||||
|
||||
export
|
||||
io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
|
||||
io_bind (MkIO fn)
|
||||
= \k => MkIO (\w => let MkIORes x' w' = fn w
|
||||
MkIO res = k x' in
|
||||
res w')
|
||||
|
||||
%extern prim__putStr : String -> (1 x : %World) -> IORes ()
|
||||
%extern prim__getStr : (1 x : %World) -> IORes String
|
||||
|
||||
public export
|
||||
data Ptr : Type where
|
||||
|
||||
public export
|
||||
data ThreadID : Type where
|
||||
|
||||
public export
|
||||
data FArgList : Type where
|
||||
Nil : FArgList
|
||||
(::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList
|
||||
|
||||
%extern prim__cCall : (ret : Type) -> String -> (1 args : FArgList) ->
|
||||
(1 x : %World) -> IORes ret
|
||||
%extern prim__schemeCall : (ret : Type) -> String -> (1 args : FArgList) ->
|
||||
(1 x : %World) -> IORes ret
|
||||
|
||||
export %inline
|
||||
primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
|
||||
primIO op = MkIO op
|
||||
|
||||
export %inline
|
||||
schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> IO ret
|
||||
schemeCall ret fn args = primIO (prim__schemeCall ret fn args)
|
||||
|
||||
export %inline
|
||||
cCall : (ret : Type) -> String -> FArgList -> IO ret
|
||||
cCall ret fn args = primIO (prim__cCall ret fn args)
|
||||
|
||||
export
|
||||
putStr : String -> IO ()
|
||||
putStr str = primIO (prim__putStr str)
|
||||
|
||||
export
|
||||
putStrLn : String -> IO ()
|
||||
putStrLn str = putStr (prim__strAppend str "\n")
|
||||
|
||||
export
|
||||
getLine : IO String
|
||||
getLine = primIO prim__getStr
|
||||
|
||||
export
|
||||
fork : (1 prog : IO ()) -> IO ThreadID
|
||||
fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act]
|
||||
|
||||
unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
|
||||
unsafeCreateWorld f = f %MkWorld
|
||||
|
||||
unsafeDestroyWorld : (1 x : %World) -> a -> a
|
||||
unsafeDestroyWorld %MkWorld x = x
|
||||
|
||||
export
|
||||
unsafePerformIO : IO a -> a
|
||||
unsafePerformIO (MkIO f)
|
||||
= unsafeCreateWorld (\w => case f w of
|
||||
MkIORes res w' => unsafeDestroyWorld w' res)
|
||||
@ -353,6 +353,29 @@ concreteDets {vars} fc defaults env top pos dets ((p, arg) :: args)
|
||||
= throw (CantSolveGoal fc [] top)
|
||||
concrete defs tm top = pure ()
|
||||
|
||||
checkConcreteDets : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> Bool ->
|
||||
Env Term vars -> (top : ClosedTerm) ->
|
||||
NF vars ->
|
||||
Core ()
|
||||
checkConcreteDets fc defaults env top (NTCon tfc tyn t a args)
|
||||
= do defs <- get Ctxt
|
||||
if isPairType tyn defs
|
||||
then case args of
|
||||
[(_, aty), (_, bty)] =>
|
||||
do anf <- evalClosure defs aty
|
||||
bnf <- evalClosure defs bty
|
||||
checkConcreteDets fc defaults env top anf
|
||||
checkConcreteDets fc defaults env top bnf
|
||||
_ => do sd <- getSearchData fc defaults tyn
|
||||
concreteDets fc defaults env top 0 (detArgs sd) args
|
||||
else
|
||||
do sd <- getSearchData fc defaults tyn
|
||||
concreteDets fc defaults env top 0 (detArgs sd) args
|
||||
checkConcreteDets fc defaults env top _
|
||||
= pure ()
|
||||
|
||||
-- Declared at the top
|
||||
searchType fc rigc defaults depth def top env (Bind nfc x (Pi c p ty) sc)
|
||||
= pure (Bind nfc x (Lam c p ty)
|
||||
@ -371,7 +394,8 @@ searchType {vars} fc rigc defaults depth def top env target
|
||||
then do logNF 10 "Next target: " env nty
|
||||
sd <- getSearchData fc defaults tyn
|
||||
-- Check determining arguments are okay for 'args'
|
||||
concreteDets fc defaults env top 0 (detArgs sd) args
|
||||
checkConcreteDets fc defaults env top
|
||||
(NTCon tfc tyn t a args)
|
||||
tryUnify
|
||||
(searchLocal fc rigc defaults depth def top env nty)
|
||||
(tryGroups nty (hintGroups sd))
|
||||
|
||||
@ -229,12 +229,36 @@ addGlobalDef modns as def
|
||||
|
||||
addTypeHint : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> (Name, Name, Bool) -> Core ()
|
||||
addTypeHint fc (tyn, hintn, d) = addHintFor fc tyn hintn d True
|
||||
addTypeHint fc (tyn, hintn, d)
|
||||
= do logC 10 (pure (show !(getFullName hintn) ++ " for " ++
|
||||
show !(getFullName tyn)))
|
||||
addHintFor fc tyn hintn d True
|
||||
|
||||
addAutoHint : {auto c : Ref Ctxt Defs} ->
|
||||
(Name, Bool) -> Core ()
|
||||
addAutoHint (hintn, d) = addGlobalHint hintn d
|
||||
|
||||
export
|
||||
updatePair : {auto c : Ref Ctxt Defs} ->
|
||||
Maybe PairNames -> Core ()
|
||||
updatePair p
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->pairnames $= (p <+>) } defs)
|
||||
|
||||
export
|
||||
updateRewrite : {auto c : Ref Ctxt Defs} ->
|
||||
Maybe RewriteNames -> Core ()
|
||||
updateRewrite r
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->rewritenames $= (r <+>) } defs)
|
||||
|
||||
export
|
||||
updatePrims : {auto c : Ref Ctxt Defs} ->
|
||||
PrimNames -> Core ()
|
||||
updatePrims p
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->primnames = p } defs)
|
||||
|
||||
-- Add definitions from a binary file to the current context
|
||||
-- Returns the "extra" section of the file (user defined data), the interface
|
||||
-- hash and the list of additional TTCs that need importing
|
||||
@ -272,8 +296,14 @@ readFromTTC loc reexp fname modNS importAs
|
||||
setNS (currentNS ttc)
|
||||
-- Set up typeHints and autoHints based on the loaded data
|
||||
traverse_ (addTypeHint loc) (typeHints ttc)
|
||||
defs <- get Ctxt
|
||||
traverse_ addAutoHint (autoHints ttc)
|
||||
-- TODO: Set up pair/rewrite etc names, name directives
|
||||
-- Set up pair/rewrite etc names
|
||||
updatePair (pairnames ttc)
|
||||
updateRewrite (rewritenames ttc)
|
||||
updatePrims (primnames ttc)
|
||||
-- TODO: Name directives
|
||||
|
||||
when (not reexp) clearSavedHints
|
||||
resetFirstEntry
|
||||
|
||||
|
||||
@ -1025,11 +1025,14 @@ addHintFor fc tyn hintn_in direct loading
|
||||
let hs = case lookup tyn (typeHints defs) of
|
||||
Just hs => hs
|
||||
Nothing => []
|
||||
let defs' = record { typeHints $= insert tyn ((hintn, direct) :: hs) }
|
||||
defs
|
||||
when True $ -- (not loading) $
|
||||
put Ctxt (record { saveTypeHints $= ((tyn, hintn, direct) :: )
|
||||
} defs')
|
||||
if loading
|
||||
then put Ctxt
|
||||
(record { typeHints $= insert tyn ((hintn, direct) :: hs)
|
||||
} defs)
|
||||
else put Ctxt
|
||||
(record { typeHints $= insert tyn ((hintn, direct) :: hs),
|
||||
saveTypeHints $= ((tyn, hintn, direct) :: )
|
||||
} defs)
|
||||
|
||||
export
|
||||
addGlobalHint : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -289,7 +289,7 @@ mutual
|
||||
glueBack defs env sc',
|
||||
fused ++ aused)
|
||||
_ => do tfty <- getTerm gfty
|
||||
throw (InternalError ("Linearity checking failed on " ++ show f' ++
|
||||
throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
|
||||
" (" ++ show tfty ++ " not a function type)"))
|
||||
|
||||
lcheck rig erase env (As fc as pat)
|
||||
@ -529,13 +529,15 @@ mutual
|
||||
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
|
||||
if linearChecked def
|
||||
then pure (type def)
|
||||
else case definition def of
|
||||
else do case definition def of
|
||||
PMDef _ _ _ pats =>
|
||||
do u <- getArgUsage (getLoc (type def))
|
||||
rig (type def) pats
|
||||
let ty' = updateUsage u (type def)
|
||||
updateTy idx ty'
|
||||
setLinearCheck idx True
|
||||
logTerm 5 ("New type of " ++
|
||||
show (fullname def)) ty'
|
||||
pure ty'
|
||||
_ => pure (type def)
|
||||
where
|
||||
@ -565,9 +567,9 @@ mutual
|
||||
substMeta (Bind bfc n (Lam c e ty) sc) (a :: as) env
|
||||
= substMeta sc as (a :: env)
|
||||
substMeta rhs [] env = pure (substs env rhs)
|
||||
substMeta _ _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n))
|
||||
expandMeta rig erase env n idx _ _
|
||||
= throw (InternalError ("Badly formed metavar solution " ++ show n))
|
||||
substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show rhs))
|
||||
expandMeta rig erase env n idx def _
|
||||
= throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def))
|
||||
|
||||
lcheckMeta : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
@ -590,7 +592,7 @@ mutual
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
ty <- quote empty env nty
|
||||
throw (InternalError ("Linearity checking failed on metavar
|
||||
throw (GenericMsg fc ("Linearity checking failed on metavar
|
||||
" ++ show n ++ " (" ++ show ty ++
|
||||
" not a function type)"))
|
||||
lcheckMeta rig erase env fc n idx [] chk nty
|
||||
|
||||
@ -105,9 +105,10 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
= pure (NDelay fc r (MkClosure topopts locs env ty)
|
||||
(MkClosure topopts locs env tm))
|
||||
eval env locs (TForce fc tm) stk
|
||||
= do tm' <- eval env locs tm stk
|
||||
= do tm' <- eval env locs tm []
|
||||
case tm' of
|
||||
NDelay fc r _ arg => evalClosure defs arg
|
||||
NDelay fc r _ arg =>
|
||||
eval env (arg :: locs) (Local {name = UN "fvar"} fc Nothing _ First) stk
|
||||
_ => pure (NForce fc tm')
|
||||
eval env locs (PrimVal fc c) stk = pure $ NPrimVal fc c
|
||||
eval env locs (Erased fc) stk = pure $ NErased fc
|
||||
|
||||
@ -160,7 +160,7 @@ defaultPPrint : PPrinter
|
||||
defaultPPrint = MkPPOpts False True False
|
||||
|
||||
defaultSession : Session
|
||||
defaultSession = MkSessionOpts True Chez 0 False
|
||||
defaultSession = MkSessionOpts False Chez 0 False
|
||||
|
||||
defaultElab : ElabDirectives
|
||||
defaultElab = MkElabDirectives True True
|
||||
|
||||
@ -650,6 +650,10 @@ Weaken Term where
|
||||
weaken tm = thin {outer = []} _ tm
|
||||
weakenNs ns tm = insertNames {outer = []} ns tm
|
||||
|
||||
export
|
||||
Weaken Var where
|
||||
weaken (MkVar p) = MkVar (Later p)
|
||||
|
||||
export
|
||||
varExtend : IsVar x idx xs -> IsVar x idx (xs ++ ys)
|
||||
-- What Could Possibly Go Wrong?
|
||||
|
||||
@ -259,7 +259,7 @@ mutual
|
||||
Just (n, Just idx) <- coreLift $ readArray r x
|
||||
| Just (n, Nothing) =>
|
||||
corrupt ("Metavar name index " ++ show x)
|
||||
| Nothing => corrupt ("Metavar name index " ++ show x)
|
||||
| Nothing => corrupt ("Metavar name index " ++ show x ++ " (not in array)")
|
||||
xs <- fromBuf r b
|
||||
pure (Meta fc (UN "metavar") idx xs)
|
||||
3 => do fc <- fromBuf r b; x <- fromBuf r b
|
||||
|
||||
@ -32,6 +32,12 @@ Eq UnifyMode where
|
||||
public export
|
||||
data AddLazy = NoLazy | AddForce | AddDelay LazyReason
|
||||
|
||||
export
|
||||
Show AddLazy where
|
||||
show NoLazy = "NoLazy"
|
||||
show AddForce = "AddForce"
|
||||
show (AddDelay _) = "AddDelay"
|
||||
|
||||
public export
|
||||
record UnifyResult where
|
||||
constructor MkUnifyResult
|
||||
@ -301,8 +307,8 @@ instantiate : {auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
instantiate {newvars} loc env mname mref mdef locs otm tm
|
||||
= do log 5 $ "Instantiating " ++ show tm ++ " in " ++ show newvars
|
||||
let Hole _ _ = definition mdef
|
||||
| def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
|
||||
-- let Hole _ _ = definition mdef
|
||||
-- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
|
||||
case fullname mdef of
|
||||
PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm)
|
||||
_ => pure ()
|
||||
@ -512,15 +518,16 @@ mutual
|
||||
{vars : _} ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
(metaname : Name) -> (metaref : Int) ->
|
||||
(args : List (AppInfo, Closure vars)) ->
|
||||
(margs : List (AppInfo, Closure vars)) ->
|
||||
(margs' : List (AppInfo, Closure vars)) ->
|
||||
(soln : NF vars) ->
|
||||
Core UnifyResult
|
||||
-- TODO: if either side is a pattern variable application, and we're in a term,
|
||||
-- (which will be a type) we can proceed because the pattern variable
|
||||
-- has to end up pi bound. Unify the right most variables, and continue.
|
||||
unifyPatVar mode loc env mname mref args tm
|
||||
unifyPatVar mode loc env mname mref margs margs' tm
|
||||
= postpone loc "Not in pattern fragment" env
|
||||
(NApp loc (NMeta mname mref args) []) tm
|
||||
(NApp loc (NMeta mname mref margs) margs') tm
|
||||
|
||||
solveHole : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
@ -580,10 +587,10 @@ mutual
|
||||
case !(patternEnv env args) of
|
||||
Nothing =>
|
||||
do Just (Hole _ inv) <- lookupDefExact (Resolved mref) (gamma defs)
|
||||
| _ => unifyPatVar mode loc env mname mref args tmnf
|
||||
| _ => unifyPatVar mode loc env mname mref margs margs' tmnf
|
||||
if inv
|
||||
then unifyHoleApp mode loc env mname mref margs margs' tmnf
|
||||
else unifyPatVar mode loc env mname mref args tmnf
|
||||
else unifyPatVar mode loc env mname mref margs margs' tmnf
|
||||
Just (newvars ** (locs, submv)) =>
|
||||
do tm <- quote empty env tmnf
|
||||
case shrinkTerm tm submv of
|
||||
@ -931,7 +938,7 @@ mutual
|
||||
unifyD _ _ mode loc env x y
|
||||
= do defs <- get Ctxt
|
||||
if x == y
|
||||
then do log 10 $ "S§kipped unification (equal already): "
|
||||
then do log 10 $ "Skipped unification (equal already): "
|
||||
++ show x ++ " and " ++ show y
|
||||
pure success
|
||||
else unify mode loc env !(nf defs env x) !(nf defs env y)
|
||||
@ -946,11 +953,8 @@ mutual
|
||||
export
|
||||
Unify Closure where
|
||||
unifyD _ _ mode loc env x y
|
||||
= do gam <- get Ctxt
|
||||
empty <- clearDefs gam
|
||||
-- 'quote' using an empty global context, because then function
|
||||
-- names won't reduce until they have to
|
||||
unify mode loc env !(quote empty env x) !(quote empty env y)
|
||||
= do defs <- get Ctxt
|
||||
unify mode loc env !(evalClosure defs x) !(evalClosure defs y)
|
||||
|
||||
export
|
||||
setInvertible : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -47,6 +47,7 @@ data CLOpt
|
||||
IdeModeSocket |
|
||||
||| Run as a checker for the core language TTImp
|
||||
Yaffle String |
|
||||
Timing |
|
||||
BlodwenPaths
|
||||
|
||||
|
||||
@ -95,7 +96,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
|
||||
MkOpt ["--help", "-h", "-?"] [] [Help]
|
||||
(Just "Display help text"),
|
||||
MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
|
||||
Nothing
|
||||
Nothing,
|
||||
MkOpt ["--timing"] [] [Timing]
|
||||
(Just "Display timing logs")
|
||||
]
|
||||
|
||||
optUsage : OptDesc -> String
|
||||
|
||||
@ -293,7 +293,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
|
||||
(FC, List FnOpt, Name, List ImpClause) ->
|
||||
Core (Name, List ImpClause)
|
||||
elabDefault tydecls (fc, opts, n, cs)
|
||||
= do orig <- branch
|
||||
= do -- orig <- branch
|
||||
let dn_in = UN ("Default implementation of " ++ show n)
|
||||
dn <- inCurrentNS dn_in
|
||||
|
||||
@ -310,7 +310,8 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
|
||||
let cs' = map (changeName dn) cs
|
||||
processDecl [] nest env (IDef fc dn cs')
|
||||
-- Reset the original context, we don't need to keep the definition
|
||||
put Ctxt orig
|
||||
-- Actually we do for the metadata and name map!
|
||||
-- put Ctxt orig
|
||||
pure (n, cs)
|
||||
where
|
||||
changeNameTerm : Name -> RawImp -> RawImp
|
||||
|
||||
@ -18,6 +18,8 @@ import Idris.REPLCommon
|
||||
import Idris.REPLOpts
|
||||
import Idris.Syntax
|
||||
|
||||
import Data.NameMap
|
||||
|
||||
import Control.Catchable
|
||||
|
||||
processDecl : {auto c : Ref Ctxt Defs} ->
|
||||
@ -204,7 +206,7 @@ processMod srcf ttcf msg mod sourcecode
|
||||
-- a phase before this which builds the dependency graph
|
||||
-- (also that we only build child dependencies if rebuilding
|
||||
-- changes the interface - will need to store a hash in .ttc!)
|
||||
traverse readImport imps
|
||||
traverse_ readImport imps
|
||||
|
||||
-- Before we process the source, make sure the "hide_everywhere"
|
||||
-- names are set to private (TODO, maybe if we want this?)
|
||||
@ -228,7 +230,9 @@ process : {auto c : Ref Ctxt Defs} ->
|
||||
process buildmsg file
|
||||
= do Right res <- coreLift (readFile file)
|
||||
| Left err => pure [FileErr file err]
|
||||
case runParser res (do p <- prog file; eoi; pure p) of
|
||||
parseRes <- logTime ("Parsing " ++ file) $
|
||||
pure (runParser res (do p <- prog file; eoi; pure p))
|
||||
case parseRes of
|
||||
Left err => pure [ParseFail (getParseErrorLoc file err) err]
|
||||
Right mod =>
|
||||
-- Processing returns a list of errors across a whole module,
|
||||
@ -236,10 +240,12 @@ process buildmsg file
|
||||
-- other possible errors
|
||||
catch (do initHash
|
||||
fn <- getTTCFileName file ".ttc"
|
||||
Just errs <- processMod file fn buildmsg mod res
|
||||
Just errs <- logTime ("Elaborating " ++ file) $
|
||||
processMod file fn buildmsg mod res
|
||||
| Nothing => pure [] -- skipped it
|
||||
if isNil errs
|
||||
then
|
||||
logTime ("Writing TTC/TTM for " ++ file) $
|
||||
do defs <- get Ctxt
|
||||
d <- getDirs
|
||||
makeBuildDirectory (pathToNS (working_dir d) file)
|
||||
|
||||
@ -45,6 +45,8 @@ preOptions (SetCG e :: opts)
|
||||
preOptions (PkgPath p :: opts)
|
||||
= do addPkgDir p
|
||||
preOptions opts
|
||||
preOptions (Timing :: opts)
|
||||
= setLogTimings True
|
||||
preOptions (_ :: opts) = preOptions opts
|
||||
|
||||
-- Options to be processed after type checking. Returns whether execution
|
||||
|
||||
@ -86,6 +86,12 @@ doBind ns (IAs fc s n pat)
|
||||
= IAs fc s n (doBind ns pat)
|
||||
doBind ns (IMustUnify fc r pat)
|
||||
= IMustUnify fc r (doBind ns pat)
|
||||
doBind ns (IDelayed fc r ty)
|
||||
= IDelayed fc r (doBind ns ty)
|
||||
doBind ns (IDelay fc tm)
|
||||
= IDelay fc (doBind ns tm)
|
||||
doBind ns (IForce fc tm)
|
||||
= IForce fc (doBind ns tm)
|
||||
doBind ns (IAlternative fc u alts)
|
||||
= IAlternative fc u (map (doBind ns) alts)
|
||||
doBind ns tm = tm
|
||||
|
||||
@ -31,7 +31,7 @@ doPLetRenames ns drops (Bind fc n b@(PLet _ _ _) sc)
|
||||
doPLetRenames ns drops (Bind fc n b sc)
|
||||
= case lookup n ns of
|
||||
Just (c, n') =>
|
||||
Bind fc n' (setMultiplicity b c)
|
||||
Bind fc n' (setMultiplicity b (max c (multiplicity b)))
|
||||
(doPLetRenames ns (n' :: drops) (renameTop n' sc))
|
||||
Nothing => Bind fc n b (doPLetRenames ns drops sc)
|
||||
doPLetRenames ns drops sc = sc
|
||||
@ -107,7 +107,8 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
linearCheck (getFC tm) rigc False env chktm
|
||||
-- Linearity checking looks in case blocks, so no
|
||||
-- need to check here.
|
||||
else pure chktm
|
||||
else do checkNoGuards
|
||||
pure chktm
|
||||
|
||||
-- Put the current hole state back to what it was (minus anything
|
||||
-- which has been solved in the meantime)
|
||||
@ -128,7 +129,8 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
-- On the RHS, erase everything in a 0-multiplicity position
|
||||
-- (This doesn't do a full linearity check, just erases by
|
||||
-- type)
|
||||
do chkErase <- linearCheck (getFC tm) rigc True env chktm
|
||||
do dumpConstraints 2 False
|
||||
chkErase <- linearCheck (getFC tm) rigc True env chktm
|
||||
pure (chktm, chkErase, chkty)
|
||||
_ => pure (chktm, chktm, chkty)
|
||||
where
|
||||
|
||||
@ -30,6 +30,10 @@ getNameType rigc env fc x
|
||||
do rigSafe rigb rigc
|
||||
let bty = binderType (getBinder lv env)
|
||||
addNameType fc x env bty
|
||||
when (isLinear rigb) $
|
||||
do est <- get EST
|
||||
put EST
|
||||
(record { linearUsed $= ((MkVar lv) :: ) } est)
|
||||
pure (Local fc (Just rigb) _ lv, gnf env bty)
|
||||
Nothing =>
|
||||
do defs <- get Ctxt
|
||||
@ -194,6 +198,27 @@ mutual
|
||||
solveIfUndefined env metavar soln
|
||||
= pure False
|
||||
|
||||
-- Defer elaborating anything which will be easier given a known target
|
||||
-- type (ambiguity, cases, etc)
|
||||
needsDelay : {auto c : Ref Ctxt Defs} ->
|
||||
(knownRet : Bool) -> RawImp ->
|
||||
Core Bool
|
||||
needsDelay False _ = pure False
|
||||
needsDelay True (IVar fc n)
|
||||
= do defs <- get Ctxt
|
||||
case !(lookupCtxtName n (gamma defs)) of
|
||||
[] => pure False
|
||||
[x] => pure False
|
||||
_ => pure True
|
||||
needsDelay True (IApp _ f _) = needsDelay True f
|
||||
needsDelay True (IImplicitApp _ f _ _) = needsDelay True f
|
||||
needsDelay True (ICase _ _ _ _) = pure True
|
||||
needsDelay True (ILocal _ _ _) = pure True
|
||||
needsDelay True (IUpdate _ _ _) = pure True
|
||||
needsDelay True (IAlternative _ _ _) = pure True
|
||||
needsDelay True (ISearch _ _) = pure True
|
||||
needsDelay True _ = pure False
|
||||
|
||||
-- Check the rest of an application given the argument type and the
|
||||
-- raw argument. We choose elaboration order depending on whether we know
|
||||
-- the return type now. If we know it, elaborate the rest of the
|
||||
@ -222,7 +247,7 @@ mutual
|
||||
then pure True
|
||||
else do sc' <- sc defs (toClosure defaultOpts env (Erased fc))
|
||||
concrete defs env sc'
|
||||
if kr then do
|
||||
if !(needsDelay kr arg) then do
|
||||
nm <- genMVName x
|
||||
empty <- clearDefs defs
|
||||
metaty <- quote empty env aty
|
||||
@ -300,6 +325,9 @@ mutual
|
||||
= do let argRig = rigMult rig rigb
|
||||
checkRestApp rig argRig elabinfo nest env fc (explApp (Just x))
|
||||
tm x aty sc arg expargs impargs kr expty
|
||||
-- Function type is delayed, so force the term and continue
|
||||
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty) expargs impargs kr expty
|
||||
= checkAppWith rig elabinfo nest env fc (TForce dfc tm) ty expargs impargs kr expty
|
||||
-- If there's no more arguments given, and the plicities of the type and
|
||||
-- the expected type line up, stop
|
||||
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi rigb Implicit aty) sc)
|
||||
|
||||
@ -113,10 +113,20 @@ toRig1 First (b :: bs)
|
||||
else b :: bs
|
||||
toRig1 (Later p) (b :: bs) = b :: toRig1 p bs
|
||||
|
||||
toRig0 : {idx : Nat} -> .(IsVar name idx vs) -> Env Term vs -> Env Term vs
|
||||
toRig0 First (b :: bs) = setMultiplicity b Rig0 :: bs
|
||||
toRig0 (Later p) (b :: bs) = b :: toRig0 p bs
|
||||
|
||||
allow : Maybe (Var vs) -> Env Term vs -> Env Term vs
|
||||
allow Nothing env = env
|
||||
allow (Just (MkVar p)) env = toRig1 p env
|
||||
|
||||
-- If the name is used elsewhere, update its multiplicity so it's
|
||||
-- not required to be used in the case block
|
||||
updateMults : List (Var vs) -> Env Term vs -> Env Term vs
|
||||
updateMults [] env = env
|
||||
updateMults (MkVar p :: us) env = updateMults us (toRig0 p env)
|
||||
|
||||
shrinkImp : SubVars outer vars ->
|
||||
(Name, ImplBinding vars) -> Maybe (Name, ImplBinding outer)
|
||||
shrinkImp sub (n, NameBinding c tm ty)
|
||||
@ -256,6 +266,10 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
|
||||
scrn <- genVarName "scr"
|
||||
casen <- genCaseName (defining est)
|
||||
|
||||
-- Update environment so that linear bindings which were used
|
||||
-- (esp. in the scrutinee!) are set to 0 in the case type
|
||||
let env = updateMults (linearUsed est) env
|
||||
|
||||
-- The 'pre_env' is the environment we apply any local (nested)
|
||||
-- names to. Here *all* the names have multiplicity 0 (we're
|
||||
-- going to abstract over them all again, in case the case block
|
||||
|
||||
@ -105,13 +105,14 @@ record EState (vars : List Name) where
|
||||
-- Holes standing for pattern variables, which we'll delete
|
||||
-- once we're done elaborating
|
||||
allowDelay : Bool -- Delaying elaborators is okay. We can't nest delays.
|
||||
linearUsed : List (Var vars)
|
||||
|
||||
export
|
||||
data EST : Type where
|
||||
|
||||
export
|
||||
initEStateSub : Int -> Env Term outer -> SubVars outer vars -> EState vars
|
||||
initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True
|
||||
initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True []
|
||||
|
||||
export
|
||||
initEState : Int -> Env Term vars -> EState vars
|
||||
@ -130,7 +131,8 @@ weakenedEState {e}
|
||||
(bindIfUnsolved est)
|
||||
(lhsPatVars est)
|
||||
(allPatVars est)
|
||||
(allowDelay est))
|
||||
(allowDelay est)
|
||||
(map weaken (linearUsed est)))
|
||||
pure eref
|
||||
where
|
||||
wknTms : (Name, ImplBinding vs) ->
|
||||
@ -158,7 +160,8 @@ strengthenedEState {n} {vars} c e fc env
|
||||
(bindIfUnsolved est)
|
||||
(lhsPatVars est)
|
||||
(allPatVars est)
|
||||
(allowDelay est))
|
||||
(allowDelay est)
|
||||
(mapMaybe dropTop (linearUsed est)))
|
||||
where
|
||||
dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
|
||||
dropSub (DropCons sub) = pure sub
|
||||
@ -185,6 +188,10 @@ strengthenedEState {n} {vars} c e fc env
|
||||
_ => throw (GenericMsg fc ("Invalid as binding " ++
|
||||
show f ++ " " ++ show xnf ++ " : " ++ show ynf))
|
||||
|
||||
dropTop : (Var (n :: vs)) -> Maybe (Var vs)
|
||||
dropTop (MkVar First) = Nothing
|
||||
dropTop (MkVar (Later p)) = Just (MkVar p)
|
||||
|
||||
export
|
||||
inScope : {auto c : Ref Ctxt Defs} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
@ -208,6 +215,7 @@ updateEnv env sub bif st
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
(linearUsed st)
|
||||
|
||||
export
|
||||
addBindIfUnsolved : Name -> RigCount -> Env Term vars -> Term vars -> Term vars ->
|
||||
@ -220,6 +228,7 @@ addBindIfUnsolved hn r env tm ty st
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
(linearUsed st)
|
||||
|
||||
clearBindIfUnsolved : EState vars -> EState vars
|
||||
clearBindIfUnsolved st
|
||||
@ -229,6 +238,7 @@ clearBindIfUnsolved st
|
||||
(lhsPatVars st)
|
||||
(allPatVars st)
|
||||
(allowDelay st)
|
||||
(linearUsed st)
|
||||
|
||||
-- Clear the 'toBind' list, except for the names given
|
||||
export
|
||||
@ -473,14 +483,15 @@ processDecl : {vars : _} ->
|
||||
-- in doing so.
|
||||
-- Returns a list of constraints which need to be solved for the conversion
|
||||
-- to work; if this is empty, the terms are convertible.
|
||||
export
|
||||
convert : {vars : _} ->
|
||||
convertWithLazy
|
||||
: {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
(withLazy : Bool) ->
|
||||
FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
|
||||
Core UnifyResult
|
||||
convert fc elabinfo env x y
|
||||
convertWithLazy withLazy fc elabinfo env x y
|
||||
= let umode : UnifyMode
|
||||
= case elabMode elabinfo of
|
||||
InLHS _ => InLHS
|
||||
@ -491,10 +502,14 @@ convert fc elabinfo env x y
|
||||
vs <- if isFromTerm x && isFromTerm y
|
||||
then do xtm <- getTerm x
|
||||
ytm <- getTerm y
|
||||
unifyWithLazy umode fc env xtm ytm
|
||||
if withLazy
|
||||
then unifyWithLazy umode fc env xtm ytm
|
||||
else unify umode fc env xtm ytm
|
||||
else do xnf <- getNF x
|
||||
ynf <- getNF y
|
||||
unifyWithLazy umode fc env xnf ynf
|
||||
if withLazy
|
||||
then unifyWithLazy umode fc env xnf ynf
|
||||
else unify umode fc env xnf ynf
|
||||
when (holesSolved vs) $
|
||||
solveConstraints umode Normal
|
||||
pure vs)
|
||||
@ -514,6 +529,15 @@ convert fc elabinfo env x y
|
||||
!(normaliseHoles defs env xtm)
|
||||
!(normaliseHoles defs env ytm) err))
|
||||
|
||||
export
|
||||
convert : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
|
||||
Core UnifyResult
|
||||
convert = convertWithLazy False
|
||||
|
||||
-- Check whether the type we got for the given type matches the expected
|
||||
-- type.
|
||||
-- Returns the term and its type.
|
||||
@ -529,11 +553,14 @@ checkExp : {vars : _} ->
|
||||
(got : Glued vars) -> (expected : Maybe (Glued vars)) ->
|
||||
Core (Term vars, Glued vars)
|
||||
checkExp rig elabinfo env fc tm got (Just exp)
|
||||
= do vs <- convert fc elabinfo env got exp
|
||||
= do vs <- convertWithLazy True fc elabinfo env got exp
|
||||
case (constraints vs) of
|
||||
[] => case addLazy vs of
|
||||
NoLazy => pure (tm, got)
|
||||
AddForce => pure (TForce fc tm, exp)
|
||||
AddForce => do logTerm 0 "Force" tm
|
||||
logGlue 0 "Got" env got
|
||||
logGlue 0 "Exp" env exp
|
||||
pure (TForce fc tm, exp)
|
||||
AddDelay r => do ty <- getTerm got
|
||||
pure (TDelay fc r ty tm, exp)
|
||||
cs => do defs <- get Ctxt
|
||||
|
||||
@ -51,7 +51,7 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
|
||||
applyEnv outer inner
|
||||
= do n' <- resolveName (Nested outer inner)
|
||||
pure (inner, (Just (Resolved n'),
|
||||
\fc, nt => applyToFull fc
|
||||
\fc, nt => applyTo fc
|
||||
(Ref fc nt (Resolved n')) env))
|
||||
|
||||
-- Update the names in the declarations to the new 'nested' names.
|
||||
|
||||
@ -371,6 +371,9 @@ findImplicits (IMustUnify fc r pat)
|
||||
= findImplicits pat
|
||||
findImplicits (IAlternative fc u alts)
|
||||
= concatMap findImplicits alts
|
||||
findImplicits (IDelayed fc _ ty) = findImplicits ty
|
||||
findImplicits (IDelay fc tm) = findImplicits tm
|
||||
findImplicits (IForce fc tm) = findImplicits tm
|
||||
findImplicits (IBindVar _ n) = [n]
|
||||
findImplicits tm = []
|
||||
|
||||
|
||||
@ -1,9 +1,9 @@
|
||||
1/1: Building Vect (Vect.idr)
|
||||
Welcome to Idris 2 version 0.0. Fingers crossed!
|
||||
Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
|
||||
Main> (interactive):1:22--1:25:When unifying Vect Z ?a and Vect (S Z) ?a
|
||||
Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
|
||||
Mismatch between:
|
||||
Z
|
||||
and
|
||||
S ?k
|
||||
and
|
||||
Z
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n Main.Nat (Main.S {k:45}) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus {k:45}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTC
|
||||
Read TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n ? (Main.S {k:45}) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus {k:45}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:20} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi RigW Explicit Nothing ((Main.Vect {k:20}) a) (%pi RigW Explicit Nothing a (%let Rig0 n ? (Main.S {k:20}) ((Main.Vect ((Main.plus {k:20}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,5 +2,5 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved102 ?Main.{a:71}_[]), ($resolved78 ?Main.{a:71}_[])]
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved94 ?Main.{a:52}_[]), ($resolved78 ?Main.{a:52}_[])]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,9 +2,9 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect2.yaff:25:1--26:1:pat 0 {b:34} : Type => pat 0 {a:33} : Type => ($resolved102 {b:34}[1] {a:33}[0] $resolved77 ($resolved92 {a:33}[0]) ($resolved92 {b:34}[1])) is not a valid impossible pattern because it typechecks
|
||||
Vect2.yaff:25:1--26:1:pat 0 {b:21} : Type => pat 0 {a:20} : Type => ($resolved91 {b:21}[1] {a:20}[0] $resolved75 ($resolved82 {a:20}[0]) ($resolved82 {b:21}[1])) is not a valid impossible pattern because it typechecks
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
|
||||
Vect3.yaff:25:9--25:11:Type mismatch: $resolved76 and ($resolved90 ?Main.{n:28}_[] ?Main.{b:26}_[])
|
||||
Vect3.yaff:25:9--25:11:Type mismatch: $resolved74 and ($resolved80 ?Main.{n:17}_[] ?Main.{b:15}_[])
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,6 +2,6 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.lookup: All cases covered
|
||||
Yaffle> Main.lookup':
|
||||
($resolved132 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3})
|
||||
Yaffle> Main.lookup'': Calls non covering function $resolved132
|
||||
($resolved114 {arg:0} {arg:1} (Main.FZ {m:0}) {arg:3})
|
||||
Yaffle> Main.lookup'': Calls non covering function $resolved114
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,14 +2,14 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot2.yaff:15:1--16:1:When elaborating left hand side of $resolved92:
|
||||
Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:92}_[] ?{P:m:92}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:92}_[] ?{P:n:92}_[])
|
||||
Dot2.yaff:15:1--16:1:When elaborating left hand side of $resolved79:
|
||||
Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:79}_[] ?{P:m:79}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:79}_[] ?{P:n:79}_[])
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot3.yaff:18:1--20:1:When elaborating left hand side of $resolved100:
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:30}_[] ?Main.{_:29}_[])
|
||||
Dot3.yaff:18:1--20:1:When elaborating left hand side of $resolved82:
|
||||
Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:8}_[] ?Main.{_:9}_[])
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTImp
|
||||
Dot4.yaff:17:1--19:1:When elaborating left hand side of $resolved100:
|
||||
Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:32}_[] ?Main.{_:31}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[])
|
||||
Dot4.yaff:17:1--19:1:When elaborating left hand side of $resolved82:
|
||||
Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:7}_[] ?Main.{_:8}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[])
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Refl [Just {b:15} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> ((Main.Refl [Just {b:7} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
Processing as TTImp
|
||||
Eta.yaff:16:10--17:1:When unifying: ($resolved84 ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) ?Main.{x:26}_[] ?Main.{x:26}_[]) and ($resolved84 ((x : Char) -> ((y : ?Main.{_:20}_[x[0]]) -> $resolved92)) (({arg:16} : Integer) -> (({arg:17} : Integer) -> $resolved92)) $resolved93 \x : Char => \y : ?Main.{_:20}_[x[0]] => ($resolved93 ?Main.{_:24}_[x[1], y[0]] ?Main.{_:23}_[x[1], y[0]]))
|
||||
Eta.yaff:16:10--17:1:When unifying: ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) ?Main.{x:16}_[] ?Main.{x:16}_[]) and ($resolved76 ((x : Char) -> ((y : ?Main.{_:12}_[x[0]]) -> $resolved84)) (({arg:8} : Integer) -> (({arg:9} : Integer) -> $resolved84)) $resolved85 \x : Char => \y : ?Main.{_:12}_[x[0]] => ($resolved85 ?Main.{_:13}_[x[1], y[0]] ?Main.{_:14}_[x[1], y[0]]))
|
||||
Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just {k:36} Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%let Rig0 n Main.Nat (Main.S (Main.S {k:36})) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:36}) a) (%let Rig1 zs ((Main.Vect (Main.S {k:36})) a) ((((Main.Cons [Just k = {k:36}]) [Just a = a]) y) ws) (%pi RigW Explicit Nothing ((Main.Vect m) a) ((Main.Vect ((Main.plus n@((Main.S (Main.S {k:36})))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just n Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:82} Main.Nat (%let Rig0 n Main.Nat (Main.S {k:82}) (%pi RigW Explicit Just x a (%pi Rig1 Explicit Just zs ((Main.Vect {k:82}) a) (%let Rig0 xs ((Main.Vect n@((Main.S {k:82}))) a) ((((Main.Cons [Just k = {k:82}]) [Just a = a]) x) zs) ((Main.Vect ((Main.plus n@((Main.S {k:82}))) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just n Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:129} Main.Nat (%let Rig0 n Main.Nat (Main.S {k:129}) (%pi RigW Explicit Just x a (%pi Rig0 Explicit Just zs ((Main.Vect {k:129}) a) (%let Rig0 xs ((Main.Vect n@((Main.S {k:129}))) a) ((((Main.Cons [Just k = {k:129}]) [Just a = a]) x) zs) (%let Rig1 ts ((Main.Vect {k:129}) a) zs ((Main.Vect ((Main.plus n@((Main.S {k:129}))) m)) a)))))))))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:14} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just ws ((Main.Vect {k:14}) a) (%pi Rig0 Explicit Just y a (%let Rig1 zs ((Main.Vect (Main.S {k:14})) a) ((((Main.Cons [Just k = {k:14}]) [Just a = a]) y) ws) (%pi RigW Explicit Nothing a (%let Rig0 n Main.Nat (Main.S (Main.S {k:14})) ((Main.Vect ((Main.plus (Main.S (Main.S {k:14}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:41} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:41}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:41})) a) ((((Main.Cons [Just k = {k:41}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:41}) ((Main.Vect ((Main.plus (Main.S {k:41})) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:69} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:69}) a) (%pi RigW Explicit Just x a (%let Rig0 xs ((Main.Vect (Main.S {k:69})) a) ((((Main.Cons [Just k = {k:69}]) [Just a = a]) x) zs) (%let Rig0 n Main.Nat (Main.S {k:69}) (%let Rig1 ts ((Main.Vect {k:69}) a) zs ((Main.Vect ((Main.plus (Main.S {k:69})) m)) a)))))))))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> (((((Main.There [Just {a:17} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
||||
Yaffle> (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
||||
Yaffle> (((((Main.There [Just {impty:14} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
||||
Yaffle> (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
||||
Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -67,7 +67,7 @@ namespace Vect
|
||||
tryMap : Nat -> Nat -> List Nat
|
||||
tryMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
|
||||
|
||||
tryVMap : Nat -> Nat -> Vect ? Nat
|
||||
tryVMap : Nat -> Nat -> Vect (S (S Z)) Nat
|
||||
tryVMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
|
||||
|
||||
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> \0 a : Type => \0 m : Main.Nat => \ys : (Main.Vect m[0] a[1]) => ys[0]
|
||||
Yaffle> \0 {k:49} : Main.Nat => \0 a : Type => \0 m : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:49}[3] a[2]) => \ys : (Main.Vect m[2] a[3]) => (Main.Cons (Main.plus {k:49}[5] m[3]) a[4] x[2] (Main.append m[3] a[4] {k:49}[5] xs[1] ys[0]))
|
||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:242}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:242}]) z) y))]
|
||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:368}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:368}]) z) w))]
|
||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:497}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:497}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => ys[0]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:22} : Main.Nat => \ys : (Main.Vect m[2] a[1]) => \xs : (Main.Vect {k:22}[1] a[2]) => \x : a[3] => (Main.Cons (Main.plus {k:22}[3] m[5]) a[4] x[0] (Main.append m[5] a[4] {k:22}[3] xs[1] ys[2]))
|
||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:191}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:191}]) z) y))]
|
||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:298}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:298}]) z) w))]
|
||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:448}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:448}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -5,5 +5,5 @@ Yaffle> Main.ack is total
|
||||
Yaffle> Main.foo is total
|
||||
Yaffle> Main.foo' is total
|
||||
Yaffle> Main.foom is total
|
||||
Yaffle> Main.pfoom is not terminating due to recursive path $resolved158 -> Main.pfoom -> Main.pfoom
|
||||
Yaffle> Main.pfoom is not terminating due to recursive path $resolved95 -> Main.pfoom -> Main.pfoom
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -3,5 +3,5 @@ Written TTC
|
||||
Yaffle> (Main.Odd (Main.S Main.Z))
|
||||
Yaffle> (Main.Even (Main.S Main.Z))
|
||||
Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:15} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
|
||||
Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:7} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user