feat: working stack-based pretty-printing

This commit also fixes a silly shadowing issue on one critical variable
during positivity checking.

I still need to understand clearly the behaviour of `Format` boxes, which
remain quite mysterious.

I also have to add a test file for coverage.

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     of (EcPrinting.PPEnv.t -> unit EcPrinting.pp)
+| DTE_NonPositive     of symbol * EI.non_positive_context
 | DTE_Empty
 
 type fxerror =

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     of (EcPrinting.PPEnv.t -> unit EcPrinting.pp)
+| DTE_NonPositive     of symbol * non_positive_context
 | DTE_Empty
 
 type fxerror =

src/ecInductive.ml

@@ -6,7 +6,6 @@ open EcTypes
 open EcDecl
 open EcCoreFol
 
-module PE = EcPrinting
 module EP = EcPath
 module FL = EcCoreFol
 
@@ -84,45 +83,23 @@ let datatype_ind_path (mode : indmode) (p : EcPath.path) =
   EcPath.pqoname (EcPath.prefix p) name
 
 (* -------------------------------------------------------------------- *)
-type variant = Concrete | Record of symbol | Variant of symbol
+type non_positive_intype = Concrete | Record of symbol | Variant of symbol
 
-type context =
-  | InType of variant
+type non_positive_description =
+  | InType of EcIdent.ident option * non_positive_intype
   | NonPositiveOcc of ty
   | AbstractTypeRestriction
   | TypePositionRestriction of ty
 
-exception NonPositiveCtx of (EP.path * context) list
+type non_positive_context = (symbol * non_positive_description) list
 
-exception NonPositive of (PE.PPEnv.t -> unit PE.pp)
+exception NonPositive of non_positive_context
 
-let render_context pp fmt (p, ctx) = match ctx with
-  | InType Concrete -> Format.fprintf fmt "... in type %a" PE.pp_path p
-  | InType (Record s) ->
-      Format.fprintf fmt "... in record field %s of type %a" s PE.pp_path p
-  | InType (Variant s) ->
-      Format.fprintf fmt "... in variant %s of type %a" s PE.pp_path p
-  | NonPositiveOcc ty ->
-      Format.fprintf fmt "non-positive occurrence of %a in type %a"
-        (PE.pp_type pp) ty PE.pp_path p
-  | AbstractTypeRestriction ->
-      Format.fprintf fmt "unauthorised abstract type constructor %a" PE.pp_path p
-  | TypePositionRestriction ty ->
-      Format.fprintf fmt
-        "recursive occurrence %a in the definition of %a has different \
-         arguments, which is not allowed."
-        (PE.pp_type pp) ty PE.pp_path p
+let with_context ?ident p ctx f =
+  try f () with NonPositive l -> raise (NonPositive ((EP.basename p, InType (ident, ctx)) :: l))
 
-let render_context_list p l pp fmt () =
-  Format.fprintf fmt "Could not verify strict positivity of type %a:@;@[<v 2>" PE.pp_path p;
-  Format.pp_print_list (render_context pp) fmt l;
-  Format.fprintf fmt "@;@]"
-
-
-let with_context p ctx f =
-  try f () with NonPositiveCtx l -> raise (NonPositiveCtx ((p, ctx) :: l))
-
-let non_positive p ctx = raise (NonPositiveCtx [(p, ctx)])
+let non_positive (p : EP.path) ctx = raise (NonPositive [(EP.basename p, ctx)])
+let non_positive' (s : EcIdent.ident) ctx = raise (NonPositive [(s.id_symb, ctx)])
 
 (** below, [fct] designates the function that takes a path to a type constructor
     and returns the corresponding type declaration *)
@@ -165,15 +142,15 @@ let rec check_positivity_in_decl fct p decl ident =
   and iter l f = List.iter f l in
 
   match decl.tyd_type with
-  | Concrete ty -> with_context p (InType Concrete) (check ty)
+  | Concrete ty -> with_context ~ident p Concrete (check ty)
   | Abstract _ -> non_positive p AbstractTypeRestriction
   | Datatype { tydt_ctors } ->
       iter tydt_ctors @@ fun (name, argty) ->
       iter argty @@ fun ty ->
-      with_context p (InType (Variant name)) (check ty)
+      with_context ~ident p (Variant name) (check ty)
   | Record (_, tys) ->
       iter tys @@ fun (name, ty) -> 
-      with_context p (InType (Record name)) (check ty)
+      with_context ~ident p (Record name) (check ty)
 
 (** Ensures all occurrences of type variable [ident] are positive in type [ty] *)
 and check_positivity_ident fct p params ident ty =
@@ -186,17 +163,17 @@ and check_positivity_ident fct p params ident 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.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 non_positive p (NonPositiveOcc ty);
+      if EcTypes.var_mem ident from then non_positive' ident (NonPositiveOcc 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 _  | Tvar _ -> ()
+  | Tglob _ | Tunivar _ | 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 non_positive p (NonPositiveOcc ty)
@@ -211,10 +188,11 @@ let rec check_positivity_path fct p ty =
       check_positivity_path fct p to_
 
 let check_positivity fct dt =
-  let tys = List.flatten (List.map snd dt.dt_ctors) in
-  try List.iter (check_positivity_path fct dt.dt_path) tys
-  with NonPositiveCtx l ->
-    raise (NonPositive (render_context_list dt.dt_path l))
+  let check ty () = check_positivity_path fct dt.dt_path ty
+  and iter l f = List.iter f l in
+  iter dt.dt_ctors @@ fun (name, argty) ->
+  iter argty @@ fun ty ->
+  with_context dt.dt_path (Variant name) (check ty)
 
 let indsc_of_datatype ?(normty = identity) (mode : indmode) (dt : datatype) =
   let tpath  = dt.dt_path in

src/ecInductive.mli

@@ -43,7 +43,17 @@ val datatype_proj_name : symbol -> symbol
 val datatype_proj_path : path -> symbol -> path
 
 (* -------------------------------------------------------------------- *)
-exception NonPositive of (EcPrinting.PPEnv.t -> unit EcPrinting.pp)
+type non_positive_intype = Concrete | Record of symbol | Variant of symbol
+
+type non_positive_description =
+  | InType of EcIdent.ident option * non_positive_intype
+  | NonPositiveOcc of ty
+  | AbstractTypeRestriction
+  | TypePositionRestriction of ty
+
+type non_positive_context = (symbol * non_positive_description) list
+
+exception NonPositive of non_positive_context
 
 val check_positivity : (path -> tydecl) -> datatype -> unit
 (** Evaluates whether a given datatype protype satisfies the strict

src/ecScope.ml

@@ -2255,8 +2255,9 @@ module Ty = struct
             ELI.check_positivity ty_from_ctor datatype;
             let tparams, tydt = ELI.datatype_as_ty_dtype datatype in
             (tparams, Datatype tydt)
-          with ELI.NonPositive f ->
-            EHI.dterror loc env (EHI.DTE_NonPositive f))
+          with ELI.NonPositive ctx ->
+            let symbol = basename datatype.dt_path in
+            EHI.dterror loc env (EHI.DTE_NonPositive (symbol, ctx)))
 
       | PTYD_Record rt ->
         let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in

src/ecUserMessages.ml

@@ -573,6 +573,7 @@ module InductiveError : sig
   val pp_fxerror : env -> Format.formatter -> fxerror -> unit
 end = struct
   open EcHiInductive
+  open EcInductive
   open TypingError
 
   let pp_rcerror env fmt error =
@@ -591,6 +592,35 @@ end = struct
     | RCE_Empty ->
         msg "this record type is empty"
 
+  let format_intype fmt p (tyvar, ctx) =
+    (match ctx with
+    | Concrete -> Format.fprintf fmt "... in type %s" p
+    | Record s -> Format.fprintf fmt "... in record field %s of type %s" s p
+    | Variant s -> Format.fprintf fmt "... in variant %s of type %s" s p);
+    let subty tyvar =
+      Format.fprintf fmt " (in an instance of type variable %a)"
+        EcIdent.pp_ident tyvar
+    in
+    Option.iter subty tyvar
+
+let format_context pp fmt (p, ctx) = match ctx with
+  | InType (tyvar, ctx) -> format_intype fmt p (tyvar, ctx)
+  | NonPositiveOcc ty ->
+      Format.fprintf fmt "non-positive occurrence of %s in type %a"
+        p (EcPrinting.pp_type pp) ty
+  | AbstractTypeRestriction ->
+      Format.fprintf fmt "unauthorised abstract type constructor %s" p
+  | TypePositionRestriction ty ->
+      Format.fprintf fmt
+        "recursive occurrence %a in the definition of %s has different \
+         arguments, which is not allowed."
+        (EcPrinting.pp_type pp) ty p
+
+let format_context_list p l pp fmt =
+  Format.fprintf fmt "Could not verify strict positivity of type %s:@.@;<0 2>@[<v>" p;
+  Format.pp_print_list (format_context pp) fmt l;
+  Format.fprintf fmt "@;@]"
+
   let pp_dterror env fmt error =
     let msg x = Format.fprintf fmt x in
     let env1  = EcPrinting.PPEnv.ofenv env in
@@ -609,7 +639,7 @@ end = struct
     | DTE_Empty ->
         msg "the datatype may be empty"
 
-    | DTE_NonPositive f -> f env1 fmt ()
+    | DTE_NonPositive (s, ctx) -> format_context_list s ctx env1 fmt
 
   let pp_fxerror env fmt error =
     match error with