Commit 0c56437c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix type inhabitance test

parent 5e8e081e
......@@ -668,25 +668,34 @@ let check_match kn d = decl_fold (check_matchT kn) () d
exception NonFoundedTypeDecl of tysymbol
let rec check_foundness kn d =
let rec check_constr s ty ls =
let vty = of_option ls.ls_value in
let m = ty_match Mtv.empty vty ty in
let check ty = check_type s (ty_inst m ty) in
List.for_all check ls.ls_args
and check_type s ty = match ty.ty_node with
| Tyvar _ -> true
| Tyapp (ts,_) ->
if Sts.mem ts s then false else
let cl = find_constructors kn ts in
if cl == [] then true else
let s = Sts.add ts s in
List.exists (check_constr s ty) cl
let rec check_ts tss tvs ts =
(* recursive data type, abandon *)
if Sts.mem ts tss then false else
let cl = find_constructors kn ts in
(* an abstract type is inhabited iff
all its type arguments are inhabited *)
if cl == [] then Stv.is_empty tvs else
(* an algebraic type is inhabited iff
we can build a value of this type *)
let tss = Sts.add ts tss in
List.exists (check_constr tss tvs) cl
and check_constr tss tvs ls =
(* we can construct a value iff every
argument is of an inhabited type *)
List.for_all (check_type tss tvs) ls.ls_args
and check_type tss tvs ty = match ty.ty_node with
| Tyvar tv ->
not (Stv.mem tv tvs)
| Tyapp (ts,tl) ->
let check acc tv ty =
if check_type tss tvs ty then acc else Stv.add tv acc in
let tvs = List.fold_left2 check Stv.empty ts.ts_args tl in
check_ts tss tvs ts
match d.d_node with
| Dtype tdl ->
let check () (ts,_) =
let tl = ty_var ts.ts_args in
if check_type Sts.empty (ty_app ts tl)
if check_ts Sts.empty Stv.empty ts
then () else raise (NonFoundedTypeDecl ts)
List.fold_left check () tdl
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