Skip to content

Positivity check in type constructors #811

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

Positivity check in type constructors #811

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
10c2378
style: use regular datatype for ty_body
loutr Sep 25, 2025
3ca2ce0
feat: positivity checker seems to work; needs more testing
loutr Sep 19, 2025
547c7c5
feat: manage error messages, some more documentation for the new func…
loutr Sep 26, 2025
d1f0eff
fix: correct spelling of 'instantiate'
loutr Sep 26, 2025
ef9b4ed
wip!
loutr Oct 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ecCoreSubst.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion src/ecCoreSubst.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
37 changes: 19 additions & 18 deletions src/ecDecl.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,36 +15,37 @@ 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 ty_dtype = {
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) 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 EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list


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 EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
]

and ty_dtype = {
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
tydt_schelim : EcCoreFol.form;
tydt_schcase : EcCoreFol.form;
}

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 =
Expand All @@ -59,10 +60,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

Expand Down
28 changes: 14 additions & 14 deletions src/ecDecl.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,33 +11,33 @@ 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 ty_dtype = {
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) 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 EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list


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 form * (EcSymbols.symbol * EcTypes.ty) list
]

and ty_dtype = {
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
tydt_schelim : form;
tydt_schcase : form;
}

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
Expand Down
27 changes: 14 additions & 13 deletions src/ecEnv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -776,10 +776,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
Expand Down Expand Up @@ -823,7 +823,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 =
Expand Down Expand Up @@ -2513,12 +2513,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
Expand Down Expand Up @@ -2554,14 +2554,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
Expand All @@ -2577,7 +2578,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
Expand Down Expand Up @@ -2783,7 +2784,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
Expand Down Expand Up @@ -2903,7 +2904,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))
Expand Down
2 changes: 1 addition & 1 deletion src/ecEnv.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,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

(* -------------------------------------------------------------------- *)
Expand Down
2 changes: 1 addition & 1 deletion src/ecFol.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,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

Expand Down
18 changes: 9 additions & 9 deletions src/ecHiInductive.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.nonpositive_description
| DTE_Empty

type fxerror =
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -132,19 +132,19 @@ 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
fun ty -> ty_instantiate tdecl.tyd_params targs ty in

match tdecl.tyd_type with
| `Abstract _ ->
| Abstract _ ->
List.exists isempty (targs)

| `Concrete ty ->
| Concrete ty ->
isempty_1 [tyinst () ty]

| `Record (_, fields) ->
| Record (_, fields) ->
isempty_1 (List.map (tyinst () |- snd) fields)

| `Datatype dt ->
| Datatype dt ->
isempty_n (List.map (List.map (tyinst ()) |- snd) dt.tydt_ctors)

in
Expand Down
2 changes: 1 addition & 1 deletion src/ecHiInductive.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 * EcInductive.nonpositive_description
| DTE_Empty

type fxerror =
Expand Down
Loading
Loading