*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] I need a fixed mutable array*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Wed, 18 Jun 2014 14:06:17 -0500*In-reply-to*: <53A0C73F.7080407@gmx.com>*References*: <53A0652B.7000509@gmx.com> <42AC1402-3D1F-48C6-98F0-47D3176D34D9@nicta.com.au> <53A0C73F.7080407@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 14-06-17 17:54, Gottfried Barrow wrote:

My idea now is to take a very minimal model of an Intel cpu andimplement pseudo-assembly language around that model, for the smallestnumber of instructions possible.

A little feedback can go a long way towards getting me to the next step.

Even further: "How do I use GOTO in a functional programming language?" That led, with some past information, to this thought (possibly wrong):

So, no mutability can lead to good things.

Regards, GB (*****************************************) theory i140618a__mem_write_execute_state_list imports Complex_Main "~~/src/HOL/Library/Code_Target_Nat" begin (*16-bit dataword and a little notation.*)

type_synonym b16T = "b8T * b8T" notation (input) False ("0\<^sub>B") notation (input) True ("1\<^sub>B") abbreviation hex00 :: b8T ("00\<cdot>") where

abbreviation hex55 :: b8T ("55\<cdot>") where

abbreviation hexAA :: b8T ("AA\<cdot>") where

abbreviation hex16 :: "b8T => b8T => b16T" where "hex16 b1 b0 == (b1, b0)" notation hex16 ("x\<bar>__" [1000, 1000] 1000)

type_synonym idxed_flist = "(nat * b16T) list * nat"

"idx0s_app_flist nlist 0 = nlist"

definition create_idxed_flist :: "nat \<Rightarrow> idxed_flist" where "create_idxed_flist lsize = (idx0s_app_flist [] lsize, lsize)" value "create_idxed_flist 0x10" value "length (fst (create_idxed_flist 0x10)) = 0x10" (*The write function.*)

where "write_idxed_flist (flist, lsize) idx data = ( if (idx >= lsize \<or> length flist \<noteq> lsize) then None else Some (flist[idx := (idx, data)], lsize) )" (*Two sequential writes done manually.*) value "write_idxed_flist

3 x\<bar>AA\<cdot>AA\<cdot>" (*Automate execution of a list of writes, to generate a list of states.*)

\<Rightarrow> (idxed_flist option) list" where "execute_list [] _ = []" |"execute_list state_list [] = state_list" |"execute_list [s] ((idx,data) # xs) = execute_list ((write_idxed_flist (the s) idx data) # [s]) xs" |"execute_list (s # ss) ((idx,data) # xs) = execute_list ((write_idxed_flist (the s) idx data) # (s # ss)) xs"

needs more conditions to speed it up more.*)

abbreviation "three_write_list ==

value "execute_list [Some (create_idxed_flist 0xF)] three_write_list"

lemma "idx < lsize \<and> length flist = lsize

by(simp) (******************************************************************************) end

theory i140618a__mem_write_execute_state_list imports Complex_Main "~~/src/HOL/Library/Code_Target_Nat" begin (*16-bit dataword and a little notation.*) type_synonym b8T = "bool * bool * bool * bool * bool * bool * bool * bool" type_synonym b16T = "b8T * b8T" notation (input) False ("0\<^sub>B") notation (input) True ("1\<^sub>B") abbreviation hex00 :: b8T ("00\<cdot>") where "hex00 == (0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B)" abbreviation hex55 :: b8T ("55\<cdot>") where "hex55 == (0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B)" abbreviation hexAA :: b8T ("AA\<cdot>") where "hexAA == (1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B)" abbreviation hex16 :: "b8T => b8T => b16T" where "hex16 b1 b0 == (b1, b0)" notation hex16 ("x\<bar>__" [1000, 1000] 1000) (*Indexed, fixed size b16T list. The list idx won't always match the pair idx.*) type_synonym idxed_flist = "(nat * b16T) list * nat" primrec idx0s_app_flist :: "(nat * b16T) list \<Rightarrow> nat \<Rightarrow> (nat * b16T) list" where "idx0s_app_flist nlist 0 = nlist" |"idx0s_app_flist nlist (Suc n) = idx0s_app_flist ((n,x\<bar>00\<cdot>00\<cdot>) # nlist) n" definition create_idxed_flist :: "nat \<Rightarrow> idxed_flist" where "create_idxed_flist lsize = (idx0s_app_flist [] lsize, lsize)" value "create_idxed_flist 0x10" value "length (fst (create_idxed_flist 0x10)) = 0x10" (*The write function.*) primrec write_idxed_flist :: "idxed_flist \<Rightarrow> nat \<Rightarrow> b16T \<Rightarrow> idxed_flist option" where "write_idxed_flist (flist, lsize) idx data = ( if (idx >= lsize \<or> length flist \<noteq> lsize) then None else Some (flist[idx := (idx, data)], lsize) )" (*Two sequential writes done manually.*) value "write_idxed_flist (the(write_idxed_flist (create_idxed_flist 0x10) 5 x\<bar>55\<cdot>55\<cdot>)) 3 x\<bar>AA\<cdot>AA\<cdot>" (*Automate execution of a list of writes, to generate a list of states.*) fun execute_list :: "(idxed_flist option) list \<Rightarrow> (nat * b16T) list \<Rightarrow> (idxed_flist option) list" where "execute_list [] _ = []" |"execute_list state_list [] = state_list" |"execute_list [s] ((idx,data) # xs) = execute_list ((write_idxed_flist (the s) idx data) # [s]) xs" |"execute_list (s # ss) ((idx,data) # xs) = execute_list ((write_idxed_flist (the s) idx data) # (s # ss)) xs" (*Adding the third condition sped up the termination proof a lot. It probably needs more conditions to speed it up more.*) (*Execute a list of three instructions. The states are shown last to first.*) abbreviation "three_write_list == [(5, x\<bar>55\<cdot>55\<cdot>), (3, x\<bar>AA\<cdot>AA\<cdot>), (0x10, x\<bar>55\<cdot>55\<cdot>)]" value "execute_list [Some (create_idxed_flist 0xF)] three_write_list" (*Prove something trivial. The value of proving this wasn't trivial. It showed me I needed the condition "length flist \<noteq> lsize" in my function above.*) lemma "idx < lsize \<and> length flist = lsize \<Longrightarrow> write_idxed_flist (flist, lsize) idx dw \<noteq> None" by(simp) (******************************************************************************) end

**References**:**[isabelle] I need a fixed mutable array***From:*Gottfried Barrow

**Re: [isabelle] I need a fixed mutable array***From:*Gerwin Klein

**Re: [isabelle] I need a fixed mutable array***From:*Gottfried Barrow

- Previous by Date: [isabelle] Code_Abstract_Nat raises exception for a variable with name g
- Next by Date: Re: [isabelle] I need a fixed mutable array
- Previous by Thread: Re: [isabelle] I need a fixed mutable array
- Next by Thread: Re: [isabelle] I need a fixed mutable array
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list