From 80cb8d743185a8a800b32e2cc583d4067f3c74dd Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Fri, 30 Jan 2026 13:16:29 +0000 Subject: [PATCH] Remove prototype type-classes implementation. Co-authored-by: Gustavo Delerue Co-authored-by: Pierre-Yves Strub --- src/ecCallbyValue.ml | 2 +- src/ecCommands.ml | 8 -- src/ecDecl.ml | 29 ++++-- src/ecDecl.mli | 9 +- src/ecEnv.ml | 73 ++----------- src/ecEnv.mli | 1 - src/ecHiGoal.ml | 6 +- src/ecHiInductive.ml | 6 +- src/ecInductive.ml | 18 ++-- src/ecLexer.mll | 1 - src/ecParser.mly | 52 +++------- src/ecParsetree.ml | 22 ++-- src/ecPrinting.ml | 64 ++++++------ src/ecProofTerm.ml | 4 +- src/ecProofTyping.ml | 5 +- src/ecReduction.ml | 4 +- src/ecScope.ml | 99 +++--------------- src/ecScope.mli | 1 - src/ecSection.ml | 64 +++++------- src/ecSmt.ml | 14 +-- src/ecSubst.ml | 22 ++-- src/ecSubst.mli | 1 - src/ecThCloning.ml | 1 - src/ecTheory.ml | 1 - src/ecTheory.mli | 1 - src/ecTheoryReplay.ml | 54 ++++------ src/ecTyping.ml | 12 +-- src/ecUnify.ml | 235 ++++++++++++++---------------------------- src/ecUnify.mli | 11 +- 29 files changed, 266 insertions(+), 554 deletions(-) diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml index f65c8f25e..482205ec8 100644 --- a/src/ecCallbyValue.ml +++ b/src/ecCallbyValue.ml @@ -300,7 +300,7 @@ and try_reduce_fixdef let body = EcFol.form_of_expr body in let body = - Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in + Tvar.f_subst ~freshen:true op.EcDecl.op_tparams tys body in Some (cbv st subst body (Args.create ty eargs)) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 135a2b3de..91cdd1f8b 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -418,13 +418,6 @@ and process_subtype (scope : EcScope.scope) (subtype : psubtype located) = EcScope.notify scope `Info "added subtype: `%s'" (unloc subtype.pl_desc.pst_name); scope -(* -------------------------------------------------------------------- *) -and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) = - EcScope.check_state `InTop "type class" scope; - let scope = EcScope.Ty.add_class scope tcd in - EcScope.notify scope `Info "added type class: `%s'" (unloc tcd.pl_desc.ptc_name); - scope - (* -------------------------------------------------------------------- *) and process_tycinst (scope : EcScope.scope) (tci : ptycinstance located) = EcScope.check_state `InTop "type class instance" scope; @@ -758,7 +751,6 @@ and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope) match g.pl_desc with | Gtype t -> `Fct (fun scope -> process_types ?src scope (List.map (mk_loc loc) t)) | Gsubtype t -> `Fct (fun scope -> process_subtype scope (mk_loc loc t)) - | Gtypeclass t -> `Fct (fun scope -> process_typeclass scope (mk_loc loc t)) | Gtycinstance t -> `Fct (fun scope -> process_tycinst scope (mk_loc loc t)) | Gmodule m -> `Fct (fun scope -> process_module ?src scope m) | Ginterface i -> `Fct (fun scope -> process_interface ?src scope i) diff --git a/src/ecDecl.ml b/src/ecDecl.ml index bcc414242..22d55c894 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -11,7 +11,7 @@ module Ssym = EcSymbols.Ssym module CS = EcCoreSubst (* -------------------------------------------------------------------- *) -type ty_param = EcIdent.t * EcPath.Sp.t +type ty_param = EcIdent.t type ty_params = ty_param list type ty_pctor = [ `Int of int | `Named of ty_params ] @@ -29,7 +29,7 @@ type ty_dtype = { type ty_body = | Concrete of EcTypes.ty - | Abstract of Sp.t + | Abstract | Datatype of ty_dtype | Record of ty_record @@ -44,7 +44,7 @@ let tydecl_as_concrete (td : tydecl) = 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 -> Some () | _ -> None let tydecl_as_datatype (td : tydecl) = match td.tyd_type with Datatype x -> Some x | _ -> None @@ -53,7 +53,7 @@ let tydecl_as_record (td : tydecl) = match td.tyd_type with Record (x, y) -> Some (x, y) | _ -> None (* -------------------------------------------------------------------- *) -let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc = +let abs_tydecl ?(params = `Int 0) lc = let params = match params with | `Named params -> @@ -61,15 +61,15 @@ let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc = | `Int n -> let fmt = fun x -> Printf.sprintf "'%s" x in List.map - (fun x -> (EcIdent.create x, Sp.empty)) + (fun x -> (EcIdent.create x)) (EcUid.NameGen.bulk ~fmt n) in - { tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; } + { tyd_params = params; tyd_type = Abstract; tyd_loca = lc; } (* -------------------------------------------------------------------- *) let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) = - let subst = CS.Tvar.init (List.map fst params) args in + let subst = CS.Tvar.init params args in CS.Tvar.subst subst ty (* -------------------------------------------------------------------- *) @@ -254,12 +254,19 @@ let operator_as_prind (op : operator) = | _ -> assert false (* -------------------------------------------------------------------- *) -let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc = +let axiomatized_op + ?(nargs = 0) + ?(nosmt = false) + (path : EcPath.path) + ((tparams, axbd) : ty_params * form) + (lc : locality) + : axiom += let axbd, axpm = - let bdpm = List.map fst tparams in + let bdpm = tparams in let axpm = List.map EcIdent.fresh bdpm in (CS.Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) axbd, - List.combine axpm (List.map snd tparams)) + axpm) in let args, axbd = @@ -271,7 +278,7 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc = in let opargs = List.map (fun (x, ty) -> f_local x (gty_as_ty ty)) args in - let tyargs = List.map (EcTypes.tvar |- fst) axpm in + let tyargs = List.map EcTypes.tvar axpm in let op = f_op path tyargs (toarrow (List.map f_ty opargs) axbd.EcAst.f_ty) in let op = f_app op opargs axbd.f_ty in let axspec = f_forall args (f_eq op axbd) in diff --git a/src/ecDecl.mli b/src/ecDecl.mli index a974a6048..61a0851b0 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -2,12 +2,11 @@ open EcUtils open EcSymbols open EcBigInt -open EcPath open EcTypes open EcCoreFol (* -------------------------------------------------------------------- *) -type ty_param = EcIdent.t * EcPath.Sp.t +type ty_param = EcIdent.t type ty_params = ty_param list type ty_pctor = [ `Int of int | `Named of ty_params ] @@ -25,7 +24,7 @@ type ty_dtype = { type ty_body = | Concrete of EcTypes.ty - | Abstract of Sp.t + | Abstract | Datatype of ty_dtype | Record of ty_record @@ -37,11 +36,11 @@ type tydecl = { } val tydecl_as_concrete : tydecl -> EcTypes.ty option -val tydecl_as_abstract : tydecl -> Sp.t option +val tydecl_as_abstract : tydecl -> unit 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 abs_tydecl : ?params:ty_pctor -> locality -> tydecl val ty_instantiate : ty_params -> ty list -> ty -> ty diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 4490390b9..6950cfc3b 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -782,13 +782,13 @@ module MC = struct match tyd.tyd_type with | Concrete _ -> mc - | Abstract _ -> mc + | Abstract -> mc | Datatype dtype -> let cs = dtype.tydt_ctors in let schelim = dtype.tydt_schelim in let schcase = dtype.tydt_schcase in - let params = List.map (fun (x, _) -> tvar x) tyd.tyd_params in + let params = List.map tvar tyd.tyd_params in let for1 i (c, aty) = let aty = EcTypes.toarrow aty (tconstr mypath params) in let aty = EcSubst.freshen_type (tyd.tyd_params, aty) in @@ -829,7 +829,7 @@ module MC = struct ) mc projs | Record (scheme, fields) -> - let params = List.map (fun (x, _) -> tvar x) tyd.tyd_params in + let params = List.map tvar tyd.tyd_params in let nfields = List.length fields in let cfields = let for1 i (f, aty) = @@ -911,7 +911,7 @@ module MC = struct let opname = EcIdent.name opid in let optype = EcSubst.subst_ty tsubst optype in let opdecl = - mk_op ~opaque:optransparent [(self, Sp.singleton mypath)] + mk_op ~opaque:optransparent [(self)] optype (Some OP_TC) loca in (opid, xpath opname, optype, opdecl) in @@ -931,7 +931,7 @@ module MC = struct List.map (fun (x, ax) -> let ax = EcSubst.subst_form fsubst ax in - (x, { ax_tparams = [(self, Sp.singleton mypath)]; + (x, { ax_tparams = [(self)]; ax_spec = ax; ax_kind = `Lemma; ax_loca = loca; @@ -1107,9 +1107,6 @@ module MC = struct else (add2mc _up_theory xsubth cth mc, None) - | Th_typeclass (x, tc) -> - (add2mc _up_typeclass x tc mc, None) - | Th_baserw (x, _) -> (add2mc _up_rwbase x (expath x) mc, None) @@ -1406,11 +1403,6 @@ module TypeClass = struct let myself = EcPath.pqname (root env) name in { env with env_tc = TC.Graph.add ~src:myself ~dst:prt env.env_tc } - let bind ?(import = true) name tc env = - let env = rebind name tc env in - let item = Th_typeclass (name, tc) in - { env with env_item = mkitem ~import item :: env.env_item } - let lookup qname (env : env) = MC.lookup_typeclass qname env @@ -2548,7 +2540,7 @@ module Ty = struct match by_path_opt name env with | Some ({ tyd_type = Concrete body } as tyd) -> Tvar.subst - (Tvar.init (List.map fst tyd.tyd_params) args) + (Tvar.init tyd.tyd_params args) body | _ -> raise (LookupFailure (`Path name)) @@ -2603,22 +2595,7 @@ module Ty = struct | _ -> None let rebind name ty env = - let env = MC.bind_tydecl name ty env in - - match ty.tyd_type with - | Abstract tc -> - let myty = - let myp = EcPath.pqname (root env) name in - let typ = List.map (fst_map EcIdent.fresh) ty.tyd_params in - (typ, EcTypes.tconstr myp (List.map (tvar |- fst) typ)) in - let instr = - Sp.fold - (fun p inst -> TypeClass.bind_instance myty (`General p) inst) - tc env.env_tci - in - { env with env_tci = instr } - - | _ -> env + MC.bind_tydecl name ty env let bind ?(import = true) name ty env = let env = rebind name ty env in @@ -2722,7 +2699,7 @@ module Op = struct let reduce ?mode ?nargs env p tys = let op, f = core_reduce ?mode ?nargs env p in - Tvar.f_subst ~freshen:true (List.map fst op.op_tparams) tys f + Tvar.f_subst ~freshen:true op.op_tparams tys f let is_projection env p = try EcDecl.is_proj (by_path p env) @@ -2815,7 +2792,7 @@ module Ax = struct 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 + Tvar.f_subst ~freshen:true ax.ax_tparams tys f | _ -> raise (LookupFailure (`Path p)) let iter ?name f (env : env) = @@ -2930,20 +2907,6 @@ module Theory = struct | Th_theory (x, cth) when cth.cth_mode = `Concrete -> bind_instance_th (xpath x) inst cth.cth_items - | Th_type (x, tyd) -> begin - match tyd.tyd_type with - | 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)) - in - Sp.fold - (fun p inst -> TypeClass.bind_instance myty (`General p) inst) - tc inst - - | _ -> inst - end - | _ -> inst (* ------------------------------------------------------------------ *) @@ -2964,17 +2927,6 @@ module Theory = struct end | _ -> odfl base (tx path base item.ti_item) - (* ------------------------------------------------------------------ *) - let bind_tc_th = - let for1 path base = function - | Th_typeclass (x, tc) -> - tc.tc_prt |> omap (fun prt -> - let src = EcPath.pqname path x in - TC.Graph.add ~src ~dst:prt base) - | _ -> None - - in bind_base_th for1 - (* ------------------------------------------------------------------ *) let bind_br_th = let for1 path base = function @@ -3047,14 +2999,13 @@ module Theory = struct | _, `Concrete -> let thname = EcPath.pqname (root env) cth.name in let env_tci = bind_instance_th thname env.env_tci items in - let env_tc = bind_tc_th thname env.env_tc items in let env_rwbase = bind_br_th thname env.env_rwbase items in let env_atbase = bind_at_th thname env.env_atbase items in let env_ntbase = bind_nt_th thname env.env_ntbase items in let env_redbase = bind_rd_th thname env.env_redbase items in let env = { env with - env_tci ; env_tc ; env_rwbase; + env_tci ; env_rwbase; env_atbase; env_ntbase; env_redbase; } in add_restr_th thname env items @@ -3106,9 +3057,6 @@ module Theory = struct | Th_theory (x, ({cth_mode = `Abstract} as th)) -> MC.import_theory (xpath x) th env - | Th_typeclass (x, tc) -> - MC.import_typeclass (xpath x) tc env - | Th_baserw (x, _) -> MC.import_rwbase (xpath x) env @@ -3265,7 +3213,6 @@ module Theory = struct | `Concrete -> { env with env_tci = bind_instance_th thpath env.env_tci cth.cth_items; - env_tc = bind_tc_th thpath env.env_tc cth.cth_items; env_rwbase = bind_br_th thpath env.env_rwbase cth.cth_items; env_atbase = bind_at_th thpath env.env_atbase cth.cth_items; env_ntbase = bind_nt_th thpath env.env_ntbase cth.cth_items; diff --git a/src/ecEnv.mli b/src/ecEnv.mli index fe21dc247..eb5d33125 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -380,7 +380,6 @@ module TypeClass : sig type t = typeclass val add : path -> env -> env - val bind : ?import:bool -> symbol -> t -> env -> env val graph : env -> EcTypeClass.graph val by_path : path -> env -> t diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index b16b7eb03..8a5ebb0a7 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -490,7 +490,7 @@ let process_exacttype qs (tc : tcenv1) = tc_error !!tc "%a" EcEnv.pp_lookup_failure cause in let tys = - List.map (fun (a,_) -> EcTypes.tvar a) + List.map (fun a -> EcTypes.tvar a) (EcEnv.LDecl.tohyps hyps).h_tvar in let pt = ptglobal ~tys p in @@ -700,7 +700,7 @@ let process_delta ~und_delta ?target (s, o, p) tc = match sform_of_form fp with | SFop ((_, tvi), []) -> begin (* FIXME: TC HOOK *) - let body = Tvar.f_subst ~freshen:true (List.map fst tparams) tvi body in + let body = Tvar.f_subst ~freshen:true tparams tvi body in let body = f_app body args topfp.f_ty in try EcReduction.h_red EcReduction.beta_red hyps body with EcEnv.NotReducible -> body @@ -723,7 +723,7 @@ let process_delta ~und_delta ?target (s, o, p) tc = | `RtoL -> let fp = (* FIXME: TC HOOK *) - let body = Tvar.f_subst ~freshen:true (List.map fst tparams) tvi body in + let body = Tvar.f_subst ~freshen:true tparams tvi body in let fp = f_app body args p.f_ty in try EcReduction.h_red EcReduction.beta_red hyps fp with EcEnv.NotReducible -> fp diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml index 72cf50e85..45edcdcc7 100644 --- a/src/ecHiInductive.ml +++ b/src/ecHiInductive.ml @@ -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; tyd_loca = lc; } in EcEnv.Ty.bind (unloc name) myself env @@ -134,7 +134,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) = let tyinst = ty_instantiate tdecl.tyd_params targs in match tdecl.tyd_type with - | Abstract _ -> + | Abstract -> List.exists isempty targs | Concrete ty -> @@ -402,7 +402,7 @@ let trans_matchfix let codom = ty_subst ts codom in let opexpr = EcPath.pqname (EcEnv.root env) name in let args = List.map (snd_map (ty_subst ts)) args in - let opexpr = e_op opexpr (List.map (tvar |- fst) tparams) + let opexpr = e_op opexpr (List.map tvar tparams) (toarrow (List.map snd args) codom) in let ebsubst = bind_elocal ts opname opexpr diff --git a/src/ecInductive.ml b/src/ecInductive.ml index f21f3003c..81f3be80d 100644 --- a/src/ecInductive.ml +++ b/src/ecInductive.ml @@ -38,7 +38,7 @@ let datatype_proj_path (p : EP.path) (x : symbol) = (* -------------------------------------------------------------------- *) let indsc_of_record (rc : record) = - let targs = List.map (tvar |- fst) rc.rc_tparams in + let targs = List.map tvar rc.rc_tparams in let recty = tconstr rc.rc_path targs in let recx = fresh_id_of_ty recty in let recfm = FL.f_local recx recty in @@ -129,7 +129,7 @@ let rec occurs ?(normty = identity) 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, _) -> + List.for_all2 (fun ty param_id -> match ty.ty_node with | Tvar id -> EcIdent.id_equal id param_id | _ -> false) @@ -143,7 +143,7 @@ let rec check_positivity_in_decl fct p decl ident = match decl.tyd_type with | Concrete ty -> with_context ~ident p Concrete (check ty) - | Abstract _ -> non_positive p AbstractTypeRestriction + | Abstract -> non_positive p AbstractTypeRestriction | Datatype { tydt_ctors } -> iter tydt_ctors @@ fun (name, argty) -> iter argty @@ fun ty -> @@ -164,7 +164,7 @@ and check_positivity_ident fct p params ident ty = let decl = fct q in List.iter (check_positivity_ident fct p params ident) args; List.combine args decl.tyd_params - |> List.filter_map (fun (arg, (ident', _)) -> + |> 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_) -> @@ -182,7 +182,7 @@ let rec check_positivity_path fct p ty = let decl = fct q in List.iter (check_positivity_path fct p) args; List.combine args decl.tyd_params - |> List.filter_map (fun (arg, (ident, _)) -> + |> 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_) -> @@ -260,11 +260,11 @@ 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 dt.dt_tparams, tpath) dt.dt_ctors + in scheme mode (dt.dt_tparams, tpath) dt.dt_ctors (* -------------------------------------------------------------------- *) let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) = - let thety = tconstr tpath (List.map (tvar |- fst) tparams) in + let thety = tconstr tpath (List.map tvar tparams) in let do1 i (cname, cty) = let thv = EcIdent.create "the" in @@ -378,7 +378,7 @@ let indsc_of_prind ({ ip_path = p; ip_prind = pri } as pr) = FL.f_forall ctor.prc_bds px in - let sc = FL.f_op p (List.map (tvar |- fst) pr.ip_tparams) prty in + let sc = FL.f_op p (List.map tvar pr.ip_tparams) prty in let sc = FL.f_imp (FL.f_app sc prag tbool) pred in let sc = FL.f_imps (List.map for1 pri.pri_ctors) sc in let sc = FL.f_forall [predx, FL.gtty tbool] sc in @@ -391,7 +391,7 @@ let introsc_of_prind ({ ip_path = p; ip_prind = pri } as pr) = let bds = List.map (snd_map FL.gtty) pri.pri_args in let clty = toarrow (List.map snd pri.pri_args) tbool in let clag = (List.map (curry FL.f_local) pri.pri_args) in - let cl = FL.f_op p (List.map (tvar |- fst) pr.ip_tparams) clty in + let cl = FL.f_op p (List.map tvar pr.ip_tparams) clty in let cl = FL.f_app cl clag tbool in let for1 ctor = diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 19536eaae..e5a5ced94 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -200,7 +200,6 @@ "section" , SECTION ; (* KW: global *) "subtype" , SUBTYPE ; (* KW: global *) "type" , TYPE ; (* KW: global *) - "class" , CLASS ; (* KW: global *) "instance" , INSTANCE ; (* KW: global *) "print" , PRINT ; (* KW: global *) "search" , SEARCH ; (* KW: global *) diff --git a/src/ecParser.mly b/src/ecParser.mly index a1c9acf08..b1146388e 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -406,7 +406,6 @@ %token CEQ %token CFOLD %token CHANGE -%token CLASS %token CLEAR %token CLONE %token COLON @@ -1637,13 +1636,18 @@ signature_item: (* EcTypes declarations / definitions *) typaram: -| x=tident { (x, []) } -| x=tident LTCOLON tc=plist1(lqident, AMP) { (x, tc) } +| x=tident + { (x : ptyparam) } typarams: -| empty { [] } -| x=tident { [(x, [])] } -| xs=paren(plist1(typaram, COMMA)) { xs } +| empty + { ([] : ptyparams) } + +| x=tident + { ([x] : ptyparams) } + +| xs=paren(plist1(typaram, COMMA)) + { (xs : ptyparams) } %inline tyd_name: | tya=typarams x=ident { (tya, x) } @@ -1656,7 +1660,7 @@ dt_ctor_def: | LBRACKET PIPE? ctors=plist1(dt_ctor_def, PIPE) RBRACKET { ctors } rec_field_def: -| x=ident COLON ty=loc(type_exp) { (x, ty); } +| x=ident COLON ty=loc(type_exp) { (x, ty) } %inline record_def: | LBRACE fields=rlist1(rec_field_def, SEMICOLON) SEMICOLON? RBRACE @@ -1664,10 +1668,7 @@ rec_field_def: typedecl: | locality=locality TYPE td=rlist1(tyd_name, COMMA) - { List.map (fun x -> mk_tydecl ~locality x (PTYD_Abstract [])) td } - -| locality=locality TYPE td=tyd_name LTCOLON tcs=rlist1(qident, COMMA) - { [mk_tydecl ~locality td (PTYD_Abstract tcs)] } + { List.map (fun x -> mk_tydecl ~locality x PTYD_Abstract) td } | locality=locality TYPE td=tyd_name EQ te=loc(type_exp) { [mk_tydecl ~locality td (PTYD_Alias te)] } @@ -1693,30 +1694,6 @@ subtype: subtype_rename: | RENAME x=STRING COMMA y=STRING { (x, y) } -(* -------------------------------------------------------------------- *) -(* Type classes *) -typeclass: -| loca=is_local TYPE CLASS x=lident inth=tc_inth? EQ LBRACE body=tc_body RBRACE { - { ptc_name = x; - ptc_inth = inth; - ptc_ops = fst body; - ptc_axs = snd body; - ptc_loca = loca; - } - } - -tc_inth: -| LTCOLON x=lqident { x } - -tc_body: -| ops=tc_op* axs=tc_ax* { (ops, axs) } - -tc_op: -| OP x=oident COLON ty=loc(type_exp) { (x, ty) } - -tc_ax: -| AXIOM x=ident COLON ax=form { (x, ax) } - (* -------------------------------------------------------------------- *) (* Type classes (instances) *) tycinstance: @@ -1770,11 +1747,9 @@ pred_tydom: tyvars_decl: | LBRACKET tyvars=rlist0(typaram, COMMA) RBRACKET +| LBRACKET tyvars=rlist2(tident, empty) RBRACKET { tyvars } -| LBRACKET tyvars=rlist2(tident , empty) RBRACKET - { List.map (fun x -> (x, [])) tyvars } - op_or_const: | OP { `Op } | CONST { `Const } @@ -3834,7 +3809,6 @@ global_action: | sig_def { Ginterface $1 } | typedecl { Gtype $1 } | subtype { Gsubtype $1 } -| typeclass { Gtypeclass $1 } | tycinstance { Gtycinstance $1 } | operator { Goperator $1 } | procop { Gprocop $1 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index e9991a3ea..169e22ba8 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -101,7 +101,8 @@ and 'a rfield = { (* -------------------------------------------------------------------- *) type pmodule_type = pqsymbol -type ptyparams = (psymbol * pqsymbol list) list +type ptyparam = psymbol +type ptyparams = ptyparam list type ptydname = (ptyparams * psymbol) located type ptydecl = { @@ -112,7 +113,7 @@ type ptydecl = { } and ptydbody = - | PTYD_Abstract of pqsymbol list + | PTYD_Abstract | PTYD_Alias of pty | PTYD_Record of precord | PTYD_Datatype of pdatatype @@ -399,7 +400,7 @@ type psubtype = { (* -------------------------------------------------------------------- *) type ptyvardecls = - (psymbol * pqsymbol list) list + psymbol list type pop_def = | PO_abstr of pty @@ -450,7 +451,7 @@ and ppind = ptybindings * (ppind_ctor list) type ppredicate = { pp_name : psymbol; - pp_tyvars : (psymbol * pqsymbol list) list option; + pp_tyvars : psymbol list option; pp_def : ppred_def; pp_locality : locality; } @@ -1061,7 +1062,7 @@ type mempred_binding = PT_MemPred of psymbol list type paxiom = { pa_name : psymbol; pa_pvars : mempred_binding option; - pa_tyvars : (psymbol * pqsymbol list) list option; + pa_tyvars : ptyparams option; pa_vars : pgtybindings option; pa_formula : pformula; pa_kind : paxiom_kind; @@ -1075,17 +1076,9 @@ type prealize = { } (* -------------------------------------------------------------------- *) -type ptypeclass = { - ptc_name : psymbol; - ptc_inth : pqsymbol option; - ptc_ops : (psymbol * pty) list; - ptc_axs : (psymbol * pformula) list; - ptc_loca : is_local; -} - type ptycinstance = { pti_name : pqsymbol; - pti_type : (psymbol * pqsymbol list) list * pty; + pti_type : ptyparams * pty; pti_ops : (psymbol * (pty list * pqsymbol)) list; pti_axs : (psymbol * ptactic_core) list; pti_args : [`Ring of (zint option * zint option)] option; @@ -1280,7 +1273,6 @@ type global_action = | Gaxiom of paxiom | Gtype of ptydecl list | Gsubtype of psubtype - | Gtypeclass of ptypeclass | Gtycinstance of ptycinstance | Gaddrw of (is_local * pqsymbol * pqsymbol list) | Greduction of puserred diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 854a61a59..4c100ca9c 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1663,7 +1663,7 @@ and try_pp_chained_orderings match match_pp_notations ~filter:(fun (p, _) -> is_ordering_op p) ppe f with | Some ((op, (tvi, _)), ue, ev, ov, [i1; i2]) -> begin let ti = Tvar.subst ov in - let tvi = List.map (ti |- tvar |- fst) tvi in + let tvi = List.map (ti |- tvar) tvi in let sb = EcMatching.MEV.assubst ue ev ppe.ppe_env in let i1 = Fsubst.f_subst sb i1 in let i2 = Fsubst.f_subst sb i2 in @@ -1802,7 +1802,7 @@ and try_pp_notations | Some ((p, (tv, nt)), ue, ev, ov, eargs) -> let ti = Tvar.subst ov in let rty = ti nt.ont_resty in - let tv = List.map (ti |- tvar |- fst) tv in + let tv = List.map (ti |- tvar) tv in let args = List.map (curry f_local |- snd_map ti) nt.ont_args in let f = f_op p tv (toarrow tv rty) in let f = f_app f args rty in @@ -2263,11 +2263,11 @@ let pp_sform ppe fmt f = (* -------------------------------------------------------------------- *) let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) = let ppe = PPEnv.enter_theory ppe (Option.get (EcPath.prefix x)) in - let ppe = PPEnv.add_locals ppe (List.map fst tyd.tyd_params) in + let ppe = PPEnv.add_locals ppe tyd.tyd_params in let name = P.basename x in let pp_prelude fmt = - match List.map fst tyd.tyd_params with + match tyd.tyd_params with | [] -> Format.fprintf fmt "type %s" name @@ -2280,7 +2280,8 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) = and pp_body fmt = match tyd.tyd_type with - | Abstract _ -> () (* FIXME: TC HOOK *) + | Abstract -> + () | Concrete ty -> Format.fprintf fmt " =@ %a" (pp_type ppe) ty @@ -2306,19 +2307,10 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) = Format.fprintf fmt "@[%a%t%t.@]" pp_locality tyd.tyd_loca pp_prelude pp_body (* -------------------------------------------------------------------- *) -let pp_tyvar_ctt (ppe : PPEnv.t) fmt (tvar, ctt) = - match EcPath.Sp.elements ctt with - | [] -> pp_tyvar ppe fmt tvar - | ctt -> - Format.fprintf fmt "%a <: %a" - (pp_tyvar ppe) tvar - (pp_list " &@ " (pp_tcname ppe)) ctt - -(* -------------------------------------------------------------------- *) -let pp_tyvarannot (ppe : PPEnv.t) fmt ids = +let pp_tyvarannot (ppe : PPEnv.t) fmt (ids: ty_param list) = match ids with | [] -> () - | ids -> Format.fprintf fmt "[%a]" (pp_list ",@ " (pp_tyvar_ctt ppe)) ids + | ids -> Format.fprintf fmt "[%a]" (pp_list ",@ " (pp_tyvar ppe)) ids let pp_pvar (ppe : PPEnv.t) fmt ids = match ids with @@ -2397,8 +2389,8 @@ let pp_codepos (ppe : PPEnv.t) (fmt : Format.formatter) ((nm, cp1) : CP.codepos) Format.fprintf fmt "%a%a" (pp_list "" pp_nm) nm (pp_codepos1 ppe) cp1 (* -------------------------------------------------------------------- *) -let pp_opdecl_pr (ppe : PPEnv.t) fmt (basename, ts, ty, op) = - let ppe = PPEnv.add_locals ppe (List.map fst ts) in +let pp_opdecl_pr (ppe : PPEnv.t) fmt ((basename, ts, ty, op): symbol * ty_param list * ty * prbody option) = + let ppe = PPEnv.add_locals ppe ts in let pp_body fmt = match op with @@ -2454,7 +2446,7 @@ let pp_opdecl_pr (ppe : PPEnv.t) fmt (basename, ts, ty, op) = (* -------------------------------------------------------------------- *) let pp_opdecl_op (ppe : PPEnv.t) fmt (basename, ts, ty, op) = - let ppe = PPEnv.add_locals ppe (List.map fst ts) in + let ppe = PPEnv.add_locals ppe ts in let pp_body fmt = match op with @@ -2538,11 +2530,13 @@ let pp_opdecl_op (ppe : PPEnv.t) fmt (basename, ts, ty, op) = pp_opname ([], basename) pp_body | _ -> Format.fprintf fmt "@[op %a %a %t.@]" - pp_opname ([], basename) (pp_tyvarannot ppe) ts pp_body + pp_opname ([], basename) (pp_tyvarannot ppe) ts pp_body (* -------------------------------------------------------------------- *) -let pp_opdecl_nt (ppe : PPEnv.t) fmt (basename, ts, _ty, nt) = - let ppe = PPEnv.add_locals ppe (List.map fst ts) in +let pp_opdecl_nt (ppe : PPEnv.t) fmt + ((basename, ts, _ty, nt) : symbol * ty_param list * ty * notation) += + let ppe = PPEnv.add_locals ppe ts in let pp_body fmt = let subppe, pplocs = @@ -2561,7 +2555,12 @@ let pp_opdecl_nt (ppe : PPEnv.t) fmt (basename, ts, _ty, nt) = pp_opname ([], basename) (pp_tyvarannot ppe) ts pp_body (* -------------------------------------------------------------------- *) -let pp_opdecl ?(long = false) (ppe : PPEnv.t) fmt (x, op) = +let pp_opdecl + ?(long = false) + (ppe : PPEnv.t) + fmt + ((x, op) : EcPath.path * operator) += let ppe = PPEnv.enter_theory ppe (Option.get (EcPath.prefix x)) in let pp_name fmt x = @@ -2584,7 +2583,7 @@ let pp_opdecl ?(long = false) (ppe : PPEnv.t) fmt (x, op) = in Format.fprintf fmt "@[%a%a%a@]" pp_locality op.op_loca pp_name x pp_decl op let pp_added_op (ppe : PPEnv.t) fmt op = - let ppe = PPEnv.add_locals ppe (List.map fst op.op_tparams) in + let ppe = PPEnv.add_locals ppe op.op_tparams in match op.op_tparams with | [] -> Format.fprintf fmt ": @[%a@]" (pp_type ppe) op.op_ty @@ -2606,7 +2605,7 @@ let tags_of_axkind = function | `Lemma -> [] let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) = - let ppe = PPEnv.add_locals ppe (List.map fst ax.ax_tparams) in + let ppe = PPEnv.add_locals ppe ax.ax_tparams in let basename = P.basename x in let pp_spec fmt = @@ -3220,7 +3219,7 @@ module PPGoal = struct in (ppe, (id, pdk)) let pp_goal1 ?(pphyps = true) ?prpo ?(idx) (ppe : PPEnv.t) fmt (hyps, concl) = - let ppe = PPEnv.add_locals ppe (List.map fst hyps.EcBaseLogic.h_tvar) in + let ppe = PPEnv.add_locals ppe hyps.EcBaseLogic.h_tvar in let ppe, pps = List.map_fold pre_pp_hyp ppe (List.rev hyps.EcBaseLogic.h_local) in idx |> oiter (Format.fprintf fmt "Goal #%d@\n"); @@ -3231,7 +3230,7 @@ module PPGoal = struct | [] -> Format.fprintf fmt "Type variables: @\n\n%!" | tv -> Format.fprintf fmt "Type variables: %a@\n\n%!" - (pp_list ", " (pp_tyvar_ctt ppe)) tv + (pp_list ", " (pp_tyvar ppe)) tv end; List.iter (fun (id, (pk, dk)) -> let pk fmt = @@ -3266,7 +3265,7 @@ end (* -------------------------------------------------------------------- *) let pp_hyps (ppe : PPEnv.t) fmt hyps = let hyps = EcEnv.LDecl.tohyps hyps in - let ppe = PPEnv.add_locals ppe (List.map fst hyps.EcBaseLogic.h_tvar) in + let ppe = PPEnv.add_locals ppe hyps.EcBaseLogic.h_tvar in let ppe, pps = List.map_fold PPGoal.pre_pp_hyp ppe (List.rev hyps.EcBaseLogic.h_local) in @@ -3275,7 +3274,7 @@ let pp_hyps (ppe : PPEnv.t) fmt hyps = | [] -> Format.fprintf fmt "Type variables: @\n\n%!" | tv -> Format.fprintf fmt "Type variables: %a@\n\n%!" - (pp_list ", " (pp_tyvar_ctt ppe)) tv + (pp_list ", " (pp_tyvar ppe)) tv end; List.iter (fun (id, (pk, dk)) -> let pk fmt = @@ -3579,11 +3578,8 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = Format.fprintf fmt "export %a." EcSymbols.pp_qsymbol (PPEnv.th_symb ppe p) - | EcTheory.Th_typeclass _ -> - Format.fprintf fmt "typeclass ." - | EcTheory.Th_instance ((typ, ty), tc, lc) -> begin - let ppe = PPEnv.add_locals ppe (List.map fst typ) in (* FIXME *) + let ppe = PPEnv.add_locals ppe typ in (* FIXME *) match tc with | (`Ring _ | `Field _) as tc -> begin @@ -3623,7 +3619,7 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = "%ainstance %s with [%a] %a@\n@[ %a@]" pp_locality lc name - (pp_paren (pp_list ",@ " (pp_tyvar ppe))) (List.map fst typ) + (pp_paren (pp_list ",@ " (pp_tyvar ppe))) typ (pp_type ppe) ty (pp_list "@\n" (fun fmt (name, op) -> diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index 0f1a19d11..9055f2462 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -225,7 +225,7 @@ let pt_of_uglobal_r ptenv p = (* FIXME: TC HOOK *) let fs = EcUnify.UniEnv.opentvi ptenv.pte_ue typ None in let ax = Fsubst.f_subst_tvar ~freshen:true fs ax in - let typ = List.map (fun (a, _) -> EcIdent.Mid.find a fs) typ in + let typ = List.map (fun a -> EcIdent.Mid.find a fs) typ in { ptev_env = ptenv; ptev_pt = ptglobal ~tys:typ p; @@ -515,7 +515,7 @@ let process_named_pterm pe (tvi, fp) = (* FIXME: TC HOOK *) let fs = EcUnify.UniEnv.opentvi pe.pte_ue typ tvi in let ax = Fsubst.f_subst_tvar ~freshen:false fs ax in - let typ = List.map (fun (a, _) -> EcIdent.Mid.find a fs) typ in + let typ = List.map (fun a -> EcIdent.Mid.find a fs) typ in (p, (typ, ax)) diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml index 2674da433..d4375e60b 100644 --- a/src/ecProofTyping.ml +++ b/src/ecProofTyping.ml @@ -7,6 +7,7 @@ open EcEnv open EcCoreGoal open EcAst open EcParsetree +open EcUnify module Msym = EcSymbols.Msym @@ -192,7 +193,7 @@ let tc1_process_Xhl_formula_xreal tc pf = (* FIXME: factor out to typing module *) (* FIXME: TC HOOK - check parameter constraints *) (* ------------------------------------------------------------------ *) -let pf_check_tvi (pe : proofenv) typ tvi = +let pf_check_tvi (pe : proofenv) (typ : EcDecl.ty_params) (tvi : tvar_inst option) = match tvi with | None -> () @@ -203,7 +204,7 @@ let pf_check_tvi (pe : proofenv) typ tvi = (List.length tyargs) (List.length typ) | Some (EcUnify.TVInamed tyargs) -> - let typnames = List.map (EcIdent.name |- fst) typ in + let typnames = List.map EcIdent.name typ in List.iter (fun (x, _) -> if not (List.mem x typnames) then diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 976c52312..3131af840 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1064,7 +1064,7 @@ let reduce_head simplify ri env hyps f = let body = EcFol.form_of_expr body in (* FIXME subst-refact can we do both subst in once *) let body = - Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in + Tvar.f_subst ~freshen:true op.EcDecl.op_tparams tys body in f_app (Fsubst.f_subst subst body) eargs f.f_ty @@ -1780,7 +1780,7 @@ module User = struct in doit empty_cst rule in let s_bds = Sid.of_list (List.map fst bds) - and s_tybds = Sid.of_list (List.map fst ax.ax_tparams) in + and s_tybds = Sid.of_list ax.ax_tparams in (* Variables appearing in types and formulas are always, respectively, * type and formula variables. diff --git a/src/ecScope.ml b/src/ecScope.ml index 1ab346c66..77e85a23e 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1384,7 +1384,7 @@ module Op = struct List.fold_left (fun scope (rname, xs, ax, codom) -> let ax = let opargs = List.map (fun (x, xty) -> e_local x xty) xs in - let opapp = List.map (tvar |- fst) tparams in + let opapp = List.map tvar tparams in let opapp = e_app (e_op opname opapp ty) opargs codom in let subst = EcSubst.add_opdef EcSubst.empty opname ([], opapp) in @@ -1399,10 +1399,10 @@ module Op = struct in let ax, axpm = - let bdpm = List.map fst tparams in + let bdpm = tparams in let axpm = List.map EcIdent.fresh bdpm in (Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) ax, - List.combine axpm (List.map snd tparams)) in + axpm) in let ax = { ax_tparams = axpm; ax_spec = ax; @@ -1419,10 +1419,10 @@ module Op = struct hierror ~loc "multiple names are only allowed for non-refined abstract operators"; let addnew scope name = - let nparams = List.map (fst_map EcIdent.fresh) tparams in + let nparams = List.map EcIdent.fresh tparams in let subst = Tvar.init - (List.map fst tparams) - (List.map (tvar |- fst) nparams) in + tparams + (List.map tvar nparams) in let rop = EcDecl.mk_op ~opaque:optransparent nparams (Tvar.subst subst ty) None lc in bind scope (unloc name, rop) in List.fold_left addnew scope op.po_aliases @@ -1439,8 +1439,8 @@ module Op = struct hierror "for tag %s, load Distr first" tag; let oppath = EcPath.pqname (path scope) (unloc op.po_name) in - let nparams = List.map (EcIdent.fresh |- fst) tyop.op_tparams in - let subst = Tvar.init (List.fst tyop.op_tparams) (List.map tvar nparams) in + let nparams = List.map EcIdent.fresh tyop.op_tparams in + let subst = Tvar.init tyop.op_tparams (List.map tvar nparams) in let ty = Tvar.subst subst tyop.op_ty in let aty, rty = EcTypes.tyfun_flat ty in @@ -1457,7 +1457,7 @@ module Op = struct let ax = EcFol.f_forall (List.map (snd_map gtty) bds) ax in let ax = - { ax_tparams = List.map (fun ty -> (ty, Sp.empty)) nparams; + { ax_tparams = nparams; ax_spec = ax; ax_kind = `Axiom (Ssym.empty, false); ax_loca = lc; @@ -2233,13 +2233,9 @@ module Ty = struct let env = env scope in let tyd_params, tyd_type = match body with - | PTYD_Abstract tcs -> - let tcs = - List.map - (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env)) - tcs in + | PTYD_Abstract -> let ue = TT.transtyvars env (loc, Some args) in - EcUnify.UniEnv.tparams ue, Abstract (Sp.of_list tcs) + EcUnify.UniEnv.tparams ue, Abstract | PTYD_Alias bd -> let ue = TT.transtyvars env (loc, Some args) in @@ -2273,7 +2269,7 @@ module Ty = struct let scope = let decl = EcDecl.{ tyd_params = []; - tyd_type = Abstract Sp.empty; + tyd_type = Abstract; tyd_loca = `Global; (* FIXME:SUBTYPE *) } in bind scope (unloc subtype.pst_name, decl) in @@ -2340,75 +2336,6 @@ module Ty = struct Ax.add_defer scope proofs - (* ------------------------------------------------------------------ *) - let bindclass ?(import = true) (scope : scope) (x, tc) = - assert (scope.sc_pr_uc = None); - let item = EcTheory.mkitem ~import (EcTheory.Th_typeclass(x, tc)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } - - (* ------------------------------------------------------------------ *) - let add_class (scope : scope) { pl_desc = tcd } = - assert (scope.sc_pr_uc = None); - let lc = tcd.ptc_loca in - let name = unloc tcd.ptc_name in - let scenv = (env scope) in - - check_name_available scope tcd.ptc_name; - - let tclass = - let uptc = - tcd.ptc_inth |> omap - (fun { pl_loc = uploc; pl_desc = uptc } -> - match EcEnv.TypeClass.lookup_opt uptc scenv with - | None -> hierror ~loc:uploc "unknown type-class: `%s'" - (string_of_qsymbol uptc) - | Some (tcp, _) -> tcp) - in - - let asty = - let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in - { tyd_params = []; - tyd_type = Abstract body; - tyd_loca = (lc :> locality); } in - let scenv = EcEnv.Ty.bind name asty scenv in - - (* Check for duplicated field names *) - Msym.odup unloc (List.map fst tcd.ptc_ops) - |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc - "duplicated operator name: `%s'" x.pl_desc); - Msym.odup unloc (List.map fst tcd.ptc_axs) - |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc - "duplicated axiom name: `%s'" x.pl_desc); - - (* Check operators types *) - let operators = - let check1 (x, ty) = - let ue = EcUnify.UniEnv.create (Some []) in - let ty = transty tp_tydecl scenv ue ty in - let uidmap = EcUnify.UniEnv.close ue in - let ty = ty_subst (Tuni.subst uidmap) ty in - (EcIdent.create (unloc x), ty) - in - tcd.ptc_ops |> List.map check1 in - - (* Check axioms *) - let axioms = - let scenv = EcEnv.Var.bind_locals operators scenv in - let check1 (x, ax) = - let ue = EcUnify.UniEnv.create (Some []) in - let ax = trans_prop scenv ue ax in - let uidmap = EcUnify.UniEnv.close ue in - let fs = Tuni.subst uidmap in - let ax = Fsubst.f_subst fs ax in - (unloc x, ax) - in - tcd.ptc_axs |> List.map check1 in - - (* Construct actual type-class *) - { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; tc_loca = lc} - in - bindclass scope (name, tclass) - (* ------------------------------------------------------------------ *) let check_tci_operators env tcty ops reqs = let ue = EcUnify.UniEnv.create (Some (fst tcty)) in @@ -2436,7 +2363,7 @@ module Ty = struct let op = EcEnv.Op.by_path p env in let opty = Tvar.subst - (Tvar.init (List.map fst op.op_tparams) tvi) + (Tvar.init op.op_tparams tvi) op.op_ty in (p, opty) diff --git a/src/ecScope.mli b/src/ecScope.mli index d64007674..283f1c4c1 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -135,7 +135,6 @@ module Ty : sig val add : ?src:string -> scope -> ptydecl located -> scope val add_subtype : scope -> psubtype located -> scope - val add_class : scope -> ptypeclass located -> scope val add_instance : scope -> Ax.proofmode -> ptycinstance located -> scope end diff --git a/src/ecSection.ml b/src/ecSection.ml index b87cf7b68..97ef2ea33 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -427,18 +427,15 @@ and on_oi (aenv : aenv) (oi : OI.t) = List.iter (on_xp aenv) (OI.allowed oi) (* -------------------------------------------------------------------- *) -and on_typeclasses (aenv : aenv) s = - Sp.iter (fun p -> aenv.cb (`Typeclass p)) s - -and on_typarams (aenv : aenv) typarams = - List.iter (fun (_,s) -> on_typeclasses aenv s) typarams +and on_typarams (_aenv : aenv) (_typarams : ty_params) = + () (* -------------------------------------------------------------------- *) and on_tydecl (aenv : aenv) (tyd : tydecl) = on_typarams aenv tyd.tyd_params; match tyd.tyd_type with | Concrete ty -> on_ty aenv ty - | Abstract s -> on_typeclasses aenv s + | Abstract -> () | Record (f, fds) -> on_form aenv f; List.iter (on_ty aenv |- snd) fds @@ -603,7 +600,7 @@ type to_clear = type to_gen = { tg_env : scenv; - tg_params : (EcIdent.t * Sp.t) list; + tg_params : ty_params; tg_binds : bind list; tg_subst : EcSubst.subst; tg_clear : to_clear; } @@ -650,15 +647,10 @@ let add_declared_mod to_gen id modty = let add_declared_ty to_gen path tydecl = assert (tydecl.tyd_params = []); - let s = - match tydecl.tyd_type with - | Abstract s -> s - | _ -> assert false in - let name = "'" ^ basename path in let id = EcIdent.create name in { to_gen with - tg_params = to_gen.tg_params @ [id, s]; + tg_params = to_gen.tg_params @ [id]; tg_subst = EcSubst.add_tydef to_gen.tg_subst path ([], tvar id); } @@ -722,7 +714,7 @@ let tydecl_fv tyd = let fv = match tyd.tyd_type with | Concrete ty -> ty_fv_and_tvar ty - | Abstract _ -> Mid.empty + | Abstract -> Mid.empty | Datatype tydt -> List.fold_left (fun fv (_, l) -> List.fold_left (fun fv ty -> @@ -731,7 +723,7 @@ let tydecl_fv tyd = | 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 + List.fold_left (fun fv id -> Mid.remove id fv) fv tyd.tyd_params let op_body_fv body ty = let fv = ty_fv_and_tvar ty in @@ -776,7 +768,7 @@ let notation_fv nota = EcIdent.fv_union (Mid.remove id fv) (ty_fv_and_tvar ty)) fv nota.ont_args let generalize_extra_ty to_gen fv = - List.filter (fun (id,_) -> Mid.mem id fv) to_gen.tg_params + List.filter (fun id -> Mid.mem id fv) to_gen.tg_params let rec generalize_extra_args binds fv = match binds with @@ -812,12 +804,12 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let fv = tydecl_fv tydecl in let extra = generalize_extra_ty to_gen fv in let tyd_params = extra @ tydecl.tyd_params in - let args = List.map (fun (id, _) -> tvar id) tyd_params in - let fst_params = List.map fst tydecl.tyd_params in - let tosubst = fst_params, tconstr path args in + let args = List.map tvar tyd_params in + let params = tydecl.tyd_params in + let tosubst = 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) -> let subst = EcSubst.empty in @@ -829,7 +821,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let tin = tconstr path args in let add_op (s, ty) = let p = pqname prefix s in - let tosubst = fst_params, e_op p args (tfun tin ty) in + let tosubst = params, e_op p args (tfun tin ty) in rsubst := EcSubst.add_opdef !rsubst p tosubst; rtg_subst := EcSubst.add_opdef !rtg_subst p tosubst; s, ty @@ -850,7 +842,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let tys = List.map subst_ty tys in let p = pqname prefix s in let pty = toarrow tys tout in - let tosubst = fst_params, e_op p args pty in + let tosubst = params, e_op p args pty in rsubst := EcSubst.add_opdef !rsubst p tosubst; rtg_subst := EcSubst.add_opdef !rtg_subst p tosubst ; s, tys in @@ -884,9 +876,8 @@ let generalize_opdecl to_gen prefix (name, operator) = let extra = generalize_extra_ty to_gen fv in let tparams = extra @ operator.op_tparams in let opty = operator.op_ty in - let args = List.map (fun (id, _) -> tvar id) tparams in - let tosubst = (List.map fst operator.op_tparams, - e_op path args opty) in + let args = List.map tvar tparams in + let tosubst = (operator.op_tparams, e_op path args opty) in let tg_subst = EcSubst.add_opdef to_gen.tg_subst path tosubst in tg_subst, mk_op ~opaque:operator.op_opaque tparams opty None `Global @@ -896,9 +887,8 @@ let generalize_opdecl to_gen prefix (name, operator) = let extra = generalize_extra_ty to_gen fv in let tparams = extra @ operator.op_tparams in let opty = operator.op_ty in - let args = List.map (fun (id, _) -> tvar id) tparams in - let tosubst = (List.map fst operator.op_tparams, - f_op path args opty) in + let args = List.map tvar tparams in + let tosubst = (operator.op_tparams, f_op path args opty) in let tg_subst = EcSubst.add_pddef to_gen.tg_subst path tosubst in tg_subst, mk_op ~opaque:operator.op_opaque tparams opty None `Global @@ -909,13 +899,12 @@ let generalize_opdecl to_gen prefix (name, operator) = let tparams = extra_t @ operator.op_tparams in let extra_a = generalize_extra_args to_gen.tg_binds fv in let opty = toarrow (List.map snd extra_a) operator.op_ty in - let t_args = List.map (fun (id, _) -> tvar id) tparams in + let t_args = List.map tvar tparams in let eop = e_op path t_args opty in let e = e_app eop (List.map (fun (id,ty) -> e_local id ty) extra_a) operator.op_ty in - let tosubst = - (List.map fst operator.op_tparams, e) in + let tosubst = (operator.op_tparams, e) in let tg_subst = EcSubst.add_opdef to_gen.tg_subst path tosubst in let body = @@ -948,13 +937,12 @@ let generalize_opdecl to_gen prefix (name, operator) = let op_tparams = extra_t @ operator.op_tparams in let extra_a = generalize_extra_args to_gen.tg_binds fv in let op_ty = toarrow (List.map snd extra_a) operator.op_ty in - let t_args = List.map (fun (id, _) -> tvar id) op_tparams in + let t_args = List.map tvar op_tparams in let fop = f_op path t_args op_ty in let f = f_app fop (List.map (fun (id,ty) -> f_local id ty) extra_a) operator.op_ty in - let tosubst = - (List.map fst operator.op_tparams, f) in + let tosubst = (operator.op_tparams, f) in let tg_subst = EcSubst.add_pddef to_gen.tg_subst path tosubst in let body = @@ -1124,7 +1112,6 @@ let rec set_lc_item lc_override item = | Th_axiom (s,ax) -> Th_axiom (s, { ax with ax_loca = set_lc lc_override ax.ax_loca }) | Th_modtype (s,ms) -> Th_modtype (s, { ms with tms_loca = set_lc lc_override ms.tms_loca }) | Th_module me -> Th_module { me with tme_loca = set_lc lc_override me.tme_loca } - | Th_typeclass (s,tc) -> Th_typeclass (s, { tc with tc_loca = set_lc lc_override tc.tc_loca }) | Th_theory (s, th) -> Th_theory (s, set_local_th lc_override th) | Th_export (p,lc) -> Th_export (p, set_lc lc_override lc) | Th_instance (ty,ti,lc) -> Th_instance (ty,ti, set_lc lc_override lc) @@ -1145,8 +1132,8 @@ let sc_decl_mod (id,mt) = SC_decl_mod (id,mt) (* ---------------------------------------------------------------- *) let is_abstract_ty = function - | Abstract _ -> true - | _ -> false + | Abstract -> true + | _ -> false (* let rec check_glob_mp_ty s scenv mp = @@ -1407,7 +1394,6 @@ let add_item_ ?(override_locality=None) (item : theory_item) (scenv:scenv) = | Th_axiom (s, ax) -> EcEnv.Ax.bind ~import s ax env | Th_modtype (s, ms) -> EcEnv.ModTy.bind ~import s ms env | Th_module me -> EcEnv.Mod.bind ~import me.tme_expr.me_name me env - | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind ~import s tc env | Th_export (p, lc) -> EcEnv.Theory.export p lc env | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance ~import tys i lc env (*FIXME: import? *) | Th_baserw (s,lc) -> EcEnv.BaseRw.add ~import s lc env @@ -1439,7 +1425,6 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i | Th_theory th -> (generalize_ctheory to_gen prefix th, None) | Th_export (p,lc) -> generalize_export to_gen (p,lc) | Th_instance (ty,i,lc) -> generalize_instance to_gen (ty,i,lc) - | Th_typeclass _ -> assert false | Th_baserw (s,lc) -> generalize_baserw to_gen prefix (s,lc) | Th_addrw (p,ps,lc) -> generalize_addrw to_gen (p, ps, lc) | Th_reduction rl -> generalize_reduction to_gen rl @@ -1540,7 +1525,6 @@ let check_item scenv item = | Th_axiom (s, ax) -> check_ax scenv prefix s ax | Th_modtype (s, ms) -> check_modtype scenv prefix s ms | Th_module me -> check_module scenv prefix me - | Th_typeclass (s,tc) -> check_typeclass scenv prefix s tc | Th_export (_, lc) -> assert (lc = `Global || scenv.sc_insec); | Th_instance (ty,tci,lc) -> check_instance scenv ty tci lc | Th_baserw (_,lc) -> diff --git a/src/ecSmt.ml b/src/ecSmt.ml index c6119dff3..fdc3d18f6 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -266,14 +266,14 @@ let trans_tv lenv id = oget (Mid.find_opt id lenv.le_tv) (* -------------------------------------------------------------------- *) let lenv_of_tparams ts = - let trans_tv env ((id, _) : ty_param) = (* FIXME: TC HOOK *) + let trans_tv env (id : ty_param) = (* FIXME: TC HOOK *) let tv = WTy.create_tvsymbol (preid id) in { env with le_tv = Mid.add id (WTy.ty_var tv) env.le_tv }, tv in List.map_fold trans_tv empty_lenv ts let lenv_of_tparams_for_hyp genv ts = - let trans_tv env ((id, _) : ty_param) = (* FIXME: TC HOOK *) + let trans_tv env (id : ty_param) = (* FIXME: TC HOOK *) let ts = WTy.create_tysymbol (preid id) [] WTy.NoDef in genv.te_task <- WTask.add_ty_decl genv.te_task ts; { env with le_tv = Mid.add id (WTy.ty_app ts []) env.le_tv }, ts @@ -400,7 +400,7 @@ 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) @@ -415,7 +415,7 @@ and trans_tydecl genv (p, tydecl) = Hp.add genv.te_ty p ts; - let wdom = tconstr p (List.map (tvar |- fst) tydecl.tyd_params) in + let wdom = tconstr p (List.map tvar tydecl.tyd_params) in let wdom = trans_ty (genv, lenv) wdom in let for_ctor (c, ctys) = @@ -434,7 +434,7 @@ and trans_tydecl genv (p, tydecl) = Hp.add genv.te_ty p ts; - let wdom = tconstr p (List.map (tvar |- fst) tydecl.tyd_params) in + let wdom = tconstr p (List.map tvar tydecl.tyd_params) in let wdom = trans_ty (genv, lenv) wdom in let for_field (fname, fty) = @@ -1034,9 +1034,9 @@ and create_op ?(body = false) (genv : tenv) p = let lenv, wparams = lenv_of_tparams op.op_tparams in let dom, codom = EcEnv.Ty.signature genv.te_env op.op_ty in let textra = - List.filter (fun (tv,_) -> not (Mid.mem tv (EcTypes.Tvar.fv op.op_ty))) op.op_tparams in + List.filter (fun tv -> not (Mid.mem tv (EcTypes.Tvar.fv op.op_ty))) op.op_tparams in let textra = - List.map (fun (tv,_) -> trans_ty (genv,lenv) (tvar tv)) textra in + List.map (fun tv -> trans_ty (genv,lenv) (tvar tv)) textra in let wdom = trans_tys (genv, lenv) dom in let wcodom = if ER.EqTest.is_bool genv.te_env codom diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 33274e240..9084b3281 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -818,15 +818,10 @@ let subst_top_module (s : subst) (m : top_module_expr) = tme_loca = m.tme_loca; } (* -------------------------------------------------------------------- *) -let subst_typeclass (s : subst) (tcs : Sp.t) = - Sp.map (subst_path s) tcs - -(* -------------------------------------------------------------------- *) -let fresh_tparam (s : subst) ((x, tcs) : ty_param) = +let fresh_tparam (s : subst) (x : ty_param) = let newx = EcIdent.fresh x in - let tcs = subst_typeclass s tcs in let s = add_tyvar s x (tvar newx) in - (s, (newx, tcs)) + (s, newx) (* -------------------------------------------------------------------- *) let fresh_tparams (s : subst) (tparams : ty_params) = @@ -841,8 +836,8 @@ 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 -> + Abstract | Concrete ty -> Concrete (subst_ty s ty) @@ -1042,9 +1037,6 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = | Th_instance (ty, tci, lc) -> Th_instance (subst_genty s ty, subst_instance s tci, lc) - | Th_typeclass (x, tc) -> - Th_typeclass (x, subst_tc s tc) - | Th_baserw _ -> item @@ -1103,12 +1095,12 @@ let init_tparams (params : (EcIdent.t * ty) list) : subst = (* -------------------------------------------------------------------- *) let open_oper op tys = - let s = List.combine (List.fst op.op_tparams) tys in + let s = List.combine op.op_tparams tys in let s = init_tparams s in (subst_ty s op.op_ty, subst_op_kind s op.op_kind) let open_tydecl tyd tys = - let s = List.combine (List.fst tyd.tyd_params) tys in + let s = List.combine tyd.tyd_params tys in let s = init_tparams s in subst_tydecl_body s tyd.tyd_type @@ -1181,4 +1173,4 @@ let ss_inv_forall_ml_ts_inv menvl inv = let ss_inv_forall_mr_ts_inv menvr inv = let inv' = f_forall_mems [menvr] (ts_inv_rebind_right inv (fst menvr)).inv in - { inv=inv'; m=inv.ml } \ No newline at end of file + { inv=inv'; m=inv.ml } diff --git a/src/ecSubst.mli b/src/ecSubst.mli index 5ad3879db..e39246835 100644 --- a/src/ecSubst.mli +++ b/src/ecSubst.mli @@ -44,7 +44,6 @@ val subst_ax : subst -> axiom -> axiom val subst_op : subst -> operator -> operator val subst_op_body : subst -> opbody -> opbody val subst_tydecl : subst -> tydecl -> tydecl -val subst_tc : subst -> typeclass -> typeclass val subst_theory : subst -> theory -> theory val subst_branches : subst -> opbranches -> opbranches diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 2731d928b..5daaded83 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -458,7 +458,6 @@ end = struct (loced (thd @ prefix, x), mode) | Th_instance _ -> (proofs, evc) - | Th_typeclass _ -> (proofs, evc) | Th_baserw _ -> (proofs, evc) | Th_addrw _ -> (proofs, evc) diff --git a/src/ecTheory.ml b/src/ecTheory.ml index ffe226d06..c4bcbfe19 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -27,7 +27,6 @@ and theory_item_r = | Th_theory of (symbol * ctheory) | Th_export of EcPath.path * is_local | Th_instance of (ty_params * EcTypes.ty) * tcinstance * is_local - | Th_typeclass of (symbol * typeclass) | Th_baserw of symbol * is_local | Th_addrw of EcPath.path * EcPath.path list * is_local | Th_reduction of (EcPath.path * rule_option * rule option) list diff --git a/src/ecTheory.mli b/src/ecTheory.mli index f246ee3f4..20c34364b 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -23,7 +23,6 @@ and theory_item_r = | Th_theory of (symbol * ctheory) | Th_export of EcPath.path * is_local | Th_instance of (ty_params * EcTypes.ty) * tcinstance * is_local - | Th_typeclass of (symbol * typeclass) | Th_baserw of symbol * is_local | Th_addrw of EcPath.path * EcPath.path list * is_local (* reduction rule does not survive to section so no locality *) diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index a6af17b16..92c8c2369 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -159,7 +159,7 @@ end = struct let rec tybody (hyps : EcEnv.LDecl.hyps) (ty_body1 : ty_body) (ty_body2 : ty_body) = match ty_body1, ty_body2 with - | Abstract _ , Abstract _ -> () (* FIXME Sp.t *) + | Abstract , Abstract -> () | Concrete ty1 , Concrete ty2 -> check (EcReduction.EqTest.for_type (toenv hyps) ty1 ty2) | Datatype ty1 , Datatype ty2 -> for_datatype hyps ty1 ty2 | Record rec1, Record rec2 -> for_record hyps rec1 rec2 @@ -180,14 +180,15 @@ end = struct for_tparams params tyd2.tyd_params; - let tparams = List.map (fun (id,_) -> tvar id) params in + let tparams = List.map tvar params in let ty_body1 = tyd1.tyd_type in let ty_body2 = EcSubst.open_tydecl tyd2 tparams in let hyps = EcEnv.LDecl.init env params in match ty_body1, ty_body2 with - | Abstract _, _ -> () (* FIXME Sp.t *) + | Abstract, _ -> () + | _, _ -> tybody hyps ty_body1 ty_body2 with CoreIncompatible -> raise (Incompatible TyBody) @@ -296,7 +297,7 @@ end = struct for_tparams oper1.op_tparams oper2.op_tparams; let oty1, okind1 = oper1.op_ty, oper1.op_kind in - let tparams = List.map (fun (id,_) -> tvar id) params in + let tparams = List.map tvar params in let oty2, okind2 = EcSubst.open_oper oper2 tparams in if not (EcReduction.EqTest.for_type env oty1 oty2) then @@ -422,9 +423,9 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd let newtyd, body = match tydov with | `BySyntax (nargs, ntyd) -> - let nargs = List.map2 - (fun (_, tc) x -> (EcIdent.create (unloc x), tc)) - otyd.tyd_params nargs in + let nargs = List.map + (fun x -> (EcIdent.create (unloc x))) + nargs in let ue = EcUnify.UniEnv.create (Some nargs) in let ntyd = EcTyping.transty EcTyping.tp_tydecl env ue ntyd in let decl = @@ -437,7 +438,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | `ByPath p -> begin match EcEnv.Ty.by_path_opt p env with | Some reftyd -> - let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) reftyd.tyd_params in + let tyargs = List.map tvar reftyd.tyd_params in let body = tconstr p tyargs in let decl = { reftyd with tyd_type = Concrete body; } in (decl, body) @@ -464,7 +465,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | `Inline _ -> let subst = EcSubst.add_tydef - subst (xpath ove x) (List.map fst newtyd.tyd_params, body) in + subst (xpath ove x) (newtyd.tyd_params, body) in let subst = (* FIXME: HACK *) @@ -472,10 +473,10 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | Datatype { tydt_ctors = octors }, Tconstr (np, _) -> begin match (EcEnv.Ty.by_path np env).tyd_type with | Datatype { tydt_ctors = _ } -> - let newtparams = List.fst newtyd.tyd_params in + let newtparams = newtyd.tyd_params in let newtparams_ty = List.map tvar newtparams in let newdtype = tconstr np newtparams_ty in - let tysubst = CS.Tvar.init (List.fst otyd.tyd_params) newtparams_ty in + let tysubst = CS.Tvar.init otyd.tyd_params newtparams_ty in List.fold_left (fun subst (name, tyargs) -> let np = EcPath.pqoname (EcPath.prefix np) name in @@ -536,7 +537,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = let newop, body = match opov with | `BySyntax opov -> - let tp = opov.opov_tyvars |> omap (List.map (fun tv -> (tv, []))) in + let tp = opov.opov_tyvars in let ue = EcTyping.transtyvars env (loc, tp) in let tp = EcTyping.tp_relax in let (ty, body) = @@ -548,8 +549,8 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = in begin try Compatible.for_ty env ue - (List.map fst reftyvars, refty) - (List.map fst (EcUnify.UniEnv.tparams ue), ty) + (reftyvars, refty) + (EcUnify.UniEnv.tparams ue, ty) with Incompatible err -> clone_error env (CE_OpIncompatible ((snd ove.ovre_prefix, x), err)) end; @@ -571,7 +572,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = | `ByPath p -> begin match EcEnv.Op.by_path_opt p env with | Some ({ op_kind = OB_oper _ } as refop) -> - let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) refop.op_tparams in + let tyargs = List.map tvar refop.op_tparams in let body = if refop.op_clinline then (match refop.op_kind with @@ -608,7 +609,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = with EcFol.CannotTranslate -> clone_error env (CE_InlinedOpIsForm (snd ove.ovre_prefix, x)) in - let subst1 = (List.map fst newop.op_tparams, body) in + let subst1 = (newop.op_tparams, body) in let subst = EcSubst.add_opdef subst (xpath ove x) subst1 in (newop, subst, x, false) in @@ -658,7 +659,7 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) = let newpr, body = match prov with | `BySyntax prov -> - let tp = prov.prov_tyvars |> omap (List.map (fun tv -> (tv, []))) in + let tp = prov.prov_tyvars in let ue = EcTyping.transtyvars env (loc, tp) in let body = let env, xs = EcTyping.trans_binding env ue prov.prov_args in @@ -671,8 +672,8 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) = begin try Compatible.for_ty env ue - (List.map fst reftyvars, refty) - (List.map fst (EcUnify.UniEnv.tparams ue), body.f_ty) + (reftyvars, refty) + (EcUnify.UniEnv.tparams ue, body.f_ty) with Incompatible err -> clone_error env (CE_OpIncompatible ((snd ove.ovre_prefix, x), err)) @@ -698,7 +699,7 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) = | `ByPath p -> begin match EcEnv.Op.by_path_opt p env with | Some ({ op_kind = OB_pred _ } as refop) -> - let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) refop.op_tparams in + let tyargs = List.map tvar refop.op_tparams in let body = if refop.op_clinline then (match refop.op_kind with @@ -733,7 +734,7 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) = (newpr, subst, x) | `Inline _ -> - let subst1 = (List.map fst newpr.op_tparams, body) in + let subst1 = (newpr.op_tparams, body) in let subst = EcSubst.add_pddef subst (xpath ove x) subst1 in (newpr, subst, x) @@ -941,14 +942,6 @@ and replay_reduction (subst, ops, proofs, scope) -(* -------------------------------------------------------------------- *) -and replay_typeclass - (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, tc) -= - let tc = EcSubst.subst_tc subst tc in - let scope = ove.ovre_hooks.hadd_item scope ~import (Th_typeclass (x, tc)) in - (subst, ops, proofs, scope) - (* -------------------------------------------------------------------- *) and replay_instance (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (typ, ty), tc, lc) @@ -1081,9 +1074,6 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) = | Th_auto at_base -> replay_auto ove (subst, ops, proofs, scope) (import, at_base) - | Th_typeclass (x, tc) -> - replay_typeclass ove (subst, ops, proofs, scope) (import, x, tc) - | Th_instance ((typ, ty), tc, lc) -> replay_instance ove (subst, ops, proofs, scope) (import, (typ, ty), tc, lc) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 6af2f28e3..593b78b72 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -206,8 +206,6 @@ let unify_or_fail (env : EcEnv.env) ue loc ~expct:ty1 ty2 = let tyinst = ty_subst (Tuni.subst uidmap) in tyerror loc env (TypeMismatch ((tyinst ty1, tyinst ty2), (tyinst t1, tyinst t2))) - | `TcCtt _ -> - tyerror loc env TypeClassMismatch (* -------------------------------------------------------------------- *) let add_glob (m:Sx.t) (x:prog_var) : Sx.t = @@ -486,8 +484,8 @@ let transtcs (env : EcEnv.env) tcs = let transtyvars (env : EcEnv.env) (loc, tparams) = let tparams = tparams |> omap (fun tparams -> - let for1 ({ pl_desc = x }, tc) = (EcIdent.create x, transtcs env tc) in - if not (List.is_unique (List.map (unloc |- fst) tparams)) then + let for1 ({ pl_desc = x }) = (EcIdent.create x) in + if not (List.is_unique (List.map unloc tparams)) then tyerror loc env DuplicatedTyVar; List.map for1 tparams) in @@ -1089,7 +1087,7 @@ let transpattern1 env ue (p : EcParsetree.plpattern) = let recty = oget (EcEnv.Ty.by_path_opt recp env) in let rec_ = snd (oget (EcDecl.tydecl_as_record recty)) in - let reccty = tconstr recp (List.map (tvar |- fst) recty.tyd_params) in + let reccty = tconstr recp (List.map tvar recty.tyd_params) in let reccty, rectvi = EcUnify.UniEnv.openty ue recty.tyd_params None reccty in let fields = List.fold_left @@ -1229,9 +1227,9 @@ let trans_record env ue (subtt, proj) (loc, b, fields) = let recty = oget (EcEnv.Ty.by_path_opt recp env) in let rec_ = snd (oget (EcDecl.tydecl_as_record recty)) in - let reccty = tconstr recp (List.map (tvar |- fst) recty.tyd_params) in + let reccty = tconstr recp (List.map tvar recty.tyd_params) in let reccty, rtvi = EcUnify.UniEnv.openty ue recty.tyd_params None reccty in - let tysopn = Tvar.init (List.map fst recty.tyd_params) rtvi in + let tysopn = Tvar.init recty.tyd_params rtvi in let fields = List.fold_left diff --git a/src/ecUnify.ml b/src/ecUnify.ml index 4664a8a71..0fff10aa6 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -13,12 +13,12 @@ module Sp = EcPath.Sp module TC = EcTypeClass (* -------------------------------------------------------------------- *) -exception UnificationFailure of [`TyUni of ty * ty | `TcCtt of ty * Sp.t] +type pb = [ `TyUni of ty * ty ] + +exception UnificationFailure of pb exception UninstantiateUni (* -------------------------------------------------------------------- *) -type pb = [ `TyUni of ty * ty | `TcCtt of ty * Sp.t ] - module UFArgs = struct module I = struct type t = uid @@ -28,31 +28,29 @@ module UFArgs = struct end module D = struct - type data = Sp.t * ty option + type data = ty option type effects = pb list let default : data = - (Sp.empty, None) + None - let isvoid ((_, x) : data) = - (x = None) + let isvoid (x : data) = + Option.is_none x - let noeffects : effects = [] + let noeffects : effects = + [] - let union d1 d2 = + let union (d1 : data) (d2 : data) = match d1, d2 with - | (tc1, None), (tc2, None) -> - ((Sp.union tc1 tc2, None), []) - - | (tc1, Some ty1), (tc2, Some ty2) -> - ((Sp.union tc1 tc2, Some ty1), [`TyUni (ty1, ty2)]) - - | (tc1, None ), (tc2, Some ty) - | (tc2, Some ty), (tc1, None ) -> - let tc = Sp.diff tc1 tc2 in - if Sp.is_empty tc - then ((Sp.union tc1 tc2, Some ty), []) - else ((Sp.union tc1 tc2, Some ty), [`TcCtt (ty, tc)]) + | None, None -> + (None, []) + + | Some ty1, Some ty2 -> + (Some ty1, [`TyUni (ty1, ty2)]) + + | None , Some ty + | Some ty, None -> + (Some ty, []) end end @@ -60,49 +58,25 @@ module UF = EcUFind.Make(UFArgs.I)(UFArgs.D) (* -------------------------------------------------------------------- *) module UnifyCore = struct - let fresh ?(tc = Sp.empty) ?ty uf = + let fresh ?ty uf = let uid = EcUid.unique () in let uf = match ty with | Some { ty_node = Tunivar id } -> - let uf = UF.set uid (tc, None) uf in - fst (UF.union uid id uf) - | None | Some _ -> UF.set uid (tc, ty) uf + let uf = UF.set uid None uf in + fst (UF.union uid id uf) + | None | Some _ -> UF.set uid ty uf in (uf, tuni uid) end (* -------------------------------------------------------------------- *) -let rec unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) pb = +let unify_core (env : EcEnv.env) (uf : UF.t) pb = let failure () = raise (UnificationFailure pb) in - let gr = EcEnv.TypeClass.graph env in - let inst = EcEnv.TypeClass.get_instances env in - let uf = ref uf in let pb = let x = Queue.create () in Queue.push pb x; x in - let instances_for_tcs tcs = - let tcfilter (i, tc) = - match tc with `General p -> Some (i, p) | _ -> None - in - List.filter - (fun (_, tc1) -> - Sp.for_all - (fun tc2 -> TC.Graph.has_path ~src:tc1 ~dst:tc2 gr) - tcs) - (List.pmap tcfilter inst) - in - - let has_tcs ~src ~dst = - Sp.for_all - (fun dst1 -> - Sp.exists - (fun src1 -> TC.Graph.has_path ~src:src1 ~dst:dst1 gr) - src) - dst - in - let ocheck i t = let i = UF.find i !uf in let map = Hint.create 0 in @@ -115,7 +89,7 @@ let rec unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) pb = | _ when i = i' -> true | _ when Hint.mem map i' -> false | _ -> - match snd (UF.data i' !uf) with + match UF.data i' !uf with | None -> Hint.add map i' (); false | Some t -> match doit t with @@ -129,15 +103,15 @@ let rec unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) pb = in let setvar i t = - let (ti, effects) = UFArgs.D.union (UF.data i !uf) (Sp.empty, Some t) in - if odfl false (snd ti |> omap (ocheck i)) then failure (); + let (ti, effects) = UFArgs.D.union (UF.data i !uf) (Some t) in + if odfl false (ti |> omap (ocheck i)) then failure (); List.iter (Queue.push^~ pb) effects; uf := UF.set i ti !uf and getvar t = match t.ty_node with - | Tunivar i -> snd_map (odfl t) (UF.data i !uf) - | _ -> (Sp.empty, t) + | Tunivar i -> odfl t (UF.data i !uf) + | _ -> t in @@ -145,7 +119,7 @@ let rec unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) pb = while not (Queue.is_empty pb) do match Queue.pop pb with | `TyUni (t1, t2) -> begin - let (t1, t2) = (snd (getvar t1), snd (getvar t2)) in + let (t1, t2) = (getvar t1, getvar t2) in match ty_equal t1 t2 with | true -> () @@ -181,49 +155,6 @@ let rec unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) pb = | _, _ -> failure () end end - - | `TcCtt (ty, tc) -> begin - let tytc, ty = getvar ty in - - match ty.ty_node with - | Tunivar i -> - uf := UF.set i (Sp.union tc tytc, None) !uf - - | Tvar x -> - let xtcs = odfl Sp.empty (Mid.find_opt x tvtc) in - if not (has_tcs ~src:xtcs ~dst:tc) then - failure () - - | _ -> - if not (has_tcs ~src:tytc ~dst:tc) then - let module E = struct exception Failure end in - - let inst = instances_for_tcs tc in - - let for1 uf p = - let for_inst ((typ, gty), p') = - try - if not (TC.Graph.has_path ~src:p' ~dst:p gr) then - raise E.Failure; - let (uf, gty) = - let (uf, subst) = - List.fold_left - (fun (uf, s) (v, tc) -> - let (uf, uid) = UnifyCore.fresh ~tc uf in - (uf, Mid.add v uid s)) - (uf, Mid.empty) typ - in - (uf, Tvar.subst subst gty) - in - try Some (unify_core env tvtc uf (`TyUni (gty, ty))) - with UnificationFailure _ -> raise E.Failure - with E.Failure -> None - in - try List.find_map for_inst inst - with Not_found -> failure () - in - uf := List.fold_left for1 !uf (Sp.elements tc) - end done in doit (); !uf @@ -239,7 +170,7 @@ let close (uf : UF.t) = | Some t -> t | None -> begin let t = - match snd (UF.data i uf) with + match UF.data i uf with | None -> tuni (UF.find i uf) | Some t -> doit t in @@ -271,7 +202,6 @@ let subst_of_uf (uf : UF.t) = type unienv_r = { ue_uf : UF.t; ue_named : EcIdent.t Mstr.t; - ue_tvtc : Sp.t Mid.t; ue_decl : EcIdent.t list; ue_closed : bool; } @@ -292,7 +222,7 @@ module UniEnv = struct let restore ~(dst:unienv) ~(src:unienv) = dst := !src - let getnamed ue x = + let getnamed (ue : unienv) (x : symbol) = match Mstr.find_opt x (!ue).ue_named with | Some a -> a | None -> begin @@ -304,11 +234,10 @@ module UniEnv = struct }; id end - let create (vd : (EcIdent.t * Sp.t) list option) = + let create (vd : EcIdent.t list option) = let ue = { ue_uf = UF.initial; ue_named = Mstr.empty; - ue_tvtc = Mid.empty; ue_decl = []; ue_closed = false; } in @@ -317,59 +246,58 @@ module UniEnv = struct match vd with | None -> ue | Some vd -> - let vdmap = List.map (fun (x, _) -> (EcIdent.name x, x)) vd in - { ue with - ue_named = Mstr.of_list vdmap; - ue_tvtc = Mid.of_list vd; - ue_decl = List.rev_map fst vd; - ue_closed = true; } + let vdmap = List.map (fun x -> (EcIdent.name x, x)) vd in + { ue with + ue_named = Mstr.of_list vdmap; + ue_decl = List.rev vd; + ue_closed = true; } in ref ue - let fresh ?tc ?ty ue = - let (uf, uid) = UnifyCore.fresh ?tc ?ty (!ue).ue_uf in + let fresh ?(ty : ty option) (ue : unienv) = + let (uf, uid) = UnifyCore.fresh ?ty (!ue).ue_uf in ue := { !ue with ue_uf = uf }; uid - let opentvi ue (params : ty_params) tvi = + let opentvi (ue : unienv) (params : ty_params) (tvi : tvar_inst option) = match tvi with | None -> List.fold_left - (fun s (v, tc) -> Mid.add v (fresh ~tc ue) s) + (fun s v -> Mid.add v (fresh ue) s) Mid.empty params | Some (TVIunamed lt) -> List.fold_left2 - (fun s (v, tc) ty -> Mid.add v (fresh ~tc ~ty ue) s) + (fun s v ty -> Mid.add v (fresh ~ty ue) s) Mid.empty params lt | Some (TVInamed lt) -> - let for1 s (v, tc) = + let for1 s v = let t = - try fresh ~tc ~ty:(List.assoc (EcIdent.name v) lt) ue - with Not_found -> fresh ~tc ue + try fresh ~ty:(List.assoc (EcIdent.name v) lt) ue + with Not_found -> fresh ue in Mid.add v t s in List.fold_left for1 Mid.empty params - let subst_tv subst params = - List.map (fun (tv, _) -> subst (tvar tv)) params + let subst_tv (subst : ty -> ty) (params : ty_params) = + List.map (fun tv -> subst (tvar tv)) params - let openty_r ue params tvi = + let openty_r (ue : unienv) (params : ty_params) (tvi : tvar_inst option) = let subst = f_subst_init ~tv:(opentvi ue params tvi) () in (subst, subst_tv (ty_subst subst) params) - let opentys ue params tvi tys = + let opentys (ue : unienv) (params : ty_params) (tvi : tvar_inst option) (tys : ty list) = let (subst, tvs) = openty_r ue params tvi in (List.map (ty_subst subst) tys, tvs) - let openty ue params tvi ty = + let openty (ue : unienv) (params : ty_params) (tvi : tvar_inst option) (ty : ty)= let (subst, tvs) = openty_r ue params tvi in (ty_subst subst ty, tvs) let repr (ue : unienv) (t : ty) : ty = match t.ty_node with - | Tunivar id -> odfl t (snd (UF.data id (!ue).ue_uf)) + | Tunivar id -> odfl t (UF.data id (!ue).ue_uf) | _ -> t let closed (ue : unienv) = @@ -379,21 +307,17 @@ module UniEnv = struct if not (closed ue) then raise UninstantiateUni; (subst_of_uf (!ue).ue_uf) - let assubst ue = subst_of_uf (!ue).ue_uf + let assubst (ue : unienv) = + subst_of_uf (!ue).ue_uf - let tparams ue = - let fortv x = odfl Sp.empty (Mid.find_opt x (!ue).ue_tvtc) in - List.map (fun x -> (x, fortv x)) (List.rev (!ue).ue_decl) + let tparams (ue : unienv) : ty_params = + List.rev (!ue).ue_decl end (* -------------------------------------------------------------------- *) -let unify env ue t1 t2 = - let uf = unify_core env (!ue).ue_tvtc (!ue).ue_uf (`TyUni (t1, t2)) in - ue := { !ue with ue_uf = uf; } - -let hastc env ue ty tc = - let uf = unify_core env (!ue).ue_tvtc (!ue).ue_uf (`TcCtt (ty, tc)) in - ue := { !ue with ue_uf = uf; } +let unify (env : EcEnv.env) (ue : unienv) (t1 : ty) (t2 : ty) = + let uf = unify_core env (!ue).ue_uf (`TyUni (t1, t2)) in + ue := { !ue with ue_uf = uf; } (* -------------------------------------------------------------------- *) let tfun_expected ue ?retty psig = @@ -404,11 +328,25 @@ let tfun_expected ue ?retty psig = type sbody = ((EcIdent.t * ty) list * expr) Lazy.t (* -------------------------------------------------------------------- *) -let select_op ?(hidden = false) ?(filter = fun _ _ -> true) tvi env name ue (psig, retty) = +type select_result = (EcPath.path * ty list) * ty * unienv * sbody option + +(* -------------------------------------------------------------------- *) +let select_op + ?(hidden : bool = false) + ?(filter : EcPath.path -> operator -> bool = fun _ _ -> true) + (tvi : tvar_inst option) + (env : EcEnv.env) + (name : qsymbol) + (ue : unienv) + (sig_ : ty list * ty option) + : select_result list += ignore hidden; (* FIXME *) let module D = EcDecl in + let (psig, retty) = sig_ in + let filter oppath op = (* Filter operator based on given type variables instanciation *) let filter_on_tvi = @@ -422,9 +360,9 @@ let select_op ?(hidden = false) ?(filter = fun _ _ -> true) tvi env name ue (psi List.length tparams = len | Some (TVInamed ls) -> fun op -> - let tparams = List.map (fst_map EcIdent.name) op.D.op_tparams in - let tparams = Msym.of_list tparams in - List.for_all (fun (x, _) -> Msym.mem x tparams) ls + let tparams = List.map EcIdent.name op.D.op_tparams in + let tparams = Ssym.of_list tparams in + List.for_all (fun (x, _) -> Msym.mem x tparams) ls in filter oppath op && filter_on_tvi op @@ -436,25 +374,6 @@ let select_op ?(hidden = false) ?(filter = fun _ _ -> true) tvi env name ue (psi let subue = UniEnv.copy ue in try - begin try - match tvi with - | None -> - () - - | Some (TVIunamed lt) -> - List.iter2 - (fun ty (_, tc) -> hastc env subue ty tc) - lt op.D.op_tparams - - | Some (TVInamed ls) -> - let tparams = List.map (fst_map EcIdent.name) op.D.op_tparams in - let tparams = Msym.of_list tparams in - List.iter (fun (x, ty) -> - hastc env subue ty (oget (Msym.find_opt x tparams))) - ls - with UnificationFailure _ -> raise E.Failure - end; - let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in let top = ty_subst tip op.D.op_ty in let texpected = tfun_expected subue ?retty psig in diff --git a/src/ecUnify.mli b/src/ecUnify.mli index 1f6ed3e45..d19596eb6 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -6,7 +6,7 @@ open EcTypes open EcDecl (* -------------------------------------------------------------------- *) -exception UnificationFailure of [`TyUni of ty * ty | `TcCtt of ty * Sp.t] +exception UnificationFailure of [`TyUni of ty * ty] exception UninstantiateUni type unienv @@ -19,10 +19,10 @@ type tvi = tvar_inst option type uidmap = uid -> ty option module UniEnv : sig - val create : (EcIdent.t * Sp.t) list option -> unienv + val create : ty_params option -> unienv val copy : unienv -> unienv (* constant time *) val restore : dst:unienv -> src:unienv -> unit (* constant time *) - val fresh : ?tc:EcPath.Sp.t -> ?ty:ty -> unienv -> ty + val fresh : ?ty:ty -> unienv -> ty val getnamed : unienv -> symbol -> EcIdent.t val repr : unienv -> ty -> ty val opentvi : unienv -> ty_params -> tvi -> ty EcIdent.Mid.t @@ -35,12 +35,13 @@ module UniEnv : sig end val unify : EcEnv.env -> unienv -> ty -> ty -> unit -val hastc : EcEnv.env -> unienv -> ty -> Sp.t -> unit val tfun_expected : unienv -> ?retty:ty -> EcTypes.ty list -> EcTypes.ty type sbody = ((EcIdent.t * ty) list * expr) Lazy.t +type select_result = (EcPath.path * ty list) * ty * unienv * sbody option + val select_op : ?hidden:bool -> ?filter:(path -> operator -> bool) @@ -49,4 +50,4 @@ val select_op : -> qsymbol -> unienv -> dom * ty option - -> ((EcPath.path * ty list) * ty * unienv * sbody option) list + -> select_result list