1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
module Encoded.Test
import Data.Stream
import Data.String
import Encoded.Arith
import Encoded.Container
import Encoded.Fin
import Encoded.Pair
import Encoded.Sum
import Encoded.Term
import Encoded.Vect
import System
import Term.Compile
import Term.Pretty
import Term.Syntax
import Term.Semantics
%ambiguity_depth 4
-- ListC : Ty -> Container
-- ListC ty = Cases [<(Nothing, 0), (Just ty, 1)]
-- List : Ty -> Ty
-- List = W . ListC
-- nil : {ty : Ty} -> Term (List ty) ctx
-- nil = App (intro . tag (There Here)) [<Vect.nil {ty = List ty}]
-- cons : {ty : Ty} -> Term (ty ~> List ty ~> List ty) ctx
-- cons = AbsAll [<_, _] (\[<x, xs] =>
-- App (intro . tag @{IsSnoc} Here) [<App pair [<x, App Vect.cons [<xs, Vect.nil]]])
-- sum : Term (List N ~> N) ctx
-- sum = App (elim {c = ListC N})
-- [<Const 0
-- , Abs' (\x => App fst x + App index [<App snd [<x], zero])
-- ]
-- fromList' : List Nat -> Term (List N) [<List N, N ~> List N ~> List N]
-- fromList' [] = Var (There Here)
-- fromList' (x :: xs) = App (Var Here) [<Op (Lit x), fromList' xs]
-- fromList : List Nat -> Term (List N) [<]
-- fromList xs = App (Abs $ Abs $ fromList' xs) [<Test.nil, Test.cons]
%inline
layoutOptions : LayoutOptions
layoutOptions = MkLayoutOptions (AvailablePerLine 213 0.5)
data Mode = Color | NoColor | FastCompile | Compile | Profile
%inline
render : Len ctx => Mode -> Term ty ctx -> IO ()
render Color t =
renderIO $
layoutSmart layoutOptions $ prettyTerm t
render NoColor t =
putStrLn $
renderShow (layoutSmart layoutOptions $ prettyTerm {ann = ()} t) ""
render _ t = pure ()
run : Show (TypeOf ty) => Len ctx => Mode -> Term ty ctx -> All TypeOf ctx -> IO ()
run FastCompile t args =
putStrLn $
renderShow (layoutCompact $ compileTerm {ann = ()} Run t) ""
run Compile t args =
putStrLn $
renderShow (layoutSmart layoutOptions $ compileTerm {ann = ()} Run t) ""
run Profile t args =
putStrLn $
renderShow (layoutSmart layoutOptions $ compileTerm {ann = ()} Profile t) ""
run _ t args = printLn (sem t args)
parseArgs : List String -> IO (Mode, Bool, Nat, Nat)
parseArgs [_, "--color", k, n] = pure (Color, True, stringToNatOrZ k, stringToNatOrZ n)
parseArgs [_, "--no-color", k, n] = pure (NoColor, True, stringToNatOrZ k, stringToNatOrZ n)
parseArgs [_, "--fast-compile", k, n] = pure (FastCompile, False, stringToNatOrZ k, stringToNatOrZ n)
parseArgs [_, "--compile", k, n] = pure (Compile, False, stringToNatOrZ k, stringToNatOrZ n)
parseArgs [_, "--profile", k, n] = pure (Profile, False, stringToNatOrZ k, stringToNatOrZ n)
parseArgs [_, k, n] = pure (Color, False, stringToNatOrZ k, stringToNatOrZ n)
parseArgs _ = do putStrLn "Bad arguments"; exitFailure
lit : Term (N ~> Term) ctx
lit = Abs' (\n => Rec n Zero Suc)
add : Term (N ~> N ~> Term) ctx
add = AbsAll [<_,_] (\[<k, n] =>
App Rec [<App lit [<k], App lit [<n], App (Abs . Suc . Var) [<0]])
AssumeNat : Eliminator N ctx
AssumeNat =
MkElim
{ var = Arb
, zero = 0
, suc = Op Suc
, rec = Arb
, abs = Arb
, app = Arb
}
main : IO ()
main = do
args <- getArgs
(mode, print, k, n) <- parseArgs args
let t : Term Term [<] = App add [<Op (Lit k), Op (Lit n)]
let t : Term Term [<] = App reduce [<4096, t]
if print then render mode t else pure ()
let t : Term N [<] = App Elim [<pack AssumeNat, t]
run mode t [<]
-- let ns = take n nats
-- let t : Term (List N) [<] = fromList ns
-- let t : Term N [<] = App sum [<t]
|
