From d7bcd7edff17b405b07ea17a38101c699e27bf8d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 10 Jul 2007 17:11:56 +0000
Subject: [PATCH] La programmazione funzionale e' come TeX, funziona meglio se
 la prendi a calci.

---
 .../matita/library/assembly/assembly.ma       | 123 +++++++++---------
 1 file changed, 60 insertions(+), 63 deletions(-)

diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma
index 875e6da8d..efc69077c 100644
--- a/helm/software/matita/library/assembly/assembly.ma
+++ b/helm/software/matita/library/assembly/assembly.ma
@@ -653,66 +653,77 @@ definition update ≝
    [ true ⇒ v
    | false ⇒ f x ].
 
+definition continuation :=
+ byte -> addr -> addr -> bool -> bool -> (addr -> byte) -> nat -> status.
+
 definition tick ≝
- λs:status.
+ \lambda continuation: continuation.
+ \lambda acc:byte.
+ \lambda pc:addr.
+ \lambda spc:addr.
+ \lambda zf:bool.
+ \lambda cf:bool.
+ \lambda mem:addr -> byte.
+ \lambda clk:nat.
   (* fetch *)
-  let opc ≝ opcode_of_byte (mem s (pc s)) in
-  let op1 ≝ mem s (S (pc s)) in
+  let opc ≝ opcode_of_byte (mem (pc)) in
+  let op1 ≝ mem (S (pc)) in
   let clk' ≝ cycles_of_opcode opc in
-  match eqb (S (clk s)) clk' with
+  match eqb (S (clk)) clk' with
    [ true ⇒
       match opc with
        [ ADDd ⇒
-          let x ≝ nat_of_byte (mem s op1) in
-          let acc' ≝ x + acc s in (* signed!!! *)
-           mk_status (byte_of_nat acc') (2 + pc s) (spc s)
-            (eqb O acc') (cf s) (mem s) 0
+          let x ≝ nat_of_byte (mem op1) in
+          let acc' ≝ x + acc in (* signed!!! *)
+           continuation (byte_of_nat acc') (2 + pc) (spc)
+            (eqb O acc') (cf) (mem) 0
        | BEQ ⇒
-          mk_status
-           (acc s)
-           (match zf s with
-             [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
-             | false ⇒ 2 + pc s
+          continuation
+           (acc)
+           (match zf with
+             [ true ⇒ 2 + op1 + pc   (* signed!!! *)
+             | false ⇒ 2 + pc
              ])
-           (spc s)
-           (zf s)
-           (cf s)
-           (mem s)
+           (spc)
+           (zf)
+           (cf)
+           (mem)
            0
        | BRA ⇒
-          mk_status
-           (acc s) (2 + op1 + pc s) (* signed!!! *)
-           (spc s)
-           (zf s)
-           (cf s)
-           (mem s)
+          continuation
+           (acc) (2 + op1 + pc) (* signed!!! *)
+           (spc)
+           (zf)
+           (cf)
+           (mem)
            0
        | DECd ⇒
-          let x ≝ bpred (mem s op1) in (* signed!!! *)
-          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 x ≝ bpred (mem op1) in (* signed!!! *)
+          let mem' ≝ update (mem) op1 x in
+           continuation (acc) (2 + pc) (spc)
+            (eqb O x) (cf) mem' 0 (* check zb!!! *)
        | LDAi ⇒
-          mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
+          continuation op1 (2 + pc) (spc) (eqb O op1) (cf) (mem) 0
        | LDAd ⇒
-          let x ≝ mem s op1 in
-           mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
+          let x ≝ mem op1 in
+           continuation x (2 + pc) (spc) (eqb O x) (cf) (mem) 0
        | STAd ⇒
-          mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
-           (update (mem s) op1 (acc s)) 0
+          continuation (acc) (2 + pc) (spc) (zf) (cf)
+           (update (mem) op1 (acc)) 0
        ]
    | false ⇒
-       mk_status
-        (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
+       continuation
+        (acc) (pc) (spc) (zf) (cf) (mem) (S (clk))
    ].
 
-let rec execute s n on n ≝
+let rec execute n on n ≝
  match n with
-  [ O ⇒ s
-  | S n' ⇒ execute (tick s) n'
+  [ O ⇒ mk_status
+  | S n' ⇒ tick (execute n')
   ].
   
-lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
+lemma foo: ∀acc,pc,zf,cf,mem,clk,n. 
+  execute (S n) acc pc zf cf mem clk = tick (execute n) acc pc zf cf mem clk.
  intros; reflexivity.
 qed.
 
@@ -735,9 +746,9 @@ definition mult_source : list byte ≝
    #BRA;  mk_byte xF x2; (* 242 = -14 *)
    #LDAd; mk_byte x2 x0].
 
-definition mult_status ≝
+definition mult_mem ≝
  λx,y.
-  mk_status (mk_byte x0 x0) 0 0 false false
+  (* mk_status (mk_byte x0 x0) 0 0 false false *)
    (λa:addr.
      match leb a 29 with
       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
@@ -746,32 +757,18 @@ definition mult_status ≝
           [ true ⇒ x
           | false ⇒ y
           ]
-      ]) 0.
+      ]) (* 0 *).
       
-(*      
 lemma foobar:
- ∀x.
-  (λi.
-    let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
-     (* pc s = 22 ∧*) mem s 32 = byte_of_nat 0) 14.
- intros;
- letin foo ≝ (execute (mult_status x (mk_byte x0 x0)) 8);
- whd in foo;
-reduce in foo:(? ? ? ? ? ? ? ?);
- whd in foo;
-
-  xxx.
- change with 
-   (let s ≝ execute (mult_status x (mk_byte x0 x0)) 14 in
-    (* pc s = 22 ∧*)  eq ? (mem s 32) (byte_of_nat 0)).
-    xxxxxxxxx
- whd in ⊢ ((\lambda i:?.(let s \def ? in ? ? % %)) ?).
- 
- reduce;
- (* split; *)
- reflexivity;
+ ∀x. 
+   let s ≝ 
+     execute 14 (mk_byte x0 x0) 0 0 false false (mult_mem x (mk_byte x0 x0)) 0 
+   in
+    pc s = 22 ∧ mem s 32 = byte_of_nat 0.
+ intros; split; reflexivity;
 qed.
 
+(*
 lemma goo1:
  ∀x.
   let i ≝ 14 in
@@ -858,4 +855,4 @@ lemma goo: True.
  
  exact I.
 qed.
-*)
\ No newline at end of file
+*)
-- 
2.39.5