Commit 3b33ad7c authored by Raphael Cauderlier's avatar Raphael Cauderlier

Example of interactive editing

parent 827252dd
.config_vars
*/*.dko
*/*.dk.depend
**/*.dko
**/*.dk.depend
dktactics
......@@ -3,7 +3,7 @@
INSTALL_BIN_DIR=/usr/local/bin
INSTALL_LIB_DIR=/usr/local/lib/dedukti/dktactics
SUBDIRS= fol meta example
SUBDIRS= fol meta prettyprint ugly example
# To activate confluence checking, set this to "--with-confluence-checking"
CONFIGURE_FLAGS=
......
include ../../.config_vars
# Dedukti files
DKMS = $(wildcard *.dkm)
DKS = $(DKMS:.dkm=.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../../fol
DKMETA_OPTIONS = -I ../../fol -I ../../meta -nl
all: $(DKOS)
%.dk: %.dkm1
$(DKCHECK) $(DKMETA_OPTIONS) -I ../../prettyprint $< > $@
$(DKMETA) $(DKMETA_OPTIONS) -I ../../prettyprint $< > $@
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
%.dkm1: %.dkm
$(DKMETA) $(DKMETA_OPTIONS) -I ../../ugly $< > $@
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dkm
$(DKDEP) $< | sed "s/\.dkm/\.dk/" > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.dk *.dkm1 *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME andcomm.
load_pretty : pretty.pretty_load.
def t : nat -> tactic.tactic.
A : fol.prop.
B : fol.prop.
[] pp.pp_prop _ A --> "A".
[] pp.pp_prop _ B --> "B".
[] t 0 --> tactic.intro (t 1).
[] t 1 --> tactic.destruct_and A B (t 2) (t 3).
[] t 2 --> tactic.assumption.
[] t 3 --> tactic.split (t 4) (t 5).
[] t 4 --> tactic.assumption.
[] t 5 --> tactic.assumption.
def and_commutes := tactic.prove (fol.imp (fol.and A B) (fol.and B A)) (t 0).
#NAME pp.
def sort := fol.sort.
def function := fol.function.
def predicate := fol.predicate.
def term := fol.term.
def sorts := fol.sorts.
def terms := fol.terms.
def fun_domain := fol.fun_domain.
def prop := fol.prop.
def pred_domain := fol.pred_domain.
def ctx := tactic.context.
def tactic := tactic.tactic.
def mtac := mtac.mtactic.
def printf := printf.printf.
def pp_sort : sort -> string.
def pp_fun : function -> string.
def pp_pred : predicate -> string.
var : A : sort -> string -> term A.
def pp_term : A : sort -> term A -> string.
def pp_terms : As : sorts -> terms As -> string.
def pp_terms_cons : A : sort -> term A -> As : sorts -> terms As -> string.
[s] pp_term _ (var _ s) --> s
[f,ts] pp_term _ (fol.apply_fun f ts) --> printf "%s(%s)" (pp_fun f) (pp_terms (fun_domain f) ts).
[] pp_terms fol.nil_sort fol.nil_term --> ""
[A,t,As,ts] pp_terms (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
pp_terms_cons A t As ts.
[B,u] pp_terms_cons B u fol.nil_sort fol.nil_term --> pp_term B u
[B,u,A,t,As,ts] pp_terms_cons B u (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
printf "%s, %s" (pp_term B u) (pp_terms_cons A t As ts).
def pp_prop : nat -> prop -> string.
[A,x,y] pp_prop _ (fol.apply_pred (eq.Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) --> printf "%s = %s" (pp_term A x) (pp_term A y)
[p,ts] pp_prop _ (fol.apply_pred p ts) --> printf "%s(%s)" (pp_pred p) (pp_terms (pred_domain p) ts)
[] pp_prop _ fol.false --> "⊥"
[] pp_prop _ (fol.imp fol.false fol.false) --> "⊤"
[n,A] pp_prop n (fol.imp A fol.false) --> printf "(¬%s)" (pp_prop n A)
[n,A,B] pp_prop n (fol.and (fol.imp A B) (fol.imp B A)) --> printf "(%s ⇔ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.and A B) --> printf "(%s ∧ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.or A B) --> printf "(%s ∨ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.imp A B) --> printf "(%s ⇒ %s)" (pp_prop n A) (pp_prop n B)
[n,A,P] pp_prop n (fol.all A P) --> (v : string => printf "(∀ %s : %s. %s)" v (pp_sort A) (pp_prop (S n) (P (var A v)))) (printf "x_%d" n)
[n,A,P] pp_prop n (fol.ex A P) --> (v : string => printf "(∃ %s : %s. %s)" v (pp_sort A) (pp_prop (S n) (P (var A v)))) (printf "x_%d" n).
def pp_ctx : ctx -> string.
[] pp_ctx tactic.nil_ctx --> ""
[A,c] pp_ctx (tactic.cons_ctx_var A _ c) --> printf "? : %s,
%s" (pp_sort A) (pp_ctx c)
[A,c] pp_ctx (tactic.cons_ctx_proof A _ c) --> printf " %s
%s" (pp_prop 0 A) (pp_ctx c).
def pp_sequent (c : ctx) (goal : prop) : string :=
printf "
%s
------------------
%s
" (pp_ctx c) (pp_prop 0 goal).
#NAME printf.
digit : Type.
d0 : digit.
d1 : digit.
d2 : digit.
d3 : digit.
d4 : digit.
d5 : digit.
d6 : digit.
d7 : digit.
d8 : digit.
d9 : digit.
(; Number in decimal notation ;)
dlist : Type.
dnil : dlist.
dsnoc : dlist -> digit -> dlist.
def dincr : dlist -> dlist.
[] dincr dnil --> dsnoc dnil d1
[l] dincr (dsnoc l d0) --> dsnoc l d1
[l] dincr (dsnoc l d1) --> dsnoc l d2
[l] dincr (dsnoc l d2) --> dsnoc l d3
[l] dincr (dsnoc l d3) --> dsnoc l d4
[l] dincr (dsnoc l d4) --> dsnoc l d5
[l] dincr (dsnoc l d5) --> dsnoc l d6
[l] dincr (dsnoc l d6) --> dsnoc l d7
[l] dincr (dsnoc l d7) --> dsnoc l d8
[l] dincr (dsnoc l d8) --> dsnoc l d9
[l] dincr (dsnoc l d9) --> dsnoc (dincr l) d0.
def nat_to_dlist : nat -> dlist.
[] nat_to_dlist 0 --> dnil
[n] nat_to_dlist (S n) --> dincr (nat_to_dlist n).
def char_to_string (c : char) : string := string_cons c "".
def string_snoc (s : string) (c : char) := string.append s (char_to_string c).
def digit_to_char : digit -> char.
[] digit_to_char d0 --> '0'
[] digit_to_char d1 --> '1'
[] digit_to_char d2 --> '2'
[] digit_to_char d3 --> '3'
[] digit_to_char d4 --> '4'
[] digit_to_char d5 --> '5'
[] digit_to_char d6 --> '6'
[] digit_to_char d7 --> '7'
[] digit_to_char d8 --> '8'
[] digit_to_char d9 --> '9'.
def dlist_to_string : dlist -> string.
def dlist_to_string_aux : dlist -> string.
[] dlist_to_string_aux dnil --> ""
[l,d] dlist_to_string_aux (dsnoc l d) -->
string_snoc (dlist_to_string_aux l) (digit_to_char d).
[] dlist_to_string dnil --> "0"
[l,d] dlist_to_string (dsnoc l d) -->
string_snoc (dlist_to_string_aux l) (digit_to_char d).
def nat_to_string (n : nat) : string :=
dlist_to_string (nat_to_dlist n).
def printf_type : string -> Type.
[] printf_type "" --> string
[s] printf_type (string_cons '%' (string_cons 'd' s)) --> nat -> printf_type s
[s] printf_type (string_cons '%' (string_cons 's' s)) --> string -> printf_type s
[s] printf_type (string_cons _ s) --> printf_type s.
def printf_acc : fmt : string -> string -> printf_type fmt.
[acc] printf_acc "" acc --> acc
[fmt,acc] printf_acc (string_cons '%' (string_cons 'd' fmt)) acc --> n : nat =>
printf_acc fmt (string.append acc (nat_to_string n))
[fmt,acc] printf_acc (string_cons '%' (string_cons 's' fmt)) acc --> str : string =>
printf_acc fmt (string.append acc str)
[c,fmt,acc] printf_acc (string_cons c fmt) acc -->
printf_acc fmt (string_snoc acc c).
def printf (fmt : string) : printf_type fmt := printf_acc fmt "".
#NAME string.
def append : string -> string -> string.
[s] append "" s --> s
[c,s1,s2] append (string_cons c s1) s2 --> string_cons c (append s1 s2).
\ No newline at end of file
include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -I ../meta -nl
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME pretty.
pretty_load : Type.
eval_tactic_pretty : tactic.tactic -> string -> goal : fol.prop ->
mtac.mtactic goal.
[ctx,goal,t] tactic.eval_tactic ctx goal t --> eval_tactic_pretty t (pp.pp_sequent ctx goal) goal.
include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -nl
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME pretty.
pretty_load : Type.
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