diff options
| author | Brian Campbell | 2017-10-23 22:30:00 +0100 |
|---|---|---|
| committer | Brian Campbell | 2017-10-23 22:30:00 +0100 |
| commit | 0c50d5d193535f277454d2fcd70e0dc502fb2c23 (patch) | |
| tree | 555f7bf95e79ab3c465ab424bc08fa7a7c1b07fd /src | |
| parent | fd21c0ca241418775d905184a6d619ddb11cafa3 (diff) | |
Type check external casts
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 58de77e1..d90e8d35 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3232,12 +3232,13 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) the difference is irrelevant for the typechecker. *) let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with - | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, false) -> (id, quants, typ, env) - | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, true) -> (id, quants, typ, Env.add_cast id env) - | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, Some ext, false) -> - let env = Env.add_extern id ext env in + | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) -> + let env = match ext_opt with + | None -> env + | Some ext -> Env.add_extern id ext env + in + let env = if is_cast then Env.add_cast id env else env in (id, quants, typ, env) - | _ -> typ_error l "Invalid valspec" in [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env |