From d2f69ec476caee3e35f6c666bfb63235cabf56fa Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 16 Dec 2024 09:27:01 +0100 Subject: [PATCH] merge typing of expressions and formulas --- dune-project | 4 +- easycrypt.opam | 2 +- src/dune | 3 +- src/ecParser.mly | 158 +----------------------------- src/ecParsetree.ml | 80 ++++++--------- src/ecTyping.ml | 235 ++++++--------------------------------------- 6 files changed, 68 insertions(+), 414 deletions(-) diff --git a/dune-project b/dune-project index a8bc5091e4..2afc50b059 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ -(lang dune 3.6) -(using menhir 2.0) +(lang dune 3.13) +(using menhir 3.0) (using dune_site 0.1) (wrapped_executables false) diff --git a/easycrypt.opam b/easycrypt.opam index 4803cf34a2..04aa7e8f02 100644 --- a/easycrypt.opam +++ b/easycrypt.opam @@ -4,7 +4,7 @@ depends: [ "batteries" {>= "3"} "camlp-streams" {>= "5"} "camlzip" - "dune" {>= "3.6" & >= "3.6"} + "dune" {>= "3.13" & >= "3.6"} "dune-build-info" "dune-site" "ocaml-inifiles" {>= "1.2"} diff --git a/src/dune b/src/dune index 1a5090d1e9..165e935b92 100644 --- a/src/dune +++ b/src/dune @@ -29,4 +29,5 @@ (menhir (modules ecParser) - (flags --table --explain)) + (explain true) + (flags --table)) diff --git a/src/ecParser.mly b/src/ecParser.mly index 71dfbc9b26..6a188d34e6 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -39,21 +39,9 @@ in try Some (nm, unloc name) with E.Invalid -> None - let mk_peid_symb loc s ti = - mk_loc loc (PEident (pqsymb_of_symb loc s, ti)) - let mk_pfid_symb loc s ti = mk_loc loc (PFident (pqsymb_of_symb loc s, ti)) - let peapp_symb loc s ti es = - PEapp (mk_peid_symb loc s ti, es) - - let peget loc ti e1 e2 = - peapp_symb loc EcCoreLib.s_get ti [e1;e2] - - let peset loc ti e1 e2 e3 = - peapp_symb loc EcCoreLib.s_set ti [e1;e2;e3] - let pfapp_symb loc s ti es = PFapp(mk_pfid_symb loc s ti, es) @@ -63,15 +51,6 @@ let pfset loc ti e1 e2 e3 = pfapp_symb loc EcCoreLib.s_set ti [e1;e2;e3] - let pe_nil loc ti = - mk_peid_symb loc EcCoreLib.s_nil ti - - let pe_cons loc ti e1 e2 = - mk_loc loc (peapp_symb loc EcCoreLib.s_cons ti [e1; e2]) - - let pelist loc ti (es : pexpr list) : pexpr = - List.fold_right (fun e1 e2 -> pe_cons loc ti e1 e2) es (pe_nil loc ti) - let pf_nil loc ti = mk_pfid_symb loc EcCoreLib.s_nil ti @@ -917,139 +896,8 @@ tyvar_annot: | LTCOLON k=loc(tyvar_annot) GT { k } (* -------------------------------------------------------------------- *) -%inline sexpr: x=loc(sexpr_u) { x } -%inline expr: x=loc( expr_u) { x } - -sexpr_u: -| e=sexpr PCENT p=uqident - { PEscope (p, e) } - -| e=sexpr p=loc(prefix(PCENT, _lident)) - { if unloc p = "top" then - PEscope (pqsymb_of_symb p.pl_loc "", e) - else - let p = lmap (fun x -> "%" ^ x) p in - PEapp (mk_loc (loc p) (PEident (pqsymb_of_psymb p, None)), [e]) } - -| LPAREN e=expr COLONTILD ty=loc(type_exp) RPAREN - { PEcast (e, ty) } - -| n=uint - { PEint n } - -| d=DECIMAL - { PEdecimal d } - -| x=qoident ti=tvars_app? - { PEident (x, ti) } - -| op=loc(numop) ti=tvars_app? - { peapp_symb op.pl_loc op.pl_desc ti [] } - -| se=sexpr DLBRACKET ti=tvars_app? e=loc(plist1(expr, COMMA)) RBRACKET - { let e = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e) (unloc e) in - peget (EcLocation.make $startpos $endpos) ti se e } - -| se=sexpr DLBRACKET ti=tvars_app? e1=loc(plist1(expr, COMMA)) LARROW e2=expr RBRACKET - { let e1 = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e1) (unloc e1) in - peset (EcLocation.make $startpos $endpos) ti se e1 e2 } - -| TICKPIPE ti=tvars_app? e=expr PIPE - { peapp_symb e.pl_loc EcCoreLib.s_abs ti [e] } - -| LBRACKET ti=tvars_app? es=loc(plist0(expr, SEMICOLON)) RBRACKET - { unloc (pelist es.pl_loc ti es.pl_desc) } - -| LBRACKET ti=tvars_app? e1=expr op=loc(DOTDOT) e2=expr RBRACKET - { let id = - PEident (mk_loc op.pl_loc EcCoreLib.s_dinter, ti) - in - PEapp(mk_loc op.pl_loc id, [e1; e2]) } - -| LPAREN es=plist0(expr, COMMA) RPAREN - { PEtuple es } - -| r=loc(RBOOL) - { PEident (mk_loc r.pl_loc EcCoreLib.s_dbool, None) } - -| LPBRACE fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE - { PErecord (None, fields) } - -| LPBRACE b=sexpr WITH fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE - { PErecord (Some b, fields) } - -| e=sexpr DOTTICK x=qident - { PEproj (e, x) } - -| e=sexpr DOTTICK n=loc(word) - { if n.pl_desc = 0 then - parse_error n.pl_loc (Some "tuple projection start at 1"); - PEproji(e,n.pl_desc - 1) } - -expr_u: -| e=sexpr_u { e } - -| e=sexpr args=sexpr+ - { PEapp (e, args) } - -| op=loc(uniop) ti=tvars_app? e=expr - { peapp_symb op.pl_loc op.pl_desc ti [e] } - -| e=expr_chained_orderings %prec prec_below_order - { fst e } - -| e1=expr op=loc(binop) ti=tvars_app? e2=expr - { peapp_symb op.pl_loc op.pl_desc ti [e1; e2] } - -| c=expr QUESTION e1=expr COLON e2=expr %prec LOP2 - { PEif (c, e1, e2) } - -| IF c=expr THEN e1=expr ELSE e2=expr - { PEif (c, e1, e2) } - -| MATCH e=expr WITH - PIPE? bs=plist0(p=mcptn(sbinop) IMPL be=expr { (p, be) }, PIPE) - END - { PEmatch (e, bs) } - -| LET p=lpattern EQ e1=expr IN e2=expr - { PElet (p, (e1, None), e2) } - -| LET p=lpattern COLON ty=loc(type_exp) EQ e1=expr IN e2=expr - { PElet (p, (e1, Some ty), e2) } - -| r=loc(RBOOL) TILD e=sexpr - { let id = PEident(mk_loc r.pl_loc EcCoreLib.s_dbitstring, None) in - let loc = EcLocation.make $startpos $endpos in - PEapp (mk_loc loc id, [e]) } - -| FUN pd=ptybindings IMPL e=expr -| FUN pd=ptybindings COMMA e=expr { PElambda (pd, e) } - -| FORALL pd=ptybindings COMMA e=expr { PEforall (pd, e) } -| EXIST pd=ptybindings COMMA e=expr { PEexists (pd, e) } - -expr_field: -| x=qident EQ e=expr - { { rf_name = x ; rf_tvi = None; rf_value = e; } } - -expr_ordering: -| e1=expr op=loc(ordering_op) ti=tvars_app? e2=expr - { (op, ti, e1, e2) } - -expr_chained_orderings: -| e=expr_ordering - { let (op, ti, e1, e2) = e in - (peapp_symb op.pl_loc (unloc op) ti [e1; e2], e2) } - -| e1=loc(expr_chained_orderings) op=loc(ordering_op) ti=tvars_app? e2=expr - { let (lce1, (e1, le)) = (e1.pl_loc, unloc e1) in - let loc = EcLocation.make $startpos $endpos in - (peapp_symb loc "&&" None - [EcLocation.mk_loc lce1 e1; - EcLocation.mk_loc loc - (peapp_symb op.pl_loc (unloc op) ti [le; e2])], - e2) } +%inline sexpr: f=sform { mk_loc f.pl_loc (Expr f) } +%inline expr: f=form { mk_loc f.pl_loc (Expr f) } (* -------------------------------------------------------------------- *) bdident_: @@ -3125,7 +2973,7 @@ interleave_info: | UNROLL b=boption(FOR) s=side? o=codepos { Punroll (s, o, b) } -| SPLITWHILE s=side? o=codepos COLON c=expr %prec prec_tactic +| SPLITWHILE s=side? o=codepos COLON c=expr { Psplitwhile (c, s, o) } | BYPHOARE info=gpterm(conseq)? diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 53eda26b84..13f8f8e604 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -65,60 +65,12 @@ type ppattern = type ptybinding = osymbol list * pty and ptybindings = ptybinding list -and pexpr_r = - | PEcast of pexpr * pty (* type cast *) - | PEint of zint (* int. literal *) - | PEdecimal of (zint * (int * zint)) (* dec. literal *) - | PEident of pqsymbol * ptyannot option (* symbol *) - | PEapp of pexpr * pexpr list (* op. application *) - | PElet of plpattern * pexpr_wty * pexpr (* let binding *) - | PEtuple of pexpr list (* tuple constructor *) - | PEif of pexpr * pexpr * pexpr (* _ ? _ : _ *) - | PEmatch of pexpr * (ppattern * pexpr) list (* match *) - | PEforall of ptybindings * pexpr (* forall quant. *) - | PEexists of ptybindings * pexpr (* exists quant. *) - | PElambda of ptybindings * pexpr (* lambda abstraction *) - | PErecord of pexpr option * pexpr rfield list (* record *) - | PEproj of pexpr * pqsymbol (* projection *) - | PEproji of pexpr * int (* tuple projection *) - | PEscope of pqsymbol * pexpr (* scope selection *) - -and pexpr = pexpr_r located -and pexpr_wty = pexpr * pty option - and 'a rfield = { rf_name : pqsymbol; rf_tvi : ptyannot option; rf_value : 'a; } -(* -------------------------------------------------------------------- *) -type plvalue_r = - | PLvSymbol of pqsymbol - | PLvTuple of pqsymbol list - | PLvMap of pqsymbol * ptyannot option * pexpr list - -and plvalue = plvalue_r located - -type pinstr_r = - | PSident of psymbol - | PSasgn of plvalue * pexpr - | PSrnd of plvalue * pexpr - | PScall of plvalue option * pgamepath * (pexpr list) located - | PSif of pscond * pscond list * pstmt - | PSwhile of pscond - | PSmatch of pexpr * psmatch - | PSassert of pexpr - -and psmatch = [ - | `Full of (ppattern * pstmt) list - | `If of (ppattern * pstmt) * pstmt option -] - -and pscond = pexpr * pstmt -and pinstr = pinstr_r located -and pstmt = pinstr list - (* -------------------------------------------------------------------- *) type is_local = [ `Local | `Global] @@ -170,7 +122,37 @@ type glob_or_var = | GVglob of pmsymbol located * pqsymbol list | GVvar of pqsymbol -type pformula = pformula_r located +(* -------------------------------------------------------------------- *) +type plvalue_r = + | PLvSymbol of pqsymbol + | PLvTuple of pqsymbol list + | PLvMap of pqsymbol * ptyannot option * pexpr list + +and plvalue = plvalue_r located + +and pinstr_r = + | PSident of psymbol + | PSasgn of plvalue * pexpr + | PSrnd of plvalue * pexpr + | PScall of plvalue option * pgamepath * (pexpr list) located + | PSif of pscond * pscond list * pstmt + | PSwhile of pscond + | PSmatch of pexpr * psmatch + | PSassert of pexpr + +and psmatch = [ + | `Full of (ppattern * pstmt) list + | `If of (ppattern * pstmt) * pstmt option +] + +and pscond = pexpr * pstmt +and pinstr = pinstr_r located +and pstmt = pinstr list + +and pexpr = pexpr_r located +and pexpr_r = Expr of pformula + +and pformula = pformula_r located and pformula_r = | PFhole diff --git a/src/ecTyping.ml b/src/ecTyping.ml index b22c2a63d9..e9e50656a8 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -424,8 +424,8 @@ let select_exp_op env mode opsc name ue tvi psig = opsc tvi env name ue psig (* -------------------------------------------------------------------- *) -let select_form_op env ~forcepv opsc name ue tvi psig = - gen_select_op ~actonly:true ~mode:`Form ~forcepv +let select_form_op env mode ~forcepv opsc name ue tvi psig = + gen_select_op ~actonly:true ~mode ~forcepv opsc tvi env name ue psig (* -------------------------------------------------------------------- *) @@ -1420,202 +1420,6 @@ let expr_of_opselect in (e_app op args codom, codom) -(* -------------------------------------------------------------------- *) -let transexp (env : EcEnv.env) mode ue e = - let rec transexp_r (osc : EcPath.path option) (env : EcEnv.env) (e : pexpr) = - let loc = e.pl_loc in - let transexp = transexp_r osc in - - match e.pl_desc with - | PEcast (pe, pty) -> - let ty = transty tp_relax env ue pty in - let (_, ety) as aout = transexp env pe in - unify_or_fail env ue pe.pl_loc ~expct:ty ety; aout - - | PEint i -> - (e_int i, tint) - - | PEdecimal (n, f) -> - (e_decimal (n, f), treal) - - | PEident ({ pl_desc = name }, tvi) -> - let tvi = tvi |> omap (transtvi env ue) in - let ops = select_exp_op env mode osc name ue tvi [] in - begin match ops with - | [] -> tyerror loc env (UnknownVarOrOp (name, [])) - - | [sel] -> - expr_of_opselect (env, ue) e.pl_loc sel [] - - | _ -> - let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in - tyerror loc env (MultipleOpMatch (name, [], matches)) - end - - | PEscope (popsc, e) -> - let opsc = lookup_scope env popsc in - transexp_r (Some opsc) env e - - | PEapp ({ pl_desc = PEident({ pl_desc = name; pl_loc = loc }, tvi)}, pes) -> - let tvi = tvi |> omap (transtvi env ue) in - let es = List.map (transexp env) pes in - let esig = snd (List.split es) in - let ops = select_exp_op env mode osc name ue tvi esig in - begin match ops with - | [] -> - let uidmap = EcUnify.UniEnv.assubst ue in - let esig = Tuni.subst_dom uidmap esig in - tyerror loc env (UnknownVarOrOp (name, esig)) - - | [sel] -> - let es = List.map2 (fun e l -> mk_loc l.pl_loc e) es pes in - expr_of_opselect (env, ue) loc sel es - - | _ -> - let uidmap = EcUnify.UniEnv.assubst ue in - let esig = Tuni.subst_dom uidmap esig in - let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in - tyerror loc env (MultipleOpMatch (name, esig, matches)) - end - - | PEapp (pe, pes) -> - let e, ty = transexp env pe in - let es = List.map (transexp env) pes in - let esig = List.map2 (fun (_, ty) l -> mk_loc l.pl_loc ty) es pes in - let codom = ty_fun_app pe.pl_loc env ue ty esig in - (e_app e (List.map fst es) codom, codom) - - | PElet (p, (pe1, paty), pe2) -> - let (penv, pt, pty) = transpattern env ue p in - let aty = paty |> omap (transty tp_relax env ue) in - - let e1, ty1 = transexp env pe1 in - unify_or_fail env ue pe1.pl_loc ~expct:pty ty1; - aty |> oiter (fun aty -> unify_or_fail env ue pe1.pl_loc ~expct:aty ty1); - - let e2, ty2 = transexp penv pe2 in - (e_let pt e1 e2, ty2) - - | PEtuple es -> begin - let tes = List.map (transexp env) es in - - match tes with - | [] -> (e_tt, EcTypes.tunit) - | [e, ty] -> (e, ty) - | _ -> - let es, tys = List.split tes in - (e_tuple es, ttuple tys) - end - - | PEif (pc, pe1, pe2) -> - let c, tyc = transexp env pc in - let e1, ty1 = transexp env pe1 in - let e2, ty2 = transexp env pe2 in - unify_or_fail env ue pc .pl_loc ~expct:tbool tyc; - unify_or_fail env ue pe2.pl_loc ~expct:ty1 ty2; - (e_if c e1 e2, ty1) - - | PEmatch (pce, pb) -> - let ce, ety = transexp env pce in - let uidmap = EcUnify.UniEnv.assubst ue in - let ety = ty_subst (Tuni.subst uidmap) ety in - let inddecl = - match (EcEnv.ty_hnorm ety env).ty_node with - | Tconstr (indp, _) -> begin - match EcEnv.Ty.by_path indp env with - | { tyd_type = `Datatype dt } -> - Some (indp, dt) - | _ -> None - end - | _ -> None in - - let (_indp, inddecl) = - match inddecl with - | None -> tyerror pce.pl_loc env NotAnInductive - | Some x -> x in - - let branches = - trans_match ~loc:e.pl_loc env ue (ety, inddecl) pb in - - let branches, bty = List.split (List.map (fun (lcs, s) -> - let env = EcEnv.Var.bind_locals lcs env in - let bdy = transexp env s in - e_lam lcs (fst bdy), (snd bdy, s.pl_loc)) branches) in - - let rty = EcUnify.UniEnv.fresh ue in - - List.iter (fun (ty, loc) -> unify_or_fail env ue loc ~expct:ty rty) bty; - e_match ce branches rty, rty - - | PEforall (xs, pe) -> - let env, xs = trans_binding env ue xs in - let e, ety = transexp env pe in - unify_or_fail env ue pe.pl_loc ~expct:tbool ety; - (e_forall xs e, tbool) - - | PEexists (xs, pe) -> - let env, xs = trans_binding env ue xs in - let e, ety = transexp env pe in - unify_or_fail env ue pe.pl_loc ~expct:tbool ety; - (e_exists xs e, tbool) - - | PElambda (bd, pe) -> - let env, xs = trans_binding env ue bd in - let e, ty = transexp env pe in - let ty = toarrow (List.map snd xs) ty in - (e_lam xs e, ty) - - | PErecord (b, fields) -> - let (ctor, fields, (rtvi, reccty)) = - let proj (recp, name, (rtvi, reccty), pty, arg) = - let proj = EcPath.pqname recp name in - let proj = e_op proj rtvi (tfun reccty pty) in - e_app proj [arg] pty - in trans_record env ue (transexp env, proj) (loc, b, fields) in - let ctor = e_op ctor rtvi (toarrow (List.map snd fields) reccty) in - let ctor = e_app ctor (List.map fst fields) reccty in - ctor, reccty - - | PEproj (sube, x) -> begin - let sube, ety = transexp env sube in - match select_proj env osc (unloc x) ue None ety with - | [] -> - tyerror x.pl_loc env (UnknownProj (unloc x)) - - | _::_::_ -> - tyerror x.pl_loc env (AmbiguousProj (unloc x)) - - | [(op, tvi), pty, subue] -> - EcUnify.UniEnv.restore ~src:subue ~dst:ue; - let rty = EcUnify.UniEnv.fresh ue in - (try EcUnify.unify env ue (tfun ety rty) pty - with EcUnify.UnificationFailure _ -> assert false); - (e_app (e_op op tvi pty) [sube] rty, rty) - end - - | PEproji (sube, i) -> begin - let sube', ety = transexp env sube in - let uidmap = EcUnify.UniEnv.assubst ue in - let ty = ty_subst (Tuni.subst uidmap) ety in - match (EcEnv.ty_hnorm ty env).ty_node with - | Ttuple l when i < List.length l -> - let ty = List.nth l i in - e_proj sube' i ty, ty - | _ -> tyerror sube.pl_loc env (AmbiguousProji(i,ty)) - end - - in - transexp_r None env e - -let transexpcast (env : EcEnv.env) mode ue t e = - let (e', t') = transexp env mode ue e in - unify_or_fail env ue e.pl_loc ~expct:t t'; e' - -let transexpcast_opt (env : EcEnv.env) mode ue oty e = - match oty with - | None -> fst (transexp env mode ue e) - | Some t -> transexpcast env mode ue t e - (* -------------------------------------------------------------------- *) let lookup_module_type (env : EcEnv.env) (name : pqsymbol) = match EcEnv.ModTy.lookup_opt (unloc name) env with @@ -1673,8 +1477,6 @@ let transcall transexp env ue loc fsig args = in (args, fsig.fs_ret) -let trans_args env ue = transcall (transexp env `InProc ue) env ue - (* -------------------------------------------------------------------- *) let trans_gamepath (env : EcEnv.env) gp = let loc = gp.pl_loc in @@ -2619,7 +2421,7 @@ and transinstr | PSasgn (plvalue, prvalue) -> begin let handle_unknown_op = function - | PEapp ({ pl_desc = PEident (f, None) }, _) + | Expr { pl_desc = PFapp ({ pl_desc = PFident (f, None) }, _) } when EcEnv.Fun.lookup_opt (unloc f) env <> None -> tyerror prvalue.pl_loc env (ProcAssign (unloc f)) | _ -> () @@ -2811,7 +2613,7 @@ and trans_gbinding env ue decl = in snd_map List.flatten (List.map_fold trans1 env decl) (* -------------------------------------------------------------------- *) -and trans_form_or_pattern env ?mv ?ps ue pf tt = +and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let state = PFS.create () in let rec transf_r opsc env f = @@ -3057,7 +2859,7 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = let ops = select_form_op ~forcepv:(PFS.isforced state) - env opsc name ue tvi [] in + env mode opsc name ue tvi [] in begin match ops with | [] -> tyerror loc env (UnknownVarOrOp (name, [])) @@ -3189,7 +2991,7 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = let esig = List.map EcFol.f_ty es in let ops = select_form_op ~forcepv:(PFS.isforced state) - env opsc name ue tvi esig in + env mode opsc name ue tvi esig in begin match ops with | [] -> @@ -3425,9 +3227,27 @@ and trans_memtype env ue (pmemtype : pmemtype) : memtype = List.fold_left add_decl mt pmemtype +(* -------------------------------------------------------------------- *) +and transexp env mode ue {pl_desc = Expr e } = + let f = trans_form_or_pattern env (`Expr mode) ue e None in + let m = Option.value ~default:mhr (EcEnv.Memory.get_active env) in + let e = expr_of_form m f in + (e, e.e_ty) + +(* -------------------------------------------------------------------- *) +and transexpcast (env : EcEnv.env) mode ue t e = + let (e', t') = transexp env mode ue e in + unify_or_fail env ue e.pl_loc ~expct:t t'; e' + +(* -------------------------------------------------------------------- *) +and transexpcast_opt (env : EcEnv.env) mode ue oty e = + match oty with + | None -> fst (transexp env mode ue e) + | Some t -> transexpcast env mode ue t e + (* -------------------------------------------------------------------- *) and trans_form_opt env ?mv ue pf oty = - trans_form_or_pattern env ?mv ue pf oty + trans_form_or_pattern env `Form ?mv ue pf oty (* -------------------------------------------------------------------- *) and trans_form env ?mv ue pf ty = @@ -3439,7 +3259,10 @@ and trans_prop env ?mv ue pf = (* -------------------------------------------------------------------- *) and trans_pattern env ps ue pf = - trans_form_or_pattern env ~ps ue pf None + trans_form_or_pattern env `Form ~ps ue pf None + +(* -------------------------------------------------------------------- *) +let trans_args env ue = transcall (transexp env `InProc ue) env ue (* -------------------------------------------------------------------- *) let trans_lv_match ?(memory : memory option) (env : EcEnv.env) (p : plvmatch) : lvmatch =