check inductive definitions

src/core/theory.ml

@@ -270,7 +270,7 @@ exception ConstructorExpected of lsymbol
 exception UnboundTypeVar of ident
 exception IllegalTypeAlias of tysymbol
 exception ClashIdent of ident
-exception BadDecl of ident
+exception BadLogicDecl of ident
 exception EmptyDecl
 
 let add_id s id =
@@ -309,19 +309,59 @@ let create_logic_decl ldl =
   if ldl = [] then raise EmptyDecl;
   let check_decl acc = function
     | Lfunction  (fs, Some (s,_,_,_)) when s != fs ->
-        raise (BadDecl fs.ls_name)
+        raise (BadLogicDecl fs.ls_name)
     | Lpredicate (ps, Some (s,_,_,_)) when s != ps ->
-        raise (BadDecl ps.ls_name)
+        raise (BadLogicDecl ps.ls_name)
     | Lfunction  (fs, _) -> add_id acc fs.ls_name
     | Lpredicate (ps, _) -> add_id acc ps.ls_name
   in
   ignore (List.fold_left check_decl Sid.empty ldl);
   create_logic_decl ldl
 
+exception InvalidIndDecl of ident * ident
+exception TooSpecificIndDecl of ident * ident * term
+exception NonPositiveIndDecl of ident * ident * lsymbol
+
+exception Found of lsymbol
+let ls_mem s sps = if Sls.mem s sps then raise (Found s) else false
+let t_pos_ps sps = t_s_all (fun _ -> true) (fun s -> not (ls_mem s sps))
+
+let rec f_pos_ps sps pol f = match f.f_node, pol with
+  | Fapp (s, _), Some false when ls_mem s sps -> false
+  | Fapp (s, _), None when ls_mem s sps -> false
+  | Fbinop (Fiff, f, g), _ ->
+      f_pos_ps sps None f && f_pos_ps sps None g
+  | Fbinop (Fimplies, f, g), _ ->
+      f_pos_ps sps (option_map not pol) f && f_pos_ps sps pol g
+  | Fnot f, _ ->
+      f_pos_ps sps (option_map not pol) f
+  | Fif (f,g,h), _ ->
+      f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
+  | _ -> f_all (t_pos_ps sps) (f_pos_ps sps pol) f
+
 let create_ind_decl idl =
   if idl = [] then raise EmptyDecl;
+  let add acc (ps,_) = Sls.add ps acc in
+  let sps = List.fold_left add Sls.empty idl in
   let check_ax ps acc pr =
-    add_id acc pr.pr_name
+    let _, f = f_open_forall pr.pr_fmla in
+    let rec clause acc f = match f.f_node with
+      | Fbinop (Fimplies, g, f) -> clause (g::acc) f
+      | _ -> (acc, f)
+    in
+    let cls, f = clause [] f in
+    match f.f_node with
+      | Fapp (s, tl) when s == ps ->
+          let tymatch sb t ty =
+            try Ty.matching sb (t.t_ty) ty with TypeMismatch ->
+              raise (TooSpecificIndDecl (ps.ls_name, pr.pr_name, t))
+          in
+          ignore (List.fold_left2 tymatch Mid.empty tl ps.ls_args);
+          (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
+          with Found ls ->
+            raise (NonPositiveIndDecl (ps.ls_name, pr.pr_name, ls)));
+          add_id acc pr.pr_name
+      | _ -> raise (InvalidIndDecl (ps.ls_name, pr.pr_name))
   in
   let check_decl acc (ps,al) =
     List.fold_left (check_ax ps) (add_id acc ps.ls_name) al

src/core/theory.mli

@@ -141,10 +141,14 @@ exception ConstructorExpected of lsymbol
 exception IllegalTypeAlias of tysymbol
 exception UnboundTypeVar of ident
 
+exception InvalidIndDecl of ident * ident
+exception TooSpecificIndDecl of ident * ident * term
+exception NonPositiveIndDecl of ident * ident * lsymbol
+
 exception IllegalConstructor of lsymbol
+exception BadLogicDecl of ident
 exception UnboundVars of Svs.t
 exception ClashIdent of ident
-exception BadDecl of ident
 exception EmptyDecl
 
 (** Environements *)

src/parser/parser.mly

@@ -340,7 +340,7 @@ indcases:
 ;
 
 indcase:
-| uident COLON lexpr { ($1,$3) }
+| uident COLON lexpr { (loc (),$1,$3) }
 ;
 
 primitive_type:

src/parser/ptree.mli

@@ -123,7 +123,7 @@ type ind_decl = {
   in_loc    : loc;
   in_ident  : ident;
   in_params : pty list;
-  in_def    : (ident * lexpr) list;
+  in_def    : (loc * ident * lexpr) list;
 }
 
 type prop_kind =

src/parser/typing.ml

@@ -755,7 +755,7 @@ let add_types dl th =
 	     i)
 	  d.td_params 
       in
-      let id = id_user id d.td_ident.id_loc in
+      let id = id_user id d.td_loc in
       let ts = match d.td_def with
 	| TDalias ty -> 
 	    let rec apply = function
@@ -811,7 +811,7 @@ let add_types dl th =
 	  let constructor (loc, id, pl) = 
 	    let param (_, t) = ty_of_dty (dty th' t) in
 	    let tyl = List.map param pl in
-	    create_fconstr (id_user id.id id.id_loc) tyl ty
+	    create_fconstr (id_user id.id loc) tyl ty
 	  in
 	  Talgebraic (List.map constructor cl)
     in
@@ -833,7 +833,7 @@ let add_logics dl th =
     let id = d.ld_ident.id in
     if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls 
       then error ~loc:d.ld_loc (Clash id);
-    let v = id_user id d.ld_ident.id_loc in
+    let v = id_user id d.ld_loc in
     let denv = create_denv th in
     Hashtbl.add denvs id denv;
     let type_ty (_,t) = ty_of_dty (dty denv t) in
@@ -921,6 +921,7 @@ let add_prop k loc s f th =
   with ClashSymbol _ ->
     error ~loc (Clash s.id)
 
+(*
 (** [check_clausal_form loc ps f] checks whether the formula [f] 
     has a valid clausal form 
       \forall x_1,.., x_k. P1 -> ... -> P_n -> P
@@ -987,6 +988,11 @@ let rec check_clausal_form loc ps f = match f.f_node with
       check_clausal_form loc ps f
   | _ -> 
       check_unquantified_clausal_form loc ps f
+*)
+
+let loc_of_id id = match id.id_origin with
+  | User loc -> loc
+  | _ -> assert false
 
 let add_inductives dl th =
   let ns = get_namespace th in
@@ -996,7 +1002,7 @@ let add_inductives dl th =
     let id = d.in_ident.id in
     if Hashtbl.mem psymbols id || Mnm.mem id ns.ns_ls 
       then error ~loc:d.in_loc (Clash id);
-    let v = id_user id d.in_ident.id_loc in
+    let v = id_user id d.in_loc in
     let denv = create_denv th in
     let type_ty t = ty_of_dty (dty denv t) in
     let pl = List.map type_ty d.in_params in
@@ -1009,16 +1015,21 @@ let add_inductives dl th =
   let type_decl d = 
     let id = d.in_ident.id in
     let ps = Hashtbl.find psymbols id in
-    let clause (id, f) = 
-      let loc = f.pp_loc in
-      let f' = fmla th' f in
-      check_clausal_form loc ps f';
-      create_prop (id_user id.id id.id_loc) f'
+    let clause (loc, id, f) = 
+      create_prop (id_user id.id loc) (fmla th' f)
     in
     ps, List.map clause d.in_def
   in
   let dl = List.map type_decl dl in
-  List.fold_left add_decl th (create_ind_decls dl)
+  try
+    List.fold_left add_decl th (create_ind_decls dl)
+  with
+  | InvalidIndDecl (_,prid) -> errorm ~loc:(loc_of_id prid)
+      "not a clausal form"
+  | NonPositiveIndDecl (_,prid,s) -> errorm ~loc:(loc_of_id prid)
+      "non-positive occurrence of %a" Pretty.print_ls s
+  | TooSpecificIndDecl (_,prid,t) -> errorm ~loc:(loc_of_id prid)
+      "term @[%a@] is too specific" Pretty.print_term t
 
 (* parse file and store all theories into parsed_theories *)