diff --git a/src/ecParser.mly b/src/ecParser.mly index 71dfbc9b2..c7d89e783 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 53eda26b8..13f8f8e60 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 b22c2a63d..2b912b758 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 522269a01..eb3e48f9f 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 1bcba2030..6973f029e 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