mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
[ re #1852 ] Partial fix without the Hole UN refactoring
This commit is contained in:
parent
5c5b3a2ae7
commit
63bf9f2900
@ -28,7 +28,7 @@ import public Libraries.Utils.Binary
|
||||
||| (Increment this when changing anything in the data format)
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 69
|
||||
ttcVersion = 70
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
|
@ -74,7 +74,8 @@ isWhitespace _ = False
|
||||
||| Given a list of definitions, a list of mappings from `RawName` to `String`,
|
||||
||| and a list of tokens to update, work out the updates to do, apply them, and
|
||||
||| return the result.
|
||||
doUpdates : {auto u : Ref UPD (List String)} ->
|
||||
doUpdates : {auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto u : Ref UPD (List String)} ->
|
||||
Defs -> Updates -> List SourcePart ->
|
||||
Core (List SourcePart)
|
||||
doUpdates defs ups [] = pure [] -- no more tokens to update, so we are done
|
||||
@ -119,7 +120,7 @@ doUpdates defs ups (Name n :: xs)
|
||||
-- and change the hole's name to the new one
|
||||
doUpdates defs ups (HoleName n :: xs)
|
||||
= do used <- get UPD
|
||||
n' <- uniqueName defs used n
|
||||
n' <- uniqueHoleName defs used n
|
||||
put UPD (n' :: used)
|
||||
pure $ HoleName n' :: !(doUpdates defs ups xs)
|
||||
-- if it's not a thing we update, leave it and continue working on the rest
|
||||
@ -129,7 +130,8 @@ doUpdates defs ups (x :: xs)
|
||||
-- State here is a list of new hole names we generated (so as not to reuse any).
|
||||
-- Update the token list with the string replacements for each match, and return
|
||||
-- the newly generated strings.
|
||||
updateAll : {auto u : Ref UPD (List String)} ->
|
||||
updateAll : {auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto u : Ref UPD (List String)} ->
|
||||
Defs -> List SourcePart -> List Updates ->
|
||||
Core (List String)
|
||||
updateAll defs l [] = pure []
|
||||
|
@ -75,7 +75,7 @@ sexp
|
||||
pure (SExpList xs)
|
||||
|
||||
ideParser : {e : _} ->
|
||||
String -> Grammar SemanticDecorations Token e ty -> Either Error ty
|
||||
String -> Grammar State Token e ty -> Either Error ty
|
||||
ideParser str p
|
||||
= do toks <- mapFst (fromLexError (Virtual Interactive)) $ idelex str
|
||||
(_, _, (parsed, _)) <- mapFst (fromParsingErrors (Virtual Interactive)) $ parseWith p toks
|
||||
|
@ -21,14 +21,10 @@ import Idris.Parser.Let
|
||||
|
||||
%default covering
|
||||
|
||||
decorationFromBounded : OriginDesc -> Decoration -> WithBounds a -> ASemanticDecoration
|
||||
decorationFromBounded fname decor bnds
|
||||
= ((fname, start bnds, end bnds), decor, Nothing)
|
||||
|
||||
decorate : OriginDesc -> Decoration -> Rule a -> Rule a
|
||||
decorate fname decor rule = do
|
||||
res <- bounds rule
|
||||
act [decorationFromBounded fname decor res]
|
||||
actD (decorationFromBounded fname decor res)
|
||||
pure res.val
|
||||
|
||||
boundedNameDecoration : OriginDesc -> Decoration -> WithBounds Name -> ASemanticDecoration
|
||||
@ -37,18 +33,20 @@ boundedNameDecoration fname decor bstr = ((fname, start bstr, end bstr)
|
||||
, Just bstr.val)
|
||||
|
||||
decorateBoundedNames : OriginDesc -> Decoration -> List (WithBounds Name) -> EmptyRule ()
|
||||
decorateBoundedNames fname decor bns = act $ map (boundedNameDecoration fname decor) bns
|
||||
decorateBoundedNames fname decor bns
|
||||
= act $ MkState (map (boundedNameDecoration fname decor) bns) []
|
||||
|
||||
decorateBoundedName : OriginDesc -> Decoration -> WithBounds Name -> EmptyRule ()
|
||||
decorateBoundedName fname decor bn = act [boundedNameDecoration fname decor bn]
|
||||
decorateBoundedName fname decor bn = actD (boundedNameDecoration fname decor bn)
|
||||
|
||||
decorateKeywords : OriginDesc -> List (WithBounds a) -> EmptyRule ()
|
||||
decorateKeywords fname = act . map (decorationFromBounded fname Keyword)
|
||||
decorateKeywords fname xs
|
||||
= act $ MkState (map (decorationFromBounded fname Keyword) xs) []
|
||||
|
||||
dependentDecorate : OriginDesc -> Rule a -> (a -> Decoration) -> Rule a
|
||||
dependentDecorate fname rule decor = do
|
||||
res <- bounds rule
|
||||
act [((fname, (start res, end res)), decor res.val, Nothing)]
|
||||
actD (decorationFromBounded fname (decor res.val) res)
|
||||
pure res.val
|
||||
|
||||
decoratedKeyword : OriginDesc -> String -> Rule ()
|
||||
@ -130,6 +128,7 @@ atom fname
|
||||
<|> do x <- bounds $ symbol "?"
|
||||
pure (PInfer (boundToFC fname x))
|
||||
<|> do x <- bounds $ holeName
|
||||
actH x.val -- record the hole name in the parser
|
||||
pure (PHole (boundToFC fname x) False x.val)
|
||||
<|> do x <- bounds $ decorate fname Data $ pragma "MkWorld"
|
||||
pure (PPrimVal (boundToFC fname x) WorldVal)
|
||||
@ -343,14 +342,14 @@ mutual
|
||||
continueWithDecorated fname indents ")"
|
||||
pure (op, e))
|
||||
(op, e) <- pure b.val
|
||||
act [(toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)]
|
||||
actD (toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)
|
||||
let fc = boundToFC fname (mergeBounds s b)
|
||||
let opFC = boundToFC fname op
|
||||
pure (PSectionL fc opFC op.val e)
|
||||
<|> do -- (.y.z) -- section of projection (chain)
|
||||
b <- bounds $ forget <$> some (bounds postfixProj)
|
||||
decoratedSymbol fname ")"
|
||||
act [(toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)]
|
||||
actD (toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)
|
||||
let projs = map (\ proj => (boundToFC fname proj, proj.val)) b.val
|
||||
pure $ PPostfixAppPartial (boundToFC fname b) projs
|
||||
-- unit type/value
|
||||
@ -358,7 +357,7 @@ mutual
|
||||
pure (PUnit (boundToFC fname (mergeBounds s b)))
|
||||
-- dependent pairs with type annotation (so, the type form)
|
||||
<|> do dpairType fname s indents <* (decorate fname Typ $ symbol ")")
|
||||
<* act [(toNonEmptyFC $ boundToFC fname s, Typ, Nothing)]
|
||||
<* actD (toNonEmptyFC $ boundToFC fname s, Typ, Nothing)
|
||||
<|> do e <- bounds (typeExpr pdef fname indents)
|
||||
-- dependent pairs with no type annotation
|
||||
(do loc <- bounds (symbol "**")
|
||||
@ -370,7 +369,7 @@ mutual
|
||||
rest.val)) <|>
|
||||
-- right sections
|
||||
((do op <- bounds (bounds iOperator <* decoratedSymbol fname ")")
|
||||
act [(toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)]
|
||||
actD (toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)
|
||||
let fc = boundToFC fname (mergeBounds s op)
|
||||
let opFC = boundToFC fname op.val
|
||||
pure (PSectionR fc opFC e.val op.val.val)
|
||||
@ -450,7 +449,7 @@ mutual
|
||||
exp <- optional (typeExpr pdef fname indents)
|
||||
pure (boundToFC fname b, exp)
|
||||
end <- continueWithDecorated fname indents ")"
|
||||
act [(toNonEmptyFC (boundToFC fname s), Keyword, Nothing)]
|
||||
actD (toNonEmptyFC (boundToFC fname s), Keyword, Nothing)
|
||||
pure $ let (start ::: rest) = vals in
|
||||
buildOutput (fst start) (mergePairs 0 start rest)
|
||||
where
|
||||
@ -484,7 +483,7 @@ mutual
|
||||
tuple fname s indents e
|
||||
= nonEmptyTuple fname s indents e
|
||||
<|> do end <- bounds (continueWithDecorated fname indents ")")
|
||||
act [(toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)]
|
||||
actD (toNonEmptyFC $ boundToFC fname s, Keyword, Nothing)
|
||||
pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
|
||||
|
||||
simpleExpr : OriginDesc -> IndentInfo -> Rule PTerm
|
||||
|
@ -317,7 +317,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin
|
||||
pure Nothing
|
||||
else -- needs rebuilding
|
||||
do iputStrLn msg
|
||||
Right (ws, decor, mod) <-
|
||||
Right (ws, MkState decor hnames, mod) <-
|
||||
logTime ("++ Parsing " ++ sourceFileName) $
|
||||
pure $ runParser (PhysicalIdrSrc origin)
|
||||
(isLitFile sourceFileName)
|
||||
@ -334,6 +334,9 @@ processMod sourceFileName ttcFileName msg sourcecode origin
|
||||
addModDocString (moduleNS mod) (documentation mod)
|
||||
|
||||
addSemanticDecorations decor
|
||||
syn <- get Syn
|
||||
put Syn ({ holeNames := hnames } syn)
|
||||
|
||||
initHash
|
||||
traverse_ addPublicHash (sort importMetas)
|
||||
resetNextVar
|
||||
|
@ -913,6 +913,7 @@ record SyntaxInfo where
|
||||
-- to be bracketed when solved)
|
||||
usingImpl : List (Maybe Name, RawImp)
|
||||
startExpr : RawImp
|
||||
holeNames : List String -- hole names in the file
|
||||
|
||||
export
|
||||
TTC Fixity where
|
||||
@ -942,6 +943,7 @@ TTC SyntaxInfo where
|
||||
(ANameMap.toList (defDocstrings syn)))
|
||||
toBuf b (bracketholes syn)
|
||||
toBuf b (startExpr syn)
|
||||
toBuf b (holeNames syn)
|
||||
|
||||
fromBuf b
|
||||
= do inf <- fromBuf b
|
||||
@ -951,12 +953,14 @@ TTC SyntaxInfo where
|
||||
defdstrs <- fromBuf b
|
||||
bhs <- fromBuf b
|
||||
start <- fromBuf b
|
||||
hnames <- fromBuf b
|
||||
pure $ MkSyntax (fromList inf) (fromList pre)
|
||||
[] (fromList moddstr)
|
||||
[] (fromList ifs)
|
||||
empty (fromList defdstrs)
|
||||
bhs
|
||||
[] start
|
||||
hnames
|
||||
|
||||
HasNames IFaceInfo where
|
||||
full gam iface
|
||||
@ -986,12 +990,12 @@ HasNames a => HasNames (ANameMap a) where
|
||||
export
|
||||
HasNames SyntaxInfo where
|
||||
full gam syn
|
||||
= pure $ record { ifaces = !(full gam (ifaces syn)),
|
||||
bracketholes = !(traverse (full gam) (bracketholes syn))
|
||||
= pure $ { ifaces := !(full gam (ifaces syn))
|
||||
, bracketholes := !(traverse (full gam) (bracketholes syn))
|
||||
} syn
|
||||
resolved gam syn
|
||||
= pure $ record { ifaces = !(resolved gam (ifaces syn)),
|
||||
bracketholes = !(traverse (resolved gam) (bracketholes syn))
|
||||
= pure $ { ifaces := !(resolved gam (ifaces syn))
|
||||
, bracketholes := !(traverse (resolved gam) (bracketholes syn))
|
||||
} syn
|
||||
|
||||
export
|
||||
@ -1008,6 +1012,7 @@ initSyntax
|
||||
[]
|
||||
[]
|
||||
(IVar EmptyFC (UN $ Basic "main"))
|
||||
[]
|
||||
|
||||
where
|
||||
|
||||
|
@ -18,9 +18,24 @@ import Libraries.Data.String.Extra
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
record State where
|
||||
constructor MkState
|
||||
decorations : SemanticDecorations
|
||||
holeNames : List String
|
||||
|
||||
export
|
||||
Semigroup State where
|
||||
MkState decs1 hs1 <+> MkState decs2 hs2
|
||||
= MkState (decs1 ++ decs2) (hs1 ++ hs2)
|
||||
|
||||
export
|
||||
Monoid State where
|
||||
neutral = MkState [] []
|
||||
|
||||
public export
|
||||
BRule : Bool -> Type -> Type
|
||||
BRule = Grammar SemanticDecorations Token
|
||||
BRule = Grammar State Token
|
||||
|
||||
public export
|
||||
Rule : Type -> Type
|
||||
@ -30,6 +45,14 @@ public export
|
||||
EmptyRule : Type -> Type
|
||||
EmptyRule = BRule False
|
||||
|
||||
export
|
||||
actD : ASemanticDecoration -> EmptyRule ()
|
||||
actD s = act (MkState [s] [])
|
||||
|
||||
export
|
||||
actH : String -> EmptyRule ()
|
||||
actH s = act (MkState [] [s])
|
||||
|
||||
export
|
||||
eoi : EmptyRule ()
|
||||
eoi = ignore $ nextIs "Expected end of input" isEOI
|
||||
@ -56,10 +79,15 @@ documentation' = terminal "Expected documentation comment" $
|
||||
DocComment d => Just d
|
||||
_ => Nothing
|
||||
|
||||
export
|
||||
decorationFromBounded : OriginDesc -> Decoration -> WithBounds a -> ASemanticDecoration
|
||||
decorationFromBounded fname decor bnds
|
||||
= ((fname, start bnds, end bnds), decor, Nothing)
|
||||
|
||||
documentation : OriginDesc -> Rule String
|
||||
documentation fname
|
||||
= do b <- bounds (some documentation')
|
||||
act [((fname, start b, end b), Comment, Nothing)]
|
||||
actD (decorationFromBounded fname Comment b)
|
||||
pure (unlines $ forget b.val)
|
||||
|
||||
export
|
||||
|
@ -17,8 +17,8 @@ export
|
||||
runParserTo : {e : _} ->
|
||||
(origin : OriginDesc) ->
|
||||
Maybe LiterateStyle -> Lexer ->
|
||||
String -> Grammar SemanticDecorations Token e ty ->
|
||||
Either Error (List Warning, SemanticDecorations, ty)
|
||||
String -> Grammar State Token e ty ->
|
||||
Either Error (List Warning, State, ty)
|
||||
runParserTo origin lit reject str p
|
||||
= do str <- mapFst (fromLitError origin) $ unlit lit str
|
||||
(cs, toks) <- mapFst (fromLexError origin) $ lexTo reject str
|
||||
@ -28,20 +28,20 @@ runParserTo origin lit reject str p
|
||||
let ws = ws <&> \ (mb, warn) =>
|
||||
let mkFC = \ b => MkFC origin (startBounds b) (endBounds b)
|
||||
in ParserWarning (maybe EmptyFC mkFC mb) warn
|
||||
Right (ws, cs ++ decs, parsed)
|
||||
Right (ws, { decorations $= (cs ++) } decs, parsed)
|
||||
|
||||
export
|
||||
runParser : {e : _} ->
|
||||
(origin : OriginDesc) -> Maybe LiterateStyle -> String ->
|
||||
Grammar SemanticDecorations Token e ty ->
|
||||
Either Error (List Warning, SemanticDecorations, ty)
|
||||
Grammar State Token e ty ->
|
||||
Either Error (List Warning, State, ty)
|
||||
runParser origin lit = runParserTo origin lit (pred $ const False)
|
||||
|
||||
export covering
|
||||
parseFile : (fname : String)
|
||||
-> (origin : OriginDesc)
|
||||
-> Rule ty
|
||||
-> IO (Either Error (List Warning, SemanticDecorations, ty))
|
||||
-> IO (Either Error (List Warning, State, ty))
|
||||
parseFile fname origin p
|
||||
= do Right str <- readFile fname
|
||||
| Left err => pure (Left (FileErr fname err))
|
||||
|
@ -364,7 +364,7 @@ getSuccessful {vars} fc rig opts mkHole env ty topty all
|
||||
let base = maybe "arg"
|
||||
(\r => nameRoot (recname r) ++ "_rhs")
|
||||
(recData opts)
|
||||
hn <- uniqueName defs (map nameRoot vars) base
|
||||
hn <- uniqueBasicName defs (map nameRoot vars) base
|
||||
(idx, tm) <- newMeta fc rig env (UN $ Basic hn) ty
|
||||
(Hole (length env) (holeInit False))
|
||||
False
|
||||
|
@ -38,6 +38,7 @@ fnName lhs n = nameRoot n
|
||||
|
||||
-- Make the hole on the RHS have a unique name
|
||||
uniqueRHS : {auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
ImpClause -> Core ImpClause
|
||||
uniqueRHS (PatClause fc lhs rhs)
|
||||
= pure $ PatClause fc lhs !(mkUniqueName rhs)
|
||||
@ -45,7 +46,7 @@ uniqueRHS (PatClause fc lhs rhs)
|
||||
mkUniqueName : RawImp -> Core RawImp
|
||||
mkUniqueName (IHole fc' rhsn)
|
||||
= do defs <- get Ctxt
|
||||
rhsn' <- uniqueName defs [] rhsn
|
||||
rhsn' <- uniqueHoleName defs [] rhsn
|
||||
pure (IHole fc' rhsn')
|
||||
mkUniqueName tm = pure tm -- it'll be a hole, but this is needed for covering
|
||||
uniqueRHS c = pure c
|
||||
@ -220,7 +221,7 @@ makeDefFromType loc opts n envlen ty
|
||||
-- We won't try splitting on these
|
||||
let pre_env = replicate envlen (Implicit loc True)
|
||||
|
||||
rhshole <- uniqueName defs [] (fnName False n ++ "_rhs")
|
||||
rhshole <- uniqueHoleName defs [] (fnName False n ++ "_rhs")
|
||||
let initcs = PatClause loc
|
||||
(apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))
|
||||
(IHole loc rhshole)
|
||||
|
@ -6,6 +6,8 @@ import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.TT
|
||||
|
||||
import Idris.Syntax
|
||||
|
||||
import TTImp.Unelab
|
||||
import TTImp.TTImp
|
||||
import TTImp.TTImp.Functor
|
||||
@ -41,12 +43,13 @@ bindableArg p _ = False
|
||||
|
||||
getArgs : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
Env Term vars -> Nat -> Term vars ->
|
||||
Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp)
|
||||
getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc)
|
||||
= do defs <- get Ctxt
|
||||
ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
|
||||
let x' = UN $ Basic !(uniqueName defs (map nameRoot vars) (nameRoot x))
|
||||
let x' = UN $ Basic !(uniqueBasicName defs (map nameRoot vars) (nameRoot x))
|
||||
(sc', ty) <- getArgs (b :: env) k (renameTop x' sc)
|
||||
-- Don't need to use the name if it's not used in the scope type
|
||||
let mn = if c == top
|
||||
@ -84,6 +87,7 @@ mkApp loc n args
|
||||
export
|
||||
makeLemma : {auto m : Ref MD Metadata} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
FC -> Name -> Nat -> ClosedTerm ->
|
||||
Core (RawImp, RawImp)
|
||||
makeLemma loc n nlocs ty
|
||||
|
@ -9,6 +9,8 @@ import Data.List
|
||||
import Data.List1
|
||||
import Data.String
|
||||
|
||||
import Idris.Syntax
|
||||
|
||||
import Libraries.Utils.String
|
||||
|
||||
%default covering
|
||||
@ -487,20 +489,26 @@ mutual
|
||||
= INamespace fc' ns (map (substLocDecl fc') ds)
|
||||
substLocDecl fc' d = d
|
||||
|
||||
nameNum : String -> (String, Int)
|
||||
nameNum str
|
||||
= case span isDigit (reverse str) of
|
||||
("", _) => (str, 0)
|
||||
(nums, pre)
|
||||
=> case unpack pre of
|
||||
('_' :: rest) => (reverse (pack rest), cast (reverse nums))
|
||||
_ => (str, 0)
|
||||
nameNum : String -> (String, Maybe Int)
|
||||
nameNum str = case span isDigit (reverse str) of
|
||||
("", _) => (str, Nothing)
|
||||
(nums, pre) => case unpack pre of
|
||||
('_' :: rest) => (reverse (pack rest), Just $ cast (reverse nums))
|
||||
_ => (str, Nothing)
|
||||
|
||||
nextNameNum : (String, Maybe Int) -> (String, Maybe Int)
|
||||
nextNameNum (str, mn) = (str, Just $ maybe 0 (1+) mn)
|
||||
|
||||
unNameNum : (String, Maybe Int) -> String
|
||||
unNameNum (str, Nothing) = str
|
||||
unNameNum (str, Just n) = fastConcat [str, "_", show n]
|
||||
|
||||
|
||||
export
|
||||
uniqueName : Defs -> List String -> String -> Core String
|
||||
uniqueName defs used n
|
||||
uniqueBasicName : Defs -> List String -> String -> Core String
|
||||
uniqueBasicName defs used n
|
||||
= if !usedName
|
||||
then uniqueName defs used (next n)
|
||||
then uniqueBasicName defs used (next n)
|
||||
else pure n
|
||||
where
|
||||
usedName : Core Bool
|
||||
@ -510,6 +518,11 @@ uniqueName defs used n
|
||||
_ => True
|
||||
|
||||
next : String -> String
|
||||
next str
|
||||
= let (n, i) = nameNum str in
|
||||
n ++ "_" ++ show (i + 1)
|
||||
next = unNameNum . nextNameNum . nameNum
|
||||
|
||||
export
|
||||
uniqueHoleName : {auto s : Ref Syn SyntaxInfo} ->
|
||||
Defs -> List String -> String -> Core String
|
||||
uniqueHoleName defs used n
|
||||
= do syn <- get Syn
|
||||
uniqueBasicName defs (used ++ holeNames syn) n
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.idr)
|
||||
Main> append {n = 0} [] ys = ?foo_1
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_2
|
||||
Main> vadd [] [] = ?bar_1
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_1
|
||||
Main> suc x x Refl = ?quux_1
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_1
|
||||
Main> append {n = 0} [] ys = ?foo_0
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_1
|
||||
Main> vadd [] [] = ?bar_0
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_0
|
||||
Main> suc x x Refl = ?quux_0
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_0
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.idr)
|
||||
Main> [] => ?bar_1
|
||||
(x :: zs) => ?bar_2
|
||||
Main> map f (MkFoo x) = ?baz_1
|
||||
map f (MkBar g) = ?baz_2
|
||||
Main> [] => ?bar_0
|
||||
(x :: zs) => ?bar_1
|
||||
Main> map f (MkFoo x) = ?baz_0
|
||||
map f (MkBar g) = ?baz_1
|
||||
Main> Bye for now!
|
||||
1/1: Building IEdit2 (IEdit2.idr)
|
||||
Main> (x :: []) => ?bar_5
|
||||
|
@ -1,5 +1,5 @@
|
||||
1/1: Building Door (Door.idr)
|
||||
Main> (val # y) => ?now_4
|
||||
Main> (val # y) => ?now_0
|
||||
Main> (False # d) => ?now_4
|
||||
(True # d) => ?now_5
|
||||
Main> 0 m : Type -> Type
|
||||
|
@ -1,40 +1,40 @@
|
||||
1/1: Building Spacing (Spacing.idr)
|
||||
Spacing> no {n = 0} = ?no_rhs_1
|
||||
no {n = (S k)} = ?no_rhs_2
|
||||
Spacing> spaced { n = 0 } = ?spaced_rhs_1
|
||||
spaced { n = (S k) } = ?spaced_rhs_2
|
||||
Spacing> s1 { n = 0} = ?s1_rhs_1
|
||||
s1 { n = (S k)} = ?s1_rhs_2
|
||||
Spacing> s2 { n = 0} = ?s2_rhs_1
|
||||
s2 { n = (S k)} = ?s2_rhs_2
|
||||
Spacing> s3 { n = 0} = ?s3_rhs_1
|
||||
s3 { n = (S k)} = ?s3_rhs_2
|
||||
Spacing> noSEq {n = 0} = ?noSEq_rhs_1
|
||||
noSEq {n = (S k)} = ?noSEq_rhs_2
|
||||
Spacing> spacedEq { n = 0 } = ?spacedEq_rhs_1
|
||||
spacedEq { n = (S k) } = ?spacedEq_rhs_2
|
||||
Spacing> s1Eq { n = 0} = ?s1Eq_rhs_1
|
||||
s1Eq { n = (S k)} = ?s1Eq_rhs_2
|
||||
Spacing> s2Eq { n = 0} = ?s2Eq_rhs_1
|
||||
s2Eq { n = (S k)} = ?s2Eq_rhs_2
|
||||
Spacing> s3Eq { n = 0} = ?s3Eq_rhs_1
|
||||
s3Eq { n = (S k)} = ?s3Eq_rhs_2
|
||||
Spacing> weirdNo {n = 0 } = ?weirdNo_rhs_1
|
||||
weirdNo {n = (S k) } = ?weirdNo_rhs_2
|
||||
Spacing> weird0a {n= 0} = ?weird0a_rhs_1
|
||||
weird0a {n= (S k)} = ?weird0a_rhs_2
|
||||
Spacing> weird0b {n =0} = ?weird0b_rhs_1
|
||||
weird0b {n =(S k)} = ?weird0b_rhs_2
|
||||
Spacing> weird1a { n= 0} = ?weird1a_rhs_1
|
||||
weird1a { n= (S k)} = ?weird1a_rhs_2
|
||||
Spacing> weird1b { n =0} = ?weird1b_rhs_1
|
||||
weird1b { n =(S k)} = ?weird1b_rhs_2
|
||||
Spacing> weird2a { n= 0} = ?weird2a_rhs_1
|
||||
weird2a { n= (S k)} = ?weird2a_rhs_2
|
||||
Spacing> weird2b { n =0} = ?weird2b_rhs_1
|
||||
weird2b { n =(S k)} = ?weird2b_rhs_2
|
||||
Spacing> weirdSpacedA { n= 0 } = ?weirdSpacedA_rhs_1
|
||||
weirdSpacedA { n= (S k) } = ?weirdSpacedA_rhs_2
|
||||
Spacing> weirdSpacedB { n =0 } = ?weirdSpacedB_rhs_1
|
||||
weirdSpacedB { n =(S k) } = ?weirdSpacedB_rhs_2
|
||||
Spacing> no {n = 0} = ?no_rhs_0
|
||||
no {n = (S k)} = ?no_rhs_1
|
||||
Spacing> spaced { n = 0 } = ?spaced_rhs_0
|
||||
spaced { n = (S k) } = ?spaced_rhs_1
|
||||
Spacing> s1 { n = 0} = ?s1_rhs_0
|
||||
s1 { n = (S k)} = ?s1_rhs_1
|
||||
Spacing> s2 { n = 0} = ?s2_rhs_0
|
||||
s2 { n = (S k)} = ?s2_rhs_1
|
||||
Spacing> s3 { n = 0} = ?s3_rhs_0
|
||||
s3 { n = (S k)} = ?s3_rhs_1
|
||||
Spacing> noSEq {n = 0} = ?noSEq_rhs_0
|
||||
noSEq {n = (S k)} = ?noSEq_rhs_1
|
||||
Spacing> spacedEq { n = 0 } = ?spacedEq_rhs_0
|
||||
spacedEq { n = (S k) } = ?spacedEq_rhs_1
|
||||
Spacing> s1Eq { n = 0} = ?s1Eq_rhs_0
|
||||
s1Eq { n = (S k)} = ?s1Eq_rhs_1
|
||||
Spacing> s2Eq { n = 0} = ?s2Eq_rhs_0
|
||||
s2Eq { n = (S k)} = ?s2Eq_rhs_1
|
||||
Spacing> s3Eq { n = 0} = ?s3Eq_rhs_0
|
||||
s3Eq { n = (S k)} = ?s3Eq_rhs_1
|
||||
Spacing> weirdNo {n = 0 } = ?weirdNo_rhs_0
|
||||
weirdNo {n = (S k) } = ?weirdNo_rhs_1
|
||||
Spacing> weird0a {n= 0} = ?weird0a_rhs_0
|
||||
weird0a {n= (S k)} = ?weird0a_rhs_1
|
||||
Spacing> weird0b {n =0} = ?weird0b_rhs_0
|
||||
weird0b {n =(S k)} = ?weird0b_rhs_1
|
||||
Spacing> weird1a { n= 0} = ?weird1a_rhs_0
|
||||
weird1a { n= (S k)} = ?weird1a_rhs_1
|
||||
Spacing> weird1b { n =0} = ?weird1b_rhs_0
|
||||
weird1b { n =(S k)} = ?weird1b_rhs_1
|
||||
Spacing> weird2a { n= 0} = ?weird2a_rhs_0
|
||||
weird2a { n= (S k)} = ?weird2a_rhs_1
|
||||
Spacing> weird2b { n =0} = ?weird2b_rhs_0
|
||||
weird2b { n =(S k)} = ?weird2b_rhs_1
|
||||
Spacing> weirdSpacedA { n= 0 } = ?weirdSpacedA_rhs_0
|
||||
weirdSpacedA { n= (S k) } = ?weirdSpacedA_rhs_1
|
||||
Spacing> weirdSpacedB { n =0 } = ?weirdSpacedB_rhs_0
|
||||
weirdSpacedB { n =(S k) } = ?weirdSpacedB_rhs_1
|
||||
Spacing> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
1/1: Building casefn (casefn.idr)
|
||||
Main> False => ?cfn_rhs_1
|
||||
True => ?cfn_rhs_2
|
||||
Main> False => ?cfn_rhs_0
|
||||
True => ?cfn_rhs_1
|
||||
Main> Bye for now!
|
||||
|
@ -1,34 +1,34 @@
|
||||
1/1: Building CS_Syntax (CS_Syntax.idr)
|
||||
Main> f n = case n of 0 => ?f_rhs_1
|
||||
(S k) => ?f_rhs_2
|
||||
Main> g n = (case n of 0 => ?g_rhs_1
|
||||
(S k) => ?g_rhs_2)
|
||||
Main> 0 => ?h_rhs_1
|
||||
(S k) => ?h_rhs_2 )
|
||||
Main> 0 => ?h_rhs_1
|
||||
(S k) => ?h_rhs_2 )
|
||||
Main> j_Where k = (case toTest k of One => ?j_Where_rhs_1
|
||||
(Two j) => ?j_Where_rhs_2
|
||||
(Three x j) => ?j_Where_rhs_3
|
||||
Four => ?j_Where_rhs_4 )
|
||||
Main> One => ?k_rhs_1
|
||||
(Two k) => ?k_rhs_2
|
||||
(Three x k) => ?k_rhs_3
|
||||
Four => ?k_rhs_4)
|
||||
Main> l n m = case n of foo => case toTest m of One => ?l_rhs_1
|
||||
(Two k) => ?l_rhs_2
|
||||
(Three x k) => ?l_rhs_3
|
||||
Four => ?l_rhs_4
|
||||
Main> m n k = (case n of foo => case toTest k of One => ?m_rhs_1
|
||||
(Two j) => ?m_rhs_2
|
||||
(Three x j) => ?m_rhs_3
|
||||
Four => ?m_rhs_4 )
|
||||
Main> One => ?n_rhs_1
|
||||
(Two j) => ?n_rhs_2
|
||||
(Three x j) => ?n_rhs_3
|
||||
Four => ?n_rhs_4
|
||||
Main> One => ?o_rhs_1
|
||||
(Two k) => ?o_rhs_2
|
||||
(Three x k) => ?o_rhs_3
|
||||
Four => ?o_rhs_4 )
|
||||
Main> f n = case n of 0 => ?f_rhs_0
|
||||
(S k) => ?f_rhs_1
|
||||
Main> g n = (case n of 0 => ?g_rhs_0
|
||||
(S k) => ?g_rhs_1)
|
||||
Main> 0 => ?h_rhs_0
|
||||
(S k) => ?h_rhs_1 )
|
||||
Main> 0 => ?h_rhs_0
|
||||
(S k) => ?h_rhs_1 )
|
||||
Main> j_Where k = (case toTest k of One => ?j_Where_rhs_0
|
||||
(Two j) => ?j_Where_rhs_1
|
||||
(Three x j) => ?j_Where_rhs_2
|
||||
Four => ?j_Where_rhs_3 )
|
||||
Main> One => ?k_rhs_0
|
||||
(Two k) => ?k_rhs_1
|
||||
(Three x k) => ?k_rhs_2
|
||||
Four => ?k_rhs_3)
|
||||
Main> l n m = case n of foo => case toTest m of One => ?l_rhs_0
|
||||
(Two k) => ?l_rhs_1
|
||||
(Three x k) => ?l_rhs_2
|
||||
Four => ?l_rhs_3
|
||||
Main> m n k = (case n of foo => case toTest k of One => ?m_rhs_0
|
||||
(Two j) => ?m_rhs_1
|
||||
(Three x j) => ?m_rhs_2
|
||||
Four => ?m_rhs_3 )
|
||||
Main> One => ?n_rhs_0
|
||||
(Two j) => ?n_rhs_1
|
||||
(Three x j) => ?n_rhs_2
|
||||
Four => ?n_rhs_3
|
||||
Main> One => ?o_rhs_0
|
||||
(Two k) => ?o_rhs_1
|
||||
(Three x k) => ?o_rhs_2
|
||||
Four => ?o_rhs_3 )
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.lidr)
|
||||
Main> > append {n = 0} [] ys = ?foo_1
|
||||
> append {n = (S k)} (x :: xs) ys = ?foo_2
|
||||
Main> > vadd [] [] = ?bar_1
|
||||
Main> > vadd (x :: xs) (y :: ys) = ?baz_1
|
||||
Main> > suc x x Refl = ?quux_1
|
||||
Main> > suc' {x = x} {y = x} Refl = ?quuz_1
|
||||
Main> > append {n = 0} [] ys = ?foo_0
|
||||
> append {n = (S k)} (x :: xs) ys = ?foo_1
|
||||
Main> > vadd [] [] = ?bar_0
|
||||
Main> > vadd (x :: xs) (y :: ys) = ?baz_0
|
||||
Main> > suc x x Refl = ?quux_0
|
||||
Main> > suc' {x = x} {y = x} Refl = ?quuz_0
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.lidr)
|
||||
Main> > [] => ?bar_1
|
||||
> (x :: zs) => ?bar_2
|
||||
Main> > map f (MkFoo x) = ?baz_1
|
||||
> map f (MkBar g) = ?baz_2
|
||||
Main> > [] => ?bar_0
|
||||
> (x :: zs) => ?bar_1
|
||||
Main> > map f (MkFoo x) = ?baz_0
|
||||
> map f (MkBar g) = ?baz_1
|
||||
Main> Bye for now!
|
||||
1/1: Building IEdit2 (IEdit2.lidr)
|
||||
Main> > (x :: []) => ?bar_5
|
||||
|
@ -1,5 +1,5 @@
|
||||
1/1: Building Door (Door.lidr)
|
||||
Main> > (val # y) => ?now_4
|
||||
Main> > (val # y) => ?now_0
|
||||
Main> > (False # d) => ?now_4
|
||||
> (True # d) => ?now_5
|
||||
Main> 0 m : Type -> Type
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.org)
|
||||
Main> append {n = 0} [] ys = ?foo_1
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_2
|
||||
Main> vadd [] [] = ?bar_1
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_1
|
||||
Main> suc x x Refl = ?quux_1
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_1
|
||||
Main> append {n = 0} [] ys = ?foo_0
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_1
|
||||
Main> vadd [] [] = ?bar_0
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_0
|
||||
Main> suc x x Refl = ?quux_0
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_0
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building IEdit (IEdit.org)
|
||||
Main> append {n = 0} [] ys = ?foo_1
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_2
|
||||
Main> vadd [] [] = ?bar_1
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_1
|
||||
Main> suc x x Refl = ?quux_1
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_1
|
||||
Main> append {n = 0} [] ys = ?foo_0
|
||||
append {n = (S k)} (x :: xs) ys = ?foo_1
|
||||
Main> vadd [] [] = ?bar_0
|
||||
Main> vadd (x :: xs) (y :: ys) = ?baz_0
|
||||
Main> suc x x Refl = ?quux_0
|
||||
Main> suc' {x = x} {y = x} Refl = ?quuz_0
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
1/1: Building casesplit (casesplit.idr)
|
||||
Main> foo False = ?help_1
|
||||
foo True = ?help_2
|
||||
Main> foo False = ?help_0
|
||||
foo True = ?help_1
|
||||
Main> Bye for now!
|
||||
|
Loading…
Reference in New Issue
Block a user