diff options
| author | Christopher Pulte | 2019-03-01 16:30:53 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2019-03-01 16:30:53 +0000 |
| commit | 6aeb20251c94f391796d86d16deed70eee59d5ef (patch) | |
| tree | 4d2d529ea57efdacb8ba221827792813e5491f0a /src | |
| parent | cbd1411dd4ddae8980e0df89abe7717c7dd3973e (diff) | |
| parent | d9db6da6d031effbf820de406f06c4ee973939a5 (diff) | |
Merge branch 'sail2' of https://github.com/rems-project/sail into sail2
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index a2612794..1afd9765 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1585,6 +1585,10 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2) + | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" -> + if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty + else unify_error l (string_of_typ typ2 ^ " must be a natural number") + | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]), Typ_app (atom, [A_aux (A_nexp m, _)]) when string_of_id range = "range" && string_of_id atom = "atom" -> |