check positivity condition for type definitions (for real now!)

also, export Ty.ty_v_* traversal functions

bench/typing/bad/wf_types1.why

+theory Main
+    type t 'a
+
+    type test1 'a = Test1 (t (test1 'a))
+end

bench/typing/bad/wf_types2.why

+theory Main
+    type id 'a = 'a
+
+    type test2 'a = Test2 (id (test2 'a))
+end

bench/typing/bad/wf_types3.why

+theory Main
+    type shell 'a = Shell 'a
+
+    type test3 'a = Test3 (shell (test3 'a))
+end

bench/typing/good/wf_types1.why

+theory Main
+    type option 'a = Some 'a | None
+
+    type test4 'a = Test4 (option (test4 'a))
+end

examples/wf_types.why

-theory Test
-    type t 'a
-
-    type test 'a = Test (t (test 'a))
-end
-
-theory Main
-    type id 'a = 'a
-    type shell 'a = Shell 'a
-    type option 'a = Some 'a | None
-
-(*
-    clone Test as T1 with type t = id
-    clone Test as T2 with type t = shell
-*)
-    clone Test as T3 with type t = option
-end

src/core/decl.ml

@@ -372,7 +372,7 @@ exception EmptyDecl
 exception EmptyAlgDecl of tysymbol
 exception EmptyIndDecl of lsymbol
 
-exception NonPositiveTypeDecl of tysymbol * lsymbol * tysymbol
+exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
 
 let news_id s id = Sid.add_new id (ClashIdent id) s
 
@@ -399,7 +399,7 @@ let create_ty_decl tdl =
       | Tyapp (ts,_) ->
           let now = Sts.mem ts tss in
           if seen && now then
-            raise (NonPositiveTypeDecl (tys,fs,ts))
+            raise (NonPositiveTypeDecl (tys,fs,ty))
           else
             let s = ty_fold (check (seen || now)) s ty in
             Sid.add ts.ts_name s
@@ -669,8 +669,55 @@ let rec check_foundness kn d =
       List.fold_left check () tdl
   | _ -> ()
 
+let rec ts_extract_pos kn sts ts =
+  if ts_equal ts ts_func then [false;true] else
+  if ts_equal ts ts_pred then [false] else
+  if Sts.mem ts sts then List.map Util.ttrue ts.ts_args else
+  match (Mid.find ts.ts_name kn).d_node with
+  | Dtype tdl -> begin match List.assq ts tdl with
+      | Tabstract -> List.map Util.ffalse ts.ts_args
+      | Talgebraic csl ->
+          let sts = Sts.add ts sts in
+          let rec get_ty stv ty = match ty.ty_node with
+            | Tyvar _ -> stv
+            | Tyapp (ts,tl) ->
+                let get acc pos =
+                  if pos then get_ty acc else ty_freevars Stv.empty in
+                List.fold_left2 get stv (ts_extract_pos kn sts ts) tl
+          in
+          let get_cs acc ls = List.fold_left get_ty acc ls.ls_args in
+          let negs = List.fold_left get_cs Stv.empty csl in
+          List.map (fun v -> not (Stv.mem v negs)) ts.ts_args
+      end
+  | _ -> assert false
+
+let check_positivity kn d = match d.d_node with
+  | Dtype tdl ->
+      let add s (ts,_) = Sts.add ts s in
+      let tss = List.fold_left add Sts.empty tdl in
+      let check_constr tys cs =
+        let rec check_ty ty = match ty.ty_node with
+          | Tyvar _ -> ()
+          | Tyapp (ts,tl) ->
+              let check pos ty =
+                if pos then check_ty ty else
+                if ty_s_any (fun ts -> Sts.mem ts tss) ty
+                then raise (NonPositiveTypeDecl (tys,cs,ty))
+              in
+              List.iter2 check (ts_extract_pos kn Sts.empty ts) tl
+        in
+        List.iter check_ty cs.ls_args
+      in
+      let check_decl (ts,td) = match td with
+        | Tabstract -> ()
+        | Talgebraic cl -> List.iter (check_constr ts) cl
+      in
+      List.iter check_decl tdl
+  | _ -> ()
+
 let known_add_decl kn d =
   let kn = known_add_decl kn d in
+  check_positivity kn d;
   check_foundness kn d;
   check_match kn d;
   kn

src/core/decl.mli

@@ -116,7 +116,7 @@ val create_prop_decl : prop_kind -> prsymbol -> term -> decl
 (* exceptions *)
 
 exception IllegalTypeAlias of tysymbol
-exception NonPositiveTypeDecl of tysymbol * lsymbol * tysymbol
+exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
 
 exception InvalidIndDecl of lsymbol * prsymbol
 exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol

src/core/pretty.ml

@@ -498,10 +498,10 @@ let () = Exn_printer.register
         print_ts ts
   | Decl.NonFoundedTypeDecl ts ->
       fprintf fmt "Cannot construct a value of type %a" print_ts ts
-  | Decl.NonPositiveTypeDecl (_ts, ls, ts1) ->
+  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
       fprintf fmt "Constructor %a \
-          contains a non strictly positive occurrence of type symbol %a"
-        print_ls ls print_ts ts1
+          contains a non strictly positive occurrence of type %a"
+        print_ls ls print_ty ty
   | Decl.InvalidIndDecl (_ls, pr) ->
       fprintf fmt "Ill-formed inductive clause %a"
         print_pr pr

src/core/ty.ml

@@ -75,13 +75,11 @@ let ts_hash ts = id_hash ts.ts_name
 let ty_hash ty = Hashweak.tag_hash ty.ty_tag
 
 let mk_ts name args def = {
-  ts_name = name;
+  ts_name = id_register name;
   ts_args = args;
   ts_def  = def;
 }
 
-let create_tysymbol name args def = mk_ts (id_register name) args def
-
 module Hsty = Hashcons.Make (struct
   type t = ty
 
@@ -132,6 +130,26 @@ let ty_all pr ty =
 let ty_any pr ty =
   try ty_fold (any_fn pr) false ty with FoldSkip -> true
 
+(* traversal functions on type variables *)
+
+let rec ty_v_map fn ty = match ty.ty_node with
+  | Tyvar v -> fn v
+  | Tyapp (f, tl) -> ty_app f (List.map (ty_v_map fn) tl)
+
+let rec ty_v_fold fn acc ty = match ty.ty_node with
+  | Tyvar v -> fn acc v
+  | Tyapp (_, tl) -> List.fold_left (ty_v_fold fn) acc tl
+
+let ty_v_all pr ty =
+  try ty_v_fold (all_fn pr) true ty with FoldSkip -> false
+
+let ty_v_any pr ty =
+  try ty_v_fold (any_fn pr) false ty with FoldSkip -> true
+
+let ty_full_inst m ty = ty_v_map (fun v -> Mtv.find v m) ty
+let ty_freevars s ty = ty_v_fold (fun s v -> Stv.add v s) s ty
+let ty_closed ty = ty_v_all Util.ffalse ty
+
 (* smart constructors *)
 
 exception BadTypeArity of tysymbol * int * int
@@ -141,20 +159,9 @@ exception UnboundTypeVar of tvsymbol
 let create_tysymbol name args def =
   let add s v = Stv.add_new v (DuplicateTypeVar v) s in
   let s = List.fold_left add Stv.empty args in
-  let rec vars () ty = match ty.ty_node with
-    | Tyvar v when not (Stv.mem v s) -> raise (UnboundTypeVar v)
-    | _ -> ty_fold vars () ty
-  in
-  option_iter (vars ()) def;
-  create_tysymbol name args def
-
-let rec tv_inst m ty = match ty.ty_node with
-  | Tyvar n -> Mtv.find n m
-  | _ -> ty_map (tv_inst m) ty
-
-let rec ty_freevars s ty = match ty.ty_node with
-  | Tyvar n -> Stv.add n s
-  | _ -> ty_fold ty_freevars s ty
+  let check v = Stv.mem v s || raise (UnboundTypeVar v) in
+  ignore (option_map (ty_v_all check) def);
+  mk_ts name args def
 
 let ty_app s tl =
   let tll = List.length tl in
@@ -164,7 +171,7 @@ let ty_app s tl =
     | Some ty ->
         let add m v t = Mtv.add v t m in
         let m = List.fold_left2 add Mtv.empty s.ts_args tl in
-        tv_inst m ty
+        ty_full_inst m ty
     | _ ->
         ty_app s tl
 

src/core/ty.mli

@@ -86,6 +86,13 @@ val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
 val ty_all : (ty -> bool) -> ty -> bool
 val ty_any : (ty -> bool) -> ty -> bool
 
+(** {3 variable-wise map/fold} *)
+(** visits every variable of the type *)
+val ty_v_map : (tvsymbol -> ty) -> ty -> ty
+val ty_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ty -> 'a
+val ty_v_all : (tvsymbol -> bool) -> ty -> bool
+val ty_v_any : (tvsymbol -> bool) -> ty -> bool
+
 (** {3 symbol-wise map/fold} *)
 (** visits every symbol of the type *)
 val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
@@ -98,6 +105,7 @@ exception TypeMismatch of ty * ty
 val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
 val ty_inst  : ty Mtv.t -> ty -> ty
 val ty_freevars : Stv.t -> ty -> Stv.t
+val ty_closed : ty -> bool
 
 val ty_equal_check : ty -> ty -> unit