summaryrefslogtreecommitdiff
path: root/src/parser.mly
diff options
context:
space:
mode:
authorjp2020-02-12 17:46:48 +0000
committerjp2020-02-12 17:46:48 +0000
commited8bccd927306551f93d5aab8d0e2a92b9e5d227 (patch)
tree55bf788c8155f0c7d024f2147f5eb3873729b02a /src/parser.mly
parent31a65c9b7383d2a87da0fbcf5c265d533146ac23 (diff)
parent4a72cb8084237161d0bccc66f27d5fb6d24315e0 (diff)
Merge branch 'sail2' of https://github.com/rems-project/sail into sail2
Diffstat (limited to 'src/parser.mly')
-rw-r--r--src/parser.mly8
1 files changed, 6 insertions, 2 deletions
diff --git a/src/parser.mly b/src/parser.mly
index 0b09468c..6a579b7a 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -657,9 +657,13 @@ typschm:
| Forall typquant Dot typ MinusGt typ Effect effect_set
{ (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
| typ Bidir typ
- { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3)) s e) s e) $startpos $endpos }
+ { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
| Forall typquant Dot typ Bidir typ
- { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6)) s e) s e) $startpos $endpos }
+ { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
+ | typ Bidir typ Effect effect_set
+ { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, $5)) s e) s e) $startpos $endpos }
+ | Forall typquant Dot typ Bidir typ Effect effect_set
+ { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, $8)) s e) s e) $startpos $endpos }
typschm_eof:
| typschm Eof