idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #239 from MarcelineVQ/elab-changes

Browse Source 
add parens for some TTImp Shows
This commit is contained in:
Edwin Brady 2020-06-08 11:54:19 +01:00 committed by GitHub
commit 73de552776
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 15 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/TTImp/TTImp.idr
View File

@ -125,11 +125,11 @@ mutual
Show RawImp where
show (IVar fc n) = show n
show (IPi fc c p n arg ret)
= "(%pi " ++ show c ++ " " ++ show p ++
" " ++ show n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
= "(%pi " ++ show c ++ " " ++ show p ++ " " ++
showPrec App n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
show (ILam fc c p n arg sc)
= "(%lam " ++ show c ++ " " ++ show p ++
" " ++ show n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
= "(%lam " ++ show c ++ " " ++ show p ++ " " ++
showPrec App n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
show (ILet fc c n ty val sc)
= "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
" " ++ show val ++ " " ++ show sc ++ ")"

4
tests/idris2/reflection003/expected
View File

@ -1,8 +1,8 @@
1/1: Building refprims (refprims.idr)
LOG 0: Name: Prelude.List.++
LOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just _) (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
LOG 0: Name: Prelude.Strings.++
LOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))
LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
LOG 0: Resolved name: Prelude.Nat
LOG 0: Constructors: [Prelude.Z, Prelude.S]
refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:

4
tests/ttimp/basic003/expected
View File

@ -1,8 +1,8 @@
Processing as TTImp
Written TTC
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
Yaffle> Bye for now!
Processing as TTC
Read TTC
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
Yaffle> Bye for now!

2
tests/ttimp/eta001/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> ((Main.Refl [Just {b:10} = 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> 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!

8
tests/ttimp/qtt001/expected
View File

@ -1,8 +1,8 @@
Processing as TTImp
QTT.yaff:14:1--16:1:When elaborating right hand side of Main.dupbad:
QTT.yaff:14:13--16:1:There are 2 uses of linear name x
Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
Yaffle> Main.baz1 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
Yaffle> Main.baz2 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
Yaffle> Main.foo : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
Yaffle> Main.bar : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
Yaffle> Main.baz1 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
Yaffle> Main.baz2 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
Yaffle> Bye for now!

4
tests/ttimp/record002/expected
View File

@ -1,7 +1,7 @@
Processing as TTImp
Written TTC
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 11) 10))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 10) 94))
Yaffle> Bye for now!