Merge pull request #363 from pataei/main

Adding first draft of P4's abstract syntax to formalization doc
verified-network-toolchain · Oct 10, 2022 · 6627cf7 · 6627cf7
2 parents fbdc1b6 + 73bfc0b
commit 6627cf7
Show file tree

Hide file tree

Showing 22 changed files with 3,620 additions and 543 deletions.
diff --git a/docs/petr4spec/Makefile b/docs/petr4spec/Makefile
@@ -1,15 +1,9 @@
 
 SPEC=Petr4-spec
 
-all: build/${SPEC}.pdf
-
-build/${SPEC}.pdf: ${SPEC}.mdk
-	madoko --pdf -vv --png --odir=build $<
-
-build/${SPEC}.pdf: grammar.mdk p4.json
 
 html: ${SPEC}.mdk grammar.mdk p4.json
-	madoko -vv --png --odir=build $<
+	madoko -vv  --odir=build $<
 
 clean:
 	${RM} -rf build
diff --git a/docs/petr4spec/Petr4-spec.mdk b/docs/petr4spec/Petr4-spec.mdk
diff --git a/docs/petr4spec/figs/actions.png b/docs/petr4spec/figs/actions.png
diff --git a/docs/petr4spec/figs/compileeval.png b/docs/petr4spec/figs/compileeval.png
diff --git a/docs/petr4spec/figs/evalmultiple.png b/docs/petr4spec/figs/evalmultiple.png
diff --git a/docs/petr4spec/figs/headerstack.png b/docs/petr4spec/figs/headerstack.png
diff --git a/docs/petr4spec/figs/maudataflow.png b/docs/petr4spec/figs/maudataflow.png
diff --git a/docs/petr4spec/figs/p4checksum.png b/docs/petr4spec/figs/p4checksum.png
diff --git a/docs/petr4spec/figs/p4interface.png b/docs/petr4spec/figs/p4interface.png
diff --git a/docs/petr4spec/figs/p4prg.png b/docs/petr4spec/figs/p4prg.png
diff --git a/docs/petr4spec/figs/p4transition.png b/docs/petr4spec/figs/p4transition.png
diff --git a/docs/petr4spec/figs/packetfilter.png b/docs/petr4spec/figs/packetfilter.png
diff --git a/docs/petr4spec/figs/parserstatemachine.png b/docs/petr4spec/figs/parserstatemachine.png
diff --git a/docs/petr4spec/figs/prgswitch.png b/docs/petr4spec/figs/prgswitch.png
diff --git a/docs/petr4spec/figs/subparser.png b/docs/petr4spec/figs/subparser.png
diff --git a/docs/petr4spec/figs/switcharch.png b/docs/petr4spec/figs/switcharch.png
diff --git a/docs/petr4spec/figs/vssarch.png b/docs/petr4spec/figs/vssarch.png
diff --git a/docs/petr4spec/figs/vssmau.png b/docs/petr4spec/figs/vssmau.png
diff --git a/docs/petr4spec/make.bat b/docs/petr4spec/make.bat
@@ -1 +1 @@
-madoko --pdf -vv --png --odir=build Petr4-spec.mdk
+madoko --pdf -vv  --odir=build Petr4-spec.mdk
diff --git a/docs/petr4spec/ops.tex b/docs/petr4spec/ops.tex
diff --git a/lib/checker.ml b/lib/checker.ml
diff --git a/lib/types.mli b/lib/types.mli
@@ -196,7 +196,7 @@ and Type : sig
     | IntType of 
         { tags: 'a; 
           expr: Expression.t}
-      (** Fixed-with signed integers *)
+      (** Fixed-width signed integers *)
     | BitType of 
         { tags: 'a; 
           expr: Expression.t}