From 774f46e6e2be26b3b352df5d0c21264adfaaea69 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 9 Apr 2020 09:15:06 +0200
Subject: [PATCH] quoting lambdas

---
 encodings/{lazy.lp => deferred.lp} | 11 ++++++-----
 sandbox/quote.lp                   | 16 +++++++++-------
 2 files changed, 15 insertions(+), 12 deletions(-)
 rename encodings/{lazy.lp => deferred.lp} (52%)

diff --git a/encodings/lazy.lp b/encodings/deferred.lp
similarity index 52%
rename from encodings/lazy.lp
rename to encodings/deferred.lp
index c350a89..4107912 100644
--- a/encodings/lazy.lp
+++ b/encodings/deferred.lp
@@ -1,19 +1,20 @@
+// Encoding of deferred terms. It ought to be used by lazy operators such as IF
+// or boolean operators
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
 
-constant symbol delayed: Set ⇒ TYPE
-constant symbol quote {T: Set}: η T ⇒ delayed T
+constant symbol t: Set ⇒ TYPE
+constant symbol quote {T: Set}: η T ⇒ t T
 
 // Application at sort type
 symbol sapp: Set ⇒ Set ⇒ Set
 rule sapp (&T ~> &S) &T → &T
 
 // Quoted terms application
-constant symbol app {T: Set} {S: Set}
-: delayed T ⇒ delayed S ⇒ delayed (sapp T S)
+constant symbol app {T: Set} {S: Set}: t T ⇒ t S ⇒ t (sapp T S)
 
 // Unquote terms
-symbol unquote {T: Set}: delayed T ⇒ η T
+symbol unquote {T: Set}: t T ⇒ η T
 rule unquote (quote &x) → &x
 rule unquote {&S} (app {&T ~> &S} {&T} &t &u) → (unquote &t) (unquote &u)
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
index e6f91de..5f0466f 100644
--- a/sandbox/quote.lp
+++ b/sandbox/quote.lp
@@ -1,17 +1,19 @@
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
-require personoj.encodings.lazy as L
+require personoj.encodings.deferred as Deferred
 
-symbol T: Set
+constant symbol T: Set
 symbol t: η T
 symbol f: η (T ~> T)
-symbol S: Set
+constant symbol S: Set
 symbol s: η S
 
 set flag "print_implicits" on
-definition qu_ko ≔ L.app (L.quote f) (L.quote s)
-compute L.unquote qu_ko
+definition qu_ko ≔ Deferred.app (Deferred.quote f) (Deferred.quote s)
+compute Deferred.unquote qu_ko
 
-definition qu_ok ≔ L.app (L.quote f) (L.quote t)
-compute L.unquote qu_ok
+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)
-- 
GitLab