Commit bddf7fdd authored by Andrei Paskevich's avatar Andrei Paskevich

Typing: a record constructor may not exist as an lsymbol

parent 19b6b500
......@@ -394,8 +394,8 @@ exception BadLogicDecl of lsymbol * lsymbol
exception BadConstructor of lsymbol
exception BadRecordField of lsymbol
exception RecordFieldMissing of lsymbol * lsymbol
exception DuplicateRecordField of lsymbol * lsymbol
exception RecordFieldMissing of lsymbol
exception DuplicateRecordField of lsymbol
exception EmptyDecl
exception EmptyAlgDecl of tysymbol
......@@ -420,21 +420,21 @@ let create_data_decl tdl =
if tdl = [] then raise EmptyDecl;
let add s (ts,_) = Sts.add ts s in
let tss = List.fold_left add Sts.empty tdl in
let check_proj cs tyv s tya ls = match ls with
let check_proj tyv s tya ls = match ls with
| None -> s
| Some ({ls_args = [ptyv]; ls_value = Some ptya; ls_constr = 0} as ls) ->
ty_equal_check tyv ptyv;
ty_equal_check tya ptya;
Sls.add_new (DuplicateRecordField (cs,ls)) ls s
Sls.add_new (DuplicateRecordField ls) ls s
| Some ls -> raise (BadRecordField ls)
in
let check_constr tys ty cll pjs (syms,news) (fs,pl) =
ty_equal_check ty (Opt.get_exn (BadConstructor fs) fs.ls_value);
let fs_pjs =
try List.fold_left2 (check_proj fs ty) Sls.empty fs.ls_args pl
try List.fold_left2 (check_proj ty) Sls.empty fs.ls_args pl
with Invalid_argument _ -> raise (BadConstructor fs) in
if not (Sls.equal pjs fs_pjs) then
raise (RecordFieldMissing (fs, Sls.choose (Sls.diff pjs fs_pjs)));
raise (RecordFieldMissing (Sls.choose (Sls.diff pjs fs_pjs)));
if fs.ls_constr <> cll then raise (BadConstructor fs);
let vs = ty_freevars Stv.empty ty in
let rec check seen ty = match ty.ty_node with
......@@ -779,12 +779,12 @@ let parse_record kn fll =
let pjs = List.fold_left (fun s pj -> Sls.add pj s) Sls.empty pjl in
let flm = List.fold_left (fun m (pj,v) ->
if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
Mls.add_new (DuplicateRecordField (cs,pj)) pj v m) Mls.empty fll in
Mls.add_new (DuplicateRecordField pj) pj v m) Mls.empty fll in
cs,pjl,flm
let make_record kn fll ty =
let cs,pjl,flm = parse_record kn fll in
let get_arg pj = Mls.find_exn (RecordFieldMissing (cs,pj)) pj flm in
let get_arg pj = Mls.find_exn (RecordFieldMissing pj) pj flm in
fs_app cs (List.map get_arg pjl) ty
let make_record_update kn t fll ty =
......
......@@ -138,8 +138,8 @@ exception EmptyIndDecl of lsymbol
exception BadConstructor of lsymbol
exception BadRecordField of lsymbol
exception RecordFieldMissing of lsymbol * lsymbol
exception DuplicateRecordField of lsymbol * lsymbol
exception RecordFieldMissing of lsymbol
exception DuplicateRecordField of lsymbol
(** {2 Utilities} *)
......
......@@ -574,9 +574,9 @@ let () = Exn_printer.register
fprintf fmt "Bad constructor: %a" print_ls ls
| Decl.BadRecordField ls ->
fprintf fmt "Not a record field: %a" print_ls ls
| Decl.RecordFieldMissing (_cs,ls) ->
| Decl.RecordFieldMissing ls ->
fprintf fmt "Field %a is missing" print_ls ls
| Decl.DuplicateRecordField (_cs,ls) ->
| Decl.DuplicateRecordField ls ->
fprintf fmt "Field %a is used twice in the same constructor" print_ls ls
| Decl.IllegalTypeAlias ts ->
fprintf fmt
......
......@@ -339,9 +339,9 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
let e1 = dterm e1 in
DTquant (q, qvl, trl, e1)
| Ptree.Trecord fl ->
let get_val cs pj = function
let get_val _cs pj = function
| Some e -> dterm tuc gvars at denv e
| None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
| None -> Loc.error ~loc (RecordFieldMissing pj) in
let cs, fl = parse_record ~loc tuc get_val fl in
DTapp (cs, fl)
| Ptree.Tupdate (e1, fl) ->
......@@ -396,7 +396,7 @@ let parse_record muc fll =
| _ -> raise (BadRecordField (ls_of_rs rs)) in
let pjs = Srs.of_list itd.itd_fields in
let flm = List.fold_left (fun m (pj,v) -> if Srs.mem pj pjs then
Mrs.add_new (DuplicateRecordField (ls_of_rs cs, ls_of_rs pj)) pj v m
Mrs.add_new (DuplicateRecordField (ls_of_rs pj)) pj v m
else raise (BadRecordField (ls_of_rs pj))) Mrs.empty fll in
cs, itd.itd_fields, flm
......@@ -607,9 +607,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Erecord fl ->
let ls_of_rs rs = match rs.rs_logic with
| RLls ls -> ls | _ -> assert false in
let get_val cs pj = function
| None -> Loc.error ~loc
(Decl.RecordFieldMissing (ls_of_rs cs, ls_of_rs pj))
let get_val _cs pj = function
| None -> Loc.error ~loc (Decl.RecordFieldMissing (ls_of_rs pj))
| Some e -> dexpr muc denv e in
let cs,fl = parse_record ~loc muc get_val fl in
expr_app loc (DErs cs) fl
......
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