diff options
| -rw-r--r-- | riscv/coq.patch | 66 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 29 |
2 files changed, 42 insertions, 53 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 := diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 99d63b55..f1726ce4 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1768,33 +1768,28 @@ let args_of_typ l env typs = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) -let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) = +let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) = let env = env_of_annot annot in - let tup_typs = match typ with - | Typ_aux (Typ_tup typs, _) -> Some typs - | _ -> match Env.expand_synonyms env typ with - | Typ_aux (Typ_tup typs, _) -> Some typs - | _ -> None - in let identity = (fun body -> body) in - match paux, tup_typs with + match paux, typs with | P_tup [], _ -> let annot = (l, mk_tannot Env.empty unit_typ no_effect) in [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity - | P_tup pats, Some typs -> List.combine pats typs, identity - | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l __POS__ "Tuple pattern against non-tuple type") - | P_wild, Some typs -> + | P_tup pats, _ -> List.combine pats typs, identity + | P_wild, _ -> let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in List.map wild typs, identity - | P_typ (_, pat), _ -> untuple_args_pat typ pat - | P_as _, Some typs | P_id _, Some typs -> + | P_typ (_, pat), _ -> untuple_args_pat typs pat + | P_as _, _::_::_ | P_id _, _::_::_ -> let argpats, argexps = args_of_typ l env typs in let argexp = E_aux (E_tuple argexps, annot) in let bindargs (E_aux (_, bannot) as body) = E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in argpats, bindargs - | _, _ -> + | _, [typ] -> [pat,typ], identity + | _, _ -> + unreachable l __POS__ "Unexpected pattern/type combination" let doc_rec (Rec_aux(r,_)) = match r with | Rec_nonrec -> string "Definition" @@ -1930,7 +1925,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let ids_to_avoid = all_ids pexp in let bound_kids = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in - let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *) + let pats, bind = untuple_args_pat arg_typs pat in (* FIXME is this needed any more? *) let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in @@ -1957,6 +1952,10 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let doc_binder (P_aux (p,ann) as pat, typ) = let env = env_of_annot ann in let exp_typ = Env.expand_synonyms env typ in + let () = + debug ctxt (lazy (" pattern " ^ string_of_pat pat)); + debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) + in match p with | P_id id | P_typ (_,P_aux (P_id id,_)) |