Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
rml [2009/10/14 16:01] vkuncak |
rml [2010/01/29 17:18] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Rich Model Language ====== | ====== Rich Model Language ====== | ||
- | Tool chain | + | ===== Syntax ===== |
* lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) | * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) | ||
* tools to provide nicer surface syntax and generate lisp syntax | * tools to provide nicer surface syntax and generate lisp syntax | ||
+ | * we have a candidate using LR(1) parser (CUP) | ||
+ | * an earlier version: [[Vepar Grammar]] | ||
+ | |||
+ | ===== Semantics ===== | ||
+ | |||
+ | Classical HOL | ||
+ | * built in operators | ||
+ | * define them whenever natural, or state strong enough properties | ||
+ | |||
+ | ===== Type System ===== | ||
+ | |||
+ | Simple types | ||
+ | |||
+ | Parametric polymorphism | ||
+ | |||
+ | ===== Starting Points ===== | ||
Document summarizing operators of interest: | Document summarizing operators of interest: | ||
- | * {{:isabellemain.pdf|What's in Isabelle Main, October 14}} | + | * {{:isabellemain.pdf|What's in Isabelle Main, October 14, 2009}} |
Some differences: | Some differences: | ||
* separate operators for + on integers, reals | * separate operators for + on integers, reals | ||
- | * no 'nat' for now, indexing lists gives unknown value | + | * no 'nat' for now, indexing lists gives unknown value for negative |
* a 'finite' predicate, no separate type | * a 'finite' predicate, no separate type | ||
* introduce a type for SMT-LIB 2.0 (same problem for maps) | * introduce a type for SMT-LIB 2.0 (same problem for maps) | ||
Line 16: | Line 33: | ||
* no set intervals | * no set intervals | ||
* option types | * option types | ||
- | * subset of list operations | + | * a subset of list operations |