:: A compiler of arithmetic expressions for { \bf SCM }
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, AFINSQ_1, AMI_1, AMI_3, FINSEQ_1, SUBSET_1, ORDINAL4,
ARYTM_3, FUNCT_1, ARYTM_1, XXREAL_0, RELAT_1, FSM_1, BINTREE1, DTCONSTR,
STRUCT_0, XBOOLE_0, LANG1, AMI_2, ZFMISC_1, TDGROUP, TARSKI, CARD_1,
TREES_4, TREES_3, QC_LANG1, CAT_1, INT_1, TREES_2, MCART_1, GRAPHSP,
CONNSP_3, FUNCT_2, MSUALG_1, SCM_COMP, EXTPRO_1, VALUED_1, COMPOS_1,
NAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, NAT_1, XTUPLE_0, MCART_1, FUNCT_1, FUNCT_2,
VALUED_1, TREES_2, TREES_3, TREES_4, AFINSQ_1, STRUCT_0, MEMSTR_0,
COMPOS_1, EXTPRO_1, AMI_2, AMI_3, FINSEQ_1, LANG1, BINTREE1, DTCONSTR,
PARTFUN1, PRE_POLY;
constructors DTCONSTR, BINTREE1, DOMAIN_1, PRE_POLY, RELSET_1, AMI_3,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1,
FUNCT_2, NUMBERS, XREAL_0, INT_1, TREES_3, STRUCT_0, DTCONSTR, BINTREE1,
AMI_3, AFINSQ_1, FINSEQ_1, COMPOS_0, MEMSTR_0, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
definition
func SCM-AE -> binary with_terminals with_nonterminals
with_useful_nonterminals strict non empty DTConstrStr means
:: SCM_COMP:def 1
Terminals
it = SCM-Data-Loc & NonTerminals it = [:1, 5:] & for x, y, z being Symbol of it
holds x ==> <*y, z*> iff x in [:1, 5:];
end;
definition
mode bin-term is Element of TS SCM-AE;
end;
definition
let nt be NonTerminal of SCM-AE;
let tl, tr be bin-term;
redefine func nt-tree (tl, tr) -> bin-term;
end;
definition
let t be Terminal of SCM-AE;
redefine func root-tree t -> bin-term;
end;
definition
let t be Terminal of SCM-AE;
func @t -> Data-Location equals
:: SCM_COMP:def 2
t;
end;
theorem :: SCM_COMP:1
for nt being NonTerminal of SCM-AE
holds nt = [0,0] or ... or nt = [0,4];
theorem :: SCM_COMP:2
[0,0] is NonTerminal of SCM-AE &
... & [0,4] is
NonTerminal of SCM-AE;
definition
let t1, t2 be bin-term;
func t1+t2 -> bin-term equals
:: SCM_COMP:def 3
[0,0]-tree(t1, t2);
func t1-t2 -> bin-term equals
:: SCM_COMP:def 4
[0,1]-tree(t1, t2);
func t1*t2 -> bin-term equals
:: SCM_COMP:def 5
[0,2]-tree(t1, t2);
func t1 div t2 -> bin-term equals
:: SCM_COMP:def 6
[0,3]-tree(t1, t2);
func t1 mod t2 -> bin-term equals
:: SCM_COMP:def 7
[0,4]-tree(t1, t2);
end;
theorem :: SCM_COMP:3 :: PRE_COMP_5:
for term being bin-term holds (ex t being Terminal of SCM-AE st term =
root-tree t) or ex tl, tr being bin-term st term = tl+tr or term = tl-tr or
term = tl*tr or term = tl div tr or term = tl mod tr;
definition
let o be NonTerminal of SCM-AE, i, j be Integer;
func o-Meaning_on (i, j) -> Integer equals
:: SCM_COMP:def 8
i+j if o = [0,0], i-j if o
= [0,1], i*j if o = [0,2], i div j if o = [0,3], i mod j if o = [0,4];
end;
registration
let s be State of SCM;
let t be Terminal of SCM-AE;
cluster s.t -> integer;
end;
definition
let D be non empty set;
let f be Function of INT, D;
let x be Integer;
redefine func f.x -> Element of D;
end;
definition
let s be State of SCM;
let term be bin-term;
func term @ s -> Integer means
:: SCM_COMP:def 9
ex f being Function of TS SCM-AE, INT
st it = f.term &
(for t being Terminal of SCM-AE holds f.(root-tree t) = s.t) &
for nt being NonTerminal of SCM-AE, tl, tr being bin-term, rtl,
rtr being Symbol of SCM-AE st
rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *>
for xl, xr being Element of INT st xl = f.tl & xr = f.tr holds
f.(nt-tree (tl, tr)) = nt-Meaning_on (xl, xr);
end;
theorem :: SCM_COMP:4
for s being State of SCM, t being Terminal of SCM-AE holds
(root-tree t)@s = s.t;
theorem :: SCM_COMP:5
for s being State of SCM, nt being NonTerminal of SCM-AE, tl, tr
being bin-term holds (nt-tree(tl, tr))@s = nt-Meaning_on(tl@s, tr@s);
theorem :: SCM_COMP:6 :: PRE_COMP_8:
for s being State of SCM, tl, tr being bin-term holds
(tl+tr)@s = (tl@s)+(tr@s) & (tl-tr)@s = (tl@s)-(tr@s) &
(tl*tr)@s = (tl@s)*(tr@s) & (tl div tr)@s = (tl@s) div (tr@s) &
(tl mod tr)@s = (tl@s) mod (tr@s);
definition
let nt be NonTerminal of SCM-AE, n be Nat;
func Selfwork(nt, n) -> XFinSequence of the InstructionsF of SCM equals
:: SCM_COMP:def 10
<%AddTo(dl.n, dl.(n+1))%> if nt = [0,0],
<%SubFrom(dl.n, dl.(n+1))%> if nt = [0,1],
<%MultBy(dl.n, dl.(n+1))%> if nt = [0,2],
<%Divide(dl.n,dl.(n+1))%> if nt = [0,3],
<%Divide(dl.n, dl.(n+1)), dl.n:=dl.(n+1)%> if nt = [0,4];
end;
definition
func SCM-Compile ->
Function of TS SCM-AE, Funcs(NAT, (the InstructionsF of SCM)^omega)
means
:: SCM_COMP:def 11
(for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = it.(root-tree t) & for n being Nat
holds g.n = <%dl.n:=@t%>) & for nt being NonTerminal of SCM-AE,
t1, t2 being bin-term, rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 &
rtr = root-label t2 & nt ==> <*rtl, rtr*>
ex g, f1, f2 being sequence of (the InstructionsF of SCM)^omega
st g = it.(nt-tree (t1, t2)) & f1 = it.t1 &
f2 = it.t2 & for n being Nat
holds g.n = (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n);
end;
definition
let term be bin-term, aux be Nat;
func SCM-Compile(term, aux) ->
XFinSequence of the InstructionsF of SCM equals
:: SCM_COMP:def 12
(SCM-Compile.term).aux;
end;
theorem :: SCM_COMP:7
for t being Terminal of SCM-AE, n being Element of NAT holds
SCM-Compile(root-tree t, n) = <% dl.n:=@t %>;
theorem :: SCM_COMP:8
for nt being NonTerminal of SCM-AE, t1, t2 being bin-term, n
being Element of NAT, rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 &
rtr = root-label t2 & nt ==> <*rtl, rtr*> holds SCM-Compile(nt-tree(t1,t2), n)
= SCM-Compile(t1, n)^SCM-Compile(t2, n+1)^Selfwork(nt, n);
definition
let t be Terminal of SCM-AE;
func d".t -> Element of NAT means
:: SCM_COMP:def 13
dl.it = t;
end;
definition
let term be bin-term;
func max_Data-Loc_in term -> Element of NAT means
:: SCM_COMP:def 14
ex f being
Function of TS SCM-AE, NAT st it = f.term & (for t being Terminal of SCM-AE
holds f.(root-tree t) = d".t) & for nt being NonTerminal of SCM-AE, tl, tr
being bin-term, rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr =
root-label tr & nt ==> <* rtl, rtr *> for xl, xr being Element of NAT st xl = f
.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = max(xl, xr);
end;
theorem :: SCM_COMP:9
for t being Terminal of SCM-AE holds max_Data-Loc_in root-tree t = d".t;
theorem :: SCM_COMP:10
for nt being NonTerminal of SCM-AE, tl, tr being bin-term holds
max_Data-Loc_in(nt-tree(tl, tr)) = max(max_Data-Loc_in tl, max_Data-Loc_in tr);
theorem :: SCM_COMP:11
for term being bin-term, s1, s2 being State of SCM st for dn
being Element of NAT st dn <= max_Data-Loc_in term holds s1.dl.dn = s2.dl.dn
holds term @ s1 = term @ s2;
reserve F for Instruction-Sequence of SCM;
theorem :: SCM_COMP:12
for F for term being bin-term for aux, n being Element of NAT
st Shift(SCM-Compile(term, aux),n) c= F
for s being n-started State of SCM
st aux > max_Data-Loc_in term
ex i being Element of NAT, u being State of SCM st u =
Comput(F,s,i+1) & i+1 = len SCM-Compile(term, aux) & IC Comput(
F,s,i) =
(n+i) & IC u = (n+(i+1)) & u.dl.aux = term@s & for dn being Element of
NAT st dn < aux holds s.dl.dn = u.dl.dn;
theorem :: SCM_COMP:13
for F for term being bin-term, aux, n being Element of NAT
st Shift(SCM-Compile(term, aux)^<%halt SCM%>,n) c= F
for s being n-started State of SCM
st aux
> max_Data-Loc_in term holds F halts_on s &
(Result(F,s)).dl.aux = term@s &
LifeSpan(F,s) = len SCM-Compile(term, aux);