Commit efaf0dc2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

be more stricte in accepting inductives and algebraics

1. We only accept an algebraic type declaration

    T 'a1 ... 'aN

whenever every constructor has ls_value = Some (T 'a1 ... 'aN),
no type variable renaming is allowed.

2. We only accept an inductive predicate declaration

    P (_x1 : T1) ... (_xN : TN)

whenever every inductive clause has a conclusion of the form
(P (t1 : T1) ... (tN : TN)), no type variable renaming is allowed.

3. To this purpose, we must typecheck the whole (mutual) inductive
declaration group in the same denv. This must be ok, since user-named
type variables cannot be destructively instantiated anyway. However,
I'd like Jean-Christoph to check my changes in Typing.add_inductives.
parent 5146df7c
......@@ -390,7 +390,7 @@ let create_ty_decl tdl =
let tss = List.fold_left add Sts.empty tdl in
let check_constr tys ty (syms,news) fs =
let vty = of_option fs.ls_value in
ignore (ty_match Mtv.empty vty ty);
if not (ty_equal ty vty) then raise (TypeMismatch (ty,vty));
let add s ty = match ty.ty_node with
| Tyvar v -> Stv.add v s
| _ -> assert false
......@@ -475,11 +475,11 @@ let create_ind_decl idl =
let cls, f = clause [] (check_fvs f) in
match f.f_node with
| Fapp (s, tl) when ls_equal s ps ->
let mtch sb t ty =
try ty_match sb (t.t_ty) ty with TypeMismatch _ ->
let mtch t ty =
if not (ty_equal t.t_ty ty) then
raise (TooSpecificIndDecl (ps, pr, t))
ignore (List.fold_left2 mtch Mtv.empty tl ps.ls_args);
List.iter2 mtch tl ps.ls_args;
(try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
syms_fmla syms f, news_id news pr.pr_name
......@@ -1023,11 +1023,10 @@ let f_pred_app_l pr tl = match List.rev tl with
| _ -> Pervasives.invalid_arg "f_pred_app_l"
let fs_tuple = Util.memo_int 17 (fun n ->
let tyl = ref [] in
for i = 1 to n
do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
let ty = ty_tuple !tyl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty)
let ts = ts_tuple n in
let tl = ty_var ts.ts_args in
let ty = ty_app ts tl in
create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) tl ty)
let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
......@@ -872,17 +872,13 @@ let type_term denv env t =
let t = dterm denv t in
term env t
let term uc = type_term (create_denv uc) Mstr.empty
let type_fmla denv env f =
let f = dfmla denv f in
fmla env f
let fmla uc = type_fmla (create_denv uc) Mstr.empty
let add_prop k loc s f th =
let pr = create_prsymbol (id_user ~labels:s.id_lab loc) in
try add_prop_decl th k pr (fmla th f)
try add_prop_decl th k pr (type_fmla (create_denv th) Mstr.empty f)
with ClashSymbol s -> error ~loc (Clash s)
let loc_of_id id = match id.id_origin with
......@@ -891,11 +887,11 @@ let loc_of_id id = match id.id_origin with
let add_inductives dl th =
(* 1. create all symbols and make an environment with these symbols *)
let denv = create_denv th in
let psymbols = Hashtbl.create 17 in
let create_symbol th d =
let id = in
let v = id_user ~labels:d.in_ident.id_lab id d.in_loc in
let denv = create_denv th in
let type_ty (_,t) = ty_of_dty (dty denv t) in
let pl = type_ty d.in_params in
let ps = create_psymbol v pl in
......@@ -904,6 +900,7 @@ let add_inductives dl th =
with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
let th' = List.fold_left create_symbol th dl in
let denv = { denv with uc = th' } in
(* 2. then type-check all definitions *)
let propsyms = Hashtbl.create 17 in
let type_decl d =
......@@ -911,7 +908,8 @@ let add_inductives dl th =
let ps = Hashtbl.find psymbols id in
let clause (loc, { id = id ; id_lab = labels }, f) =
Hashtbl.replace propsyms id loc;
create_prsymbol (id_user ~labels id loc), fmla th' f
let f = type_fmla denv Mstr.empty f in
create_prsymbol (id_user ~labels id loc), f
ps, clause d.in_def
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