diff options
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 1 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 12 | ||||
| -rw-r--r-- | test/coq/skip | 12 |
3 files changed, 25 insertions, 0 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 7e4abe29..ebab269f 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -497,3 +497,4 @@ Definition set_slice_int len n lo (v : mword len) : Z := else n. Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt. +Definition print_bits {a} (s : string) (bs : mword a) : unit := tt. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 10339c20..ff3812ef 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -2693,10 +2693,22 @@ let doc_axiom_typschm typ_env l (tqs,typ) = | _ -> true) qs),l) | _ -> tqs in + let typ_count = ref 0 in + let fresh_var () = + let n = !typ_count in + let () = typ_count := n+1 in + string ("x" ^ string_of_int n) + in let doc_typ' typ = match Type_check.destruct_atom_nexp typ_env typ with | Some (Nexp_aux (Nexp_var kid,_)) when KidSet.mem kid args -> parens (doc_var empty_ctxt kid ^^ string " : Z") + (* This case is silly, but useful for tests *) + | Some (Nexp_aux (Nexp_constant n,_)) -> + let v = fresh_var () in + parens (v ^^ string " : Z") ^/^ + bquote ^^ braces (string "ArithFact " ^^ + parens (v ^^ string " = " ^^ string (Big_int.to_string n))) | _ -> match Type_check.destruct_atom_bool typ_env typ with | Some (NC_aux (NC_var kid,_)) when KidSet.mem kid args -> diff --git a/test/coq/skip b/test/coq/skip index f224e5fa..b1fa50be 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -31,3 +31,15 @@ exist1.sail exist2.sail XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere exist_synonym.sail +reg_32_64.sail +XXXXX Examples where int(...) should be expanded internally, but not yet supported +exit1.sail +exit2.sail +inline_typ.sail +XXXXX Examples with exponentials that the solver can't handle +pow_32_64.sail +XXXXX Register constructor doesn't use expanded type from type checker - need environment for type definition to fix this easily +reg_mod.sail +reg_ref.sail +XXXXX Dodgy division/modulo stuff +Replicate.sail |