all: Add documentation headers in preparation for the release

mit-plv · Nov 25, 2019 · 9a4771c · 9a4771c
1 parent b41edd5
commit 9a4771c
Show file tree

Hide file tree

Showing 71 changed files with 73 additions and 26 deletions.
diff --git a/coq/CircuitCorrectness.v b/coq/CircuitCorrectness.v
@@ -1,3 +1,4 @@
+(*! Circuits | Compiler correctness proof !*)
 Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring Coq.setoid_ring.Ring.
 
 Require Import

diff --git a/coq/CircuitProperties.v b/coq/CircuitProperties.v
@@ -1,3 +1,4 @@
+(*! Circuits | Lemmas used in the compiler-correctness proof !*)
 Require Export Koika.Circuits.
 Require Import Koika.Common Koika.Environments Koika.Types.
 

diff --git a/coq/Circuits.v b/coq/Circuits.v
@@ -1,3 +1,4 @@
+(*! Circuits | Syntax, semantics, compilation, and optimization of circuits !*)
 Require Export Koika.Common Koika.Environments.
 Require Import Koika.Syntax Koika.TypedSyntax Koika.TypedSyntaxTools.
 

diff --git a/coq/Common.v b/coq/Common.v
@@ -1,3 +1,4 @@
+(*! Utilities | Shared utilities !*)
 Require Export Coq.omega.Omega.
 Require Export Coq.Lists.List Coq.Bool.Bool Coq.Strings.String.
 Require Export Koika.EqDec Koika.Vect Koika.FiniteType Koika.Show.

diff --git a/coq/DeriveShow.v b/coq/DeriveShow.v
@@ -1,3 +1,4 @@
+(*! Utilities | Automatic derivation of Show instances !*)
 Require Import Koika.Show.
 
 Require Koika.IdentParsing.

diff --git a/coq/Desugaring.v b/coq/Desugaring.v
@@ -1,3 +1,4 @@
+(*! Frontend | Desugaring of untyped actions !*)
 Require Import Koika.Common Koika.Environments Koika.Syntax Koika.TypedSyntax Koika.ErrorReporting Koika.SyntaxMacros.
 
 Section Desugaring.

diff --git a/coq/Environments.v b/coq/Environments.v
@@ -1,3 +1,4 @@
+(*! Utilities | Environments used to track variable bindings !*)
 Require Import Koika.Common.
 Require Export Koika.Member.
 

diff --git a/coq/EqDec.v b/coq/EqDec.v
@@ -1,3 +1,4 @@
+(*! Utilities | Decidable equality typeclass !*)
 Require Import Coq.Strings.String.
 Require Import Coq.Vectors.Vector.
 

diff --git a/coq/ErrorReporting.v b/coq/ErrorReporting.v
@@ -1,3 +1,4 @@
+(*! Frontend | Typechecking errors and error-reporting functions !*)
 Require Import Koika.Common Koika.Types.
 
 Section TypeErrors.

diff --git a/coq/Extraction.v b/coq/Extraction.v
@@ -1,3 +1,4 @@
+(*! Interop | Extraction to OCaml (compiler and utilities) !*)
 Require Import Koika.ExtractionSetup.
 
 Require Koika.Common

diff --git a/coq/ExtractionSetup.v b/coq/ExtractionSetup.v
@@ -1,3 +1,4 @@
+(*! Interop | Custom extraction settings (also used by external Kôika programs !*)
 Require Export Coq.extraction.Extraction.
 From Coq.extraction Require Export ExtrOcamlBasic ExtrOcamlString ExtrOcamlNatInt ExtrOcamlZInt.
 

diff --git a/coq/FiniteType.v b/coq/FiniteType.v
@@ -1,3 +1,4 @@
+(*! Utilities | Finiteness typeclass !*)
 Require Import Coq.Lists.List.
 Require Import Coq.omega.Omega.
 Import ListNotations.

diff --git a/coq/Frontend.v b/coq/Frontend.v
@@ -1,3 +1,4 @@
+(*! Frontend | Top-level module imported by Kôika programs !*)
 Require Export
         Koika.SyntaxMacros
         Koika.Desugaring
@@ -9,7 +10,8 @@ Require Export
         Koika.TypedSyntaxTools
         Koika.Interop
         Koika.Parsing
-        Koika.DeriveShow.
+        Koika.DeriveShow
+        Koika.ExtractionSetup.
 
 Notation compile_scheduler :=
   (compile_scheduler opt_constprop).

diff --git a/coq/IdentParsing.v b/coq/IdentParsing.v
@@ -1,3 +1,4 @@
+(*! Frontend | Ltac2-based identifier parsing for prettier notations !*)
 Require Import Coq.NArith.NArith Coq.Strings.String.
 Require Import Coq.Init.Byte.
 Require Import Ltac2.Ltac2.

diff --git a/coq/IndexUtils.v b/coq/IndexUtils.v
@@ -1,3 +1,4 @@
+(*! Utilities | Functions on Vect.index elements !*)
 Require Coq.Logic.FinFun.
 Require Import Koika.Common Koika.Vect Koika.Member.
 

diff --git a/coq/Interop.v b/coq/Interop.v
@@ -1,3 +1,4 @@
+(*! Interop | Exporting Kôika programs for use with the cuttlec command-line tool !*)
 Require Import Koika.Common Koika.Environments Koika.Types Koika.TypedSyntax Koika.Circuits.
 Require Export Koika.Primitives.
 

diff --git a/coq/Member.v b/coq/Member.v
@@ -1,3 +1,4 @@
+(*! Utilities | Dependent type tracking membership into a list !*)
 Require Import Koika.Common.
 
 Inductive member {K: Type}: K -> list K -> Type :=

diff --git a/coq/OneRuleAtATime.v b/coq/OneRuleAtATime.v
@@ -1,3 +1,4 @@
+(*! ORAAT | Proof of the One-rule-at-a-time theorem !*)
 Require Import Koika.Common Koika.Syntax Koika.TypedSyntax Koika.SemanticProperties.
 Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring Coq.setoid_ring.Ring.
 

diff --git a/coq/Parsing.v b/coq/Parsing.v
@@ -1,3 +1,4 @@
+(*! Frontend | Parser for the Kôika EDSL !*)
 Require Import
         Koika.Common
         Koika.Syntax

diff --git a/coq/PrimitiveProperties.v b/coq/PrimitiveProperties.v
@@ -1,3 +1,4 @@
+(*! Equations showing how to implement functions on structures and arrays as bitfuns !*)
 Require Import Koika.Primitives.
 Import BitFuns.
 

diff --git a/coq/Primitives.v b/coq/Primitives.v
@@ -1,3 +1,4 @@
+(*! Language | Combinational primitivies available in all Kôika programs !*)
 Require Export Koika.Common Koika.Environments Koika.IndexUtils Koika.Types Koika.ErrorReporting.
 
 Inductive bits_comparison :=

diff --git a/coq/SemanticProperties.v b/coq/SemanticProperties.v
@@ -1,3 +1,4 @@
+(*! ORAAT | Properties of the semantics used in the one-rule-at-a-time theorem !*)
 Require Export Koika.Common Koika.Semantics.
 
 Section Lists.

diff --git a/coq/Semantics.v b/coq/Semantics.v
@@ -1,3 +1,4 @@
+(*! Language | Semantics of typed Kôika programs !*)
 Require Export Koika.Common Koika.Environments Koika.Vect Koika.Syntax Koika.TypedSyntax.
 
 Section Logs.

diff --git a/coq/Show.v b/coq/Show.v
@@ -1,3 +1,4 @@
+(*! Utilities | Show typeclass (α → string) !*)
 Require Export Coq.Strings.String.
 
 Class Show (A: Type) :=

diff --git a/coq/Std.v b/coq/Std.v
@@ -1,3 +1,4 @@
+(*! Stdlib | Standard library !*)
 Require Import Koika.Frontend.
 
 Module Type Fifo.

diff --git a/coq/Syntax.v b/coq/Syntax.v
@@ -1,3 +1,4 @@
+(*! Frontend | Untyped syntax !*)
 Require Export Koika.Common Koika.Primitives Koika.Types Koika.ErrorReporting.
 
 Section Syntax.

diff --git a/coq/SyntaxMacros.v b/coq/SyntaxMacros.v
@@ -1,3 +1,4 @@
+(*! Frontend | Macros used in untyped programs !*)
 Require Import Koika.Common Koika.Syntax Koika.TypedSyntax Koika.Primitives.
 Import PrimUntyped.
 

diff --git a/coq/TypeInference.v b/coq/TypeInference.v
@@ -1,3 +1,4 @@
+(*! Frontend | Type inference and typechecking !*)
 Require Import
         Koika.Common Koika.Environments
         Koika.Syntax Koika.TypedSyntax Koika.SyntaxMacros

diff --git a/coq/TypedSyntax.v b/coq/TypedSyntax.v
@@ -1,3 +1,4 @@
+(*! Language | Typed ASTs !*)
 Require Export Koika.Common Koika.Environments Koika.Types Koika.Primitives.
 
 Import PrimTyped PrimSignatures.

diff --git a/coq/TypedSyntaxProperties.v b/coq/TypedSyntaxProperties.v
@@ -1,3 +1,4 @@
+(*! Tools | Lemmas pertaining to tools on typed syntax !*)
 Require Import Koika.TypedSyntaxTools Koika.Semantics.
 
 Section TypedSyntaxProperties.

diff --git a/coq/TypedSyntaxTools.v b/coq/TypedSyntaxTools.v
@@ -1,3 +1,4 @@
+(*! Tools | Functions defined on typed ASTs !*)
 Require Import Koika.Member Koika.TypedSyntax.
 
 Section TypedSyntaxTools.

diff --git a/coq/Types.v b/coq/Types.v
@@ -1,3 +1,4 @@
+(*! Language | Types used by Kôika programs !*)
 Require Export Coq.Strings.String.
 Require Export Koika.Common Koika.Vect Koika.IndexUtils.
 

diff --git a/coq/UntypedSyntaxTools.v b/coq/UntypedSyntaxTools.v
@@ -1,3 +1,4 @@
+(*! Frontend | Functions on untyped ASTs, including error localization !*)
 Require Import Koika.Syntax.
 
 Section SyntaxTools.

diff --git a/coq/Vect.v b/coq/Vect.v
@@ -1,3 +1,4 @@
+(*! Utilities | Vectors and bitvector library !*)
 Require Import Coq.Lists.List.
 Require Import Coq.omega.Omega.
 Require Export Coq.NArith.NArith.          (* Coq bug: If this isn't exported, other files can't import Vect.vo *)

diff --git a/etc/gen_dune.ml b/etc/gen_dune.ml
diff --git a/examples/collatz.lv b/examples/collatz.lv
@@ -1,3 +1,5 @@
+;;; Computing terms of the Collatz sequence (Lispy Verilog version)
+
 (defun times_three ((v (bits 16))) (bits 16)
   (+ (<< v 1'1) v))
 

diff --git a/examples/collatz.v b/examples/collatz.v
@@ -1,3 +1,4 @@
+(*! Computing terms of the Collatz sequence (Coq version) !*)
 Require Import Koika.Frontend.
 
 Module Collatz.

diff --git a/examples/datatypes.v b/examples/datatypes.v
@@ -1,3 +1,4 @@
+(*! Using structures, enums, and arrays !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := input | output.

diff --git a/examples/external_rule.v b/examples/external_rule.v
@@ -1,3 +1,4 @@
+(*! Calling external (verilog) modules from Kôika !*)
 Require Import Koika.Frontend.
 Require Koika.Std.
 

diff --git a/examples/function_call.v b/examples/function_call.v
@@ -1,3 +1,4 @@
+(*! Calling external functions !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := pc | next_instr.

diff --git a/examples/gcd_machine.v b/examples/gcd_machine.v
@@ -1,3 +1,4 @@
+(*! Computing GCDs !*)
 Require Import Koika.Frontend.
 Require Import Koika.Std.
 

diff --git a/examples/method_call.v b/examples/method_call.v
@@ -1,3 +1,4 @@
+(*! Calling methods of internal modules !*)
 Require Import Koika.Frontend.
 Require Import Koika.Std.
 

diff --git a/examples/pipeline.v b/examples/pipeline.v
@@ -1,3 +1,4 @@
+(*! Building simple pipelines !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := r0 | outputReg | inputReg | invalid | correct.

diff --git a/examples/rv/RVCore.v b/examples/rv/RVCore.v
@@ -1,3 +1,4 @@
+(*! Implementation of our RISC-V core !*)
 Require Import Koika.Frontend.
 Require Import Coq.Lists.List.
 

diff --git a/examples/rv/RVEncoding.v b/examples/rv/RVEncoding.v
@@ -1,3 +1,4 @@
+(*! Encoding-related constants !*)
 Require Import Koika.Frontend.
 
 Definition opcode_LOAD      := Ob~0~0~0~0~0~1~1.

diff --git a/examples/rv/Scoreboard.v b/examples/rv/Scoreboard.v
@@ -1,3 +1,4 @@
+(*! Implementation of a scoreboard !*)
 Require Import Coq.Lists.List.
 
 Require Import Koika.Frontend.

diff --git a/examples/rv/TopLevel.v b/examples/rv/TopLevel.v
@@ -1,3 +1,4 @@
+/*! Verilog wrapper for the RISC-V processor !*/
 module TopLevel(
  input 		   clock,
  input 		   reset,

diff --git a/examples/rv/rv32i_core_pipelined.v b/examples/rv/rv32i_core_pipelined.v
@@ -1,3 +1,4 @@
+(*! Pipelined instantiation of the RISC-V processor !*)
 Require Import Koika.Frontend.
 Require Import RV.RVCore.
 Import RV32ICore.

diff --git a/examples/vector.v b/examples/vector.v
@@ -1,3 +1,4 @@
+(*! Representing vectors of registers using Coq inductives !*)
 Require Import Koika.Frontend.
 
 Definition nregs := 16.

diff --git a/ocaml/backends/coq.ml b/ocaml/backends/coq.ml
@@ -1,3 +1,4 @@
+(*! Coq backend (from Lispy Verilog sources) !*)
 open Common
 open Frontends.Lv
 open Format

diff --git a/ocaml/backends/cpp.ml b/ocaml/backends/cpp.ml
@@ -1,3 +1,4 @@
+(*! C++ backend !*)
 open Common
 module Extr = Cuttlebone.Extr
 

diff --git a/ocaml/backends/dot.ml b/ocaml/backends/dot.ml
@@ -1,3 +1,4 @@
+(*! Graphviz backend !*)
 open Common
 open Cuttlebone
 open Cuttlebone.Graphs

diff --git a/ocaml/backends/gen.ml b/ocaml/backends/gen.ml
@@ -1,3 +1,4 @@
+(*! Embed preamble.hpp into cppPreamble.ml at build time !*)
 let cpp_preamble =
   let inc = open_in "preamble.hpp" in
   let preamble = really_input_string inc (in_channel_length inc) in

diff --git a/ocaml/backends/preamble.hpp b/ocaml/backends/preamble.hpp
@@ -1,3 +1,4 @@
+/*! Preamble shared by all Kôika programs compiled to C++ !*/
 #ifndef _PREAMBLE_HPP
 #define _PREAMBLE_HPP
 

diff --git a/ocaml/backends/verilog.ml b/ocaml/backends/verilog.ml
@@ -1,4 +1,4 @@
-
+(*! Verilog backend !*)
 open Common
 open Cuttlebone
 open Cuttlebone.Util

diff --git a/ocaml/common/common.ml b/ocaml/common/common.ml
@@ -1,3 +1,4 @@
+(*! Shared utilities !*)
 type size_t = int
 type ptr_t = int
 

diff --git a/ocaml/cuttlebone/cuttlebone.ml b/ocaml/cuttlebone/cuttlebone.ml
@@ -1,3 +1,4 @@
+(*! OCaml wrappers around functionality provided by the library extracted from Coq !*)
 type __ = Obj.t
 let __ = let rec f _ = Obj.repr f in Obj.repr f
 

diff --git a/ocaml/cuttlec.ml b/ocaml/cuttlec.ml
@@ -1,3 +1,4 @@
+(*! Command line interface to the compilers !*)
 open Common
 open Printf
 open Frontends

diff --git a/ocaml/frontends/coq.ml b/ocaml/frontends/coq.ml
@@ -1,3 +1,4 @@
+(*! Simple frontend to compile and load OCaml files extracted from Coq !*)
 let ensure_koikalib () =
   Printf.eprintf "Path to Koika: %!";
   Common.command "ocamlfind" ["query"; "koika"]

diff --git a/ocaml/frontends/lv.ml b/ocaml/frontends/lv.ml
@@ -1,3 +1,4 @@
+(*! Lispy Verilog frontend !*)
 open Common
 
 let lcnt x = x.lcnt

diff --git a/ocaml/interop.ml b/ocaml/interop.ml
@@ -1,3 +1,4 @@
+(*! Functions to use if compiling Kôika programs straight from Coq, without going through cuttlec !*)
 open Cuttlebone
 
 let fname ?directory (pkg: _ Extr.koika_package_t) ext =

diff --git a/ocaml/koika.ml b/ocaml/koika.ml
@@ -1,3 +1,4 @@
+(*! Top-level library definition !*)
 module Common = Common
 module Cuttlebone = Cuttlebone
 module Frontends = Frontends

diff --git a/ocaml/registry.ml b/ocaml/registry.ml
@@ -1,3 +1,4 @@
+(*! Stub used to load Kôika programs extracted from Coq into cuttlec  !*)
 let registered_interop_packages : Cuttlebone.Extr.interop_package_t list ref =
   ref []
 

diff --git a/tests/double_write.v b/tests/double_write.v
@@ -1,4 +1,4 @@
-(* Double writes *)
+(*! Double-write detection and prevention !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := reg0.

diff --git a/tests/errors.v b/tests/errors.v
@@ -1,4 +1,4 @@
-(*;;; Syntax and typing errors *)
+(*! Syntax and typing errors in Coq !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := R0.

diff --git a/tests/extcall.v b/tests/extcall.v
@@ -1,4 +1,4 @@
-(* External functions *)
+(*! External functions !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := reg0.

diff --git a/tests/large_writeset.v b/tests/large_writeset.v
@@ -1,4 +1,4 @@
-(* Make sure that the large writeset heuristics in the scheduler don't break things *)
+(*! Make sure that the large writeset heuristics in the scheduler don't break things !*)
 Require Import Koika.Frontend.
 
 Definition N := 10.

diff --git a/tests/name_mangling.lv b/tests/name_mangling.lv
@@ -1,4 +1,4 @@
-;;; Name mangling unit tests
+;;; Unit tests for name mangling
 
 (enum lv_gensym_collisions
   ::_lvs_0 2'0

diff --git a/tests/register_file_bypassing.v b/tests/register_file_bypassing.v
@@ -1,4 +1,4 @@
-(* Ensure that area is reasonable when bypass doesn't need extra tracking *)
+(*! Ensure that area is reasonable when bypasses don't need extra tracking !*)
 Require Import Koika.Frontend.
 Require Import Koika.Std.
 

diff --git a/tests/shadowing.lv b/tests/shadowing.lv
@@ -1,4 +1,4 @@
-;;; Shadowing unit tests
+;;; Unit tests for name shadowing
 
 (module shadowing
   (register r 32'0)

diff --git a/tests/unpack.v b/tests/unpack.v
@@ -1,4 +1,4 @@
-(*;;; Unpacking structures *)
+(*! Structure unpacking !*)
 Require Import Koika.Frontend.
 
 Inductive reg_t := Rpacked | Runpacked.