Move around generating functions

2 files changed, 68 insertions, 68 deletions

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index b2fdd63..8e8c9b5 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -289,6 +289,70 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest
       Some (new_p, f <-e pruned)
   end.
 
+Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => (f #r (Reg r)) :: lst
+  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p => lst
+  | RBexit p c => lst
+  end.
+
+Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => lst
+  | RBload  p chunk addr rl r => lst
+  | RBstore p chunk addr rl r => (f #r Mem) :: lst
+  | RBsetpred p' c args p => lst
+  | RBexit p c => lst
+  end.
+
+Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pred_op :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => lst
+  | RBload  p chunk addr rl r => lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p => from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) :: lst
+  | RBexit p c => lst
+  end.
+
+Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
+  let '(p, f, l, lm) := s in
+  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
+
+Definition update'' (s: pred_op * forest * list pred_expr * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list pred_op) :=
+  let '(p, f, l, lm, lp) := s in
+  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i).
+
+Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) :=
+  match i with
+  | RBop (Some p) _ _ _
+  | RBload (Some p) _ _ _ _
+  | RBstore (Some p) _ _ _ _
+  | RBexit (Some p) _ =>
+    Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p))
+  | RBsetpred p' c args p =>
+    let preds' := match p' with
+                  | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'')
+                  | None => preds
+                  end
+    in
+    match preds' ! p with
+    | Some _ => None
+    | None => Some (PTree.set p tt preds')
+    end
+  | _ => Some preds
+  end.
+
+Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
+  Option.bind (fun x => Option.bind (fun _ => Some x)
+    (mfold_left gather_predicates b (Some (PTree.empty _))))
+      (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
+        (mfold_left update' b (Some (Ptrue, empty, nil, nil)))).
+
 (*Compute match update (T, mk_forest (PTree.empty _) (PTree.empty _) (NE.singleton (T, EEbase)))
   (RBop None Op.Odiv (1::2::nil) 3) with
   | Some x =>
@@ -311,10 +375,10 @@ Get a sequence from the basic block.
 Definition abstract_sequence (b : list instr) : option forest :=
   Option.map snd (mfold_left update b (Some (Ptrue, empty))).
 
-Compute Option.bind (fun x => RTree.get (Reg 3) (forest_regs x))
-  (abstract_sequence
-    [RBop None Op.Odiv [1;2] 3;
-     RBop None (Op.Ointconst (Int.repr 10)) nil 3]).
+(* Compute Option.bind (fun x => RTree.get (Reg 3) (forest_regs x)) *)
+(*   (abstract_sequence *)
+(*     [RBop None Op.Odiv [1;2] 3; *)
+(*      RBop None (Op.Ointconst (Int.repr 10)) nil 3]). *)
 
 (*|
 Check equivalence of control flow instructions.  As none of the basic blocks
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 29667f1..815f005 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -73,44 +73,6 @@ Context (prog: GibleSeq.program) (tprog : GiblePar.program).
 Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog.
 Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog.
 
-Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
-  match i with
-  | RBnop => lst
-  | RBop p op rl r => (f #r (Reg r)) :: lst
-  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
-  | RBstore p chunk addr rl r => lst
-  | RBsetpred p' c args p => lst
-  | RBexit p c => lst
-  end.
-
-Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
-  match i with
-  | RBnop => lst
-  | RBop p op rl r => lst
-  | RBload  p chunk addr rl r => lst
-  | RBstore p chunk addr rl r => (f #r Mem) :: lst
-  | RBsetpred p' c args p => lst
-  | RBexit p c => lst
-  end.
-
-Definition remember_expr_p (f : forest) (lst: list pred_op) (i : instr): list pred_op :=
-  match i with
-  | RBnop => lst
-  | RBop p op rl r => lst
-  | RBload  p chunk addr rl r => lst
-  | RBstore p chunk addr rl r => lst
-  | RBsetpred p' c args p => from_predicated_inv (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f))) :: lst
-  | RBexit p c => lst
-  end.
-
-Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
-  let '(p, f, l, lm) := s in
-  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
-
-Definition update'' (s: pred_op * forest * list pred_expr * list pred_expr * list pred_op) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr * list pred_op) :=
-  let '(p, f, l, lm, lp) := s in
-  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i, remember_expr_p f lp i)) (update (p, f) i).
-
 Lemma equiv_update:
   forall i p f l lm p' f' l' lm',
     mfold_left update' i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -170,32 +132,6 @@ Lemma equiv_update'':
     mfold_left update i (Some (p, f)) = Some (p', f').
 Proof. eauto using equiv_update', equiv_update. Qed.
 
-Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) :=
-  match i with
-  | RBop (Some p) _ _ _
-  | RBload (Some p) _ _ _ _
-  | RBstore (Some p) _ _ _ _
-  | RBexit (Some p) _ =>
-    Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p))
-  | RBsetpred p' c args p =>
-    let preds' := match p' with
-                  | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'')
-                  | None => preds
-                  end
-    in
-    match preds' ! p with
-    | Some _ => None
-    | None => Some (PTree.set p tt preds')
-    end
-  | _ => Some preds
-  end.
-
-Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
-  Option.bind (fun x => Option.bind (fun _ => Some x)
-    (mfold_left gather_predicates b (Some (PTree.empty _))))
-      (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
-        (mfold_left update' b (Some (Ptrue, empty, nil, nil)))).
-
 Definition i_state (s: istate): instr_state :=
   match s with
   | Iexec t => t