Isabelle pragmas (#105)

* Adds pragmas and builtins needed for the translation to Isabelle/HOL.
* Depends on anoma/juvix#2868

Stdlib/Data/Bool/Base.juvix

@@ -4,6 +4,7 @@ import Juvix.Builtin.V1.Bool open public;
 import Stdlib.Data.Fixity open;
 
 --- Logical negation.
+{-# isabelle-function: {name: "¬"} #-}
 not : Bool → Bool
   | true := false
   | false := true;

Stdlib/Data/List/Base.juvix

@@ -47,7 +47,7 @@ foldl {A B} (f : B → A → B) (z : B) : List A → B
 
 syntax iterator for {init := 1; range := 1};
 
-{-# inline: 0 #-}
+{-# inline: 0, isabelle-function: {name: "foldl"} #-}
 for : {A B : Type} → (B → A → B) → B → List A → B := foldl;
 
 syntax iterator map {init := 0; range := 1};
@@ -71,6 +71,7 @@ filter {A} (f : A → Bool) : List A → List A
 length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc};
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
+{-# isabelle-function: {name: "rev"} #-}
 reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc};
 
 --- Returns a ;List; of length n where every element is the given value.
@@ -123,6 +124,7 @@ syntax operator ++ cons;
 snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil;
 
 --- Concatenates a ;List; of ;List;s.
+{-# isabelle-function: {name: "concat"} #-}
 flatten : {A : Type} → List (List A) → List A := foldl (++) nil;
 
 --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
@@ -136,6 +138,7 @@ intersperse {A} (sep : A) : List A → List A
   | (x :: xs) := x :: prependToAll sep xs;
 
 --- 𝒪(1). Drops the first element of a ;List;.
+{-# isabelle-function: {name: "tl"} #-}
 tail {A} : List A → List A
   | (_ :: xs) := xs
   | nil := nil;

Stdlib/Data/Maybe/Base.juvix

@@ -10,7 +10,7 @@ fromMaybe {A} (a : A) : Maybe A → A
 
 --- Applies a function to the value from a ;Maybe; if present, else returns the
 --- given value.
-{-# inline: true #-}
+{-# inline: true, isabelle-function: {name: "case_option"} #-}
 maybe {A B} (b : B) (f : A → B) : Maybe A → B
   | nothing := b
   | (just a) := f a;

Stdlib/Data/Pair/Base.juvix

@@ -5,6 +5,7 @@ import Stdlib.Data.Fixity open;
 syntax operator , pair;
 
 --- Inductive pair. I.e. a tuple with two components.
+builtin pair
 type Pair (A B : Type) := , : A → B → Pair A B;
 
 --- Converts a function of two arguments to a function with a product argument.

Stdlib/Trait/DivMod.juvix

@@ -3,7 +3,9 @@ module Stdlib.Trait.DivMod;
 trait
 type DivMod A :=
   mkDivMod {
+    {-# isabelle-operator: {name: "div", prec: 70, assoc: left} #-}
     div : A -> A -> A;
+    {-# isabelle-operator: {name: "mod", prec: 70, assoc: left} #-}
     mod : A -> A -> A
   };
 

Stdlib/Trait/Eq.juvix

@@ -10,9 +10,9 @@ type Eq A := mkEq {eq : A -> A -> Bool};
 syntax operator == comparison;
 syntax operator /= comparison;
 
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: "=", prec: 50, assoc: none} #-}
 == {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
 
 --- Tests for inequality.
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-}
 /= {A} {{Eq A}} (x y : A) : Bool := not (x == y);

Stdlib/Trait/Integral.juvix

@@ -9,6 +9,7 @@ type Integral A :=
   mkIntegral {
     naturalI : Natural A;
     syntax operator - additive;
+    {-# isabelle-operator: {name: "-", prec: 65, assoc: left} #-}
     - : A -> A -> A;
     builtin from-int
     fromInt : Int -> A

Stdlib/Trait/Ord.juvix

@@ -37,7 +37,7 @@ type Ord A := mkOrd {cmp : A -> A -> Ordering};
 syntax operator <= comparison;
 
 --- Returns ;true; iff the first element is less than or equal to the second.
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: "≤", prec: 50, assoc: none} #-}
 <= {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
     | EQ := true
@@ -47,7 +47,7 @@ syntax operator <= comparison;
 syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: "<", prec: 50, assoc: none} #-}
 < {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
     | EQ := false
@@ -57,13 +57,13 @@ syntax operator < comparison;
 syntax operator > comparison;
 
 --- Returns ;true; iff the first element is greater than the second.
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: ">", prec: 50, assoc: none} #-}
 > {A} {{Ord A}} (x y : A) : Bool := y < x;
 
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
-{-# inline: always #-}
+{-# inline: always, isabelle-operator: {name: "≥", prec: 50, assoc: none} #-}
 >= {A} {{Ord A}} (x y : A) : Bool := y <= x;
 
 --- Returns the smaller element.

Stdlib/Trait/Ord/Eq.juvix

@@ -9,6 +9,7 @@ fromOrdToEq {A} {{Ord A}} : Eq.Eq A := Eq.mkEq (==);
 
 syntax operator == comparison;
 
+{-# isabelle-operator: {name: "=", prec: 50, assoc: none} #-}
 == {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
     | EQ := true
@@ -17,5 +18,5 @@ syntax operator == comparison;
 syntax operator /= comparison;
 
 --- Tests for inequality.
-{-# inline: true #-}
+{-# inline: true, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-}
 /= {A} {{Ord A}} (x y : A) : Bool := not (x == y);