mirror of
https://github.com/anoma/juvix.git
synced 2024-10-26 17:52:17 +03:00
Fix: format juvix files in test/positive (#1978)
This PR fixes a formatting issue that drops blank lines between axiom declarations. It goes after: - #1980 - Closes https://github.com/anoma/juvix/issues/1986
This commit is contained in:
parent
b14a81a81d
commit
4d0267ebb9
6
.github/workflows/ci.yml
vendored
6
.github/workflows/ci.yml
vendored
@ -23,7 +23,7 @@ concurrency:
|
||||
cancel-in-progress: true
|
||||
|
||||
env:
|
||||
SKIP: ormolu,format-juvix-examples,typecheck-juvix-examples
|
||||
SKIP: ormolu,format-juvix-files,typecheck-juvix-examples
|
||||
|
||||
jobs:
|
||||
pre-commit:
|
||||
@ -119,7 +119,7 @@ jobs:
|
||||
continue-on-error: true
|
||||
run: |
|
||||
cd main
|
||||
make check-format-juvix-examples
|
||||
make check-format-juvix-files
|
||||
make typecheck-juvix-examples
|
||||
|
||||
- name: Add ~/.local/bin to PATH
|
||||
@ -317,7 +317,7 @@ jobs:
|
||||
if: ${{ success() }}
|
||||
run: |
|
||||
cd main
|
||||
make -s check-format-juvix-examples
|
||||
make -s check-format-juvix-files
|
||||
make -s typecheck-juvix-examples
|
||||
|
||||
- name: Install Smoke
|
||||
|
@ -42,9 +42,9 @@ repos:
|
||||
|
||||
- repo: local
|
||||
hooks:
|
||||
- id: format-juvix-examples
|
||||
- id: format-juvix-files
|
||||
name: format Juvix examples
|
||||
entry: make -s format-juvix-examples
|
||||
entry: make -s format-juvix-files
|
||||
language: system
|
||||
verbose: false
|
||||
pass_filenames: false
|
||||
|
20
Makefile
20
Makefile
@ -10,7 +10,7 @@ EXAMPLES= Collatz/Collatz.juvix \
|
||||
HelloWorld/HelloWorld.juvix \
|
||||
PascalsTriangle/PascalsTriangle.juvix \
|
||||
TicTacToe/CLI/TicTacToe.juvix \
|
||||
Tutorial/Tutorial.juvix \
|
||||
Tutorial/Tutorial.juvix
|
||||
|
||||
DEMO_EXAMPLE=examples/demo/Demo.juvix
|
||||
|
||||
@ -130,20 +130,22 @@ format:
|
||||
clang-format:
|
||||
@cd runtime && ${MAKE} format
|
||||
|
||||
JUVIXEXAMPLEFILES=$(shell find ./examples -name "*.juvix" -print)
|
||||
JUVIXFILESTOFORMAT=$(shell find ./examples ./tests/positive -type d -name ".juvix-build" -prune -o -type f -name "*.juvix" -print)
|
||||
JUVIXFORMATFLAGS?=--in-place
|
||||
JUVIXTYPECHECKFLAGS?=--only-errors
|
||||
|
||||
.PHONY: format-juvix-examples
|
||||
format-juvix-examples:
|
||||
@for file in $(JUVIXEXAMPLEFILES); do \
|
||||
${JUVIXBIN} format $(JUVIXFORMATFLAGS) "$$file"; \
|
||||
.PHONY: format-juvix-files
|
||||
format-juvix-files:
|
||||
@for file in $(JUVIXFILESTOFORMAT); do \
|
||||
juvix format $(JUVIXFORMATFLAGS) "$$file"; \
|
||||
done
|
||||
|
||||
.PHONY: check-format-juvix-examples
|
||||
check-format-juvix-examples:
|
||||
.PHONY: check-format-juvix-files
|
||||
check-format-juvix-files:
|
||||
@export JUVIXFORMATFLAGS=--check
|
||||
@${MAKE} format-juvix-examples
|
||||
@make format-juvix-files
|
||||
|
||||
JUVIXEXAMPLEFILES=$(shell find ./examples -name "*.juvix" -print)
|
||||
|
||||
.PHONY: typecheck-juvix-examples
|
||||
typecheck-juvix-examples:
|
||||
|
@ -82,7 +82,7 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
|
||||
(StatementOpenModule {}, _) -> False
|
||||
(StatementInductive {}, _) -> False
|
||||
(StatementModule {}, _) -> False
|
||||
(StatementAxiom {}, StatementAxiom {}) -> True
|
||||
(StatementAxiom {}, StatementAxiom {}) -> False
|
||||
(StatementAxiom {}, _) -> False
|
||||
(StatementTypeSignature sig, StatementFunctionClause fun) ->
|
||||
case sing :: SStage s of
|
||||
|
@ -177,11 +177,10 @@ instance PrettyPrint (AxiomDef 'Scoped) where
|
||||
axiomName' <- P.annDef _axiomName <$> P.ppSymbol _axiomName
|
||||
let builtin' :: Maybe (Sem r ()) = (<> line) . (\x -> P.ppCode x >>= morpheme (getLoc x)) <$> _axiomBuiltin
|
||||
_axiomDoc' :: Maybe (Sem r ()) = ppCode <$> _axiomDoc
|
||||
axiom' = (<> line) . ppCode $ _axiomKw
|
||||
_axiomDoc'
|
||||
?<> builtin'
|
||||
?<> axiom'
|
||||
<> morpheme (getLoc _axiomName) axiomName'
|
||||
?<> ppCode _axiomKw
|
||||
<+> morpheme (getLoc _axiomName) axiomName'
|
||||
<+> noLoc P.kwColon
|
||||
<+> ppCode _axiomType
|
||||
|
||||
|
@ -1,14 +1,12 @@
|
||||
module M;
|
||||
|
||||
type Bool :=
|
||||
true : Bool
|
||||
| true : Bool
|
||||
| false : Bool;
|
||||
|
||||
type Pair (A : Type) (B : Type) :=
|
||||
mkPair : A → B → Pair A B;
|
||||
| mkPair : A → B → Pair A B;
|
||||
|
||||
f : _ → _;
|
||||
f (mkPair false true) := true;
|
||||
f _ := false;
|
||||
|
||||
end;
|
||||
|
@ -1,14 +1,14 @@
|
||||
module M;
|
||||
|
||||
type Bool :=
|
||||
true : Bool
|
||||
| true : Bool
|
||||
| false : Bool;
|
||||
|
||||
type T :=
|
||||
t : T;
|
||||
| t : T;
|
||||
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| zero : Nat
|
||||
| suc : Nat → Nat;
|
||||
|
||||
f : _;
|
||||
@ -16,9 +16,7 @@ f false false := true;
|
||||
f true _ := false;
|
||||
|
||||
type Pair (A : Type) (B : Type) :=
|
||||
mkPair : A → B → Pair A B;
|
||||
| mkPair : A → B → Pair A B;
|
||||
|
||||
g : _;
|
||||
g (mkPair (mkPair zero false) true) := mkPair false zero;
|
||||
|
||||
end;
|
||||
|
@ -1,36 +1,30 @@
|
||||
module Ape;
|
||||
|
||||
builtin string
|
||||
axiom
|
||||
String : Type;
|
||||
axiom String : Type;
|
||||
|
||||
infixl 7 *;
|
||||
axiom
|
||||
* : String → String → String;
|
||||
axiom * : String → String → String;
|
||||
|
||||
infixr 3 -;
|
||||
axiom
|
||||
- : String → String → String;
|
||||
axiom - : String → String → String;
|
||||
|
||||
infixl 1 >>;
|
||||
axiom
|
||||
>> : String → String → String;
|
||||
axiom >> : String → String → String;
|
||||
|
||||
infixl 6 +;
|
||||
axiom
|
||||
+ : String → String → String;
|
||||
axiom + : String → String → String;
|
||||
|
||||
infixr 6 ++;
|
||||
axiom
|
||||
++ : String → String → String;
|
||||
axiom
|
||||
f : String → String;
|
||||
axiom ++ : String → String → String;
|
||||
|
||||
axiom f : String → String;
|
||||
|
||||
x : String;
|
||||
x := "" + ("" ++ "");
|
||||
|
||||
axiom
|
||||
wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String → String;
|
||||
axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String
|
||||
→ String;
|
||||
|
||||
nesting : String;
|
||||
nesting :=
|
||||
|
@ -1,4 +1,3 @@
|
||||
module Axiom;
|
||||
|
||||
axiom
|
||||
Action : Type;
|
||||
axiom Action : Type;
|
||||
|
@ -1,5 +1,3 @@
|
||||
module A;
|
||||
|
||||
import Nat;
|
||||
|
||||
end;
|
||||
|
@ -2,5 +2,3 @@ module Input;
|
||||
|
||||
import A;
|
||||
import Nat;
|
||||
|
||||
end;
|
||||
|
@ -2,7 +2,5 @@ module Nat;
|
||||
|
||||
builtin nat
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| zero : Nat
|
||||
| suc : Nat → Nat;
|
||||
|
||||
end;
|
||||
|
@ -1,5 +1,3 @@
|
||||
module A;
|
||||
|
||||
open import Nat;
|
||||
|
||||
end;
|
||||
|
@ -2,5 +2,3 @@ module Input;
|
||||
|
||||
open import A;
|
||||
open import Nat;
|
||||
|
||||
end;
|
||||
|
@ -2,7 +2,5 @@ module Nat;
|
||||
|
||||
builtin nat
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| zero : Nat
|
||||
| suc : Nat → Nat;
|
||||
|
||||
end;
|
||||
|
@ -1,5 +1,3 @@
|
||||
module Base;
|
||||
|
||||
axiom Base : Type;
|
||||
|
||||
end;
|
||||
|
@ -5,5 +5,3 @@ open import Base;
|
||||
axiom Extra : Type;
|
||||
|
||||
axiom _A : Base;
|
||||
|
||||
end;
|
||||
|
@ -13,8 +13,7 @@ go n s :=
|
||||
|
||||
module M;
|
||||
infixr 4 ,;
|
||||
axiom
|
||||
, : String → String → String;
|
||||
axiom , : String → String → String;
|
||||
end;
|
||||
|
||||
-- qualified commas
|
||||
@ -48,24 +47,19 @@ t3 :=
|
||||
, "1234";
|
||||
|
||||
infixl 7 +l7;
|
||||
axiom
|
||||
+l7 : String → String → String;
|
||||
axiom +l7 : String → String → String;
|
||||
|
||||
infixr 3 +r3;
|
||||
axiom
|
||||
+r3 : String → String → String;
|
||||
axiom +r3 : String → String → String;
|
||||
|
||||
infixl 1 +l1;
|
||||
axiom
|
||||
+l1 : String → String → String;
|
||||
axiom +l1 : String → String → String;
|
||||
|
||||
infixl 6 +l6;
|
||||
axiom
|
||||
+l6 : String → String → String;
|
||||
axiom +l6 : String → String → String;
|
||||
|
||||
infixr 6 +r6;
|
||||
axiom
|
||||
+r6 : String → String → String;
|
||||
axiom +r6 : String → String → String;
|
||||
|
||||
-- nesting of chains
|
||||
t : String;
|
||||
|
@ -8,8 +8,7 @@ module M;
|
||||
end;
|
||||
|
||||
infixr 2 +;
|
||||
axiom
|
||||
+ : Type → Type → Type;
|
||||
axiom + : Type → Type → Type;
|
||||
end;
|
||||
|
||||
import M;
|
||||
|
@ -11,12 +11,14 @@ infixr 9 ∘;
|
||||
→ C;
|
||||
∘ {_} {B} {_} f g x := f (g x);
|
||||
|
||||
builtin nat type Nat :=
|
||||
builtin nat
|
||||
type Nat :=
|
||||
| zero : Nat
|
||||
| suc : Nat → Nat;
|
||||
|
||||
infixl 6 +;
|
||||
builtin nat-plus + : Nat → Nat → Nat;
|
||||
builtin nat-plus
|
||||
+ : Nat → Nat → Nat;
|
||||
+ zero b := b;
|
||||
+ (suc a) b := suc (a + b);
|
||||
|
||||
|
@ -1,6 +1,7 @@
|
||||
module LiteralString;
|
||||
|
||||
builtin string axiom String : Type;
|
||||
builtin string
|
||||
axiom String : Type;
|
||||
|
||||
type A :=
|
||||
| a : A;
|
||||
|
@ -1,14 +1,13 @@
|
||||
module E5;
|
||||
|
||||
type T0 (A : Type) :=
|
||||
c0 : (A -> T0 A) -> T0 A;
|
||||
| c0 : (A -> T0 A) -> T0 A;
|
||||
|
||||
axiom B : Type;
|
||||
|
||||
type T1 (A : Type) :=
|
||||
c1 : (B -> T0 A) -> T1 A;
|
||||
| c1 : (B -> T0 A) -> T1 A;
|
||||
|
||||
positive
|
||||
type T2 :=
|
||||
c2 : (B -> (B -> T1 T2)) -> T2;
|
||||
|
||||
end;
|
||||
| c2 : (B -> B -> T1 T2) -> T2;
|
||||
|
@ -1,6 +1,7 @@
|
||||
module Judoc;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
axiom b : Type;
|
||||
|
||||
type T :=
|
||||
|
@ -1,11 +1,10 @@
|
||||
module Literals;
|
||||
|
||||
axiom
|
||||
Int : Type;
|
||||
axiom
|
||||
String : Type;
|
||||
axiom
|
||||
+ : Int → Int → Int;
|
||||
axiom Int : Type;
|
||||
|
||||
axiom String : Type;
|
||||
|
||||
axiom + : Int → Int → Int;
|
||||
|
||||
a : Int;
|
||||
a := 12313;
|
||||
|
@ -1,8 +1,7 @@
|
||||
module Operators;
|
||||
|
||||
infixl 5 +;
|
||||
axiom
|
||||
+ : Type → Type → Type;
|
||||
axiom + : Type → Type → Type;
|
||||
|
||||
plus : Type → Type → Type;
|
||||
plus := (+);
|
||||
|
@ -1,8 +1,7 @@
|
||||
module M;
|
||||
|
||||
module O;
|
||||
axiom
|
||||
A : Type;
|
||||
axiom A : Type;
|
||||
end;
|
||||
|
||||
open O;
|
||||
|
@ -2,8 +2,7 @@ module M;
|
||||
|
||||
module N;
|
||||
module O;
|
||||
axiom
|
||||
A : Type;
|
||||
axiom A : Type;
|
||||
end;
|
||||
end;
|
||||
|
||||
@ -13,5 +12,4 @@ module O;
|
||||
|
||||
end;
|
||||
|
||||
axiom
|
||||
B : O.A;
|
||||
axiom B : O.A;
|
||||
|
@ -3,9 +3,7 @@ module N;
|
||||
import M;
|
||||
|
||||
module M;
|
||||
axiom
|
||||
A : Type;
|
||||
axiom A : Type;
|
||||
end;
|
||||
|
||||
axiom
|
||||
B : M.A;
|
||||
axiom B : M.A;
|
||||
|
@ -1,20 +1,17 @@
|
||||
module Data.Bool;
|
||||
|
||||
type Bool :=
|
||||
true : Bool |
|
||||
false : Bool;
|
||||
| true : Bool
|
||||
| false : Bool;
|
||||
|
||||
not : Bool → Bool;
|
||||
not true := false;
|
||||
not false := true;
|
||||
|
||||
-- infixr 2 ||;
|
||||
-- || : Bool → Bool → Bool;
|
||||
-- || false a := a;
|
||||
-- || true _ := true;
|
||||
|
||||
-- infixr 2 &&;
|
||||
-- && : Bool → Bool → Bool;
|
||||
-- && false _ := false;
|
||||
-- && true a := a;
|
||||
|
||||
end;
|
||||
|
@ -1,7 +1,5 @@
|
||||
module Data.Maybe;
|
||||
|
||||
type Maybe (a : Type) :=
|
||||
nothing : Maybe a |
|
||||
just : a → Maybe a;
|
||||
|
||||
end;
|
||||
| nothing : Maybe a
|
||||
| just : a → Maybe a;
|
||||
|
@ -1,7 +1,8 @@
|
||||
module Data.Nat;
|
||||
|
||||
type ℕ :=
|
||||
zero : ℕ |
|
||||
suc : ℕ → ℕ;
|
||||
| zero : ℕ
|
||||
| suc : ℕ → ℕ;
|
||||
|
||||
infixl 6 +;
|
||||
+ : ℕ → ℕ → ℕ;
|
||||
@ -12,5 +13,3 @@ module Data.Nat;
|
||||
* : ℕ → ℕ → ℕ;
|
||||
* zero b := zero;
|
||||
* (suc a) b := b + a * b;
|
||||
|
||||
end;
|
||||
|
@ -1,6 +1,6 @@
|
||||
module Data.Ord;
|
||||
|
||||
type Ordering :=
|
||||
LT : Ordering |
|
||||
EQ : Ordering |
|
||||
GT : Ordering;
|
||||
end;
|
||||
| LT : Ordering
|
||||
| EQ : Ordering
|
||||
| GT : Ordering;
|
||||
|
@ -2,6 +2,4 @@ module Data.Product;
|
||||
|
||||
infixr 2 ×;
|
||||
type × (a : Type) (b : Type) :=
|
||||
, : a → b → a × b;
|
||||
|
||||
end;
|
||||
| , : a → b → a × b;
|
||||
|
@ -14,5 +14,3 @@ g x y := f y;
|
||||
|
||||
h : {A : Type} -> A -> Maybe Bool;
|
||||
h x := nothing;
|
||||
|
||||
end;
|
||||
|
@ -7,6 +7,4 @@ test : {A : Type} -> A -> A;
|
||||
test x := x;
|
||||
|
||||
type Unit :=
|
||||
unit : Unit;
|
||||
|
||||
end;
|
||||
| unit : Unit;
|
||||
|
@ -5,5 +5,3 @@ open import Stdlib.Prelude;
|
||||
|
||||
k : Bool;
|
||||
k := true;
|
||||
|
||||
end;
|
||||
|
@ -2,8 +2,7 @@ module ShadowPublicOpen;
|
||||
|
||||
module M;
|
||||
module N;
|
||||
axiom
|
||||
A : Type;
|
||||
axiom A : Type;
|
||||
end;
|
||||
|
||||
open N public;
|
||||
@ -11,5 +10,4 @@ end;
|
||||
|
||||
open M;
|
||||
|
||||
axiom
|
||||
A : Type;
|
||||
axiom A : Type;
|
||||
|
@ -1,5 +1,4 @@
|
||||
module A;
|
||||
|
||||
type Foo := bar : Foo;
|
||||
|
||||
end;
|
||||
type Foo :=
|
||||
| bar : Foo;
|
||||
|
@ -1,4 +1,5 @@
|
||||
module StdlibImport;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
import A;
|
||||
@ -8,4 +9,3 @@ module StdlibImport;
|
||||
|
||||
foo : A.Foo;
|
||||
foo := A.bar;
|
||||
end;
|
||||
|
@ -29,8 +29,7 @@ infixl 7 ·;
|
||||
主功能 : Nat;
|
||||
主功能 := (0);
|
||||
|
||||
axiom
|
||||
= : Type;
|
||||
axiom = : Type;
|
||||
|
||||
K : Nat → Nat → Nat;
|
||||
K =a@zero (=) := =a · =;
|
||||
|
@ -1,4 +1,5 @@
|
||||
module Ack;
|
||||
|
||||
import Data.Nat;
|
||||
open Data.Nat;
|
||||
|
||||
@ -6,5 +7,3 @@ module Ack;
|
||||
ack zero n := suc n;
|
||||
ack (suc m) zero := ack m (suc zero);
|
||||
ack (suc m) (suc n) := ack m (ack (suc m) n);
|
||||
|
||||
end;
|
||||
|
@ -1,7 +1,8 @@
|
||||
module Data.Bool;
|
||||
|
||||
type Bool :=
|
||||
true : Bool |
|
||||
false : Bool;
|
||||
| true : Bool
|
||||
| false : Bool;
|
||||
|
||||
not : Bool → Bool;
|
||||
not true := false;
|
||||
@ -20,5 +21,3 @@ module Data.Bool;
|
||||
ite : {a : Type} → Bool → a → a → a;
|
||||
ite true a _ := a;
|
||||
ite false _ b := b;
|
||||
|
||||
end;
|
||||
|
@ -7,15 +7,17 @@ import Data.Nat;
|
||||
open Data.Nat;
|
||||
|
||||
type List (A : Type) :=
|
||||
nil : List A |
|
||||
cons : A → List A → List A;
|
||||
| nil : List A
|
||||
| cons : A → List A → List A;
|
||||
|
||||
-- Do not remove implicit arguments. Useful for testing.
|
||||
foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
|
||||
foldr :
|
||||
{A : Type} → {B : Type} → (A → B → B) → B → List A → B;
|
||||
foldr _ z nil := z;
|
||||
foldr f z (cons h hs) := f h (foldr {_} f z hs);
|
||||
|
||||
foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
|
||||
foldl :
|
||||
{A : Type} → {B : Type} → (B → A → B) → B → List A → B;
|
||||
foldl f z nil := z;
|
||||
foldl {_} {_} f z (cons h hs) := foldl {_} f (f z h) hs;
|
||||
|
||||
@ -25,9 +27,8 @@ map f (cons h hs) := cons (f h) (map f hs);
|
||||
|
||||
filter : {A : Type} → (A → Bool) → List A → List A;
|
||||
filter f nil := nil;
|
||||
filter f (cons h hs) := ite (f h)
|
||||
(cons h (filter {_} f hs))
|
||||
(filter f hs);
|
||||
filter f (cons h hs) :=
|
||||
ite (f h) (cons h (filter {_} f hs)) (filter f hs);
|
||||
|
||||
length : {A : Type} → List A → ℕ;
|
||||
length nil := zero;
|
||||
@ -51,5 +52,3 @@ take _ _ := nil;
|
||||
concat : {A : Type} → List A → List A → List A;
|
||||
concat nil ys := ys;
|
||||
concat (cons x xs) ys := cons x (concat xs ys);
|
||||
|
||||
end;
|
||||
|
@ -1,7 +1,8 @@
|
||||
module Data.Nat;
|
||||
|
||||
type ℕ :=
|
||||
zero : ℕ |
|
||||
suc : ℕ → ℕ;
|
||||
| zero : ℕ
|
||||
| suc : ℕ → ℕ;
|
||||
|
||||
infixl 6 +;
|
||||
+ : ℕ → ℕ → ℕ;
|
||||
@ -17,6 +18,7 @@ module Data.Nat;
|
||||
open Data.Bool;
|
||||
|
||||
even : ℕ → Bool;
|
||||
|
||||
odd : ℕ → Bool;
|
||||
|
||||
even zero := true;
|
||||
@ -24,4 +26,3 @@ module Data.Nat;
|
||||
|
||||
odd zero := false;
|
||||
odd (suc n) := even n;
|
||||
end;
|
||||
|
@ -1,7 +1,7 @@
|
||||
module Fib;
|
||||
|
||||
type Nat :=
|
||||
zero : Nat
|
||||
| zero : Nat
|
||||
| suc : Nat → Nat;
|
||||
|
||||
infixl 6 +;
|
||||
@ -11,7 +11,5 @@ infixl 6 +;
|
||||
|
||||
fib : Nat -> Nat;
|
||||
fib zero := zero;
|
||||
fib (suc (zero)) := suc zero;
|
||||
fib (suc zero) := suc zero;
|
||||
fib (suc (suc n)) := fib (suc n) + fib n;
|
||||
|
||||
end;
|
||||
|
@ -2,10 +2,11 @@ module Mutual;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
terminating f : A -> A -> A;
|
||||
terminating g : A -> A -> A;
|
||||
terminating
|
||||
f : A -> A -> A;
|
||||
|
||||
terminating
|
||||
g : A -> A -> A;
|
||||
g x y := f x x;
|
||||
f x y := g x (f x x);
|
||||
|
||||
end;
|
||||
f x y := g x (f x x);
|
||||
|
@ -1,4 +1,5 @@
|
||||
module TreeGen;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
type Tree :=
|
||||
@ -14,4 +15,3 @@ module TreeGen;
|
||||
gen2 zero := leaf;
|
||||
gen2 (suc zero) := node leaf leaf;
|
||||
gen2 (suc n@(suc n')) := node (gen2 n') (gen2 n);
|
||||
end;
|
||||
|
@ -1,7 +1,7 @@
|
||||
module Undefined;
|
||||
|
||||
axiom A : Type;
|
||||
terminating undefined : A;
|
||||
undefined := undefined;
|
||||
|
||||
end;
|
||||
terminating
|
||||
undefined : A;
|
||||
undefined := undefined;
|
||||
|
@ -1,6 +1,4 @@
|
||||
module M;
|
||||
|
||||
type T (A : Type) :=
|
||||
c : T _;
|
||||
|
||||
end;
|
||||
| c : T _;
|
||||
|
@ -1,8 +1,8 @@
|
||||
module M;
|
||||
|
||||
type ℕ :=
|
||||
z : ℕ |
|
||||
s : ℕ → ℕ;
|
||||
| z : ℕ
|
||||
| s : ℕ → ℕ;
|
||||
|
||||
nat : Type;
|
||||
nat := ℕ;
|
||||
@ -14,5 +14,3 @@ infixl 1 +;
|
||||
+ : nat2 → nat → nat;
|
||||
+ z b := b;
|
||||
+ (s a) b := s (a + b);
|
||||
|
||||
end;
|
||||
|
@ -1,7 +1,15 @@
|
||||
module M;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
|
||||
S : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → (A → B) → A → C;
|
||||
S :
|
||||
{A : Type}
|
||||
→ {B : Type}
|
||||
→ {C : Type}
|
||||
→ (A → B → C)
|
||||
→ (A → B)
|
||||
→ A
|
||||
→ C;
|
||||
S x y z := x z (y z);
|
||||
|
||||
K : {A : Type} → {B : Type} → A → B → A;
|
||||
@ -11,12 +19,11 @@ module M;
|
||||
I := S K (K {_} {Bool});
|
||||
|
||||
main : IO;
|
||||
main := printNatLn
|
||||
main :=
|
||||
printNatLn
|
||||
$ I {Nat} 1
|
||||
+ I I 1
|
||||
+ I (I 1)
|
||||
+ I 1
|
||||
+ I (I I) I (I I I) 1
|
||||
+ I I I (I I I (I I)) I (I I) I I I 1;
|
||||
|
||||
end;
|
||||
|
@ -1,11 +1,13 @@
|
||||
module builtinFail;
|
||||
|
||||
open import Stdlib.Data.String;
|
||||
open import Stdlib.System.IO;
|
||||
|
||||
builtin fail axiom fail : {A : Type} → String → A;
|
||||
builtin fail
|
||||
axiom fail : {A : Type} → String → A;
|
||||
|
||||
main : IO;
|
||||
main := printStringLn "Get"
|
||||
main :=
|
||||
printStringLn "Get"
|
||||
>> fail "Enough"
|
||||
>> printStringLn "Sleep";
|
||||
end;
|
||||
|
@ -1,8 +1,10 @@
|
||||
module builtinTrace;
|
||||
|
||||
open import Stdlib.Prelude;
|
||||
open import Stdlib.Data.Nat.Ord;
|
||||
|
||||
builtin trace axiom trace : {A : Type} → {B : Type} → A → B → B;
|
||||
builtin trace
|
||||
axiom trace : {A : Type} → {B : Type} → A → B → B;
|
||||
|
||||
terminating
|
||||
f : Nat → Nat → Nat;
|
||||
@ -22,4 +24,3 @@ trace 4 (f 3 0)
|
||||
-}
|
||||
main : IO;
|
||||
main := printNatLn $ f 4 0;
|
||||
end;
|
||||
|
@ -1,4 +1,5 @@
|
||||
module LetSynonym;
|
||||
|
||||
type T :=
|
||||
| t : T;
|
||||
|
||||
@ -10,4 +11,3 @@ module LetSynonym;
|
||||
x : A;
|
||||
x := t;
|
||||
in x;
|
||||
end;
|
||||
|
Loading…
Reference in New Issue
Block a user