:: A compiler of arithmetic expressions for { \bf SCM } :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received December 30, 1993 :: Copyright (c) 1993-2021 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, 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);