diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index 7e0253c63..aeeeabad1 100644 --- a/src/ecCoreSubst.ml +++ b/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; diff --git a/src/ecCoreSubst.mli b/src/ecCoreSubst.mli index 80531ef9c..f829b8d38 100644 --- a/src/ecCoreSubst.mli +++ b/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; diff --git a/src/ecDecl.ml b/src/ecDecl.ml index c22745a78..f8fa4f62f 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -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 = @@ -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 diff --git a/src/ecDecl.mli b/src/ecDecl.mli index 6bde7e114..27f87acd1 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -11,25 +11,25 @@ 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 @@ -37,7 +37,7 @@ val tydecl_as_record : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) 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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index c663f5ba9..31bf5049b 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -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 @@ -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 = @@ -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 @@ -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 @@ -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 @@ -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 @@ -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)) diff --git a/src/ecEnv.mli b/src/ecEnv.mli index b5c51c9f9..78f5b6fab 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -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 (* -------------------------------------------------------------------- *) diff --git a/src/ecFol.mli b/src/ecFol.mli index 403224fe8..0b3ac3e5a 100644 --- a/src/ecFol.mli +++ b/src/ecFol.mli @@ -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 diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml index a51dede08..26c2f5eb0 100644 --- a/src/ecHiInductive.ml +++ b/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.nonpositive_description | 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 @@ -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 diff --git a/src/ecHiInductive.mli b/src/ecHiInductive.mli index 32fd11645..c2796b33e 100644 --- a/src/ecHiInductive.mli +++ b/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 * EcInductive.nonpositive_description | DTE_Empty type fxerror = diff --git a/src/ecInductive.ml b/src/ecInductive.ml index a873688f4..36b6ae480 100644 --- a/src/ecInductive.ml +++ b/src/ecInductive.ml @@ -83,10 +83,90 @@ 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 +type nonpositive_description = + | NonPositive of ty + | AbstractTypeRestriction of EcPath.path + | TypePositionRestriction of ty + +exception NonPositive of nonpositive_description + +(** 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ᵢ) + + Crucially, this has to be checked whenever p occurs in an instance of + another type constructor. *) + +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 + +(** Tests whether the first list is a list of type variables, matching the + identifiers of the second list. *) +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) + +(** Ensures all occurrences of type variable [ident] are positive in type + declaration [decl] (with name [p]) *) +let rec check_positivity_in_decl fct p decl ident = + let tys_to_inspect = + match decl.tyd_type with + | Concrete ty -> [ ty ] + | Abstract _ -> + raise (NonPositive (AbstractTypeRestriction 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 _ | 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 (NonPositive (TypePositionRestriction 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 (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 (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 (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 +183,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 +230,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 (* -------------------------------------------------------------------- *) diff --git a/src/ecInductive.mli b/src/ecInductive.mli index 2b1c5a97c..68757fe4f 100644 --- a/src/ecInductive.mli +++ b/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,21 @@ val datatype_proj_name : symbol -> symbol val datatype_proj_path : path -> symbol -> path (* -------------------------------------------------------------------- *) -exception NonPositive +type nonpositive_description = + | NonPositive of ty + | AbstractTypeRestriction of EcPath.path + | TypePositionRestriction of ty + +(** A failure raised during a strict-positivity check. *) +exception NonPositive of nonpositive_description + +(** 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 diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 6643c8e3c..8447c6c71 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -138,7 +138,7 @@ module LowApply = struct | PTGlobal (p, tys) -> (* FIXME: poor API ==> poor error recovery *) let env = LDecl.toenv (hyps_of_ckenv tc) in - (pt, EcEnv.Ax.instanciate p tys env, subgoals) + (pt, EcEnv.Ax.instantiate p tys env, subgoals) | PTTerm pt -> let pt, ax, subgoals = check_ `Elim pt subgoals tc in diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 5d06b827b..6dda628e0 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -879,7 +879,7 @@ let f_match opts hyps (ue, ev) f1 f2 = raise MatchFailure; let clue = try EcUnify.UniEnv.close ue - with EcUnify.UninstanciateUni -> raise MatchFailure + with EcUnify.UninstantiateUni -> raise MatchFailure in (ue, clue, ev) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index f7da6ecd6..d317edd65 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1272,7 +1272,7 @@ let pp_opapp let recp = EcDecl.operator_as_rcrd op in match EcEnv.Ty.by_path_opt recp env with - | Some { tyd_type = `Record (_, fields) } + | Some { tyd_type = Record (_, fields) } when List.length fields = List.length es -> begin let wmap = @@ -2242,12 +2242,12 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) = and pp_body fmt = match tyd.tyd_type with - | `Abstract _ -> () (* FIXME: TC HOOK *) + | Abstract _ -> () (* FIXME: TC HOOK *) - | `Concrete ty -> + | Concrete ty -> Format.fprintf fmt " =@ %a" (pp_type ppe) ty - | `Datatype { tydt_ctors = cs } -> + | Datatype { tydt_ctors = cs } -> let pp_ctor fmt (c, cty) = match cty with | [] -> @@ -2258,7 +2258,7 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) = in Format.fprintf fmt " =@ [@[%a@]]" (pp_list " |@ " pp_ctor) cs - | `Record (_, fields) -> + | Record (_, fields) -> let pp_field fmt (f, fty) = Format.fprintf fmt "%s: @[%a@]" f (pp_type ppe) fty in diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index 7f3c3d0e1..0f1a19d11 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -193,7 +193,7 @@ let pt_of_hyp_r ptenv x = (* -------------------------------------------------------------------- *) let pt_of_global pf hyps p tys = let ptenv = ptenv_of_penv hyps pf in - let ax = EcEnv.Ax.instanciate p tys (LDecl.toenv hyps) in + let ax = EcEnv.Ax.instantiate p tys (LDecl.toenv hyps) in { ptev_env = ptenv; ptev_pt = ptglobal ~tys p; @@ -202,7 +202,7 @@ let pt_of_global pf hyps p tys = (* -------------------------------------------------------------------- *) let pt_of_global_r ptenv p tys = let env = LDecl.toenv ptenv.pte_hy in - let ax = EcEnv.Ax.instanciate p tys env in + let ax = EcEnv.Ax.instantiate p tys env in { ptev_env = ptenv; ptev_pt = ptglobal ~tys p; diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml index b7676c6d0..c257110b0 100644 --- a/src/ecProofTyping.ml +++ b/src/ecProofTyping.ml @@ -25,7 +25,7 @@ let process_form_opt ?mv hyps pf oty = let ts = Tuni.subst (EcUnify.UniEnv.close ue) in EcFol.Fsubst.f_subst ts ff - with EcUnify.UninstanciateUni -> + with EcUnify.UninstantiateUni -> EcTyping.tyerror pf.EcLocation.pl_loc (LDecl.toenv hyps) EcTyping.FreeTypeVariables diff --git a/src/ecScope.ml b/src/ecScope.ml index 95d7674e0..090545d6d 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1946,25 +1946,30 @@ module Ty = struct (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env)) tcs in let ue = TT.transtyvars env (loc, Some args) in - EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs) + EcUnify.UniEnv.tparams ue, Abstract (Sp.of_list tcs) | PTYD_Alias bd -> let ue = TT.transtyvars env (loc, Some args) in 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 + EcUnify.UniEnv.tparams ue, Concrete body + + | 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 let scheme = ELI.indsc_of_record record in - record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields) + record.ELI.rc_tparams, Record (scheme, record.ELI.rc_fields) in bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; }) @@ -1977,7 +1982,7 @@ module Ty = struct let scope = let decl = EcDecl.{ tyd_params = []; - tyd_type = `Abstract Sp.empty; + tyd_type = Abstract Sp.empty; tyd_loca = `Global; (* FIXME:SUBTYPE *) } in bind scope (unloc subtype.pst_name, decl) in @@ -2072,7 +2077,7 @@ module Ty = struct let asty = let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in { tyd_params = []; - tyd_type = `Abstract body; + tyd_type = Abstract body; tyd_loca = (lc :> locality); } in let scenv = EcEnv.Ty.bind name asty scenv in diff --git a/src/ecSection.ml b/src/ecSection.ml index 8dd953fe7..c177bfea4 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -362,12 +362,12 @@ let on_typarams cb typarams = let on_tydecl (cb : cb) (tyd : tydecl) = on_typarams cb tyd.tyd_params; match tyd.tyd_type with - | `Concrete ty -> on_ty cb ty - | `Abstract s -> on_typeclasses cb s - | `Record (f, fds) -> + | Concrete ty -> on_ty cb ty + | Abstract s -> on_typeclasses cb s + | Record (f, fds) -> on_form cb f; List.iter (on_ty cb |- snd) fds - | `Datatype dt -> + | Datatype dt -> List.iter (List.iter (on_ty cb) |- snd) dt.tydt_ctors; List.iter (on_form cb) [dt.tydt_schelim; dt.tydt_schcase] @@ -574,7 +574,7 @@ let add_declared_ty to_gen path tydecl = assert (tydecl.tyd_params = []); let s = match tydecl.tyd_type with - | `Abstract s -> s + | Abstract s -> s | _ -> assert false in let name = "'" ^ basename path in @@ -643,14 +643,14 @@ and fv_and_tvar_f f = let tydecl_fv tyd = let fv = match tyd.tyd_type with - | `Concrete ty -> ty_fv_and_tvar ty - | `Abstract _ -> Mid.empty - | `Datatype tydt -> + | Concrete ty -> ty_fv_and_tvar ty + | Abstract _ -> Mid.empty + | Datatype tydt -> List.fold_left (fun fv (_, l) -> List.fold_left (fun fv ty -> EcIdent.fv_union fv (ty_fv_and_tvar ty)) fv l) Mid.empty tydt.tydt_ctors - | `Record (_f, l) -> + | Record (_f, l) -> List.fold_left (fun fv (_, ty) -> EcIdent.fv_union fv (ty_fv_and_tvar ty)) Mid.empty l in List.fold_left (fun fv (id, _) -> Mid.remove id fv) fv tyd.tyd_params @@ -739,9 +739,9 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let tosubst = fst_params, tconstr path args in let tg_subst, tyd_type = match tydecl.tyd_type with - | `Concrete _ | `Abstract _ -> + | Concrete _ | Abstract _ -> EcSubst.add_tydef to_gen.tg_subst path tosubst, tydecl.tyd_type - | `Record (f, prs) -> + | Record (f, prs) -> let subst = EcSubst.empty in let tg_subst = to_gen.tg_subst in let subst = EcSubst.add_tydef subst path tosubst in @@ -758,8 +758,8 @@ let generalize_tydecl to_gen prefix (name, tydecl) = in let prs = List.map add_op prs in let f = EcSubst.subst_form !rsubst f in - !rtg_subst, `Record (f, prs) - | `Datatype dt -> + !rtg_subst, Record (f, prs) + | Datatype dt -> let subst = EcSubst.empty in let tg_subst = to_gen.tg_subst in let subst = EcSubst.add_tydef subst path tosubst in @@ -779,7 +779,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let tydt_ctors = List.map add_op dt.tydt_ctors in let tydt_schelim = EcSubst.subst_form !rsubst dt.tydt_schelim in let tydt_schcase = EcSubst.subst_form !rsubst dt.tydt_schcase in - !rtg_subst, `Datatype {tydt_ctors; tydt_schelim; tydt_schcase } + !rtg_subst, Datatype {tydt_ctors; tydt_schelim; tydt_schcase } in @@ -1066,7 +1066,7 @@ let sc_decl_mod (id,mt) = SC_decl_mod (id,mt) (* ---------------------------------------------------------------- *) let is_abstract_ty = function - | `Abstract _ -> true + | Abstract _ -> true | _ -> false (* diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 84943dc4b..d9793cc50 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -400,16 +400,16 @@ and trans_tydecl genv (p, tydecl) = let ts, opts, decl = match tydecl.tyd_type with - | `Abstract _ -> + | Abstract _ -> let ts = WTy.create_tysymbol pid tparams WTy.NoDef in (ts, [], WDecl.create_ty_decl ts) - | `Concrete ty -> + | Concrete ty -> let ty = trans_ty (genv, lenv) ty in let ts = WTy.create_tysymbol pid tparams (WTy.Alias ty) in (ts, [], WDecl.create_ty_decl ts) - | `Datatype dt -> + | Datatype dt -> let ncs = List.length dt.tydt_ctors in let ts = WTy.create_tysymbol pid tparams WTy.NoDef in @@ -429,7 +429,7 @@ and trans_tydecl genv (p, tydecl) = (ts, opts, WDecl.create_data_decl [ts, wdtype]) - | `Record (_, rc) -> + | Record (_, rc) -> let ts = WTy.create_tysymbol pid tparams WTy.NoDef in Hp.add genv.te_ty p ts; diff --git a/src/ecSubst.ml b/src/ecSubst.ml index f667dcccf..a0f8d259b 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -860,21 +860,21 @@ let subst_genty (s : subst) (tparams, ty) = (* -------------------------------------------------------------------- *) let subst_tydecl_body (s : subst) (tyd : ty_body) = match tyd with - | `Abstract tc -> - `Abstract (subst_typeclass s tc) + | Abstract tc -> + Abstract (subst_typeclass s tc) - | `Concrete ty -> - `Concrete (subst_ty s ty) + | Concrete ty -> + Concrete (subst_ty s ty) - | `Datatype dtype -> + | Datatype dtype -> let dtype = { tydt_ctors = List.map (snd_map (List.map (subst_ty s))) dtype.tydt_ctors; tydt_schelim = subst_form s dtype.tydt_schelim; tydt_schcase = subst_form s dtype.tydt_schcase; } - in `Datatype dtype + in Datatype dtype - | `Record (scheme, fields) -> - `Record (subst_form s scheme, List.map (snd_map (subst_ty s)) fields) + | Record (scheme, fields) -> + Record (subst_form s scheme, List.map (snd_map (subst_ty s)) fields) (* -------------------------------------------------------------------- *) let subst_tydecl (s : subst) (tyd : tydecl) = diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 3bdb4682e..46fade781 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -98,14 +98,14 @@ let get_open_tydecl hyps p tys = let rec tybody_compatible exn hyps ty_body1 ty_body2 = match ty_body1, ty_body2 with - | `Abstract _, `Abstract _ -> () (* FIXME Sp.t *) - | `Concrete ty1 , `Concrete ty2 -> error_body exn (EcReduction.EqTest.for_type (EcEnv.LDecl.toenv hyps) ty1 ty2) - | `Datatype ty1 , `Datatype ty2 -> datatype_compatible exn hyps ty1 ty2 - | `Record (f1,pr1), `Record(f2,pr2) -> record_compatible exn hyps f1 pr1 f2 pr2 - | _, `Concrete {ty_node = Tconstr(p, tys) } -> + | Abstract _, Abstract _ -> () (* FIXME Sp.t *) + | Concrete ty1 , Concrete ty2 -> error_body exn (EcReduction.EqTest.for_type (EcEnv.LDecl.toenv hyps) ty1 ty2) + | Datatype ty1 , Datatype ty2 -> datatype_compatible exn hyps ty1 ty2 + | Record (f1,pr1), Record(f2,pr2) -> record_compatible exn hyps f1 pr1 f2 pr2 + | _, Concrete {ty_node = Tconstr(p, tys) } -> let ty_body2 = get_open_tydecl hyps p tys in tybody_compatible exn hyps ty_body1 ty_body2 - | `Concrete{ty_node = Tconstr(p, tys) }, _ -> + | Concrete{ty_node = Tconstr(p, tys) }, _ -> let ty_body1 = get_open_tydecl hyps p tys in tybody_compatible exn hyps ty_body1 ty_body2 | _, _ -> raise exn (* FIXME should we do more for concrete version other *) @@ -119,7 +119,7 @@ let tydecl_compatible env tyd1 tyd2 = let exn = Incompatible (TyBody(*tyd1,tyd2*)) in let hyps = EcEnv.LDecl.init env params in match ty_body1, ty_body2 with - | `Abstract _, _ -> () (* FIXME Sp.t *) + | Abstract _, _ -> () (* FIXME Sp.t *) | _, _ -> tybody_compatible exn hyps ty_body1 ty_body2 (* -------------------------------------------------------------------- *) @@ -358,7 +358,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd let ntyd = EcTyping.transty EcTyping.tp_tydecl env ue ntyd in let decl = { tyd_params = nargs; - tyd_type = `Concrete ntyd; + tyd_type = Concrete ntyd; tyd_loca = otyd.tyd_loca; } in (decl, ntyd) @@ -368,7 +368,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | Some reftyd -> let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) reftyd.tyd_params in let body = tconstr p tyargs in - let decl = { reftyd with tyd_type = `Concrete body; } in + let decl = { reftyd with tyd_type = Concrete body; } in (decl, body) | _ -> assert false @@ -378,7 +378,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd assert (List.is_empty otyd.tyd_params); let decl = { tyd_params = []; - tyd_type = `Concrete ty; + tyd_type = Concrete ty; tyd_loca = otyd.tyd_loca; } in (decl, ty) @@ -398,9 +398,9 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd let subst = (* FIXME: HACK *) match otyd.tyd_type, body.ty_node with - | `Datatype { tydt_ctors = octors }, Tconstr (np, _) -> begin + | Datatype { tydt_ctors = octors }, Tconstr (np, _) -> begin match (EcEnv.Ty.by_path np env).tyd_type with - | `Datatype { tydt_ctors = _ } -> + | Datatype { tydt_ctors = _ } -> let newtparams = List.fst newtyd.tyd_params in let newtparams_ty = List.map tvar newtparams in let newdtype = tconstr np newtparams_ty in diff --git a/src/ecTypes.ml b/src/ecTypes.ml index 3da35d728..760b0a026 100644 --- a/src/ecTypes.ml +++ b/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 diff --git a/src/ecTypes.mli b/src/ecTypes.mli index 34b7b4cbf..95ee26bb3 100644 --- a/src/ecTypes.mli +++ b/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 diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 39490a68d..03aa6abb5 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2722,7 +2722,7 @@ and transinstr match (EcEnv.ty_hnorm ety env).ty_node with | Tconstr (indp, _) -> begin match EcEnv.Ty.by_path indp env with - | { tyd_type = `Datatype dt } -> + | { tyd_type = Datatype dt } -> Some (indp, dt) | _ -> None end @@ -3336,7 +3336,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = match (EcEnv.ty_hnorm cfty env).ty_node with | Tconstr (indp, _) -> begin match EcEnv.Ty.by_path indp env with - | { tyd_type = `Datatype dt } -> + | { tyd_type = Datatype dt } -> Some (indp, dt) | _ -> None end diff --git a/src/ecUnify.ml b/src/ecUnify.ml index e5bb56299..4664a8a71 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -14,7 +14,7 @@ module TC = EcTypeClass (* -------------------------------------------------------------------- *) exception UnificationFailure of [`TyUni of ty * ty | `TcCtt of ty * Sp.t] -exception UninstanciateUni +exception UninstantiateUni (* -------------------------------------------------------------------- *) type pb = [ `TyUni of ty * ty | `TcCtt of ty * Sp.t ] @@ -376,7 +376,7 @@ module UniEnv = struct UF.closed (!ue).ue_uf let close (ue : unienv) = - if not (closed ue) then raise UninstanciateUni; + if not (closed ue) then raise UninstantiateUni; (subst_of_uf (!ue).ue_uf) let assubst ue = subst_of_uf (!ue).ue_uf diff --git a/src/ecUnify.mli b/src/ecUnify.mli index 90488fabc..1f6ed3e45 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -7,7 +7,7 @@ open EcDecl (* -------------------------------------------------------------------- *) exception UnificationFailure of [`TyUni of ty * ty | `TcCtt of ty * Sp.t] -exception UninstanciateUni +exception UninstantiateUni type unienv diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index 9c947c1b6..6391b9c28 100644 --- a/src/ecUserMessages.ml +++ b/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,12 +606,24 @@ 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_Empty -> msg "the datatype may be empty" + | DTE_NonPositive (name, desc) -> ( + let prefix = Printf.sprintf "while defining type `%s`:" name in + match desc with + | NonPositive ty -> + msg "%s non strictly-positive occurrence in `%a`" prefix + (EcPrinting.pp_type env1) ty + | AbstractTypeRestriction p -> + msg "%s unauthorised use within abstract type `%a`" prefix + EcPrinting.pp_path p + | TypePositionRestriction ty -> + msg + "%s unauthorised use of type `%a`, which changes the position of \ + its type parameters" + prefix (EcPrinting.pp_type env1) ty) + let pp_fxerror env fmt error = match error with | FXLowError ee -> diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml index 767138a3a..214ed0b71 100644 --- a/src/phl/ecPhlRwEquiv.ml +++ b/src/phl/ecPhlRwEquiv.ml @@ -145,7 +145,7 @@ let process_rewrite_equiv info tc = let res = omap (fun v -> EcTyping.transexpcast subenv `InProc ue ret_ty v) pres in let es = e_subst (Tuni.subst (EcUnify.UniEnv.close ue)) in Some (List.map es args, omap (EcModules.lv_of_expr |- es) res) - with EcUnify.UninstanciateUni -> + with EcUnify.UninstantiateUni -> EcTyping.tyerror (loc pargs) env EcTyping.FreeTypeVariables end in