Thanks Petros ! I didn't notice the difference between override_interface and overload_interface when copy from the tutorial !!!
side effects !!! does that means the hol -light system can be so easily break . anyway , side effect is a double edge sword. 2011/5/16 Petros Papapanagiotou <[email protected]>: > > On 16/5/2011 1:16 πμ, hao deng wrote: >> let str_IND, str_RECUR = define_type "str = Str (int list)";; >> >> let expr_IND, expr_RECUR = define_type >> " expr = Lit num >> |Var str >> |Plus expr expr >> |Times expr expr ";; >> >> let cmd_IND, cmd_REC = define_type >> "cmd = Assign str expr >> | Seq cmd cmd >> | If expr cmd cmd >> | While expr cmd";; >> >> parse_as_infix(";;", (18, "right"));; >> parse_as_infix(":=", (20, "right"));; >> override_interface(";;", `Seq`);; >> override_interface(":= ", `Assign`);; >> override_interface("+", `Plus`);; >> override_interface("*", `Times`);; >> > > The problem is "+" and "*" are overloadable identifiers. This means they > can be (and are) used to represent different things depending on the > involved types (most notably addition and multiplication of natural > numbers). > > Using override_interface on an overloadable identifier, removes all > overloadings, essentially creating a mess of a number of definitions > that include "+" and "*". This is why you get the "unstable state" of > the system after you load your code. > > In simpler words, you essentially "break" all +'s and *'s in HOL Light > except yours. > > If you want to use them to represent your defined `Plus` and `Times` you > will have to use overload_interface instead of override_interface. This > will have the effect that you are looking for. > > Hope this helps. > > Regards, > > Petros > > >> let value = define >> `(value (Lit n ) s = n ) >> /\ (value (Var x) s = s(x) ) >> /\ (value (e + f) s = value e s + value f s ) >> /\ (value (e * f) s = value e s * value f s ) `;; > > -- > Petros Papapanagiotou > CISA, School of Informatics > The University of Edinburgh > > Email: [email protected] > > --- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > > > ------------------------------------------------------------------------------ > Achieve unprecedented app performance and reliability > What every C/C++ and Fortran developer should know. > Learn how Intel has extended the reach of its next-generation tools > to help boost performance applications - inlcuding clusters. > http://p.sf.net/sfu/intel-dev2devmay > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > ------------------------------------------------------------------------------ Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
