Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
rml [2010/01/12 12:52] vkuncak |
rml [2010/01/29 16:45] 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 | ||
| + | |||
| + | ===== Starting Points ===== | ||
| Document summarizing operators of interest: | Document summarizing operators of interest: | ||
| Line 16: | Line 27: | ||
| * no set intervals | * no set intervals | ||
| * option types | * option types | ||
| - | * subset of list operations | + | * a subset of list operations |
| - | + | ||
| - | [[Vepar Grammar]] | + | |