Commit 3daedc38 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Use dkmeta to separate the meta-level unsafe functions from safe mode

parent a990090b
.bkp/ .bkp/
*.dko *.dko
*.dkm
*.dk *.dk
*.trs
!builtins.dk !builtins.dk
.depend .depend
_build/ _build/
......
...@@ -49,19 +49,39 @@ SKINDENT=skindent ...@@ -49,19 +49,39 @@ SKINDENT=skindent
SKCHECK=skcheck SKCHECK=skcheck
SKDEP=skdep SKDEP=skdep
DKDEP=dkdep DKDEP=dkdep
DKMETA=../dedukti/dkmeta.native
CONFLUENCECHECKER=$(shell locate csiho.sh) CONFLUENCECHECKER=$(shell locate csiho.sh)
DKCHECKOPTIONS=-v -d #-cc $(CONFLUENCECHECKER) CCOPT=-cc $(CONFLUENCECHECKER)
DKCHECKOPTIONS=-v -d $(CCOPT)
DKDEPOPTIONS=-v DKDEPOPTIONS=-v
all: $(DKOS) sigmaid all: $(DKOS) sigmaid
%.dkm: %.sk
$(SKINDENT) $< > $@
%.dk: %.dkm unsafe/dk_obj_dec.dko
$(DKMETA) -I unsafe $< > $@
%.dko: %.dk
$(DKCHECK) -e $(DKCHECKOPTIONS) $<
builtins.dko: builtins.dk builtins.dko: builtins.dk
$(DKCHECK) -e $< $(DKCHECK) -e $<
%.dko: %.sk dk_type.dko: dk_type.sk builtins.dko
$(SKCHECK) -e $(DKCHECKOPTIONS) $< $(SKCHECK) -e $<
dk_obj_dec.dko: dk_obj_dec.sk
$(SKCHECK) -e -nl $< dk_obj.dko: dk_obj.sk dk_type.dko builtins.dko
$(SKCHECK) -e $<
unsafe/dk_obj_dec.dko: unsafe/dk_obj_dec.sk builtins.dko dk_type.dko dk_obj.dko
cd unsafe && $(SKCHECK) -I .. -e -nl ../$<
test.sk: sigmaid.$(COMPILE_MODE)
./sigmaid.$(COMPILE_MODE) test.sigma
test.dk: dk_obj_examples.dko
.v.vo: .v.vo:
coqc $< coqc $<
...@@ -71,13 +91,10 @@ dk_obj_dec.dko: dk_obj_dec.sk ...@@ -71,13 +91,10 @@ dk_obj_dec.dko: dk_obj_dec.sk
.ml.byte: .ml.byte:
ocamlbuild -use-menhir $@ ocamlbuild -use-menhir $@
depend: .depend
.depend: $(SKS)
$(SKDEP) $(DKDEPOPTIONS) $(SKS) > .depend
clean: clean:
rm -rf *.dko dk_*.dk *.vo *.glob .depend tmp.* \ rm -rf *.dko *.dkm dk_*.dk *.vo *.glob .depend tmp.* \
test.sk test.v \ test.sk test.dk test.v \
unsafe/*.dko \
sigmaid sigmaid.native sigmaid.byte _build sigmaid sigmaid.native sigmaid.byte _build
sigmaid: sigmaid.$(COMPILE_MODE) sigmaid: sigmaid.$(COMPILE_MODE)
...@@ -86,14 +103,9 @@ sigmaid: sigmaid.$(COMPILE_MODE) ...@@ -86,14 +103,9 @@ sigmaid: sigmaid.$(COMPILE_MODE)
install: sigmaid install: sigmaid
install sigmaid $(INSTALL_DIR)/ install sigmaid $(INSTALL_DIR)/
test.sk: sigmaid.$(COMPILE_MODE)
./sigmaid.$(COMPILE_MODE) test.sigma
test.v: sigmaid.$(COMPILE_MODE) test.v: sigmaid.$(COMPILE_MODE)
./sigmaid.$(COMPILE_MODE) test.sigma ./sigmaid.$(COMPILE_MODE) test.sigma
test.dko: test.sk dk_obj_examples.dko
test.vo: test.v coq_obj.vo test.vo: test.v coq_obj.vo
test: test.dko test.vo test: test.dko test.vo
......
...@@ -225,7 +225,7 @@ def colorPoint := ...@@ -225,7 +225,7 @@ def colorPoint :=
def ColorPoint := Expr colorPoint. def ColorPoint := Expr colorPoint.
def ColorPoint_to_Point : ColorPoint -> Point def ColorPoint_to_Point : ColorPoint -> Point
:= dk_obj.coerce colorPoint point (dk_obj_dec.find_st colorPoint point). := dk_obj.coerce colorPoint point (dk_obj_dec.find_sub colorPoint point).
def myPoint : Point def myPoint : Point
:= :=
...@@ -273,15 +273,15 @@ def PrivateCell := Expr privateCell. ...@@ -273,15 +273,15 @@ def PrivateCell := Expr privateCell.
def Private_to_Prom : PrivateCell -> PromCell def Private_to_Prom : PrivateCell -> PromCell
:= :=
dk_obj.coerce privateCell promCell (dk_obj_dec.find_st privateCell promCell). dk_obj.coerce privateCell promCell (dk_obj_dec.find_sub privateCell promCell).
def Prom_to_Rom : PromCell -> RomCell def Prom_to_Rom : PromCell -> RomCell
:= :=
dk_obj.coerce promCell romCell (dk_obj_dec.find_st promCell romCell). dk_obj.coerce promCell romCell (dk_obj_dec.find_sub promCell romCell).
def Private_to_Rom : PrivateCell -> RomCell def Private_to_Rom : PrivateCell -> RomCell
:= :=
dk_obj.coerce privateCell romCell (dk_obj_dec.find_st privateCell romCell). dk_obj.coerce privateCell romCell (dk_obj_dec.find_sub privateCell romCell).
def myRom : RomCell def myRom : RomCell
:= :=
......
...@@ -129,7 +129,7 @@ let rec print_term out_fmter : tterm -> unit = function ...@@ -129,7 +129,7 @@ let rec print_term out_fmter : tterm -> unit = function
print_label l print_label l
print_par_meth m print_par_meth m
| Tcast (t, ty1, ty2) -> | Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>dk_obj.coerce@ %a@ %a@ (@[dk_obj_dec.find_st@ %a@ %a@])@ %a@]" Format.fprintf out_fmter "@[<hov>dk_obj.coerce@ %a@ %a@ (@[dk_obj_dec.find_sub@ %a@ %a@])@ %a@]"
print_par_ty ty1 print_par_ty ty1
print_par_ty ty2 print_par_ty ty2
print_par_ty ty1 print_par_ty ty1
......
...@@ -47,3 +47,6 @@ def find_pos_2 : l : label -> A : type -> B : type -> pos l A B. ...@@ -47,3 +47,6 @@ def find_pos_2 : l : label -> A : type -> B : type -> pos l A B.
def find_st : A : type -> B : type -> dk_type.st A B. def find_st : A : type -> B : type -> dk_type.st A B.
[A] find_st A dk_type.tnil --> dk_type.st_nil A [A] find_st A dk_type.tnil --> dk_type.st_nil A
[A,l,B,C] find_st A (dk_type.tcons l B C) --> dk_type.st_cons A l B C (find_pos_2 l B A) (find_st A C). [A,l,B,C] find_st A (dk_type.tcons l B C) --> dk_type.st_cons A l B C (find_pos_2 l B A) (find_st A C).
def find_sub (A : type) (B : type) : dk_type.sub A B :=
dk_type.domain_subtype A B (find_st A B).
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