If nat/nat.ma is not compiled yet, I do not know what happens.
try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
let absurd_URI () =
try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
let absurd_URI () =
try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
+
+let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
+
+let zero = Cic.MutConstruct (nat_URI,0,1,[])
+let succ = Cic.MutConstruct (nat_URI,0,2,[])
+
+let build_nat n =
+ if n < 0 then assert false;
+ let rec aux = function
+ | 0 -> zero
+ | n -> Cic.Appl [ succ; (aux (n - 1)) ]
+ in
+ aux n
val true_URI : unit -> UriManager.uri option
val absurd_URI : unit -> UriManager.uri option
val true_URI : unit -> UriManager.uri option
val absurd_URI : unit -> UriManager.uri option
+val build_nat : int -> Cic.term
let _ =
DisambiguateChoices.add_num_choice
("natural number",
let _ =
DisambiguateChoices.add_num_choice
("natural number",
+ (fun _ num _ -> LibraryObjects.build_nat (int_of_string num)));
+ DisambiguateChoices.add_num_choice
+ ("Coq natural number",
(fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("real number",
(fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("real number",
include "nat/compare.ma".
include "list/list.ma".
include "nat/compare.ma".
include "list/list.ma".
-alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+(*alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias id "SS" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
let rec matita_nat_of_coq_nat n ≝
alias id "SS" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
let rec matita_nat_of_coq_nat n ≝
].
coercion cic:/matita/assembly/matita_nat_of_coq_nat.con.
alias num (instance 0) = "natural number".
].
coercion cic:/matita/assembly/matita_nat_of_coq_nat.con.
alias num (instance 0) = "natural number".
definition byte ≝ nat.
definition addr ≝ nat.
definition byte ≝ nat.
definition addr ≝ nat.
| LDAd: opcode (* 3, 182 *)
| STAd: opcode. (* 3, 183 *)
| LDAd: opcode (* 3, 182 *)
| STAd: opcode. (* 3, 183 *)
-let rec cycles_of_opcode op ≝
+alias num (instance 0) = "natural number".
+let rec cycles_of_opcode op : nat ≝
- [ ADDd ⇒ matita_nat_of_coq_nat 3
- | BEQ ⇒ matita_nat_of_coq_nat 3
- | BRA ⇒ matita_nat_of_coq_nat 3
- | DECd ⇒ matita_nat_of_coq_nat 5
- | LDAi ⇒ matita_nat_of_coq_nat 2
- | LDAd ⇒ matita_nat_of_coq_nat 3
- | STAd ⇒ matita_nat_of_coq_nat 3
+ [ ADDd ⇒ 3
+ | BEQ ⇒ 3
+ | BRA ⇒ 3
+ | DECd ⇒ 5
+ | LDAi ⇒ 2
+ | LDAd ⇒ 3
+ | STAd ⇒ 3
].
inductive cartesian_product (A,B: Type) : Type ≝
].
inductive cartesian_product (A,B: Type) : Type ≝
| cons c tl ⇒
match c with
[ couple op n ⇒
| cons c tl ⇒
match c with
[ couple op n ⇒
- match eqb (matita_nat_of_coq_nat n) b with
[ true ⇒ op
| false ⇒ aux tl
]]]
[ true ⇒ op
| false ⇒ aux tl
]]]
λop.
let rec aux l ≝
match l with
λop.
let rec aux l ≝
match l with
- [ nil ⇒ matita_nat_of_coq_nat 0
| cons c tl ⇒
match c with
[ couple op' n ⇒
match opcodeeqb op op' with
| cons c tl ⇒
match c with
[ couple op' n ⇒
match opcodeeqb op op' with
- [ true ⇒ matita_nat_of_coq_nat n
interpretation "byte_of_opcode" 'byte_of_opcode a =
(cic:/matita/assembly/byte_of_opcode.con a).
interpretation "byte_of_opcode" 'byte_of_opcode a =
(cic:/matita/assembly/byte_of_opcode.con a).
-definition byte_of_coq_nat : nat → byte ≝ matita_nat_of_coq_nat.
-
-notation "hvbox(@ break a)"
- non associative with precedence 80
-for @{ 'matita_nat_of_coq_nat $a }.
-interpretation "matita_nat_of_coq_nat" 'matita_nat_of_coq_nat a =
- (cic:/matita/assembly/byte_of_coq_nat.con a).
-
definition mult_source : list byte ≝
definition mult_source : list byte ≝
- [#LDAi; @0;
- #STAd; @18; (* 18 = locazione $12 *)
- #LDAd; @17; (* 17 = locazione $11 *)
- #BEQ; @14;
- #LDAd; @18;
- #DECd; @17;
- #ADDd; @16; (* 16 = locazione $10 *)
- #STAd; @18;
- #LDAd; @17;
- #BRA; @246; (* 246 = -10 *)
- #LDAd; @18].
+ [#LDAi; 0;
+ #STAd; 32; (* 18 = locazione $12 *)
+ #LDAd; 31; (* 17 = locazione $11 *)
+ #BEQ; 12;
+ #LDAd; 18;
+ #DECd; 31;
+ #ADDd; 30; (* 16 = locazione $10 *)
+ #STAd; 32;
+ #LDAd; 31;
+ #BRA; 246; (* 242 = -14 *)
+ #LDAd; 32].
definition mult_source' : list byte.
definition mult_source' : list byte.
}.
definition mult_status : status ≝
}.
definition mult_status : status ≝
- mk_status @0 @0 @0 false false (λa:addr. nth ? mult_source @0 a) 0.
+ mk_status 0 0 0 false false (λa:addr. nth ? mult_source 0 a) 0.
+
+definition update ≝
+ λf: addr → byte.λa.λv.λx.
+ match eqb x a with
+ [ true ⇒ v
+ | false ⇒ f x ].
-alias id "update" = "cic:/Marseille/GC/card/card/update.con".
definition tick ≝
λs:status.
(* fetch *)
definition tick ≝
λs:status.
(* fetch *)
let mem' ≝ update (mem s) op1 x in
mk_status (acc s) (2 + pc s) (spc s)
(eqb O x) (cf s) mem' 0 (* check zb!!! *)
let mem' ≝ update (mem s) op1 x in
mk_status (acc s) (2 + pc s) (spc s)
(eqb O x) (cf s) mem' 0 (* check zb!!! *)
- | LDAi ⇒ s
- | LDAd ⇒ s
- | STAd ⇒ s
+ | LDAi ⇒
+ mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
+ | LDAd ⇒
+ let x ≝ pred (mem s op1) in
+ mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
+ | STAd ⇒
+ mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
+ (update (mem s) op1 (acc s)) 0
lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
intros; reflexivity.
qed.
lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
intros; reflexivity.
qed.
+(*
+lemma goo: pc (execute mult_status 4) = O.
+ reduce;
+ CSC.
+
-lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status.
+ whd in ⊢ (? ? (? (? (? %))) ?);
+ do 2 (simplify in match (matita_nat_of_coq_nat ?));
+ simplify in match (matita_nat_of_coq_nat ?);
+ whd in ⊢ (? ? (? (? (? (? ? ? ? ? ? ? %)))) ?);
+ whd in ⊢ (? ? (? (? (? %))) ?);
+
+
+
+
+
+
+
+
+
+
+
+
change with (tick (tick (tick mult_status)) = mult_status);
change with (tick (tick mult_status) = mult_status);
change with (tick mult_status = mult_status);
change with (tick (tick (tick mult_status)) = mult_status);
change with (tick (tick mult_status) = mult_status);
change with (tick mult_status = mult_status);
|STAd\rArr ?] ?);
simplify;
reflexivity.
|STAd\rArr ?] ?);
simplify;
reflexivity.
*)
\ No newline at end of file
*)
\ No newline at end of file