From c7e32b892301ee76b27c41efe634db315dd7ffd1 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 9 Apr 2020 11:14:55 +0200
Subject: [PATCH] booleans

---
 adlib/booleans.lp     |  3 +--
 encodings/booleans.lp |  8 ++++++++
 encodings/if.lp       | 11 ++++++++++-
 encodings/subtype.lp  |  3 +++
 sandbox/quote.lp      |  2 ++
 5 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 encodings/booleans.lp

diff --git a/adlib/booleans.lp b/adlib/booleans.lp
index 528c4cc..71bb5c8 100644
--- a/adlib/booleans.lp
+++ b/adlib/booleans.lp
@@ -1,6 +1,7 @@
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
+  personoj.encodings.booleans
 
 definition false ≔ forall {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -19,8 +20,6 @@ set infix 7 "⇔" ≔ biff
 
 definition when P Q ≔ imp Q P
 
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
 set builtin "imp" ≔ imp
 set builtin "not" ≔ bnot
 set builtin "and" ≔ band
diff --git a/encodings/booleans.lp b/encodings/booleans.lp
new file mode 100644
index 0000000..9a300d1
--- /dev/null
+++ b/encodings/booleans.lp
@@ -0,0 +1,8 @@
+require open personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
diff --git a/encodings/if.lp b/encodings/if.lp
index f625e1f..02c8556 100644
--- a/encodings/if.lp
+++ b/encodings/if.lp
@@ -1,6 +1,15 @@
 require open personoj.encodings.lhol
   personoj.encodings.pvs_cert
-  personoj.encodings.subtype
+  personoj.encodings.booleans
+require personoj.encodings.deferred as Deferred
+require open personoj.encodings.subtype //FIXME: why must it be the last import?
 
 symbol if {U: Set} {V: Set} (S: Set)
 : ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ η U ⇒ η V ⇒ η S
+
+symbol lif {U: Set} {V: Set} (S: Set)
+: ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ Deferred.t U ⇒ Deferred.t V ⇒ η S
+
+// lazy if
+rule lif _ &pr _ true &t _ → ↑ &pr (Deferred.unquote &t)
+rule lif _ _ &pr false _ &f → ↑ &pr (Deferred.unquote &f)
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 6f27ed9..4ed85f1 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -1,6 +1,8 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
+set declared "↑"
+
 symbol subtype : Set ⇒ Set ⇒ Bool
 set infix left 6 "⊑" ≔ subtype
 
@@ -14,6 +16,7 @@ symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
 : ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
 
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
+definition ↑ {A} {B} ≔ upcast {A} {B}
 
 symbol root: Set ⇒ Set
 rule root (psub {&T} _) → root &T
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
index 5f0466f..0cf4195 100644
--- a/sandbox/quote.lp
+++ b/sandbox/quote.lp
@@ -17,3 +17,5 @@ definition qu_ok ≔ Deferred.app (Deferred.quote f) (Deferred.quote t)
 compute Deferred.unquote qu_ok
 
 compute Deferred.quote {T ~> T} (λx:η T, f x)
+
+symbol lor: Deferred.t bool ⇒ Deferred.t bool ⇒ Bool
-- 
GitLab