On 16/5/2011 10:12 πμ, hao deng wrote: > 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. > >
Well it depends what you mean by "breaking" (and that's why I used quotation marks both times). For example, soundness could only break if you misuse the new_axiom command (or any method that uses new_axiom). In your example you are only "breaking" the parser. You are choosing to not use "+" for anything other than your definition of `Plus`. This may, in some cases, be the desirable effect. That being said, I agree that side-effects have their pros and cons. Regards, Petros > > 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 >> -- 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
