Use sumbool instead of option for decide_ram_wf

3 files changed, 12 insertions, 12 deletions

diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index 8b24336..276ba74 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -162,8 +162,8 @@ Section APPLY_EXTERNCTRL.
           zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned,
           decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk',
           max_list_dec mod_params' mod_st',
-          option_ram_wf mod_clk' (HTL.mod_ram m) with
-    | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some WFRAM =>
+          decide_ram_wf mod_clk' (HTL.mod_ram m) with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS, left WFRAM =>
       OK (HTL.mkmodule
           mod_params'
           mod_datapath'
@@ -189,7 +189,7 @@ Section APPLY_EXTERNCTRL.
     | _, right _, _, _, _ => Error (Errors.msg "ApplyExternctrl: More than 2^32 controlpath states")
     | _, _, right _, _, _ => Error (Errors.msg "ApplyExternctrl: Incorrect ordering of control registers")
     | _, _, _, right _, _ => Error (Errors.msg "ApplyExternctrl: Parameter registers conflict with control registers")
-    | _, _, _, _, None    => Error (Errors.msg "ApplyExternctrl: Ram address register conflicts with control registers")
+    | _, _, _, _, right _ => Error (Errors.msg "ApplyExternctrl: Ram address register conflicts with control registers")
     end.
 End APPLY_EXTERNCTRL.
 
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 3116af3..303dc70 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -448,16 +448,16 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}
                    end; unfold module_ordering; auto.
 Defined.
 
-Definition option_ram_wf (clk : reg) (mr : option HTL.ram) :
-  option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive).
+Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) :
+  {forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive} + {True}.
   refine (
       match mr with
       | Some r =>
         match (plt clk (ram_addr r)) with
-        | left LE => Some _
-        | _ => None
+        | left LE => left _
+        | _ => right I
         end
-      | None => None
+      | None => left _
       end).
-  crush.
+  all: crush.
 Defined.
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v
index b088926..91a6673 100644
--- a/src/hls/Renaming.v
+++ b/src/hls/Renaming.v
@@ -166,8 +166,8 @@ Definition renumber_module (m : HTL.module) : mon HTL.module :=
           zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned,
           decide_order mod_st' mod_finish' mod_return' mod_stk' mod_start' mod_reset' mod_clk',
           max_list_dec mod_params' mod_st',
-          option_ram_wf mod_clk' (HTL.mod_ram m) with
-    | left LEDATA, left LECTRL, left MORD, left WFPARAMS, Some WFRAM =>
+          decide_ram_wf mod_clk' (HTL.mod_ram m) with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS, left WFRAM =>
       ret (HTL.mkmodule
           mod_params'
           mod_datapath'
@@ -193,7 +193,7 @@ Definition renumber_module (m : HTL.module) : mon HTL.module :=
     | _, right _, _, _, _ => error (Errors.msg "Renaming: More than 2^32 controlpath states")
     | _, _, right _, _, _ => error (Errors.msg "Renaming: Incorrect ordering of control registers")
     | _, _, _, right _, _ => error (Errors.msg "Renaming: Parameter registers conflict with control registers")
-    | _, _, _, _, None    => error (Errors.msg "Renaming: Ram address register conflicts with control registers")
+    | _, _, _, _, right _ => error (Errors.msg "Renaming: Ram address register conflicts with control registers")
     end.
 
 Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef :=