Coq: use function type more carefully in untupling

And update the RISC-V patch accordingly.

1 files changed, 28 insertions, 38 deletions

diff --git a/riscv/coq.patch b/riscv/coq.patch
index d1cf3041..6c40e6e2 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,43 +1,34 @@
---- riscv.v.orig	2018-10-22 17:27:20.456069232 +0100
-+++ riscv.v	2018-10-22 17:29:35.588974872 +0100
-@@ -1366,7 +1366,7 @@
- 
- Definition ex_nat (n : ({n : Z & ArithFact (n >= 0)})) 
- : {syn_n : Z & ArithFact (syn_n >= 0)} :=
--   build_ex(n).
-+   (n).
- 
- Definition ex_int (n : (Z))  : {syn_n : Z & ArithFact (True)} := build_ex(n).
- 
-@@ -1441,6 +1441,9 @@
+--- riscv.v	2018-10-22 18:20:01.512785981 +0100
++++ riscv.v.good	2018-10-22 18:19:27.556562080 +0100
+@@ -1260,6 +1260,9 @@
     let v64 : bits 64 := EXTS 64 v in
     subrange_vec_dec (shift_bits_right v64 shift) 31 0.
  
 +Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} :=
 + build_ex (Z.of_nat (n_leading_spaces s)).
 +(*
- Fixpoint n_leading_spaces (arg0 : string) 
+ Fixpoint n_leading_spaces (s : string) 
  : {n : Z & ArithFact (n >= 0)} :=
-    build_ex(let s := (arg0) in
-@@ -1456,7 +1459,7 @@
+    build_ex(let p0_ := s in
+@@ -1273,7 +1276,7 @@
+                                                                              (string_drop s
                                                                                  (build_ex 1)))))))
                    : {n : Z & ArithFact (n >= 0)}))))
-      else 0).
--
-+*)
- Definition spc_forwards '(tt : (unit))  : string := " ".
+-     else 0).
++     else 0).*)
  
- Definition spc_backwards (arg0 : string) 
-@@ -1470,7 +1473,7 @@
+ Definition spc_forwards '(tt : unit)  : string := " ".
+ 
+@@ -1284,7 +1287,7 @@
     let 'n := projT1 (n_leading_spaces s) in
     let p0_ := n in
     if sumbool_of_bool ((Z.eqb p0_ 0)) then None
 -   else Some ((tt, n)).
 +   else Some ((tt, build_ex n)).
  
- Definition opt_spc_forwards '(tt : (unit))  : string := "".
+ Definition opt_spc_forwards '(tt : unit)  : string := "".
  
-@@ -11079,14 +11082,13 @@
+@@ -10432,14 +10435,13 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -54,7 +45,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -11099,27 +11101,27 @@
+@@ -10452,27 +10454,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -88,7 +79,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -11129,10 +11131,10 @@
+@@ -10482,10 +10484,10 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -101,7 +92,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -11258,7 +11260,7 @@
+@@ -10611,7 +10613,7 @@
          : M (TR39_Result)
      | None =>
         (curPTB39 tt) >>= fun w__6 : mword 56 =>
@@ -110,13 +101,12 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -15511,138 +15513,145 @@
+@@ -14651,137 +14653,144 @@
     returnm (true
      : bool).
  
--Fixpoint execute (arg0 : ast) 
+-Fixpoint execute (merge_var : ast) 
 -: M (bool) :=
--   let merge_var := (arg0) in
 -   match merge_var with
 +Definition expand_ast (i : ast) : ast :=
 +match i with
@@ -308,37 +298,37 @@
 +| i => i
 +end.
 +
-+Fixpoint execute (arg0 : ast) 
++Fixpoint execute (merge_var : ast) 
 +: M (bool) :=
-+   let merge_var := (arg0) in
 +let merge_var := expand_ast merge_var in
 +   match merge_var with
 +
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -15682,6 +15691,7 @@
+@@ -14821,6 +14830,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
     | C_ILLEGAL (s) => (execute_C_ILLEGAL s)  : M (bool)
 +| _ => Fail "Unexpanded instruction"
     end.
  
- Definition assembly_forwards (arg0 : ast) 
-@@ -36869,6 +36879,7 @@
+ Definition assembly_forwards (arg_ : ast) 
+@@ -35792,7 +35802,7 @@
     returnm (stepped
      : bool).
  
-+(*
- Definition loop '(tt : (unit)) 
+-Definition loop '(tt : unit) 
++(*Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -36909,7 +36920,7 @@
+    let i : Z := 0 in
+@@ -35832,7 +35842,7 @@
             : M (Z)) >>= fun i : Z =>
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
 -    : unit).
 +    : unit).*)
  
- Definition read_kind_of_num (arg0 : Z) `{ArithFact (0 <= arg0 /\ arg0 <= 11)} 
+ Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
  : read_kind :=