Skip to content

Commit

Permalink
Add tests for issues #1338 and #1339
Browse files Browse the repository at this point in the history
  • Loading branch information
lukaszcz committed Jul 18, 2022
1 parent 4e5a4bc commit bd98f0c
Show file tree
Hide file tree
Showing 7 changed files with 54 additions and 0 deletions.
2 changes: 2 additions & 0 deletions test/BackendC/Positive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ tests =
[ PosTest "HelloWorld" "HelloWorld" StdlibExclude,
PosTest "Inductive types and pattern matching" "Nat" StdlibExclude,
PosTest "Polymorphic types" "Polymorphism" StdlibExclude,
PosTest "Polymorphic axioms" "PolymorphicAxioms" StdlibExclude,
PosTest "Polymorphic target" "PolymorphicTarget" StdlibExclude,
PosTest "Multiple modules" "MultiModules" StdlibExclude,
PosTest "Higher Order Functions" "HigherOrder" StdlibExclude,
PosTest "Higher Order Functions and explicit holes" "PolymorphismHoles" StdlibExclude,
Expand Down
26 changes: 26 additions & 0 deletions tests/positive/MiniC/PolymorphicAxioms/Input.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module Input;

inductive Unit {
unit : Unit;
};

axiom Action : Type;

compile Action {
c ↦ "int";
};

axiom ignore : {A : Type} -> A -> Action;

compile ignore {
c ↦ "ignore";
};

foreign c {
static int ignore(uintptr_t ptr) { return 0; \}
};

main : Action;
main := ignore unit;

end;
Empty file.
Empty file.
26 changes: 26 additions & 0 deletions tests/positive/MiniC/PolymorphicTarget/Input.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module Input;

inductive Unit {
unit : Unit;
};

terminating
loop : {A : Type} -> A;
loop := loop;

const : {A : Type} -> A -> A -> A;
const x y := x;

fail : Unit;
fail := const unit loop;

axiom Action : Type;

compile Action {
c ↦ "int";
};

main : Action;
main := 0;

end;
Empty file.
Empty file.

0 comments on commit bd98f0c

Please sign in to comment.