From bf30879134fe6183830b7d7f71699ecb2ca3da8e Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 8 Apr 2020 17:50:04 +0200
Subject: [PATCH] quoting terms

---
 encodings/lazy.lp |  9 ++++++---
 sandbox/quote.lp  | 17 +++++++++++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 sandbox/quote.lp

diff --git a/encodings/lazy.lp b/encodings/lazy.lp
index 80b424b..c350a89 100644
--- a/encodings/lazy.lp
+++ b/encodings/lazy.lp
@@ -5,12 +5,15 @@ require open
 constant symbol delayed: Set ⇒ TYPE
 constant symbol quote {T: Set}: η T ⇒ delayed T
 
-constant symbol s_app: Set ⇒ Set ⇒ Set
+// 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 (s_app T S)
+: delayed T ⇒ delayed S ⇒ delayed (sapp T S)
 
+// Unquote terms
 symbol unquote {T: Set}: delayed 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
new file mode 100644
index 0000000..e6f91de
--- /dev/null
+++ b/sandbox/quote.lp
@@ -0,0 +1,17 @@
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+require personoj.encodings.lazy as L
+
+symbol T: Set
+symbol t: η T
+symbol f: η (T ~> T)
+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_ok ≔ L.app (L.quote f) (L.quote t)
+compute L.unquote qu_ok
-- 
GitLab