Commit ac5e027d authored by Andrei Paskevich's avatar Andrei Paskevich

unify the syntax of binders in logic and programs

Also, ghost fields in algerbraic types are now accepted in programs.

As of now, "function", "predicate", "inductive", "val", "let", "fun",
and constructors in algebraic type declarations all accept the same
syntax for parameters. In "function", "predicate", "inductive", "val",
and constructors in algebraic type declarations, binders without
colons are treated as type expressions:

    function f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    function f (_: int) (_: list bool) (_: (int,real)) (ghost _: bool)

In "let" and "fun", single unqualified idents are treated as parameter
names whose types are to be inferred, other binders without colons are
treated as type expressions:

    let f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    let f (int: ?) (_: list bool) (_: (int,real)) (ghost bool: ?)

Anonymous binders ("_") are accepted only if their type is specified.
parent 0445849f
......@@ -37,6 +37,17 @@ end
let floc_ij i j = Loc.extract (loc_ij i j)
*)
let pty_of_id i = PPTtyapp (Qident i, [])
let params_of_binders bl = List.map (function
| l, None, _, None -> Loc.errorm ~loc:l "cannot determine the type"
| l, Some i, gh, None -> l, None, gh, pty_of_id i
| l, i, gh, Some t -> l, i, gh, t) bl
let quvars_of_lidents ty ll = List.map (function
| l, None -> Loc.errorm ~loc:l "anonymous binders are not allowed here"
| _, Some i -> i, ty) ll
let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
let mk_pp d = mk_ppl (floc ()) d
(* dead code
......@@ -475,7 +486,7 @@ typecases:
;
typecase:
| uident labels params { (floc (), add_lab $1 $2, $3) }
| uident labels list0_param { (floc (), add_lab $1 $2, $3) }
;
/* Logic declarations */
......@@ -502,28 +513,23 @@ logic_decl_constant:
;
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
| lident_rich labels list0_param COLON primitive_type logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;
logic_decl_predicate:
| lident_rich labels params logic_def_option
| lident_rich labels list0_param logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = None; ld_def = $4 } }
;
logic_decl:
| lident_rich labels params logic_type_option logic_def_option
| lident_rich labels list0_param opt_cast logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = $4; ld_def = $5 } }
;
logic_type_option:
| /* epsilon */ { None }
| COLON primitive_type { Some $2 }
;
logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr { Some $2 }
......@@ -537,7 +543,7 @@ list1_inductive_decl:
;
inductive_decl:
| lident_rich labels params inddefn
| lident_rich labels list0_param inddefn
{ { in_loc = floc (); in_ident = add_lab $1 $2;
in_params = $3; in_def = $4 } }
;
......@@ -573,6 +579,11 @@ primitive_type_args:
| primitive_type_arg primitive_type_args { $1 :: $2 }
;
primitive_type_args_non_lident:
| primitive_type_arg_non_lident { [$1] }
| primitive_type_arg_non_lident primitive_type_args { $1 :: $2 }
;
primitive_type_arg:
| lident { PPTtyapp (Qident $1, []) }
| primitive_type_arg_non_lident { $1 }
......@@ -635,7 +646,7 @@ lexpr:
{ mk_pp (PPapp ($1, $2)) }
| IF lexpr THEN lexpr ELSE lexpr
{ mk_pp (PPif ($2, $4, $6)) }
| quant list1_param_var_sep_comma triggers DOT lexpr
| quant list1_quant_vars triggers DOT lexpr
{ mk_pp (PPquant ($1, $2, $3, $5)) }
| label lexpr %prec prec_named
{ mk_pp (PPnamed ($1, $2)) }
......@@ -651,7 +662,7 @@ lexpr:
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
{ mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
| EPSILON lident labels COLON primitive_type DOT lexpr
{ mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
{ mk_pp (PPeps ((add_lab $2 $3, Some $5), $7)) }
| lexpr COLON primitive_type
{ mk_pp (PPcast ($1, $3)) }
| lexpr_arg
......@@ -798,68 +809,113 @@ pat_field:
| lqualid EQUAL pattern { ($1, $3) }
;
/* Parameters */
/* Binders */
params:
| /* epsilon */ { [] }
| param params { $1 @ $2 }
list0_param:
| /* epsilon */ { [] }
| list1_param { $1 }
;
param:
| LEFTPAR param_var RIGHTPAR
{ $2 }
| LEFTPAR param_type RIGHTPAR
{ [None, $2] }
| LEFTPAR param_type COMMA list1_primitive_type_sep_comma RIGHTPAR
{ [None, PPTtuple ($2::$4)] }
| LEFTPAR RIGHTPAR
{ [None, PPTtuple []] }
list1_param:
| list1_binder { params_of_binders $1 }
;
list1_binder:
| binder { $1 }
| binder list1_binder { $1 @ $2 }
;
binder:
| type_var
{ [None, PPTtyvar $1] }
| lqualid
{ [None, PPTtyapp ($1, [])] }
{ [floc (), None, false, Some (PPTtyvar $1)] }
| lqualid_qualified
{ [floc (), None, false, Some (PPTtyapp ($1, []))] }
| lident labels
{ [floc (), Some (add_lab $1 $2), false, None] }
| UNDERSCORE
{ Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" }
| LEFTPAR RIGHTPAR
{ [floc (), None, false, Some (PPTtuple [])] }
| LEFTPAR binder_in RIGHTPAR
{ $2 }
| LEFTPAR GHOST binder_in RIGHTPAR
{ List.map (fun (l,i,_,t) -> (l,i,true,t)) $3 }
| LEFTPAR binder_type COMMA list1_primitive_type_sep_comma RIGHTPAR
{ [floc (), None, false, Some (PPTtuple ($2::$4))] }
;
param_type:
| lident param_type_cont
{ PPTtyapp (Qident $1, $2) }
| lident list1_lident param_type_cont
{ let id2ty i = PPTtyapp (Qident i, []) in
PPTtyapp (Qident $1, List.map id2ty $2 @ $3) }
binder_in:
| lident labels
{ [floc (), Some (add_lab $1 $2), false, None] }
| UNDERSCORE
{ Loc.errorm ~loc:(floc ()) "untyped anonymous parameters are not allowed" }
| binder_type_rest
{ [floc (), None, false, Some $1] }
| binder_vars COLON primitive_type
{ List.map (fun (l,v) -> l, v, false, Some $3) $1 }
;
binder_type:
| lident { PPTtyapp (Qident $1, []) }
| binder_type_rest { $1 }
;
binder_type_rest:
| lident list1_lident
{ PPTtyapp (Qident $1, List.map pty_of_id $2) }
| lident list0_lident primitive_type_args_non_lident
{ PPTtyapp (Qident $1, List.map pty_of_id $2 @ $3) }
| primitive_type_non_lident
{ $1 }
;
param_type_cont:
| /* epsilon */ { [] }
| primitive_type_arg_non_lident { [$1] }
| primitive_type_arg_non_lident primitive_type_args { $1 :: $2 }
binder_vars:
| list1_lident
{ List.map (fun id -> id.id_loc, Some id) $1 }
| list1_lident UNDERSCORE list0_lident_labels
{ List.map (fun id -> id.id_loc, Some id) $1 @ (floc_i 2, None) :: $3 }
| lident list1_lident label labels list0_lident_labels
{ let l = match List.rev ($1 :: $2) with
| i :: l -> add_lab i ($3 :: $4) :: l
| [] -> assert false in
List.fold_left (fun acc id -> (id.id_loc, Some id) :: acc) $5 l }
| lident label labels list0_lident_labels
{ ($1.id_loc, Some (add_lab $1 ($2 :: $3))) :: $4 }
| UNDERSCORE list0_lident_labels
{ (floc_i 1, None) :: $2 }
;
list1_param_var_sep_comma:
| param_var { $1 }
| param_var COMMA list1_param_var_sep_comma { $1 @ $3 }
list0_lident:
| /* epsilon */ { [] }
| list1_lident { $1 }
;
param_var:
| list1_lident COLON primitive_type
{ List.map (fun id -> (Some id, $3)) $1 }
| list1_lident label labels list0_lident_labels COLON primitive_type
{ let l = match List.rev $1 with
| i :: l -> add_lab i ($2 :: $3) :: l
| [] -> assert false
in
List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
list1_lident:
| lident list0_lident { $1 :: $2 }
;
list1_lident:
| lident { [$1] }
| lident list1_lident { $1 :: $2 }
list1_quant_vars:
| quant_vars { $1 }
| quant_vars COMMA list1_quant_vars { $1 @ $3 }
;
quant_vars:
| list1_lident_labels COLON primitive_type
{ quvars_of_lidents (Some $3) $1 }
;
list0_lident_labels:
| /* epsilon */ { [] }
| lident labels list0_lident_labels { add_lab $1 $2 :: $3 }
| /* epsilon */ { [] }
| list1_lident_labels { $1 }
;
list1_lident_labels:
| lident_labels list0_lident_labels { $1 :: $2 }
;
lident_labels:
| lident labels { floc (), Some (add_lab $1 $2) }
| UNDERSCORE { floc (), None }
;
/* Idents */
......@@ -940,6 +996,10 @@ lqualid_copy:
| uqualid DOT lident { Qdot ($1, $3) }
;
lqualid_qualified:
| uqualid DOT lident { Qdot ($1, $3) }
;
uqualid:
| uident { Qident $1 }
| uqualid DOT uident { Qdot ($1, $3) }
......@@ -1037,7 +1097,7 @@ type_v:
;
arrow_type_v:
| list1_type_v_param tail_type_c { Tarrow ($1, $2) }
| list1_param tail_type_c { Tarrow ($1, $2) }
;
tail_type_c:
......@@ -1060,17 +1120,17 @@ list1_rec_defn:
;
rec_defn:
| ghost lident_rich labels list1_type_v_binder opt_cast spec EQUAL spec expr
| ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
{ floc (), add_lab $2 $3, $1, $4, (cast_body $5 $9, spec_union $6 $8) }
;
fun_defn:
| list1_type_v_binder opt_cast spec EQUAL spec expr
| list1_binder opt_cast spec EQUAL spec expr
{ mk_expr_i 6 (Efun ($1, (cast_body $2 $6, spec_union $3 $5))) }
;
fun_expr:
| FUN list1_type_v_binder spec ARROW spec expr
| FUN list1_binder spec ARROW spec expr
{ mk_expr (Efun ($2, ($6, spec_union $3 $5))) }
;
......@@ -1274,34 +1334,6 @@ for_direction:
| DOWNTO { Downto }
;
list1_type_v_binder:
| type_v_binder { $1 }
| type_v_binder list1_type_v_binder { $1 @ $2 }
;
list1_type_v_param:
| type_v_param { $1 }
| type_v_param list1_type_v_param { $1 @ $2 }
;
type_v_binder:
| ghost lident labels
{ [add_lab $2 $3, $1, None] }
| type_v_param
{ $1 }
;
type_v_param:
| LEFTPAR RIGHTPAR
{ [id_anonymous (), false, Some (ty_unit ())] }
| LEFTPAR ghost lidents_lab COLON primitive_type RIGHTPAR
{ List.map (fun i -> (i, $2, Some $5)) $3 }
;
lidents_lab:
| lident labels list0_lident_labels { add_lab $1 $2 :: $3 }
;
loop_annotation:
| /* epsilon */
{ { loop_invariant = []; loop_variant = [] } }
......@@ -1403,7 +1435,7 @@ single_variant:
;
opt_cast:
| /* epsilon */ { None }
| /* epsilon */ { None }
| COLON primitive_type { Some $2 }
;
......
......@@ -43,7 +43,11 @@ type pty =
| PPTtyapp of qualid * pty list
| PPTtuple of pty list
type param = ident option * pty
type ghost = bool
type binder = loc * ident option * ghost * pty option
type param = loc * ident option * ghost * pty
type quvar = ident * pty option
type pattern =
{ pat_loc : loc; pat_desc : pat_desc }
......@@ -71,10 +75,10 @@ and pp_desc =
| PPbinop of lexpr * pp_binop * lexpr
| PPunop of pp_unop * lexpr
| PPif of lexpr * lexpr * lexpr
| PPquant of pp_quant * param list * lexpr list list * lexpr
| PPquant of pp_quant * quvar list * lexpr list list * lexpr
| PPnamed of label * lexpr
| PPlet of ident * lexpr * lexpr
| PPeps of ident * pty * lexpr
| PPeps of quvar * lexpr
| PPmatch of lexpr * (pattern * lexpr) list
| PPcast of lexpr * pty
| PPtuple of lexpr list
......@@ -178,8 +182,6 @@ type loop_annotation = {
type for_direction = To | Downto
type ghost = bool
type pre = lexpr
type post = loc * (pattern * lexpr) list
type xpost = loc * (qualid * pattern * lexpr) list
......@@ -193,11 +195,9 @@ type spec = {
sp_variant : variant list;
}
type binder = ident * ghost * pty option
type type_v =
| Tpure of pty
| Tarrow of binder list * type_c
| Tarrow of param list * type_c
and type_c = type_v * spec
......
......@@ -337,12 +337,27 @@ let rec trigger_not_a_term_exn = function
| Loc.Located (_, exn) -> trigger_not_a_term_exn exn
| _ -> false
let check_quant_linearity uqu =
let param_tys uc pl =
let s = ref Sstr.empty in
let check id =
s := Loc.try3 id.id_loc Sstr.add_new (DuplicateVar id.id) id.id !s
in
List.iter (fun (idl, _) -> Opt.iter check idl) uqu
let ty_of_param (loc,id,gh,ty) =
if gh then Loc.errorm ~loc "ghost parameters are not allowed here";
Opt.iter (fun { id = id; id_loc = loc } ->
s := Loc.try3 loc Sstr.add_new (DuplicateVar id) id !s) id;
ty_of_dty (dty uc ty) in
List.map ty_of_param pl
let quant_var uc env (id,ty) =
let ty = match ty with
| None -> Denv.fresh_type_var id.id_loc
| Some ty -> dty uc ty in
add_var id.id ty env, (id,ty)
let quant_vars uc env qvl =
let s = ref Sstr.empty in
let add env (({ id = id; id_loc = loc }, _) as qv) =
s := Loc.try3 loc Sstr.add_new (DuplicateVar id) id !s;
quant_var uc env qv in
Lists.map_fold_left add env qvl
let check_highord uc env x tl = match x with
| Qident { id = x } when Mstr.mem x env.dvars -> true
......@@ -445,22 +460,12 @@ and dterm_node ~localize loc uc env = function
let e3 = dterm ~localize uc env e3 in
unify_raise ~loc e3.dt_ty e2.dt_ty;
Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
| PPeps (x, ty, e1) ->
let ty = dty uc ty in
let env = add_var x.id ty env in
| PPeps (b, e1) ->
let env, (x, ty) = quant_var uc env b in
let e1 = dfmla ~localize uc env e1 in
Teps (x, ty, e1), ty
| PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
check_quant_linearity uqu;
let uquant env (idl,ty) =
let ty = dty uc ty in
let id = match idl with
| Some id -> id
| None -> assert false
in
add_var id.id ty env, (id,ty)
in
let env, uqu = Lists.map_fold_left uquant env uqu in
let env, uqu = quant_vars uc env uqu in
let trigger e =
try
TRterm (dterm ~localize uc env e)
......@@ -570,16 +575,7 @@ and dfmla_node ~localize loc uc env = function
Fif (dfmla ~localize uc env a,
dfmla ~localize uc env b, dfmla ~localize uc env c)
| PPquant (q, uqu, trl, a) ->
check_quant_linearity uqu;
let uquant env (idl,ty) =
let ty = dty uc ty in
let id = match idl with
| Some id -> id
| None -> assert false
in
add_var id.id ty env, (id,ty)
in
let env, uqu = Lists.map_fold_left uquant env uqu in
let env, uqu = quant_vars uc env uqu in
let trigger e =
try
TRterm (dterm ~localize uc env e)
......@@ -806,8 +802,7 @@ let add_types dl th =
| TDalgebraic cl ->
let ht = Hstr.create 17 in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let param (_,t) = ty_of_dty (dty th' t) in
let projection (id,_) fty = match id with
let projection (_,id,_,_) fty = match id with
| None -> None
| Some id ->
try
......@@ -823,7 +818,7 @@ let add_types dl th =
Some pj
in
let constructor (loc, id, pl) =
let tyl = List.map param pl in
let tyl = param_tys th' pl in
let pjl = List.map2 projection pl tyl in
Hstr.replace csymbols id.id loc;
create_fsymbol (create_user_id id) tyl ty, pjl
......@@ -861,7 +856,7 @@ let prepare_typedef td =
f_mutable = mut; f_ghost = gh } =
if mut then errorm ~loc "a logic record field cannot be mutable";
if gh then errorm ~loc "a logic record field cannot be ghost";
Some id, ty
loc, Some id, false, ty
in
(* constructor for type t is "mk t" (and not String.capitalize t) *)
let id = { td.td_ident with id = "mk " ^ td.td_ident.id } in
......@@ -880,18 +875,17 @@ let add_logics dl th =
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
let v = create_user_id d.ld_ident in
let denv = denv_empty in
Hstr.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty th t) in
let pl = List.map type_ty d.ld_params in
let v = create_user_id d.ld_ident in
let pl = param_tys th d.ld_params in
let add d = match d.ld_type with
| None -> (* predicate *)
let ps = create_psymbol v pl in
Hstr.add psymbols id ps;
add_param_decl th ps
| Some t -> (* function *)
let t = type_ty (None, t) in
let t = ty_of_dty (dty th t) in
let fs = create_fsymbol v pl t in
Hstr.add fsymbols id fs;
add_param_decl th fs
......@@ -902,21 +896,18 @@ let add_logics dl th =
(* 2. then type-check all definitions *)
let type_decl d (abst,defn) =
let id = d.ld_ident.id in
check_quant_linearity d.ld_params;
let dadd_var denv (x, ty) = match x with
| None -> denv
let dadd_var denv (_,x,_,ty) = match x with
| Some id -> add_var id.id (dty th' ty) denv
| None -> denv
in
let denv = Hstr.find denvs id in
let denv = List.fold_left dadd_var denv d.ld_params in
let create_var (x, _) ty =
let create_var (loc,x,_,_) ty =
let id = match x with
| None -> id_fresh "%x"
| Some id -> create_user_id id
in
create_vsymbol id ty
in
let mk_vlist = List.map2 create_var d.ld_params in
| None -> id_user "_" loc in
create_vsymbol id ty in
let mk_vlist tyl = List.map2 create_var d.ld_params tyl in
match d.ld_type with
| None -> (* predicate *)
let ps = Hstr.find psymbols id in
......@@ -976,8 +967,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 type_ty (_,t) = ty_of_dty (dty th t) in
let pl = List.map type_ty d.in_params in
let pl = param_tys th d.in_params in
let ps = create_psymbol v pl in
Hstr.add psymbols id ps;
Loc.try2 d.in_loc add_param_decl th ps
......
......@@ -388,14 +388,20 @@ and dpat_app denv gloc ({ de_loc = loc } as de) ppl dity =
(* specifications *)
let dbinders denv bl =
let hv = Hstr.create 3 in
let dbinder (id,gh,pty) (denv,bl,tyl) =
if Hstr.mem hv id.id then raise (DuplicateProgVar id.id);
Hstr.add hv id.id ();
let s = ref Sstr.empty in
let dbinder (loc,id,gh,pty) (denv,bl,tyl) =
let dity = match pty with
| Some pty -> dity_of_pty denv pty
| None -> create_type_variable () in
add_var id dity denv, (id,gh,dity)::bl, dity::tyl
| None -> create_type_variable ()
in
let denv, id = match id with
| Some ({ id = x; id_loc = loc } as id) ->
s := Loc.try3 loc Sstr.add_new (DuplicateProgVar x) x !s;
add_var id dity denv, id
| None ->
denv, { id = "_"; id_loc = loc; id_lab = [] }
in
denv, (id,gh,dity)::bl, dity::tyl
in
List.fold_right dbinder bl (denv,[],[])
......@@ -443,6 +449,7 @@ and dtype_v denv = function
let dity = dity_of_pty denv pty in
DSpecV dity, ([],dity)
| Tarrow (bl,tyc) ->
let bl = List.map (fun (l,i,g,t) -> l,i,g,Some t) bl in
let denv,bl,tyl = dbinders denv bl in
let tyc,(argl,res) = dtype_c denv tyc in
DSpecA (bl,tyc), (tyl @ argl,res)
......@@ -1525,7 +1532,7 @@ let add_type_invariant loc uc id params inv =
let look_for_loc tdl s =
let look_id loc id = if id.id = s then Some id.id_loc else loc in
let look_pj loc (id,_) = Opt.fold look_id loc id in
let look_pj loc (_,id,_,_) = Opt.fold look_id loc id in
let look_cs loc (csloc,id,pjl) =
let loc = if id.id = s then Some csloc else loc in
List.fold_left look_pj loc pjl in
......@@ -1590,7 +1597,8 @@ let add_types ~wp uc tdl =
| TDabstract -> false
| TDalias ty -> check ty
| TDalgebraic csl ->
let cons (_,_,l) = List.exists (fun (_,ty) -> check ty) l in
let check (_,_,gh,ty) = gh || check ty in
let cons (_,_,l) = List.exists check l in
td.td_inv <> [] || td.td_vis <> Public || List.exists cons csl
| TDrecord fl ->
let field f = f.f_ghost || f.f_mutable || check f.f_pty in
......@@ -1626,7 +1634,8 @@ let add_types ~wp uc tdl =
| TDabstract -> false
| TDalias ty -> check ty
| TDalgebraic csl ->
let cons (_,_,l) = List.exists (fun (_,ty) -> check ty) l in
let check (_,_,_,ty) = check ty in
let cons (_,_,l) = List.exists check l in
td.td_inv <> [] || List.exists cons csl
| TDrecord fl ->
let field f = f.f_mutable || check f.f_pty in
......@@ -1692,9 +1701,9 @@ let add_types ~wp uc tdl =
(* to check projections' types we must fix the tyvars *)
let add s v = let t = ity_var v in ity_match s t t in
let sbs = List.fold_left add ity_subst_empty vl in
let mk_proj (regs,inv) (id,pty) =
let mk_proj (regs,inv) (_loc,id,gh,pty) =
let ity = parse pty in
let fd = mk_field ity false None in
let fd = mk_field ity gh None in
let inv = inv || ity_has_inv ity in
match id with
| None ->
......@@ -1703,8 +1712,8 @@ let add_types ~wp uc tdl =
| Some id ->
try
let fd = Hstr.find projs id.id in
(* TODO: once we have ghost/mutable fields in algebraics,
don't forget to check here that they coincide, too *)
if gh <> fd.fd_ghost then Loc.errorm ~loc:id.id_loc
"this field must be ghost in every constructor";
ignore (Loc.try3 id.id_loc ity_match sbs fd.fd_ity ity);
(regs, inv), (Some (Denv.create_user_id id), fd)
with Not_found ->
......@@ -1787,16 +1796,16 @@ let add_types ~wp uc tdl =
abstr, (ts, Hstr.find predefs x) :: algeb, alias
| TDalgebraic csl ->
let projs = Hstr.create 5 in
let mk_proj (id,pty) =
let mk_proj (_loc,id,gh,pty) =
let ity = parse pty in
let fd = mk_field ity false None in
let fd = mk_field ity gh None in
match id with
| None -> None, fd
| Some id ->
try
let fd = Hstr.find projs id.id in
(* once we have ghost/mutable fields in algebraics,
don't forget to check here that they coincide, too *)
if gh <> fd.fd_ghost then Loc.errorm ~loc:id.id_loc
"this field must be ghost in every constructor";
Loc.try2 id.id_loc ity_equal_check fd.fd_ity ity;
Some (Denv.create_user_id id), fd
with Not_found ->
......
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