diff options
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9e1f156..d292722 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -57,8 +57,8 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). Module HTLState <: State. @@ -516,13 +516,13 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (st_controllogic s)) (create_arr_state_incr s sz ln i). -Definition max_pc_map (m : Maps.PTree.t stmnt) := +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. Lemma max_pc_map_sound: - forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). Proof. - intros until i. + intros until i. unfold max_pc_function. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). (* extensionality *) intros. apply H0. rewrite H; auto. @@ -530,14 +530,13 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. unfold Ple, Plt in *. lia. - apply Ple_trans with a. auto. - unfold Ple, Plt in *. lia. + inv H2. xomega. + apply Ple_trans with a. auto. xomega. Qed. Lemma max_pc_wf : - forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - map_well_formed m. + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. Proof. unfold map_well_formed. intros. exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. @@ -591,7 +590,8 @@ Definition add_data_instr (n : node) (st : stmnt) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + (AssocMap.set n (Vseq (AssocMapExt.get_default + _ Vskip n s.(st_datapath)) st) s.(st_datapath)) s.(st_controllogic)) (add_data_instr_state_incr s n st). @@ -655,7 +655,6 @@ Abort. (AssocMap.set n st s.(st_controllogic))) (add_control_instr_force_state_incr s n st). - Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => |