feat: new strict-positivity checking for datatypes

style: use regular datatype for ty_body

fix: correct spelling of 'instantiate'

The spelling 'instanciate' is only acknowledged in the Wiktionary, while
all other dictionaries prefer the spelling with a 't'.

ex.: https://dictionary.cambridge.org/dictionary/english/instantiate

feat: working stack-based pretty-printing, with extended capacities

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.

fix: perform positivity check in type arguments of type constructors

test: add a simple test file for positivity checking.

Author: loutr

src/ecCoreSubst.ml

@@ -14,7 +14,7 @@ type mod_extra = {
   mex_glob  : memory -> form;
 }
 
-type sc_instanciate = {
+type sc_instantiate = {
   sc_memtype : memtype;
   sc_mempred : mem_pr Mid.t;
   sc_expr    : expr Mid.t;

src/ecCoreSubst.mli

@@ -8,7 +8,7 @@ open EcCoreModules
 open EcCoreFol
 
 (* -------------------------------------------------------------------- *)
-type sc_instanciate = {
+type sc_instantiate = {
   sc_memtype : memtype;
   sc_mempred : mem_pr Mid.t;
   sc_expr    : expr Mid.t;

src/ecDecl.ml

@@ -15,42 +15,42 @@ type ty_param  = EcIdent.t * EcPath.Sp.t
 type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
-type tydecl = {
-  tyd_params : ty_params;
-  tyd_type   : ty_body;
-  tyd_loca   : locality;
-}
-
-and ty_body = [
-  | `Concrete of EcTypes.ty
-  | `Abstract of Sp.t
-  | `Datatype of ty_dtype
-  | `Record   of ty_record
-]
-
-and ty_record =
+type ty_record =
   EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
 
-and ty_dtype_ctor =
+type ty_dtype_ctor =
   EcSymbols.symbol * EcTypes.ty list
 
-and ty_dtype = {
+type ty_dtype = {
   tydt_ctors   : ty_dtype_ctor list;
   tydt_schelim : EcCoreFol.form;
   tydt_schcase : EcCoreFol.form;
 }
 
+type ty_body = 
+  | Concrete of EcTypes.ty
+  | Abstract of Sp.t
+  | Datatype of ty_dtype
+  | Record   of ty_record
+
+
+type tydecl = {
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
+}
+
 let tydecl_as_concrete (td : tydecl) =
-  match td.tyd_type with `Concrete x -> Some x | _ -> None
+  match td.tyd_type with Concrete x -> Some x | _ -> None
 
 let tydecl_as_abstract (td : tydecl) =
-  match td.tyd_type with `Abstract x -> Some x | _ -> None
+  match td.tyd_type with Abstract x -> Some x | _ -> None
 
 let tydecl_as_datatype (td : tydecl) =
-  match td.tyd_type with `Datatype x -> Some x | _ -> None
+  match td.tyd_type with Datatype x -> Some x | _ -> None
 
 let tydecl_as_record (td : tydecl) =
-  match td.tyd_type with `Record x -> Some x | _ -> None
+  match td.tyd_type with Record (x, y) -> Some (x, y) | _ -> None
 
 (* -------------------------------------------------------------------- *)
 let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
@@ -65,10 +65,10 @@ let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }
+  { tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; }
 
 (* -------------------------------------------------------------------- *)
-let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =
+let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) =
   let subst = CS.Tvar.init (List.map fst params) args in
   CS.Tvar.subst subst ty
 

src/ecDecl.mli

@@ -11,39 +11,39 @@ type ty_param  = EcIdent.t * EcPath.Sp.t
 type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
-type tydecl = {
-  tyd_params : ty_params;
-  tyd_type   : ty_body;
-  tyd_loca   : locality;
-}
-
-and ty_body = [
-  | `Concrete of EcTypes.ty
-  | `Abstract of Sp.t
-  | `Datatype of ty_dtype
-  | `Record   of ty_record
-]
-
-and ty_record =
+type ty_record =
   EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
 
-and ty_dtype_ctor =
+type ty_dtype_ctor =
   EcSymbols.symbol * EcTypes.ty list
 
-and ty_dtype = {
+type ty_dtype = {
   tydt_ctors   : ty_dtype_ctor list;
   tydt_schelim : EcCoreFol.form;
   tydt_schcase : EcCoreFol.form;
 }
 
+type ty_body = 
+  | Concrete of EcTypes.ty
+  | Abstract of Sp.t
+  | Datatype of ty_dtype
+  | Record   of ty_record
+
+
+type tydecl = {
+  tyd_params : ty_params;
+  tyd_type   : ty_body;
+  tyd_loca   : locality;
+}
+
 val tydecl_as_concrete : tydecl -> EcTypes.ty option
 val tydecl_as_abstract : tydecl -> Sp.t option
 val tydecl_as_datatype : tydecl -> ty_dtype option
 val tydecl_as_record   : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) option
 
 val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
 
-val ty_instanciate : ty_params -> ty list -> ty -> ty
+val ty_instantiate : ty_params -> ty list -> ty -> ty
 
 (* -------------------------------------------------------------------- *)
 type locals = EcIdent.t list

src/ecEnv.ml

@@ -781,10 +781,10 @@ module MC = struct
       let loca    = tyd.tyd_loca in
 
       match tyd.tyd_type with
-      | `Concrete _  -> mc
-      | `Abstract _ -> mc
+      | Concrete _  -> mc
+      | Abstract _ -> mc
 
-      | `Datatype dtype ->
+      | Datatype dtype ->
           let cs      = dtype.tydt_ctors   in
           let schelim = dtype.tydt_schelim in
           let schcase = dtype.tydt_schcase in
@@ -828,7 +828,7 @@ module MC = struct
               _up_operator candup mc name (ipath name, op)
             ) mc projs
 
-      | `Record (scheme, fields) ->
+      | Record (scheme, fields) ->
           let params  = List.map (fun (x, _) -> tvar x) tyd.tyd_params in
           let nfields = List.length fields in
           let cfields =
@@ -2544,12 +2544,12 @@ module Ty = struct
 
   let defined (name : EcPath.path) (env : env) =
     match by_path_opt name env with
-    | Some { tyd_type = `Concrete _ } -> true
+    | Some { tyd_type = Concrete _ } -> true
     | _ -> false
 
   let unfold (name : EcPath.path) (args : EcTypes.ty list) (env : env) =
     match by_path_opt name env with
-    | Some ({ tyd_type = `Concrete body } as tyd) ->
+    | Some ({ tyd_type = Concrete body } as tyd) ->
         Tvar.subst
           (Tvar.init (List.map fst tyd.tyd_params) args)
           body
@@ -2585,14 +2585,15 @@ module Ty = struct
       match ty.ty_node with
       | Tconstr (p, tys) -> begin
           match by_path_opt p env with
-          | Some ({ tyd_type = (`Datatype _ | `Record _) as body }) ->
+          | Some ({ tyd_type = (Datatype _ | Record _) as body }) ->
               let prefix   = EcPath.prefix   p in
               let basename = EcPath.basename p in
               let basename =
                 match body, mode with
-                | `Record   _, (`Ind | `Case) -> basename ^ "_ind"
-                | `Datatype _, `Ind           -> basename ^ "_ind"
-                | `Datatype _, `Case          -> basename ^ "_case"
+                | Record   _, (`Ind | `Case) -> basename ^ "_ind"
+                | Datatype _, `Ind           -> basename ^ "_ind"
+                | Datatype _, `Case          -> basename ^ "_case"
+                | _, _ -> assert false
               in
                 Some (EcPath.pqoname prefix basename, tys)
           | _ -> None
@@ -2608,7 +2609,7 @@ module Ty = struct
     let env = MC.bind_tydecl name ty env in
 
     match ty.tyd_type with
-    | `Abstract tc ->
+    | Abstract tc ->
         let myty =
           let myp = EcPath.pqname (root env) name in
           let typ = List.map (fst_map EcIdent.fresh) ty.tyd_params in
@@ -2814,7 +2815,7 @@ module Ax = struct
   let rebind name ax env =
     MC.bind_axiom name ax env
 
-  let instanciate p tys env =
+  let instantiate p tys env =
     match by_path_opt p env with
     | Some ({ ax_spec = f } as ax) ->
         Tvar.f_subst ~freshen:true (List.map fst ax.ax_tparams) tys f
@@ -2934,7 +2935,7 @@ module Theory = struct
 
     | Th_type (x, tyd) -> begin
         match tyd.tyd_type with
-        | `Abstract tc ->
+        | Abstract tc ->
             let myty =
               let typ = List.map (fst_map EcIdent.fresh) tyd.tyd_params in
                 (typ, EcTypes.tconstr (xpath x) (List.map (tvar |- fst) typ))

src/ecEnv.mli

@@ -168,7 +168,7 @@ module Ax : sig
   val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
   val all  : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
 
-  val instanciate : path -> EcTypes.ty list -> env -> form
+  val instantiate : path -> EcTypes.ty list -> env -> form
 end
 
 (* -------------------------------------------------------------------- *)

src/ecFol.mli

@@ -116,7 +116,7 @@ val f_ty_app : EcEnv.env -> form -> form list -> form
 
 (* -------------------------------------------------------------------- *)
 (* WARNING : this function should be use only in a context ensuring
- * that the quantified variables can be instanciated *)
+ * that the quantified variables can be instantiated *)
 
 val f_betared : form -> form
 

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 * EI.non_positive_context
 | 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;
 
@@ -84,7 +84,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
   let env0  =
     let myself = {
       tyd_params  = EcUnify.UniEnv.tparams ue;
-      tyd_type    = `Abstract EcPath.Sp.empty;
+      tyd_type    = Abstract EcPath.Sp.empty;
       tyd_loca    = lc;
     } in
       EcEnv.Ty.bind (unloc name) myself env
@@ -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
@@ -131,21 +131,24 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
 
       let tdecl = EcEnv.Ty.by_path_opt tname env0
         |> odfl (EcDecl.abs_tydecl ~params:(`Named tparams) lc) in
-      let tyinst () =
-        fun ty -> ty_instanciate tdecl.tyd_params targs ty in
+      let tyinst = ty_instantiate tdecl.tyd_params targs in
 
       match tdecl.tyd_type with
-      | `Abstract _ ->
-          List.exists isempty (targs)
+      | Abstract _ ->
+          List.exists isempty targs
 
-      | `Concrete ty ->
-          isempty_1 [tyinst () ty]
+      | Concrete ty ->
+          isempty_1 [ tyinst ty ]
 
-      | `Record (_, fields) ->
-          isempty_1 (List.map (tyinst () |- snd) fields)
+      | Record (_, fields) ->
+          isempty_1 (List.map (tyinst |- snd) fields)
 
-      | `Datatype dt ->
-          isempty_n (List.map (List.map (tyinst ()) |- snd) dt.tydt_ctors)
+      | Datatype dt ->
+          (* FIXME: Inspecting all constructors recursively causes
+             non-termination in some cases. One can have the same
+             limitation as is done for positivity in order to limit this
+             unfolding to well-behaved cases. *)
+          isempty_n (List.map (List.map tyinst |- snd) dt.tydt_ctors)
 
     in
 

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 * non_positive_context
 | DTE_Empty
 
 type fxerror =