Commit 827252dd authored by Raphael Cauderlier's avatar Raphael Cauderlier

Switch to Sukerujo for pretty-printing of strings

parent 26f51c58
......@@ -117,11 +117,9 @@ done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
#find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
#find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.6" &&
find_and_check_binary "skcheck" ".native" "DKCHECK" "-version" "Sukerujo devel" &&
find_and_check_binary "skdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "skmeta" ".native" "DKMETA" "-version" "" &&
if $CONFLUENCE_CHECKING
then
......
......@@ -18,10 +18,6 @@ def fun_apply := fol.fun_apply.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
def 2 := nat.S 1.
(; Signature ;)
A : sort.
LEQ : predicate.
......
......@@ -18,7 +18,7 @@ def Joe : fol.term BAR := fol.fun_apply JOE.
(; The "drink" predicate. ;)
DRINK : fol.predicate.
[] fol.pred_domain DRINK --> fol.read_sorts (nat.S nat.O) BAR.
[] fol.pred_domain DRINK --> fol.read_sorts 1 BAR.
def drink (x : fol.term BAR) : fol.prop := fol.pred_apply DRINK x.
def drinker_statement : fol.prop :=
......
......@@ -18,9 +18,6 @@ def fun_apply := fol.fun_apply.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
(; Signature ;)
A : sort.
P : predicate.
......@@ -28,13 +25,13 @@ P : predicate.
O : function.
[] fol.fun_domain O --> nil_sort.
[] fol.fun_codomain O --> A.
S : function.
[] fol.fun_domain S --> read_sorts 1 A.
[] fol.fun_codomain S --> A.
S_ : function.
[] fol.fun_domain S_ --> read_sorts 1 A.
[] fol.fun_codomain S_ --> A.
def p : term A -> prop := pred_apply P.
def o : term A := fun_apply O.
def s : term A -> term A := fun_apply S.
def s : term A -> term A := fun_apply S_.
(; Axioms ;)
def A0 := p o.
......
......@@ -13,9 +13,15 @@ DKCHECK_OPTIONS =
all: $(DKOS)
builtins.dko: builtins.dk
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) -nk $<
%.dko:
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) $<
builtins.dk.depend: builtins.dk
echo > $@
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
......
#NAME builtins.
nat : Type.
0 : nat.
S : nat -> nat.
char : Type.
char_of_nat : nat -> char.
string : Type.
string_nil : string.
string_cons : char -> string -> string.
......@@ -23,12 +23,9 @@ def fun_domain := fol.fun_domain.
def fun_codomain := fol.fun_codomain.
def apply_fun := fol.apply_fun.
def O := nat.O.
def S := nat.S.
(; Equality is a family of binary predicate symbols. ;)
Eq : sort -> predicate.
[A] fol.pred_domain (Eq A) --> read_sorts (S (S O)) A A.
[A] fol.pred_domain (Eq A) --> read_sorts 2 A A.
def eq (A : sort) : term A -> term A -> prop := pred_apply (Eq A).
[A,x,y]
......
......@@ -17,12 +17,12 @@ cons_sort : sort -> sorts -> sorts.
cons_sort A1 (cons_sort A2 (... cons_sort An nil_sort))
;)
def nat := nat.Nat.
(; The type of the read_sorts function is defined inductively ;)
def read_sorts_T : nat -> Type.
[] read_sorts_T nat.O --> sorts.
[n] read_sorts_T (nat.S n) --> sort -> read_sorts_T n.
[] read_sorts_T 0 --> sorts.
[n] read_sorts_T (S n) --> sort -> read_sorts_T n.
(; Adding an element to the tail of a list of sorts:
snoc_sort [A1 .. An] B = [A1 .. An B] ;)
......@@ -34,9 +34,9 @@ def snoc_sort : sorts -> sort -> sorts.
read_tyes_acc m [A1 .. An] B1 .. Bm = [A1 .. An B1 .. Bm]
;)
def read_sorts_acc : n : nat -> sorts -> read_sorts_T n.
[acc] read_sorts_acc nat.O acc --> acc
[acc] read_sorts_acc 0 acc --> acc
[n,acc]
read_sorts_acc (nat.S n) acc
read_sorts_acc (S n) acc
--> t : sort => read_sorts_acc n (snoc_sort acc t).
(; read_sorts n A1 .. An = [A1 .. An] ;)
......@@ -122,14 +122,14 @@ def nand_list : props -> prop.
(; nand_type n == propⁿ -> prop ;)
def nand_type : nat -> Type.
[] nand_type nat.O --> prop
[n] nand_type (nat.S n) --> prop -> nand_type n.
[] nand_type 0 --> prop
[n] nand_type (S n) --> prop -> nand_type n.
(; nand_aux [B₁; …; Bₘ] n A₁ … Aₙ == nand_list [B₁; …; Bₘ; A₁; …; Aₙ]
== B₁ ∧ … ∧ Bₘ ∧ A₁ ∧ … ∧ Aₙ ;)
def nand_aux : props -> n : nat -> nand_type n.
[Bs] nand_aux Bs nat.O --> nand_list Bs
[Bs,n] nand_aux Bs (nat.S n) --> A => nand_aux (snoc_prop Bs A) n.
[Bs] nand_aux Bs 0 --> nand_list Bs
[Bs,n] nand_aux Bs (S n) --> A => nand_aux (snoc_prop Bs A) n.
def nand : n : nat -> nand_type n := nand_aux nil_prop.
......@@ -140,8 +140,8 @@ def nor_list : props -> prop.
--> or A1 (nor_list (cons_prop A2 As)).
def nor_aux : props -> n : nat -> nand_type n.
[Bs] nor_aux Bs nat.O --> nor_list Bs
[Bs,n] nor_aux Bs (nat.S n) --> A => nor_aux (snoc_prop Bs A) n.
[Bs] nor_aux Bs 0 --> nor_list Bs
[Bs,n] nor_aux Bs (S n) --> A => nor_aux (snoc_prop Bs A) n.
def nor : n : nat -> nand_type n := nor_aux nil_prop.
......@@ -149,11 +149,11 @@ def nimp_list : props -> prop -> prop.
[B] nimp_list nil_prop B --> B
[A,As,B] nimp_list (cons_prop A As) B --> imp A (nimp_list As B).
def nimp_aux : props -> n : nat -> nand_type (nat.S n).
[Bs] nimp_aux Bs nat.O --> A => nimp_list Bs A
[Bs,n] nimp_aux Bs (nat.S n) --> A => nimp_aux (snoc_prop Bs A) n.
def nimp_aux : props -> n : nat -> nand_type (S n).
[Bs] nimp_aux Bs 0 --> A => nimp_list Bs A
[Bs,n] nimp_aux Bs (S n) --> A => nimp_aux (snoc_prop Bs A) n.
def nimp : n : nat -> nand_type (nat.S n) := nimp_aux nil_prop.
def nimp : n : nat -> nand_type (S n) := nimp_aux nil_prop.
(; nall n A₁ A₂ … Aₙ (a₁ : term A₁ => a₂ : term A₂ => … => aₙ : term Aₙ => P a₁ a₂ … aₙ)
==
......@@ -175,16 +175,16 @@ def nex_aux : As : sorts -> nall_aux_type As -> prop.
(; nall_aux2 [B₁; …; Bₘ] n A₁ … Aₙ = nall_aux [B₁; …; Bₘ; A₁; …; Aₙ] ;)
(; nall_aux2_type Bs n A₁ … Aₙ = nall_aux_type (Bs^As) -> prop ;)
def nall_aux2_type : sorts -> nat -> Type.
[Bs] nall_aux2_type Bs nat.O --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (nat.S n) --> A : sort -> nall_aux2_type (snoc_sort Bs A) n.
[Bs] nall_aux2_type Bs 0 --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (S n) --> A : sort -> nall_aux2_type (snoc_sort Bs A) n.
def nall_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nall_aux2 Bs nat.O --> nall_aux Bs
[Bs,n] nall_aux2 Bs (nat.S n) --> A => nall_aux2 (snoc_sort Bs A) n.
[Bs] nall_aux2 Bs 0 --> nall_aux Bs
[Bs,n] nall_aux2 Bs (S n) --> A => nall_aux2 (snoc_sort Bs A) n.
def nex_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nex_aux2 Bs nat.O --> nex_aux Bs
[Bs,n] nex_aux2 Bs (nat.S n) --> A => nex_aux2 (snoc_sort Bs A) n.
[Bs] nex_aux2 Bs 0 --> nex_aux Bs
[Bs,n] nex_aux2 Bs (S n) --> A => nex_aux2 (snoc_sort Bs A) n.
def nall (n : nat) : nall_aux2_type nil_sort n := nall_aux2 nil_sort n.
def nex (n : nat) : nall_aux2_type nil_sort n := nex_aux2 nil_sort n.
......
#NAME nat.
Nat : Type.
O : Nat.
S : Nat -> Nat.
......@@ -21,35 +21,35 @@ ONE : fol.function.
ADD : fol.function.
(; Arities ;)
[] fol.pred_domain EQ --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.pred_domain EQ --> fol.read_sorts 2 Nat Nat.
[] fol.fun_domain ZERO --> fol.nil_sort.
[] fol.fun_domain ONE --> fol.nil_sort.
[] fol.fun_domain ADD --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_domain ADD --> fol.read_sorts 2 Nat Nat.
[] fol.fun_codomain ZERO --> Nat.
[] fol.fun_codomain ONE --> Nat.
[] fol.fun_codomain ADD --> Nat.
(; Abbreviations ;)
def eq := fol.pred_apply EQ.
def 0 := fol.fun_apply ZERO.
def 1 := fol.fun_apply ONE.
def 0_ := fol.fun_apply ZERO.
def 1_ := fol.fun_apply ONE.
def add := fol.fun_apply ADD.
def succ (x : fol.term Nat) := add x 1.
def succ (x : fol.term Nat) := add x 1_.
(; Axioms ;)
(; 0 != x + 1 ;)
P1 : fol.proof (fol.all Nat (x => fol.not (eq 0 (succ x)))).
P1 : fol.proof (fol.all Nat (x => fol.not (eq 0_ (succ x)))).
(; x+1 = y+1 -> x = y ;)
P2 : fol.proof (fol.all Nat (x => fol.all Nat (y => fol.imp (eq (succ x) (succ y)) (eq x y)))).
(; x+0 = x ;)
P3 : fol.proof (fol.all Nat (x => eq (add x 0) x)).
P3 : fol.proof (fol.all Nat (x => eq (add x 0_) x)).
(; x + (y + 1) = (x + y) + 1 ;)
P4 : fol.proof (fol.all Nat (x => fol.all Nat (y => eq (add x (succ y)) (succ (add x y))))).
(; Axiom schema of induction ;)
P5 : p : (fol.term Nat -> fol.prop) ->
fol.proof (fol.imp (fol.and (p 0) (fol.all Nat (x => fol.imp (p x) (p (succ x))))) (fol.all Nat p)).
\ No newline at end of file
fol.proof (fol.imp (fol.and (p 0_) (fol.all Nat (x => fol.imp (p x) (p (succ x))))) (fol.all Nat p)).
\ No newline at end of file
......@@ -36,7 +36,6 @@ def sort := fol.sort.
def term := fol.term.
def tactic := tactic.tactic.
def substitution := unif.substitution.
def nat := nat.Nat.
(; Some properties of disjunction ;)
......@@ -86,27 +85,27 @@ def cproof (C : clauses.clause) := proof (cprop C).
(; /!\ nth_lit n C does not fully reduce if n ≥ lenght(C) ;)
def nth_lit : nat -> clauses.clause -> clauses.literal.
[l] nth_lit nat.O (clauses.cons_clause l _) --> l
[n,C] nth_lit (nat.S n) (clauses.cons_clause _ C) --> nth_lit n C.
[l] nth_lit 0 (clauses.cons_clause l _) --> l
[n,C] nth_lit (S n) (clauses.cons_clause _ C) --> nth_lit n C.
(; /!\ remove_nth n C does not fully reduce if n ≥ length(C) ;)
(; /!\ not tail-rec ;)
def remove_nth : nat -> clauses.clause -> clauses.clause.
[C] remove_nth nat.O (clauses.cons_clause _ C) --> C
[n,l,C] remove_nth (nat.S n) (clauses.cons_clause l C) --> clauses.cons_clause l (remove_nth n C).
[C] remove_nth 0 (clauses.cons_clause _ C) --> C
[n,l,C] remove_nth (S n) (clauses.cons_clause l C) --> clauses.cons_clause l (remove_nth n C).
def cycle_nth (n : nat) (C : clauses.clause) : clauses.clause :=
clauses.cons_clause (nth_lit n C) (remove_nth n C).
def cycle_nth_correct : n : nat -> C : clauses.clause -> cproof C -> cproof (cycle_nth n C).
[l,C,H] cycle_nth_correct nat.O (clauses.cons_clause l C) H --> H
[n,l,C,H] cycle_nth_correct (nat.S n) (clauses.cons_clause l C) H -->
fol.or_elim (lprop l) (cprop C) (cprop (cycle_nth (nat.S n) (clauses.cons_clause l C))) H
[l,C,H] cycle_nth_correct 0 (clauses.cons_clause l C) H --> H
[n,l,C,H] cycle_nth_correct (S n) (clauses.cons_clause l C) H -->
fol.or_elim (lprop l) (cprop C) (cprop (cycle_nth (S n) (clauses.cons_clause l C))) H
(Hl => or_intro_2 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C)))
(or_intro_1 (lprop l) (cprop (remove_nth n C)) Hl))
(HC =>
fol.or_elim (lprop (nth_lit n C)) (cprop (remove_nth n C))
(cprop (cycle_nth (nat.S n) (clauses.cons_clause l C)))
(cprop (cycle_nth (S n) (clauses.cons_clause l C)))
(cycle_nth_correct n C HC)
(Hn => or_intro_1 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C))) Hn)
(Hr => or_intro_2 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C))) (or_intro_2 (lprop l) (cprop (remove_nth n C)) Hr))).
......
......@@ -126,44 +126,44 @@ def refine2 (A : prop) (B : prop) (C : prop) (f : proof A -> proof B -> proof C)
(; refinen n A1 ... An B f c1 ... cn proves G |- B if each ci proves G |- Ai ;)
props : nat.Nat -> Type.
nil_prop : props nat.O.
cons_prop : n : nat.Nat -> prop -> props n -> props (nat.S n).
def snoc_prop : n : nat.Nat -> props n -> prop -> props (nat.S n).
[p] snoc_prop nat.O nil_prop p --> cons_prop nat.O p nil_prop
[n,p,ps,q] snoc_prop (nat.S n) (cons_prop _ p ps) q --> cons_prop (nat.S n) p (snoc_prop n ps q).
tactics : nat.Nat -> Type.
nil_tactic : tactics nat.O.
cons_tactic : n : nat.Nat -> tactic -> tactics n -> tactics (nat.S n).
def f_T : n : nat.Nat -> prop -> props n -> Type.
[B] f_T nat.O B nil_prop --> proof B
[n,B,A,As] f_T (nat.S n) B (cons_prop _ A As) --> proof A -> f_T n B As.
def refinen_aux : n : nat.Nat -> As : props n -> B : prop -> f_T n B As -> tactics n -> tactic.
[B,b] refinen_aux (nat.O) nil_prop B b nil_tactic --> exact B b
[n,A,As,B,f,c,cs] refinen_aux (nat.S n) (cons_prop _ A As) B f (cons_tactic _ c cs) -->
props : nat -> Type.
nil_prop : props 0.
cons_prop : n : nat -> prop -> props n -> props (S n).
def snoc_prop : n : nat -> props n -> prop -> props (S n).
[p] snoc_prop 0 nil_prop p --> cons_prop 0 p nil_prop
[n,p,ps,q] snoc_prop (S n) (cons_prop _ p ps) q --> cons_prop (S n) p (snoc_prop n ps q).
tactics : nat -> Type.
nil_tactic : tactics 0.
cons_tactic : n : nat -> tactic -> tactics n -> tactics (S n).
def f_T : n : nat -> prop -> props n -> Type.
[B] f_T 0 B nil_prop --> proof B
[n,B,A,As] f_T (S n) B (cons_prop _ A As) --> proof A -> f_T n B As.
def refinen_aux : n : nat -> As : props n -> B : prop -> f_T n B As -> tactics n -> tactic.
[B,b] refinen_aux 0 nil_prop B b nil_tactic --> exact B b
[n,A,As,B,f,c,cs] refinen_aux (S n) (cons_prop _ A As) B f (cons_tactic _ c cs) -->
bind A c (a : proof A =>
refinen_aux n As B (f a) cs).
def ntactics_T : nat.Nat -> Type.
[] ntactics_T nat.O --> tactic
[n] ntactics_T (nat.S n) --> tactic -> ntactics_T n.
def ntactics_T : nat -> Type.
[] ntactics_T 0 --> tactic
[n] ntactics_T (S n) --> tactic -> ntactics_T n.
def read_certs : n : nat.Nat -> (tactics n -> tactic) -> ntactics_T n.
[c] read_certs nat.O c --> c nil_tactic
[n,f] read_certs (nat.S n) f --> c => read_certs n (cs => f (cons_tactic n c cs)).
def read_certs : n : nat -> (tactics n -> tactic) -> ntactics_T n.
[c] read_certs 0 c --> c nil_tactic
[n,f] read_certs (S n) f --> c => read_certs n (cs => f (cons_tactic n c cs)).
def refinen_T : m : nat.Nat -> n : nat.Nat -> nat.Nat -> props m -> Type.
[m,k,As] refinen_T m nat.O k As --> B : prop -> f_T m B As -> ntactics_T k.
[m,n,k,As] refinen_T m (nat.S n) k As --> A : prop -> refinen_T (nat.S m) n k (snoc_prop m As A).
def refinen_T : m : nat -> n : nat -> nat -> props m -> Type.
[m,k,As] refinen_T m 0 k As --> B : prop -> f_T m B As -> ntactics_T k.
[m,n,k,As] refinen_T m (S n) k As --> A : prop -> refinen_T (S m) n k (snoc_prop m As A).
def read_props : m : nat.Nat -> n : nat.Nat -> k : nat.Nat -> As : props m -> refinen_T m n k As.
[m,f,As] read_props m nat.O m As --> B => f => read_certs m (refinen_aux m As B f)
[m,n,k,f,As] read_props m (nat.S n) k As --> A => read_props (nat.S m) n k (snoc_prop m As A).
def read_props : m : nat -> n : nat -> k : nat -> As : props m -> refinen_T m n k As.
[m,As] read_props m 0 m As --> B => f => read_certs m (refinen_aux m As B f)
[m,n,k,As] read_props m (S n) k As --> A => read_props (S m) n k (snoc_prop m As A).
def refinen (n : nat.Nat) := read_props nat.O n n nil_prop.
def refinen (n : nat) := read_props 0 n n nil_prop.
(; fix_term A f a proves G |- B if f (fix_term A f) a proves G |- B ;)
def fix_term : A : sort -> ((term A -> tactic) -> term A -> tactic) -> term A -> tactic.
......@@ -344,7 +344,7 @@ proves G,A |- C, and c3 proves G,B |- C ;)
def destruct_or (A : prop) (B : prop) (c1 : tactic) (c2 : tactic) (c3 : tactic) : tactic
:=
with_goal (G =>
refinen (nat.S (nat.S (nat.S nat.O)))
refinen (S (S (S 0)))
(fol.or A B)
(fol.imp A G)
(fol.imp B G)
......@@ -367,7 +367,7 @@ def assert (A : prop) (c1 : tactic) (c2 : tactic) : tactic
c2 proves G |- A, and c2 proves G,B |- C ;)
def destruct_imp (A : prop) (B : prop) (c1 : tactic) (c2 : tactic) (c3 : tactic) : tactic
:=
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => fol.imp_elim B G bg (fol.imp_elim A B ab a)) c1 c2 (intro c3)).
with_goal (G => refinen (S (S (S 0))) (imp A B) A (imp B G) G (ab => a => bg => fol.imp_elim B G bg (fol.imp_elim A B ab a)) c1 c2 (intro c3)).
(; absurd proves anything if the current context contains an
assumption and its negation. ;)
......
......@@ -211,15 +211,15 @@ def unify' (pb : unify_problem) :=
A : sort.
f : function.
[] fol.fun_domain f --> read_sorts (nat.S (nat.S nat.O)) A A.
[] fol.fun_domain f --> read_sorts 2 A A.
[] fol.fun_codomain f --> A.
a : function.
[] fol.fun_domain a --> read_sorts nat.O.
[] fol.fun_domain a --> read_sorts 0.
[] fol.fun_codomain a --> A.
b : function.
[] fol.fun_domain b --> read_sorts nat.O.
[] fol.fun_domain b --> read_sorts 0.
[] fol.fun_codomain b --> A.
x : term A.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment