summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/coq/Sail2_values.v187
-rw-r--r--lib/vector_dec.sail6
-rw-r--r--mips/mips_extras.v2
-rw-r--r--src/pretty_print_coq.ml6
-rw-r--r--src/state.ml8
5 files changed, 197 insertions, 12 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index db0339d8..ee193865 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -124,9 +124,29 @@ Fixpoint repeat' {a} (xs : list a) n :=
| O => []
| S n => xs ++ repeat' xs n
end.
+Lemma repeat'_length {a} {xs : list a} {n : nat} : List.length (repeat' xs n) = (n * List.length xs)%nat.
+induction n.
+* reflexivity.
+* simpl.
+ rewrite app_length.
+ auto with arith.
+Qed.
Definition repeat {a} (xs : list a) (n : Z) :=
if n <=? 0 then []
else repeat' xs (Z.to_nat n).
+Lemma repeat_length {a} {xs : list a} {n : Z} (H : n >= 0) : length_list (repeat xs n) = n * length_list xs.
+unfold length_list, repeat.
+destruct n.
++ reflexivity.
++ simpl (List.length _).
+ rewrite repeat'_length.
+ rewrite Nat2Z.inj_mul.
+ rewrite positive_nat_Z.
+ reflexivity.
++ exfalso.
+ auto with zarith.
+Qed.
+
(*declare {isabelle} termination_argument repeat = automatic
Definition duplicate_to_list bit length := repeat [bit] length
@@ -187,6 +207,32 @@ lemma just_list_spec:
((forall xs. (just_list xs = None) <-> List.elem None xs) &&
(forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))*)
+Lemma just_list_length {A} : forall (l : list (option A)) (l' : list A),
+ Some l' = just_list l -> List.length l = List.length l'.
+induction l.
+* intros.
+ simpl in H.
+ inversion H.
+ reflexivity.
+* intros.
+ destruct a; simplify_eq H.
+ simpl in *.
+ destruct (just_list l); simplify_eq H.
+ intros.
+ subst.
+ simpl.
+ f_equal.
+ apply IHl.
+ reflexivity.
+Qed.
+
+Lemma just_list_length_Z {A} : forall (l : list (option A)) l', Some l' = just_list l -> length_list l = length_list l'.
+unfold length_list.
+intros.
+f_equal.
+auto using just_list_length.
+Qed.
+
(*** Bits *)
Inductive bitU := B0 | B1 | BU.
@@ -641,10 +687,10 @@ Definition update_list {A} (is_inc : bool) (xs : list A) n x :=
| [] => failwith "extract_only_element called for empty list"
| [e] => e
| _ => failwith "extract_only_element called for list with more elements"
-end
+end*)
(*** Machine words *)
-*)
+
Definition mword (n : Z) :=
match n with
| Zneg _ => False
@@ -1272,6 +1318,38 @@ Definition index_list from to step :=
index_list' from to step (S (Z.abs_nat (from - to)))
else [].
+Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Vars) : Vars :=
+ if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then
+ match n with
+ | O => vars
+ | S n => let vars := body from vars in foreach_Z' (from + step) to step n vars body
+ end
+ else vars.
+
+Definition foreach_Z {Vars} from to step vars body :=
+ foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body.
+
+Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars :=
+ if sumbool_of_bool (from + off <=? to) then
+ match n with
+ | O => vars
+ | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body
+ end
+ else vars.
+
+Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars :=
+ if sumbool_of_bool (to <=? from + off) then
+ match n with
+ | O => vars
+ | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body
+ end
+ else vars.
+
+Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} :=
+ foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} :=
+ foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
+
(*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars
Fixpoint while vars cond body :=
if cond vars then while (body vars) cond body else vars
@@ -1385,3 +1463,108 @@ Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <=
Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} :=
build_ex (Z.max a b).
+
+(*** Generic vectors *)
+
+Definition vec (T:Type) (n:Z) := { l : list T & length_list l = n }.
+Definition vec_length {T n} (v : vec T n) := n.
+Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+ access_list_dec (projT1 v) m.
+Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T :=
+ access_list_inc (projT1 v) m.
+
+Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >= 0)} : vec T n :=
+ existT _ (repeat [t] n) _.
+Next Obligation.
+rewrite repeat_length; auto using fact.
+unfold length_list.
+simpl.
+auto with zarith.
+Qed.
+
+Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat.
+revert l.
+induction n.
+* simpl. auto with arith.
+* intros l H.
+ destruct l.
+ + inversion H.
+ + simpl in H.
+ simpl.
+ rewrite IHn; auto with arith.
+Qed.
+Lemma update_list_inc_length {T} {l:list T} {m x} : 0 <= m < length_list l -> length_list (update_list_inc l m x) = length_list l.
+unfold update_list_inc, list_update, length_list.
+intro H.
+f_equal.
+assert ((0 <= Z.to_nat m < Datatypes.length l)%nat).
+{ destruct H as [H1 H2].
+ split.
+ + change 0%nat with (Z.to_nat 0).
+ apply Z2Nat.inj_le; auto with zarith.
+ + rewrite <- Nat2Z.id.
+ apply Z2Nat.inj_lt; auto with zarith.
+}
+rewrite app_length.
+rewrite firstn_length_le; only 2:omega.
+cbn -[skipn].
+rewrite skipn_length;
+omega.
+Qed.
+
+Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _.
+Next Obligation.
+unfold update_list_dec.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+ destruct v. simpl (projT1 _). rewrite e.
+ omega.
+Qed.
+
+Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _.
+Next Obligation.
+rewrite update_list_inc_length.
++ destruct v. apply e.
++ destruct H.
+ destruct v. simpl (projT1 _). rewrite e.
+ omega.
+Qed.
+
+Program Definition vec_map {S T} (f : S -> T) {n} (v : vec S n) : vec T n := existT _ (List.map f (projT1 v)) _.
+Next Obligation.
+destruct v as [l H].
+cbn.
+unfold length_list.
+rewrite map_length.
+apply H.
+Qed.
+
+Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) :=
+ match just_list (projT1 v) with
+ | None => None
+ | Some v' => Some (existT _ v' _)
+ end.
+Next Obligation.
+rewrite <- (just_list_length_Z _ _ Heq_anonymous).
+destruct v.
+assumption.
+Qed.
+
+Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
+
+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.
+symmetry.
+apply Z.eqb_eq.
+assumption.
+Qed.
+
+Definition vec_of_list_len {A} (l : list A) : vec A (length_list l) := existT _ l (eq_refl _).
+
+Definition map_bind {A B} (f : A -> option B) (a : option A) : option B :=
+match a with
+| Some a' => f a'
+| None => None
+end. \ No newline at end of file
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 86bbe601..8abcd218 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -22,7 +22,7 @@ val vector_length = {
ocaml: "length",
lem: "length_list",
c: "length",
- coq: "length_list"
+ coq: "vec_length"
} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
overload length = {bitvector_length, vector_length}
@@ -68,7 +68,7 @@ val bitvector_access = {
val plain_vector_access = {
ocaml: "access",
lem: "access_list_dec",
- coq: "access_list_dec",
+ coq: "vec_access_dec",
c: "vector_access"
} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
@@ -84,7 +84,7 @@ val bitvector_update = {
val plain_vector_update = {
ocaml: "update",
lem: "update_list_dec",
- coq: "update_list_dec",
+ coq: "vec_update_dec",
c: "vector_update"
} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 49899107..cc905f11 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -107,7 +107,7 @@ Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%st
Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
-Definition undefined_vector {rv a e} len (u : a) : monad rv (list a) e := returnm (repeat u len).
+Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len).
(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 38395b07..e68a6dd9 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -382,7 +382,7 @@ let doc_typ, doc_atomic_typ =
let tpp = match elem_typ with
| Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
string "mword " ^^ doc_nexp ctx (nexp_simp m)
- | _ -> string "list" ^^ space ^^ typ elem_typ in
+ | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx (nexp_simp m) in
if atyp_needed then parens tpp else tpp
| Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
let tpp = string "register_ref regstate register_value " ^^ typ etyp in
@@ -1122,7 +1122,9 @@ let doc_exp_lem, doc_let_lem =
if is_bit_typ etyp then
let bepp = string "vec_of_bits" ^^ space ^^ align epp in
(align (group (prefix 0 1 bepp (doc_tannot_lem ctxt (env_of full_exp) false t))), true)
- else (epp,aexp_needed) in
+ else
+ let vepp = string "vec_of_list_len" ^^ space ^^ align epp in
+ (vepp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
| E_vector_update(v,e1,e2) ->
raise (Reporting_basic.err_unreachable l
diff --git a/src/state.ml b/src/state.ml
index c591f753..e788ab6a 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -411,7 +411,7 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
let size = string_of_nexp (nexp_simp size) in
let is_inc = if is_order_inc ord then "true" else "false" in
let etyp_of, of_etyp = regval_convs_coq etyp in
- "(fun v => vector_of_regval " ^ etyp_of ^ " v)",
+ "(fun v => vector_of_regval " ^ size ^ " " ^ etyp_of ^ " v)",
"(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)"
| Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)])
when string_of_id id = "list" ->
@@ -430,12 +430,12 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with
let register_refs_coq registers =
let generic_convs =
separate_map hardline string [
- "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
- " | Regval_vector (_, _, v) => just_list (List.map of_regval v)";
+ "Definition vector_of_regval {a} n (of_regval : register_value -> option a) (rv : register_value) : option (vec a n) := match rv with";
+ " | Regval_vector (n', _, v) => if n =? n' then map_bind (vec_of_list n) (just_list (List.map of_regval v)) else None";
" | _ => None";
"end.";
"";
- "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs).";
+ "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : vec a size) : register_value := Regval_vector (size, is_inc, List.map regval_of (list_of_vec xs)).";
"";
"Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with";
" | Regval_list v => just_list (List.map of_regval v)";
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:01:43 +0000