Commit 1c2e307c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Typing: only accept opaqueness annotations in prototypes

TODO: impose the same restriction in programs
parent 02fcd207
......@@ -104,20 +104,28 @@ let create_user_tv =
Hstr.add hs s tv;
tv
let rec ty_of_pty uc = function
| PPTtyvar ({id=x}, _) ->
ty_var (create_user_tv x)
| PPTtyapp (x, p) ->
let ts = find_tysymbol x uc in
let tyl = List.map (ty_of_pty uc) p in
Loc.try2 ~loc:(qloc x) ty_app ts tyl
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
ty_app ts (List.map (ty_of_pty uc) tyl)
| PPTarrow (ty1, ty2) ->
ty_func (ty_of_pty uc ty1) (ty_of_pty uc ty2)
| PPTparen ty ->
ty_of_pty uc ty
let ty_of_pty_top ~noop uc pty =
let rec get_ty = function
| PPTtyvar ({id_loc = loc}, true) when noop ->
Loc.errorm ~loc "Opaqueness@ annotations@ are@ only@ \
allowed@ in@ function@ and@ predicate@ prototypes"
| PPTtyvar ({id = x}, _) ->
ty_var (create_user_tv x)
| PPTtyapp (x, p) ->
let ts = find_tysymbol x uc in
let tyl = List.map get_ty p in
Loc.try2 ~loc:(qloc x) ty_app ts tyl
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
ty_app ts (List.map get_ty tyl)
| PPTarrow (ty1, ty2) ->
ty_func (get_ty ty1) (get_ty ty2)
| PPTparen ty ->
get_ty ty
in
get_ty pty
let ty_of_pty uc pty = ty_of_pty_top ~noop:true uc pty
let opaque_tvs args value =
let rec opaque_tvs acc = function
......@@ -329,11 +337,11 @@ let type_fmla uc gfn f =
(** Typing declarations *)
let tyl_of_params uc pl =
let tyl_of_params ~noop uc pl =
let ty_of_param (loc,_,gh,ty) =
if gh then Loc.errorm ~loc
"ghost parameters are not allowed in pure declarations";
ty_of_pty uc ty in
ty_of_pty_top ~noop uc ty in
List.map ty_of_param pl
let add_types dl th =
......@@ -438,7 +446,7 @@ let add_types dl th =
Some pj
in
let constructor (loc, id, pl) =
let tyl = tyl_of_params th' pl in
let tyl = tyl_of_params ~noop:true th' pl in
let pjl = List.map2 projection pl tyl in
Hstr.replace csymbols id.id loc;
create_fsymbol ~opaque ~constr (create_user_id id) tyl ty, pjl
......@@ -491,8 +499,8 @@ let add_logics dl th =
let create_symbol th d =
let id = d.ld_ident.id in
let v = create_user_id d.ld_ident in
let pl = tyl_of_params th d.ld_params in
let ty = Opt.map (ty_of_pty th) d.ld_type in
let pl = tyl_of_params ~noop:false th d.ld_params in
let ty = Opt.map (ty_of_pty_top ~noop:false th) d.ld_type in
let opaque = opaque_tvs d.ld_params d.ld_type in
let ls = create_lsymbol ~opaque v pl ty in
Hstr.add lsymbols id ls;
......@@ -575,7 +583,7 @@ let add_inductives s dl th =
let create_symbol th d =
let id = d.in_ident.id in
let v = create_user_id d.in_ident in
let pl = tyl_of_params th d.in_params in
let pl = tyl_of_params ~noop:false th d.in_params in
let opaque = opaque_tvs d.in_params None in
let ps = create_psymbol ~opaque v pl in
Hstr.add psymbols id ps;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment