1 files changed, 14 insertions, 36 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index ac9ac2c..31ea51f 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../lit/scheduler.org::rtlpargen-main][rtlpargen-main]] *)
+(* [[file:../../docs/scheduler.org::rtlpargen-main][rtlpargen-main]] *)
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Globalenvs.
@@ -35,18 +35,12 @@ Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
 Import NE.NonEmptyNotation.
 
-(** * RTLPar Generation *)
-
 #[local] Open Scope positive.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
+(* rtlpargen-main ends here *)
 
-(** ** Abstract Computations
-
-Define the abstract computation using the [update] function, which will set each register to its
-symbolic value.  First we need to define a few helper functions to correctly translate the
-predicates.  *)
-
+(* [[file:../../docs/scheduler.org::rtlpargen-generation][rtlpargen-generation]] *)
 Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
   match l with
   | nil => nil
@@ -139,19 +133,9 @@ Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) :=
 
 Definition pred_ret {A: Type} (a: A) : predicated A :=
   NE.singleton (T, a).
+(* rtlpargen-generation ends here *)
 
-(** *** Update Function
-
-The [update] function will generate a new forest given an existing forest and a new instruction,
-so that it can evaluate a symbolic expression by folding over a list of instructions.  The main
-problem is that predicates need to be merged as well, so that:
-
-1. The predicates are *independent*.
-2. The expression assigned to the register should still be correct.
-
-This is done by multiplying the predicates together, and assigning the negation of the expression to
-the other predicates.  *)
-
+(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-update-function]] *)
 Definition update (f : forest) (i : instr) : forest :=
   match i with
   | RBnop => f
@@ -181,28 +165,22 @@ Definition update (f : forest) (i : instr) : forest :=
        (f # (Pred p))
        (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))
   end.
+(* rtlpargen-update-function ends here *)
 
-(** Implementing which are necessary to show the correctness of the translation validation by
-showing that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
-
-Get a sequence from the basic block.  *)
-
+(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-abstract-seq]] *)
 Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
   | nil => f
   | i :: l => abstract_sequence (update f i) l
   end.
+(* rtlpargen-abstract-seq ends here *)
 
-(** Check equivalence of control flow instructions.  As none of the basic blocks should have been
-moved, none of the labels should be different, meaning the control-flow instructions should match
-exactly.  *)
-
+(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-check-functions]] *)
 Definition check_control_flow_instr (c1 c2: cf_instr) : bool :=
   if cf_instr_eq c1 c2 then true else false.
+(* rtlpargen-check-functions ends here *)
 
-(** We define the top-level oracle that will check if two basic blocks are equivalent after a
-scheduling transformation.  *)
-
+(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-top-check-functions]] *)
 Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
   match bb with
   | nil =>
@@ -241,9 +219,9 @@ Lemma check_scheduled_trees_correct2:
     PTree.get x f1 = None ->
     PTree.get x f2 = None.
 Proof. solve_scheduled_trees_correct. Qed.
+(* rtlpargen-top-check-functions ends here *)
 
-(** ** Top-level Functions  *)
-
+(* [[file:../../docs/scheduler.org::rtlpargen-top-level-functions][rtlpargen-top-level-functions]] *)
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
 Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
@@ -261,4 +239,4 @@ Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
-(* rtlpargen-main ends here *)
+(* rtlpargen-top-level-functions ends here *)