Hi Mark, thanks, then I conclude that nothing prevents me from using them in my own code base!
V. Le 16/08/2012 23:21, "Mark" a écrit : > Hi Vincent, > > That's a good question. I think it's mainly down to history. HOL Light was > originally implemented in Caml Light, and was ported to OCaml when it was > already quite a substantial system. Caml Light didn't have a module system, > and modules were not added in the port (except for the inference kernel). > > There are another few things about HOL Light that are explained by this: > - Caml Light used '&' and 'or' instead of OCaml's'&&' and '||' (although > OCaml still allows the old operator names, so HOL Light kept them); > - Caml Light's lexical syntax was different (which explains most of the > point of using Camlp4/Camlp5 to change the OCaml lexical syntax). > > Mark. > > > on 16/8/12 10:21 PM, Vincent Aravantinos<[email protected]> > wrote: > >> Hi list, >> >> is there a good reason for not using Ocaml modules in HOL Light? >> >> This would yield a better name management, and shorter and more readable >> proofs. >> >> For instance, instead of having: >> >> # REAL_ADD_SYM;; >> val it : thm = |- !x y. x + y = y + x >> # REAL_ADD_LID;; >> val it : thm = |- !x.&0 + x = x >> # REAL_ADD_ASSOC;; >> val it : thm = |- !x y z. x + y + z = (x + y) + z >> # ... >> >> We could have: >> >> module Real : sig >> val ( ADD_SYM ) : thm >> val ( ADD_LID ) : thm >> val ( ADD_ASSOC ) : thm >> ... >> end >> >> And similarly: >> >> module Complex : sig >> val ( ADD_SYM ) : thm >> val ( ADD_LID ) : thm >> val ( ADD_ASSOC ) : thm >> ... >> end >> >> Then, if in a context where real numbers are prominent, one could just >> open the Real module, but still access Complex theorems by using the dot >> notation. >> >> Going further, we could even use the local opening >> (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc77) or >> aliasing >> (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc74) of >> modules. But both seem incompatible with the current camlp5 extension >> used by HOL Light. >> >> -- >> Vincent Aravantinos >> Postdoctoral Fellow, Concordia University, Hardware Verification Group >> http://users.encs.concordia.ca/~vincent >> >> >> > ---------------------------------------------------------------------------- >> -- >> Live Security Virtual Conference >> Exclusive live event will cover all the ways today's security and >> threat landscape has changed and how IT managers can respond. Discussions >> will include endpoint security, mobile security and the latest in malware >> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >> -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
