[DMS-12] Variant types #16
Conversation
| let {it = (e_ds, e_stmts);_} = stmt local_ctxt e in | ||
| let the = (p_ds @ e_ds, p_stmts @ e_stmts) in | ||
| let els = switch_stmts ctxt at scrut cs in | ||
| [], [!!(IfS(conjoin conds at, !!the, !!els))] |
There was a problem hiding this comment.
Suggestion: do cojoin conds in pat_match
There was a problem hiding this comment.
It makes code a bit more general and maybe a bit simpler. But I am fine with current code.
There was a problem hiding this comment.
I think it's better to return a list of conditions from pat_match so that it's possible to check for irrefutable patterns by conds == []
src/viper/syntax.ml
Outdated
| @@ -11,10 +11,13 @@ type prog = (item list, info) Source.annotated_phrase | |||
| and item = (item', info) Source.annotated_phrase | |||
| and item' = | |||
| (* | import path *) | |||
| | AdtI of string * string list * adt_con list | |||
There was a problem hiding this comment.
| | AdtI of string * string list * adt_con list | |
| | AdtI of id * id list * adt_con list |
I think it should be string with location of original ids from the source code.
I know that we are not checking this in tests and even manually, but I think it's a good thing to keep common style of definitions at least in types. In the translation you can put Source.no_region as a stab value.
src/viper/syntax.ml
Outdated
| | FieldI of id * typ | ||
| | MethodI of id * par list * par list * exp list * exp list * seqn option | ||
| | InvariantI of string * exp | ||
|
|
||
| and adt_con = { con_name : string; con_fields : typ list } |
There was a problem hiding this comment.
| and adt_con = { con_name : string; con_fields : typ list } | |
| and adt_con = { con_name : id; con_fields : typ list } |
+1 for the previous thread
src/viper/syntax.ml
Outdated
| @@ -98,4 +101,5 @@ and typ' = | |||
| | RefT | |||
| | ArrayT | |||
| | TupleT | |||
| | ConT of string * typ list | |||
There was a problem hiding this comment.
| | ConT of string * typ list | |
| | ConT of id * typ list |
+1 for the previous thread
New test case:
test/viper/variants.mo