feat: positivity checker seems to work; needs more testing

Author: loutr

src/ecDecl.ml

@@ -30,7 +30,6 @@ type ty_body =
 
 type tydecl = {
   tyd_params : ty_params;
-  (* tyd_positivity : bool list; *)
   tyd_type   : ty_body;
   tyd_loca   : locality;
 }

src/ecInductive.ml

@@ -66,7 +66,7 @@ type ctors = ctor list
 
 type datatype = {
   dt_path    : EcPath.path;
-  dt_tparams : (ty_param * bool) list;
+  dt_tparams : ty_params;
   dt_ctors   : ctors
 }
 
@@ -84,48 +84,76 @@ let datatype_ind_path (mode : indmode) (p : EcPath.path) =
 
 (* -------------------------------------------------------------------- *)
 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
 
-(** below, [fct] designates the function that takes a path to a type constructor
-    and returns the corresponding type declaration *)
+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
 
-(** Strict positivity enforces the following, for every variant of the datatype p:
-    - for each subterm (a → b), p ∉ fv(a);
-    - recursive occurences a₁ a₂ .. aₙ p are such that ∀i. p ∉ fv(aᵢ) *)
-
-let rec check_positivity_dt fct p ty (q, args) =
-  let tydecl = fct q in
-  let inst = EcDecl.ty_instanciate tydecl.tyd_params args in
-  match tydecl.tyd_type with
-  | Abstract _ -> ()
-  | Concrete ty' -> check_positivity_ty fct p ty ty'
-  | Record (_, fields) ->
-      List.iter (check_positivity_ty fct p ty) (List.map (inst |- snd) fields)
-  | Datatype dt -> check_positivity_ctors fct p inst ty dt.tydt_ctors
-
-and check_positivity_ctors fct p inst ty =
-  List.iter (fun (_variant, parameters) ->
-      List.iter (check_positivity_ty fct p ty) (List.map inst parameters))
-
-and check_positivity_ty fct p ty traversed_ty =
-  match traversed_ty.ty_node with
+(** 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_ty fct p ty) tys
+  | Ttuple tys -> List.iter (check_positivity_path fct p) tys
   | Tconstr (q, args) when EcPath.p_equal q p ->
-      if List.exists (fun ty -> occurs p ty) args then
-        raise (NonPositive traversed_ty)
-  | Tconstr (q, args) -> check_positivity_dt fct p ty (q, args)
+      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 ty from then raise (NonPositive traversed_ty);
-      check_positivity_ty fct p ty to_
+      if occurs p from then raise (NonPositive ty);
+      check_positivity_path fct p to_
 
 let check_positivity fct dt =
-    check_positivity_ctors fct dt.dt_path identity dt.dt_path dt.dt_ctors
+    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) =
@@ -192,7 +220,7 @@ let indsc_of_datatype ?(normty = identity) (mode : indmode) (dt : datatype) =
     let form   = FL.f_forall [predx, GTty predty] form in
       form
 
-  in scheme mode (List.map (fst |- fst) dt.dt_tparams, tpath) dt.dt_ctors
+  in scheme mode (List.map fst dt.dt_tparams, tpath) dt.dt_ctors
 
 (* -------------------------------------------------------------------- *)
 let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) =
@@ -229,7 +257,7 @@ let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) =
 let datatype_as_ty_dtype datatype =
   let indsc    = indsc_of_datatype `Elim datatype in
   let casesc   = indsc_of_datatype `Case datatype in
-  List.map fst datatype.dt_tparams,
+  datatype.dt_tparams,
     { tydt_ctors   = datatype.dt_ctors ;
       tydt_schcase = casesc;
       tydt_schelim = indsc ; }

src/ecInductive.mli

@@ -22,8 +22,7 @@ type ctors = ctor list
 
 type datatype = {
   dt_path       : path;
-  dt_tparams    : (ty_param * bool) list;
-  dt_positivity : bool array;
+  dt_tparams    : ty_params;
   dt_ctors      : ctors
 }
 

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