From 5812a269a8fc6e8ed477840186ac85614463374f Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 21 Apr 2020 13:19:52 +0200
Subject: [PATCH] syntax, removed ad_hoc

---
 encodings/ad_hoc.lp           | 11 -----------
 encodings/cert_f.lp           |  8 ++++----
 encodings/deferred.lp         |  9 ++++-----
 encodings/deferred_erasure.lp | 15 +++++++--------
 4 files changed, 15 insertions(+), 28 deletions(-)
 delete mode 100644 encodings/ad_hoc.lp

diff --git a/encodings/ad_hoc.lp b/encodings/ad_hoc.lp
deleted file mode 100644
index fbbd9d3..0000000
--- a/encodings/ad_hoc.lp
+++ /dev/null
@@ -1,11 +0,0 @@
-// Prenex ad-hoc polymorphism
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require personoj.encodings.prenex as P
-require open personoj.encodings.subtype
-
-constant symbol forallS: Set → (Set → Scheme) → Scheme
-rule P.χ (forallS $T $C) ↪ ΠU: Set, ε (U ⊑ $T) → P.χ ($C U)
-
-constant symbol forallB: Set → (Set → Bool) → Bool
-rule ε (forallB $T $C) ↪ ΠU: Set, ε (U ⊑ $T) → ε ($C U)
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 7f460ed..9d9bfa9 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -18,13 +18,13 @@ constant symbol uType : Univ Kind
 // of the rule.
 symbol Rule : Sort → Sort → Sort
 rule Rule Prop Prop ↪ Prop
- and Rule Type Type ↪ Type
- and Rule Type Prop ↪ Prop
+with Rule Type Type ↪ Type
+with Rule Type Prop ↪ Prop
 
 // [Term s t] decodes term [t] of encoded sort [s]
 injective symbol Term {s: Sort}: Univ s → TYPE
 rule Term uProp ↪ Univ Prop
- and Term uType ↪ Univ Type
+with Term uType ↪ Univ Type
 
 // [prod s1 s2 A B] encodes [Π x : (A: s1). (B: s2)]
 symbol prod {sA: Sort} {sB: Sort} (A: Univ sA):
@@ -79,7 +79,7 @@ set declared "↑"
 symbol ↑ {T: Term uType} (U: Term uType): Term (T ⊑ U) → Term T → Term U
 rule ↑ {$T} $T _ $x ↪ $x // Identity cast
 // NOTE: a cast from a type [{x: A | P}] to type [A] is a [fst],
-and ↑ {Psub {$T} $P} $T _ ↪ fst {$T} {$P}
+with ↑ {Psub {$T} $P} $T _ ↪ fst {$T} {$P}
 // and a "downcast" is the pair constructor
 set declared "↓"
 
diff --git a/encodings/deferred.lp b/encodings/deferred.lp
index a004713..e389f34 100644
--- a/encodings/deferred.lp
+++ b/encodings/deferred.lp
@@ -1,8 +1,7 @@
 // Deep encoding of terms carrying their types.
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
 
 /// Type carried with  the encoded terms
 constant symbol t: Set → TYPE
@@ -16,7 +15,7 @@ rule η (APP (arrd {$T} $bU) $T $y) ↪ η ($bU (unquote $y))
 
 // Quoted terms application
 constant symbol app {T: Set} {S: Set}: t T → Πy: t S, t (APP T S y)
-rule unquote (app {arrd {$a} $b} {$a} $t $u) ↪ (unquote $t) (unquote $u)
+rule unquote (app {arrd {$a} _} {$a} $t $u) ↪ (unquote $t) (unquote $u)
 
 constant symbol p: Bool → TYPE
 constant symbol quote_p {P: Bool}: ε P → p P
diff --git a/encodings/deferred_erasure.lp b/encodings/deferred_erasure.lp
index 6dbc56c..c29fb9f 100644
--- a/encodings/deferred_erasure.lp
+++ b/encodings/deferred_erasure.lp
@@ -1,10 +1,9 @@
 // Deep encoding using type erasure. Deferred terms do not carry their type, but
 // the unquoting function takes a type as argument and unquotes the term
 // according to this type.
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
 
 constant symbol t: TYPE
 constant symbol quote {T: Set}: η T → t
@@ -18,9 +17,9 @@ symbol quote_B {P: Bool}: ε P → t
 symbol unquote_B (P: Bool): t → ε P
 
 rule unquote (arrd $b) $f $x ↪ unquote ($b $x) (app $f (quote $x))
- and unquote_B (impd $b) $h $x ↪ unquote_B ($b $x) (app $h (quote_B $x))
- and unquote_B (forall $b) $f $x ↪ unquote_B ($b $x) (app $f (quote $x))
+with unquote_B (impd $b) $h $x ↪ unquote_B ($b $x) (app $h (quote_B $x))
+with unquote_B (forall $b) $f $x ↪ unquote_B ($b $x) (app $f (quote $x))
 
-symbol if (T: Set) (p: Bool): t → t → η T
+symbol if (T: Set): Bool → t → t → η T
 rule if $T true $then _ ↪ unquote $T $then
- and if $T false _ $else ↪ unquote $T $else
+with if $T false _ $else ↪ unquote $T $else
-- 
GitLab