diff options
| author | Kathy Gray | 2014-02-27 14:01:59 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-27 14:01:59 +0000 |
| commit | bfe28e3e443fd28e7182cfeff1cf8b5fa5bc4e5a (patch) | |
| tree | 715adfee820c1b59b0db2fd93f2614b07a69c8c9 /language/l2.ott | |
| parent | 88a18f8abc20fc1b421d22ed06a75a51bb293414 (diff) | |
| parent | 7582bed6349cd05d7237168a39d5dad99ede7e38 (diff) | |
Merge branch 'interp_typed'
Conflicts:
src/lem_interp/interp.lem
src/lem_interp/run_interp.ml
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/language/l2.ott b/language/l2.ott index 8cbacf0d..aa981cc7 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -58,7 +58,9 @@ open import Set_extra type l = | Unknown | Trans of string * maybe l - | Range of nat * nat + | Range of string * nat * nat * nat * nat + +type annot 'a = l * 'a val duplicates : forall 'a. list 'a -> list 'a @@ -102,7 +104,7 @@ l :: '' ::= {{ phantom }} annot :: '' ::= {{ phantom }} {{ ocaml 'a annot }} - {{ lem annot }} + {{ lem annot 'a }} {{ hol unit }} id :: '' ::= @@ -195,13 +197,13 @@ effect :: 'Effect_' ::= | pure :: M :: pure {{ com sugar for empty effect set }} {{ lem (Effect_set []) }} {{icho [[{}]] }} | effect1 u+ .. u+ effectn :: M :: union {{ com meta operation for combining sets of effects }} {{ icho [] }} - {{ lem (List.foldr effect_union (Effect_set []) [[effect1..effectn]]) }} + {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} embed {{ lem let effect_union e1 e2 = match (e1,e2) with - | (Effect_set els,Effect_set els2) -> Effect_set (els++els2) + | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l end }} @@ -727,7 +729,7 @@ grammar tannot_opt :: 'Typ_annot_opt_' ::= {{ com Optional type annotation for functions}} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} % | :: :: none % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return | typquant typ :: :: some @@ -740,7 +742,7 @@ rec_opt :: 'Rec_' ::= effect_opt :: 'Effect_opt_' ::= {{ com Optional effect annotation for functions }} - {{ aux _ annot }} {{ auxparam 'a }} + {{ aux _ l }} | :: :: pure {{ com sugar for empty effect set }} | effectkw effect :: :: effect @@ -837,6 +839,8 @@ defs :: '' ::= | def1 .. defn :: :: Defs + + terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} |