diff options
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 20 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 38 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 56 |
3 files changed, 74 insertions, 40 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index b5bcfe5f..e37e9d26 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -9,12 +9,6 @@ Require Import ZArith. Require Import Omega. Require Import Eqdep_dec. -Module Z_eq_dec. -Definition U := Z. -Definition eq_dec := Z.eq_dec. -End Z_eq_dec. -Module ZEqdep := DecidableEqDep (Z_eq_dec). - Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q. refine ( match p, q with @@ -444,6 +438,20 @@ Definition sgteq_vec := sgteq_bv. *) +Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}. +refine (match n with +| Z0 => _ +| Zpos m => _ +| Zneg m => _ +end). +* simpl. apply Word.weq. +* simpl. apply Word.weq. +* simpl. destruct x. +Defined. + +Instance Decidable_eq_mword {n} : forall (x y : mword n), Decidable (x = y) := + Decidable_eq_from_dec eq_vec_dec. + Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n := match n with | S (S (S (S (S (S (S (S m))))))) => diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 83fe1dc7..48cfc222 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -8,10 +8,18 @@ Require Import bbv.Word. Require Export List. Require Export Sumbool. Require Export DecidableClass. +Require Import Eqdep_dec. Import ListNotations. Open Scope Z. +Module Z_eq_dec. +Definition U := Z. +Definition eq_dec := Z.eq_dec. +End Z_eq_dec. +Module ZEqdep := DecidableEqDep (Z_eq_dec). + + (* Constraint solving basics. A HintDb which unfolding hints and lemmata can be added to, and a typeclass to wrap constraint arguments in to trigger automatic solving. *) @@ -93,6 +101,22 @@ split. tauto. Qed. +Definition generic_dec {T:Type} (x y:T) `{Decidable (x = y)} : {x = y} + {x <> y}. +refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H' => _ else fun H' => _) Decidable_spec). +* left. tauto. +* right. intuition. +Defined. + +(* Used by generated code that builds Decidable equality instances for records. *) +Ltac cmp_record_field x y := + let H := fresh "H" in + case (generic_dec x y); + intro H; [ | + refine (Build_Decidable _ false _); + split; [congruence | intros Z; destruct H; injection Z; auto] + ]. + + (* Project away range constraints in comparisons *) Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r. @@ -1736,6 +1760,20 @@ Qed. Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v. +Definition vec_eq_dec {T n} (D : forall x y : T, {x = y} + {x <> y}) (x y : vec T n) : + {x = y} + {x <> y}. +refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _). +* apply eq_sigT_hprop; auto using ZEqdep.UIP. +* contradict n0. rewrite n0. reflexivity. +Defined. + +Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) : + forall x y : vec T n, Decidable (x = y) := { + Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y)) +}. +destruct (vec_eq_dec _ x y); simpl; split; congruence. +Defined. + Program Definition vec_of_list {A} n (l : list A) : option (vec A n) := if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None. Next Obligation. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 163cd183..5c4dfab4 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1690,41 +1690,29 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with space ^^ string "|})." in let updates_pp = separate hardline (List.map doc_update_field fs) in - (* let doc_field (ftyp, fid) = - let reftyp = - mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), - [mk_typ_arg (Typ_arg_typ rectyp); - mk_typ_arg (Typ_arg_typ ftyp)])) in - let rfannot = doc_tannot empty_ctxt env false reftyp in - let get, set = - string "rec_val" ^^ dot ^^ fname fid, - anglebars (space ^^ string "rec_val with " ^^ - (doc_op equals (fname fid) (string "v")) ^^ space) in - let base_ftyp = match annot with - | Some (env, _, _) -> Env.base_typ_of env ftyp - | _ -> ftyp in - let (start, is_inc) = - try - let start, (_, ord, _) = vector_start_index base_ftyp, vector_typ_args_of base_ftyp in - match nexp_simp start with - | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord) - | _ -> - raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ - ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) - with - | _ -> (Big_int.zero, true) in - doc_op equals - (concat [string "let "; parens (concat [doc_id id; underscore; doc_id fid; rfannot])]) - (anglebars (concat [space; - doc_op equals (string "field_name") (string_lit (doc_id fid)); semi_sp; - doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp; - doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; - doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; - doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in *) + let id_pp = doc_id_type id in + let numfields = List.length fs in + let intros_pp s = + string " intros [" ^^ + separate space (List.init numfields (fun n -> string (s ^ string_of_int n))) ^^ + string "]." ^^ hardline + in + let eq_pp = + string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^/^ + string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y)." ^^ + hardline ^^ intros_pp "x" ^^ intros_pp "y" ^^ + separate hardline (List.init numfields + (fun n -> + let ns = string_of_int n in + string ("cmp_record_field x" ^ ns ^ " y" ^ ns ^ "."))) ^^ + hardline ^^ + string "refine (Build_Decidable _ true _). subst. split; reflexivity." ^^ hardline ^^ + string "Defined." ^^ hardline + in doc_op coloneq - (separate space [string "Record"; doc_id_type id; doc_typquant_items empty_ctxt parens typq]) + (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt parens typq]) ((*doc_typquant typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ - dot ^^ hardline ^^ updates_pp + dot ^^ hardline ^^ eq_pp ^^ updates_pp | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1766,7 +1754,7 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with (concat [string "Inductive"; space; id_pp]) (enums_doc) in let eq1_pp = string "Scheme Equality for" ^^ space ^^ id_pp ^^ dot in - let eq2_pp = string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^^ space ^^ + let eq2_pp = string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^/^ string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :=" ^/^ string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec." in typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline) |