feat: positivity checker seems to work; needs more testing

Author: loutr

src/ecHiInductive.ml

@@ -23,7 +23,7 @@ type dterror =
 | DTE_TypeError       of TT.tyerror
 | DTE_DuplicatedCtor  of symbol
 | DTE_InvalidCTorType of symbol * TT.tyerror
-| DTE_NonPositive
+| DTE_NonPositive     of symbol * ty
 | DTE_Empty
 
 type fxerror =
@@ -52,7 +52,7 @@ let trans_record (env : EcEnv.env) (name : ptydname) (rc : precord) =
   Msym.odup unloc (List.map fst rc) |> oiter (fun (x, y) ->
     rcerror y.pl_loc env (RCE_DuplicatedField x.pl_desc));
 
-  (* Check for emptyness *)
+  (* Check for emptiness *)
   if List.is_empty rc then
     rcerror loc env RCE_Empty;
 
@@ -106,7 +106,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
       dt |> List.map for1
   in
 
-  (* Check for emptyness *)
+  (* Check for emptiness *)
   begin
     let rec isempty_n (ctors : (ty list) list) =
       List.for_all isempty_1 ctors

src/ecHiInductive.mli

@@ -16,7 +16,7 @@ type dterror =
 | DTE_TypeError       of EcTyping.tyerror
 | DTE_DuplicatedCtor  of symbol
 | DTE_InvalidCTorType of symbol * EcTyping.tyerror
-| DTE_NonPositive
+| DTE_NonPositive     of symbol * EcTypes.ty
 | DTE_Empty
 
 type fxerror =

src/ecInductive.ml

@@ -83,10 +83,80 @@ let datatype_ind_path (mode : indmode) (p : EcPath.path) =
   EcPath.pqoname (EcPath.prefix p) name
 
 (* -------------------------------------------------------------------- *)
-exception NonPositive
-
-let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
-  let normty = odfl (identity : ty -> ty) normty in
+exception NonPositive of ty
+exception NonPositiveAbstract of EcPath.path
+exception NonPositiveParams of ty
+
+(** below, [fct] designates the function that takes a path to a type constructor
+    and returns the corresponding type declaration *)
+(** Strict positivity enforces the following, for every variant of the datatype p:
+    - for each subterm (a → b), p ∉ fv(a);
+    - inductive occurences a₁ a₂ .. aₙ p are such that ∀i. p ∉ fv(aᵢ) *)
+
+let rec occurs ?(normty = identity) p t =
+  match (normty t).ty_node with
+  | Tconstr (p', _) when EcPath.p_equal p p' -> true
+  | _ -> EcTypes.ty_sub_exists (occurs p) t
+
+let ty_params_compat =
+  List.for_all2 (fun ty (param_id, _) ->
+      match ty.ty_node with
+      | Tvar id -> EcIdent.id_equal id param_id
+      | _ -> false)
+
+let rec check_positivity_in_decl fct p decl ident =
+  let tys_to_inspect =
+    match decl.tyd_type with
+    | Concrete ty -> [ ty ]
+    | Abstract _ -> raise @@ NonPositiveAbstract p
+    | Datatype { tydt_ctors } -> List.flatten (List.map snd tydt_ctors)
+    | Record (_, tys) -> List.map snd tys
+  in
+  List.iter (check_positivity_ident fct p decl.tyd_params ident) tys_to_inspect
+
+(** Ensures all occurrences of type variable [ident] are positive in type [ty] *)
+and check_positivity_ident fct p params ident ty = match ty.ty_node with
+  | Tglob _ | Tunivar _ -> assert false
+  | Tvar _ -> ()
+  | Ttuple tys -> List.iter (check_positivity_ident fct p params ident) tys
+  | Tconstr (q, args) when EcPath.p_equal q p ->
+    if not (ty_params_compat args params) then raise @@ NonPositiveParams ty
+  | Tconstr (q, args) -> 
+      let decl = fct q in
+      List.combine args decl.tyd_params
+      |> List.filter_map
+        (fun (arg, (ident, _)) -> if EcTypes.var_mem ident arg then Some ident else None)
+      |> List.iter (check_positivity_in_decl fct q decl)
+  | Tfun (from, to_) ->
+    if EcTypes.var_mem ident from then raise @@ NonPositive ty;
+    check_positivity_ident fct p params ident to_
+
+    
+(** Ensures all occurrences of path [p] are positive in type [ty] *)
+let rec check_positivity_path fct p ty =
+  match ty.ty_node with
+  | Tglob _ | Tunivar _ -> assert false
+  | Tvar _ -> ()
+  | Ttuple tys -> List.iter (check_positivity_path fct p) tys
+  | Tconstr (q, args) when EcPath.p_equal q p ->
+      if List.exists (occurs p) args then raise (NonPositive ty)
+  | Tconstr (q, args) ->
+      let decl = fct q in
+      List.combine args decl.tyd_params
+      |> List.filter_map
+        (fun (arg, (ident, _)) -> if occurs p arg then Some ident else None)
+      |> List.iter (check_positivity_in_decl fct q decl)
+    
+  | Tfun (from, to_) ->
+      if occurs p from then raise (NonPositive ty);
+      check_positivity_path fct p to_
+
+let check_positivity fct dt =
+    let tys = List.flatten (List.map snd dt.dt_ctors) in
+    List.iter (check_positivity_path fct dt.dt_path) tys
+
+
+let indsc_of_datatype ?(normty = identity) (mode : indmode) (dt : datatype) =
   let tpath  = dt.dt_path in
 
   let rec scheme1 p (pred, fac) ty =
@@ -103,13 +173,11 @@ let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
           | scs -> Some (FL.f_let (LTuple xs) fac (FL.f_ands scs))
     end
 
-    | Tconstr (p', ts)  ->
-        if List.exists (occurs p) ts then raise NonPositive;
+    | Tconstr (p', _)  ->
         if not (EcPath.p_equal p p') then None else
           Some (FL.f_app pred [fac] tbool)
 
     | Tfun (ty1, ty2) ->
-        if occurs p ty1 then raise NonPositive;
         let x = fresh_id_of_ty ty1 in
           scheme1 p (pred, FL.f_app fac [FL.f_local x ty1] ty2) ty2
             |> omap (FL.f_forall [x, GTty ty1])
@@ -152,11 +220,6 @@ let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
     let form   = FL.f_forall [predx, GTty predty] form in
       form
 
-  and occurs p t =
-    match (normty t).ty_node with
-    | Tconstr (p', _) when EcPath.p_equal p p' -> true
-    | _ -> EcTypes.ty_sub_exists (occurs p) t
-
   in scheme mode (List.map fst dt.dt_tparams, tpath) dt.dt_ctors
 
 (* -------------------------------------------------------------------- *)

src/ecInductive.mli

@@ -21,9 +21,9 @@ type ctor  = symbol * (EcTypes.ty list)
 type ctors = ctor list
 
 type datatype = {
-  dt_path    : path;
-  dt_tparams : ty_params;
-  dt_ctors   : ctors
+  dt_path       : path;
+  dt_tparams    : ty_params;
+  dt_ctors      : ctors
 }
 
 (* -------------------------------------------------------------------- *)
@@ -43,7 +43,17 @@ val datatype_proj_name : symbol -> symbol
 val datatype_proj_path : path -> symbol -> path
 
 (* -------------------------------------------------------------------- *)
-exception NonPositive
+(** A failure raised during a strict-positivity check. The companion type
+    is the term responsible for the failure. *)
+exception NonPositive of ty
+
+(** Evaluates whether a given datatype protype satisfies the strict
+    positivity check. The first argument defines how to retrieve the
+    effective definition of a type constructor from its path.
+
+    raises the exception [NonPositive] if the check fails, otherwise
+    the function returns a unit value. *)
+val check_positivity : (path -> tydecl) -> datatype -> unit
 
 val indsc_of_datatype : ?normty:(ty -> ty) -> [`Elim|`Case] -> datatype -> form
 

src/ecScope.ml

@@ -1953,13 +1953,18 @@ module Ty = struct
         let body   = transty tp_tydecl env ue bd in
         EcUnify.UniEnv.tparams ue, Concrete body
 
-      | PTYD_Datatype dt ->
-        let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
-        let tparams, tydt =
-          try ELI.datatype_as_ty_dtype datatype
-          with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
-        in
-        tparams, Datatype tydt
+      | PTYD_Datatype dt -> (
+          let datatype = EHI.trans_datatype env (mk_loc loc (args, name)) dt in
+          (* Maybe this is not _the_ one way to build it, compare to
+             ecHiInductive.ml#L132-L134 *)
+          let ty_from_ctor ctor = EcEnv.Ty.by_path ctor env in
+          try
+            ELI.check_positivity ty_from_ctor datatype;
+            let tparams, tydt = ELI.datatype_as_ty_dtype datatype in
+            (tparams, Datatype tydt)
+          with ELI.NonPositive ty ->
+            EHI.dterror loc env
+              (EHI.DTE_NonPositive (basename datatype.dt_path, ty)))
 
       | PTYD_Record rt ->
         let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in

src/ecTypes.ml

@@ -154,6 +154,12 @@ let rec ty_check_uni t =
   | Tunivar _ -> raise FoundUnivar
   | _ -> ty_iter ty_check_uni t
 
+let rec var_mem ?(check_glob = false) id t =
+  match t.ty_node with
+  | Tvar id' -> EcIdent.id_equal id id'
+  | Tglob id' when check_glob -> EcIdent.id_equal id id'
+  | _ -> ty_sub_exists (var_mem ~check_glob id) t
+
 (* -------------------------------------------------------------------- *)
 let symbol_of_ty (ty : ty) =
   match ty.ty_node with

src/ecTypes.mli

@@ -79,6 +79,8 @@ val ty_sub_exists : (ty -> bool) -> ty -> bool
 val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
 val ty_iter : (ty -> unit) -> ty -> unit
 
+val var_mem : ?check_glob:bool -> EcIdent.t -> ty -> bool
+
 (* -------------------------------------------------------------------- *)
 val symbol_of_ty   : ty -> string
 val fresh_id_of_ty : ty -> EcIdent.t

src/ecUserMessages.ml

@@ -593,6 +593,7 @@ end = struct
 
   let pp_dterror env fmt error =
     let msg x = Format.fprintf fmt x in
+    let env1  = EcPrinting.PPEnv.ofenv env in
 
     match error with
     | DTE_TypeError ee ->
@@ -605,8 +606,9 @@ end = struct
         msg "invalid constructor type: `%s`: %a'"
           name (pp_tyerror env) ee
 
-    | DTE_NonPositive ->
-        msg "the datatype does not respect the positivity condition"
+    | DTE_NonPositive (name, ty) ->
+        msg "non strictly-positive occurrence of type `%s` in `%a`"
+          name (EcPrinting.pp_type env1) ty
 
     | DTE_Empty ->
         msg "the datatype may be empty"