forbid non-positive constructors in algbraic types

src/core/decl.ml

@@ -373,6 +373,8 @@ exception EmptyDecl
 exception EmptyAlgDecl of tysymbol
 exception EmptyIndDecl of lsymbol
 
+exception NonPositiveTypeDecl of tysymbol * lsymbol * tysymbol
+
 let news_id s id = Sid.add_new id (ClashIdent id) s
 
 let syms_ts s ts = Sid.add ts.ts_name s
@@ -384,7 +386,9 @@ let syms_fmla s f = f_s_fold syms_ts syms_ls s f
 
 let create_ty_decl tdl =
   if tdl = [] then raise EmptyDecl;
-  let check_constr ty (syms,news) fs =
+  let add s (ts,_) = Sts.add ts s in
+  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);
     let add s ty = match ty.ty_node with
@@ -392,12 +396,18 @@ let create_ty_decl tdl =
       | _ -> assert false
     in
     let vs = ty_fold add Stv.empty vty in
-    let rec check s ty = match ty.ty_node with
+    let rec check seen s ty = match ty.ty_node with
       | Tyvar v when Stv.mem v vs -> s
       | Tyvar v -> raise (UnboundTypeVar v)
-      | Tyapp (ts,_) -> Sid.add ts.ts_name (ty_fold check s ty)
+      | Tyapp (ts,_) ->
+          let now = Sts.mem ts tss in
+          if seen && now then
+            raise (NonPositiveTypeDecl (tys,fs,ts))
+          else
+            let s = ty_fold (check (seen || now)) s ty in
+            Sid.add ts.ts_name s
     in
-    let syms = List.fold_left check syms fs.ls_args in
+    let syms = List.fold_left (check false) syms fs.ls_args in
     syms, news_id news fs.ls_name
   in
   let check_decl (syms,news) (ts,td) = match td with
@@ -409,7 +419,7 @@ let create_ty_decl tdl =
         if ts.ts_def <> None then raise (IllegalTypeAlias ts);
         let news = news_id news ts.ts_name in
         let ty = ty_app ts (List.map ty_var ts.ts_args) in
-        List.fold_left (check_constr ty) (syms,news) cl
+        List.fold_left (check_constr ts ty) (syms,news) cl
   in
   let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
   mk_decl (Dtype tdl) syms news

src/core/decl.mli

@@ -117,6 +117,7 @@ val create_prop_decl : prop_kind -> prsymbol -> fmla -> decl
 (* exceptions *)
 
 exception IllegalTypeAlias of tysymbol
+exception NonPositiveTypeDecl of tysymbol * lsymbol * tysymbol
 
 exception InvalidIndDecl of lsymbol * prsymbol
 exception TooSpecificIndDecl of lsymbol * prsymbol * term

src/core/pretty.ml

@@ -512,6 +512,10 @@ let () = Exn_printer.register
       fprintf fmt
         "Type symbol %a is a type alias and cannot be declared as algebraic"
         print_ts ts
+  | Decl.NonPositiveTypeDecl (_ts, ls, ts1) ->
+      fprintf fmt "Constructor %a \
+          contains a non strictly positive occurrence of type symbol %a"
+        print_ls ls print_ts ts1
   | Decl.InvalidIndDecl (_ls, pr) ->
       fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
         print_pr pr
@@ -520,8 +524,7 @@ let () = Exn_printer.register
           has too type-specific conclusion %a"
         print_pr pr print_term t
   | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
-      fprintf fmt "Clause %a in inductive predicate declaration \
-          contains a negative occurrence of dependent symbol %a"
+      fprintf fmt "Clause %a contains a negative occurrence of symbol %a"
         print_pr pr print_ls ls1
   | Decl.BadLogicDecl (ls1,ls2) ->
       fprintf fmt "Ill-formed definition: symbols %a and %a are different"