From ec01f8d0ba44c7972619062b4e8f3e633bf30823 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 This is a step forward removing expressions from EasyCrypt. This commit removes all parsing and typing code specific to expressions. Expressions are now parsed as formulas, utilizing the formula type checker instead of an expression-specific type checker. If a formula does not represent a valid expression, it is the type checker's responsibility to raise a meaningful error message. --- src/ecParser.mly | 156 +-------------------- src/ecParsetree.ml | 80 +++++------ src/ecTyping.ml | 310 +++++++++--------------------------------- src/ecTyping.mli | 1 + src/ecUserMessages.ml | 14 ++ 5 files changed, 116 insertions(+), 445 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 71dfbc9b26..c7d89e783c 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_: 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..2b912b7583 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -174,6 +174,7 @@ type tyerror = | NoDefaultMemRestr | ProcAssign of qsymbol | PositiveShouldBeBeforeNegative +| NotAnExpression of [`Unknown | `LL | `Pr | `Logic | `Glob | `MemSel] (* -------------------------------------------------------------------- *) exception TyError of EcLocation.t * EcEnv.env * tyerror @@ -424,8 +425,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 (* -------------------------------------------------------------------- *) @@ -1384,238 +1385,6 @@ let var_or_proj fvar fproj pv ty = | `Var pv -> fvar pv ty | `Proj(pv, ap) -> fproj (fvar pv ap.arg_ty) ap.arg_pos ty -let expr_of_opselect - (env, ue) loc ((sel, ty, subue, _) : OpSelect.gopsel) args -= - EcUnify.UniEnv.restore ~src:subue ~dst:ue; - - let esig = List.map (lmap snd) args in - let args = List.map (fst |- unloc) args in - let codom = ty_fun_app loc env ue ty esig in - - let op, args = - match sel with - | `Nt (lazy (bds, body)) -> - let nbds = List.length bds in - let nargs = List.length args in - - let ((tosub, args), elam) = - if nbds <= nargs then - (List.split_at nbds args, []) - else - let xs = snd (List.split_at nargs bds) in - let xs = List.map (fst_map EcIdent.fresh) xs in - ((args @ List.map (curry e_local) xs, []), xs) in - let lcmap = List.map2 (fun (x, _) y -> (x, y)) bds tosub in - let subst = f_subst_init ~freshen:true ~esloc:(Mid.of_list lcmap) () in - let body = e_subst subst body in - (e_lam elam body, args) - - | (`Op _ | `Lc _ | `Pv _) as sel -> let op = match sel with - | `Op (p, tys) -> e_op p tys ty - | `Lc id -> e_local id ty - - | `Pv (_me, pv) -> var_or_proj e_var e_proj pv ty - in (op, args) - - 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 +1442,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 +2386,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 +2578,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 = @@ -3030,6 +2797,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = transf_r (Some opsc) env f | PFglob gp -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Glob); + let mp = fst (trans_msymbol env gp) in let me = match EcEnv.Memory.current env with @@ -3057,7 +2827,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, [])) @@ -3077,6 +2847,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = end | PFside (f, (force, side)) -> begin + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `MemSel); + let (sloc, side) = (side.pl_loc, unloc side) in let me = match EcEnv.Memory.lookup side env with @@ -3099,6 +2872,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = end | PFeqveq (xs, om) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `MemSel); + let lookup me x = match EcEnv.Var.lookup_progvar_opt ~side:me (unloc x) env with | None -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) @@ -3161,6 +2937,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = EcFol.f_ands (List.map do1 xs) | PFeqf fs -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `MemSel); + let check_mem loc me = match EcEnv.Memory.byid me env with | None -> tyerror loc env (UnknownMemName (EcIdent.name me)) @@ -3189,7 +2968,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 | [] -> @@ -3324,6 +3103,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = end | PFprob (gp, args, m, event) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Pr); + let fpath = trans_gamepath env gp in let fun_ = EcEnv.Fun.by_xpath fpath env in let args,_ = @@ -3336,6 +3118,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = f_pr memid fpath (f_tuple args) event' | PFhoareF (pre, gp, post) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Logic); + let fpath = trans_gamepath env gp in let penv, qenv = EcEnv.Fun.hoareF fpath env in let pre' = transf penv pre in @@ -3343,7 +3128,11 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = unify_or_fail penv ue pre.pl_loc ~expct:tbool pre' .f_ty; unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty; f_hoareF pre' fpath post' + | PFehoareF (pre, gp, post) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Logic); + let fpath = trans_gamepath env gp in let penv, qenv = EcEnv.Fun.hoareF fpath env in let pre' = transf penv pre in @@ -3353,6 +3142,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = f_eHoareF pre' fpath post' | PFBDhoareF (pre, gp, post, hcmp, bd) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Logic); + let fpath = trans_gamepath env gp in let penv, qenv = EcEnv.Fun.hoareF fpath env in let pre' = transf penv pre in @@ -3365,10 +3157,15 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = f_bdHoareF pre' fpath post' hcmp bd' | PFlsless gp -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `LL); let fpath = trans_gamepath env gp in f_losslessF fpath | PFequivF (pre, (gp1, gp2), post) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Logic); + let fpath1 = trans_gamepath env gp1 in let fpath2 = trans_gamepath env gp2 in let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in @@ -3379,6 +3176,9 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt = f_equivF pre' fpath1 fpath2 post' | PFeagerF (pre, (s1,gp1,gp2,s2), post) -> + if mode <> `Form then + tyerror f.pl_loc env (NotAnExpression `Logic); + let fpath1 = trans_gamepath env gp1 in let fpath2 = trans_gamepath env gp2 in let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in @@ -3425,9 +3225,32 @@ and trans_memtype env ue (pmemtype : pmemtype) : memtype = List.fold_left add_decl mt pmemtype +(* -------------------------------------------------------------------- *) +and transexp env mode ue { pl_desc = Expr e; pl_loc = loc; } = + 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 = + try + expr_of_form m f + with CannotTranslate -> + (* This should not happen. *) + tyerror loc env (NotAnExpression `Unknown) 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 +3262,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 = diff --git a/src/ecTyping.mli b/src/ecTyping.mli index 522269a016..eb3e48f9f1 100644 --- a/src/ecTyping.mli +++ b/src/ecTyping.mli @@ -166,6 +166,7 @@ type tyerror = | NoDefaultMemRestr | ProcAssign of qsymbol | PositiveShouldBeBeforeNegative +| NotAnExpression of [`Unknown | `LL | `Pr | `Logic | `Glob | `MemSel] exception TymodCnvFailure of tymod_cnv_failure exception TyError of EcLocation.t * env * tyerror diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index 1bcba20307..6973f029ee 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -519,6 +519,20 @@ end = struct | PositiveShouldBeBeforeNegative -> msg "positive restriction are only allowed before negative restriction" + | NotAnExpression `Unknown -> + msg "this expression contains form-like constructors" + + | NotAnExpression ((`LL | `Pr | `Logic | `Glob | `MemSel) as what) -> begin + msg "expressions cannot contain a %s" + begin match what with + | `LL -> "lossless statement" + | `Pr -> "Pr[...] statement" + | `Logic -> "program logic statement" + | `Glob -> "glob statement" + | `MemSel -> "memory selector" + end + end + let pp_restr_error env fmt (w, e) = let ppe = EcPrinting.PPEnv.ofenv env in