Fix up some more documentation

1 files changed, 13 insertions, 26 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 2ab79cf..01f2fd9 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -38,14 +38,11 @@ Require Import vericert.hls.Predicate.
 #[local] Open Scope positive.
 #[local] Open Scope pred_op.
 
-(*|
-Schedule Oracle
-===============
+(** ** Schedule Oracle
 
 This oracle determines if a schedule was valid by performing symbolic execution on the input and
 output and showing that these behave the same.  This acts on each basic block separately, as the
-rest of the functions should be equivalent.
-|*)
+rest of the functions should be equivalent.  *)
 
 Definition reg := positive.
 
@@ -54,10 +51,8 @@ Inductive resource : Set :=
 | Pred : reg -> resource
 | Mem : resource.
 
-(*|
-The following defines quite a few equality comparisons automatically, however, these can be
-optimised heavily if written manually, as their proofs are not needed.
-|*)
+(** The following defines quite a few equality comparisons automatically, however, these can be
+optimised heavily if written manually, as their proofs are not needed.  *)
 
 Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
 Proof.
@@ -179,11 +174,9 @@ Proof.
   repeat decide equality.
 Defined.
 
-(*|
-We then create equality lemmas for a resource and a module to index resources uniquely.  The
+(** We then create equality lemmas for a resource and a module to index resources uniquely.  The
 indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be
-shifted right by 1.  This means that they will never overlap.
-|*)
+shifted right by 1.  This means that they will never overlap.  *)
 
 Module R_indexed.
   Definition t := resource.
@@ -200,8 +193,7 @@ Module R_indexed.
   Definition eq := resource_eq.
 End R_indexed.
 
-(*|
-We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use
+(** We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use
 expressions instead of registers as their inputs and outputs.  This means that we can accumulate all
 the results of the operations as general expressions that will be present in those registers.
 
@@ -211,8 +203,7 @@ the results of the operations as general expressions that will be present in tho
 - Estore: A store from a register to a memory location.
 
 Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as
-that enables mutual recursive definitions over the datatypes.
-|*)
+that enables mutual recursive definitions over the datatypes.  *)
 
 Inductive expression : Type :=
 | Ebase : resource -> expression
@@ -321,10 +312,8 @@ Definition predicated A := NE.non_empty (pred_op * A).
 
 Definition pred_expr := predicated expression.
 
-(*|
-Using IMap we can create a map from resources to any other type, as resources can be uniquely
-identified as positive numbers.
-|*)
+(** Using IMap we can create a map from resources to any other type, as resources can be uniquely
+identified as positive numbers.  *)
 
 Module Rtree := ITree(R_indexed).
 
@@ -356,10 +345,8 @@ Definition get_m i := match i with mk_instr_state a b c => c end.
 Definition eval_predf_opt pr p :=
   match p with Some p' => eval_predf pr p' | None => true end.
 
-(*|
-Finally we want to define the semantics of execution for the expressions with symbolic values, so
-the result of executing the expressions will be an expressions.
-|*)
+(** Finally we want to define the semantics of execution for the expressions with symbolic values,
+so the result of executing the expressions will be an expressions.  *)
 
 Section SEMANTICS.
 
@@ -682,7 +669,7 @@ Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
 
 Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
   match pe1, pe2 with
-  (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
+  (* PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
   | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 =>
     if beq_expression e1 e2
     then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with