diff options
| -rw-r--r-- | Makefile | 25 | ||||
| -rw-r--r-- | _CoqProject | 12 | ||||
| -rw-r--r-- | env.mkiv | 6 | ||||
| -rw-r--r-- | main.org | 11 |
4 files changed, 41 insertions, 13 deletions
diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..bb42417 --- /dev/null +++ b/Makefile @@ -0,0 +1,25 @@ +COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser +COQINCLUDES := -Q . predaware \ + -R ../vericert/src vericert \ + $(foreach d, $(COMPCERTRECDIRS), -R ../vericert/lib/CompCert/$(d) compcert.$(d)) \ + -R ../vericert/lib/CompCert/flocq Flocq \ + -R ../vericert/lib/CompCert/MenhirLib MenhirLib + +COQMAKE := $(COQBIN)coq_makefile + +VS := Main.v + +all: Makefile.coq _CoqProject + $(MAKE) -f Makefile.coq + +Makefile.coq _CoqProject: force + @echo "COQMAKE Makefile.coq" + $(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq + echo "$(COQINCLUDES)" >_CoqProject + +force: + +clean: + git clean -dfx + +.PHONY: force all clean diff --git a/_CoqProject b/_CoqProject index 2255ae0..872ea42 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,11 +1 @@ --R ../vericert/src vericert --R ../vericert/lib/CompCert/lib compcert.lib --R ../vericert/lib/CompCert/common compcert.common --R ../vericert/lib/CompCert/verilog compcert.verilog --R ../vericert/lib/CompCert/backend compcert.backend --R ../vericert/lib/CompCert/cfrontend compcert.cfrontend --R ../vericert/lib/CompCert/driver compcert.driver --R ../vericert/lib/CompCert/cparser compcert.cparser --R ../vericert/lib/CompCert/flocq Flocq --R ../vericert/lib/CompCert/MenhirLib MenhirLib --Q . symb +-Q . predaware -R ../vericert/src vericert -R ../vericert/lib/CompCert/lib compcert.lib -R ../vericert/lib/CompCert/common compcert.common -R ../vericert/lib/CompCert/verilog compcert.verilog -R ../vericert/lib/CompCert/backend compcert.backend -R ../vericert/lib/CompCert/cfrontend compcert.cfrontend -R ../vericert/lib/CompCert/driver compcert.driver -R ../vericert/lib/CompCert/cparser compcert.cparser -R ../vericert/lib/CompCert/flocq Flocq -R ../vericert/lib/CompCert/MenhirLib MenhirLib @@ -87,4 +87,10 @@ \setupvimtyping[OrgBlkSrcCoq][margin=5mm] +\setupregister[OrgConcept][ + style={\bfa\tt}, + color=darkcyan, + textstyle=tt, +] + \stopenvironment @@ -4,6 +4,7 @@ #+context_header_extra: \environment env #+options: syntax:vim toc:nil #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v +#+auto_tangle: t One main optimisation in compilers targeting parallel architectures is /instruction scheduling/, where instructions are placed into time-slots statically so that these can be executed in parallel. @@ -90,8 +91,8 @@ with expression_list : Type := The interesting thing to note about this abstract expression type is that it is weakly typed, meaning predicates are not any different to standard expressions. The correctness is therefore governed by how the expressions are generated, and to what resource they are assigned to in the -final expression tree. We will also need some kind of equality check for these expressions, so we -can assume that we can implement a decidable check like the following: +final expression tree.[fn:2] We will also need some kind of equality check for these expressions, so +we can assume that we can implement a decidable check like the following: #+begin_src coq Axiom expression_dec: @@ -122,6 +123,8 @@ Definition predicated A := NE.non_empty (pred_op * A). Definition pred_expr := predicated expression. #+end_src +We can then also speak about equivalence between two predicates by + #+begin_src coq Definition apred : Type := expression. Definition apred_op := @Predicate.pred_op apred. @@ -240,5 +243,9 @@ End R_indexed. * Footnotes +[fn:2] We can see that predicates are actually not needed in the semantics of any other +expressions. It might therefore be better to create a separate ~predicate_expression~ which will +only set predicates based on a condition. + [fn:1] This post uses noweb syntax to specify pieces of code defined elsewhere, and will link to those pieces of code directly. |