From c3857c9bad721273043667a0657ffc7372cd4b21 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sun, 17 May 2020 16:50:15 +0200
Subject: [PATCH] more complete makefile, cleaning
---
GNUmakefile | 23 +++++-
encodings/{useless => }/pvs_core.lp | 0
encodings/useless/cert_f.lp | 100 --------------------------
encodings/useless/deferred.lp | 22 ------
encodings/useless/deferred_erasure.lp | 25 -------
sandbox/boolops_if.lp | 9 ---
sandbox/quote.lp | 30 --------
7 files changed, 20 insertions(+), 189 deletions(-)
rename encodings/{useless => }/pvs_core.lp (100%)
delete mode 100644 encodings/useless/cert_f.lp
delete mode 100644 encodings/useless/deferred.lp
delete mode 100644 encodings/useless/deferred_erasure.lp
delete mode 100644 sandbox/boolops_if.lp
delete mode 100644 sandbox/quote.lp
diff --git a/GNUmakefile b/GNUmakefile
index ab95430..d98fb01 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -1,7 +1,24 @@
-LP = lambdapi
+LP_SRC = $(shell find . -type f -name "*.lp")
+LP_OBJ = $(LP_SRC:%.lp=%.lpo)
+
+all: $(LP_OBJ)
+
+$(LP_OBJ)&: $(LP_SRC)
+ lambdapi check --gen-obj $^
+
+install: $(LP_OBJ) lambdapi.pkg
+ lambdapi install lambdapi.pkg $(LP_OBJ) $(LP_SRC)
+
+.PHONY: uninstall
+uninstall:
+ lambdapi uninstall lambdapi.pkg
+
+.PHONY: clean
+clean:
+ $(RM) -r $(LP_OBJ)
tests:
@echo "Checking [core] prelude"
- $(LP) prelude/core/*.lp
+ lambdapi prelude/core/*.lp
@echo "Checking [cert] prelude"
- $(LP) prelude/cert_f/*.lp
+ lambdapi prelude/cert_f/*.lp
diff --git a/encodings/useless/pvs_core.lp b/encodings/pvs_core.lp
similarity index 100%
rename from encodings/useless/pvs_core.lp
rename to encodings/pvs_core.lp
diff --git a/encodings/useless/cert_f.lp b/encodings/useless/cert_f.lp
deleted file mode 100644
index 9d9bfa9..0000000
--- a/encodings/useless/cert_f.lp
+++ /dev/null
@@ -1,100 +0,0 @@
-// PVS cert with functional PTS
-constant symbol Sort : TYPE
-constant symbol Univ : Sort → TYPE
-
-constant symbol Kind : Sort
-constant symbol Type : Sort
-constant symbol Prop : Sort
-
-// Axioms: (Prop, Type), (Type, Kind)
-// Prop: Type
-constant symbol uProp : Univ Type
-// Type: Kind
-constant symbol uType : Univ Kind
-
-// Encoding of rules
-// (Prop, Prop, Prop), (Type, Type, Type), (Type, Prop, Prop)
-// Since the PTS is functional, [Rule s1 s2] rewrites the the 3rd element
-// of the rule.
-symbol Rule : Sort → Sort → Sort
-rule Rule Prop 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
-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):
- (Term A → Univ sB) → Univ (Rule sA sB)
-
-rule Term (prod {$sA} {$sB} $A $B) ↪ Πx: Term {$sA} $A, Term {$sB} ($B x)
-
-// Predicate subtyping
-// can be seen as a dependant pair type with
-// - first element is a term of some type [A] and
-// - second is a predicate on [A] verified by the first element.
-constant symbol Psub {T: Term uType}: (Term T → Term uProp) → Term uType
-
-// Γ ⊢ M : { v : T | P }
-// —————————————————————PROJl
-// Γ ⊢ fst(M) : T
-symbol fst {T: Univ Type} {P: Term T → Univ Prop}: Term (Psub P) → Term T
-
-// Γ ⊢ M : { v : T | P }
-// ——————————————————————————PROJr
-// Γ ⊢ snd(M) : P[v ≔ fst(M)]
-constant symbol snd {T: Univ Type} {P: Term T → Univ Prop}
- (M: Term (Psub P)):
- Term (P (fst M))
-
-// An inhabitant of a predicate subtype, that is, a pair of
-// an element and the proof that it satisfies the predicate
-// Γ ⊢ M : T Γ ⊢ N : P[v ≔ M] Γ ⊢ { v : T | P }
-// ——————————————————————————————————————————————————PAIR
-// Γ ⊢ ⟨M, N⟩ : {v : T | P}
-symbol pair {T: Univ Type} (P: Term T → Univ Prop) (M: Term T):
- Term (P M) → Term (Psub P)
-
-// opair is a pair forgetting its snd argument
-protected symbol opair (T: Univ Type) (P: Term T → Univ Prop) (M: Term T):
- Term (Psub P)
-
-// Two pairs are convertible if their first element is
-rule pair {$T} $P $M _ ↪ opair $T $P $M
-
-rule fst (opair _ _ $M) ↪ $M
-// and opair _ $P (fst {_} {$P} $X) ↪ $X // Surjective pairing
-//NOTE: can we remove non linearity?
-
-// The subtype relation
-symbol subtype: Term uType → Term uType → Term uProp
-set infix left 6 "⊑" ≔ subtype
-
-// [↑ {T} U p t] casts element [t] from type [T] to type [U] given
-// the proof [p] that [T] is a subtype of [U]
-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],
-with ↑ {Psub {$T} $P} $T _ ↪ fst {$T} {$P}
-// and a "downcast" is the pair constructor
-set declared "↓"
-
-// Auxiliary definitions
-
-// [↓ {T} P t π] down casts term [t] to type [{x: T | P(x)}] given the
-// proof [Ï€] that [t] verifies predicate [P].
-definition ↓ {T} ≔ pair {T}
-// NOTE: we can only down-cast from a type to its direct sub-type
-
-definition arrow {sA} {sB} (A: Univ sA) (B: Univ sB) ≔ prod A (λ_, B)
-set infix left 5 "~>" ≔ arrow
-// Builtins
-definition T ≔ Term {Type}
-set builtin "T" ≔ T
-
-definition P ≔ Term {Prop}
-set builtin "P" ≔ P
diff --git a/encodings/useless/deferred.lp b/encodings/useless/deferred.lp
deleted file mode 100644
index e389f34..0000000
--- a/encodings/useless/deferred.lp
+++ /dev/null
@@ -1,22 +0,0 @@
-// Deep encoding of terms carrying their types.
-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
-constant symbol quote {T: Set}: η T → t T
-injective symbol unquote {T: Set}: t T → η T
-rule unquote (quote $t) ↪ $t
-
-// Coding of applied types
-constant symbol APP: Set → ΠU: Set, t U → Set
-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} _} {$a} $t $u) ↪ (unquote $t) (unquote $u)
-
-constant symbol p: Bool → TYPE
-constant symbol quote_p {P: Bool}: ε P → p P
-symbol unquote_p {P: Bool}: p P → ε P
diff --git a/encodings/useless/deferred_erasure.lp b/encodings/useless/deferred_erasure.lp
deleted file mode 100644
index c29fb9f..0000000
--- a/encodings/useless/deferred_erasure.lp
+++ /dev/null
@@ -1,25 +0,0 @@
-// 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
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.bool_hol
-
-constant symbol t: TYPE
-constant symbol quote {T: Set}: η T → t
-injective symbol app: t → t → t
-constant symbol abs: (t → t) → t
-
-rule app (abs $b) $a ↪ $b $a
-
-symbol unquote (T: Set): t → η T
-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))
-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): Bool → t → t → η T
-rule if $T true $then _ ↪ unquote $T $then
-with if $T false _ $else ↪ unquote $T $else
diff --git a/sandbox/boolops_if.lp b/sandbox/boolops_if.lp
deleted file mode 100644
index 987a030..0000000
--- a/sandbox/boolops_if.lp
+++ /dev/null
@@ -1,9 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.boolops_if
-
-theorem trivial (P: η bool): ε (P ⊃ (λ_, P))
-proof
- assume P
- refine λ_ _ f, f
-qed
diff --git a/sandbox/quote.lp b/sandbox/quote.lp
deleted file mode 100644
index afcfb53..0000000
--- a/sandbox/quote.lp
+++ /dev/null
@@ -1,30 +0,0 @@
-require open
- personoj.encodings.lhol
- personoj.encodings.pvs_cert
- personoj.encodings.if
- personoj.encodings.booleans
-require personoj.encodings.deferred as Deferred
-require open personoj.encodings.subtype
-
-constant symbol T: Set
-symbol t: η T
-symbol f: η (T ~> T)
-constant symbol S: Set
-symbol s: η S
-
-set flag "print_implicits" on
-definition qu_ko ≔ Deferred.app (Deferred.quote f) (Deferred.quote s)
-compute Deferred.unquote qu_ko
-
-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
-
-compute let f' ≔ Deferred.quote f in
- let t' ≔ Deferred.quote t in
- let s' ≔ Deferred.quote s in
- let refl_t' ≔ Deferred.quote_p (S_Refl T) in
- lif T refl_t' refl_t' true (Deferred.app f' t') (Deferred.app f' s')
--
GitLab