(* -------------------------------------------------------------------- * Copyright (c) - 2012--2016 - IMDEA Software Institute * Copyright (c) - 2012--2018 - Inria * Copyright (c) - 2012--2018 - Ecole Polytechnique * * Distributed under the terms of the CeCILL-C-V1 license * -------------------------------------------------------------------- *) (* -------------------------------------------------------------------- *) open EcUtils open EcPath open EcMaps open EcSymbols open EcLocation open EcParsetree open EcTypes open EcDecl open EcModules open EcFol module MMsym = EcSymbols.MMsym module Sid = EcIdent.Sid module Mid = EcIdent.Mid module EqTest = EcReduction.EqTest module NormMp = EcEnv.NormMp module TC = EcTypeClass (* -------------------------------------------------------------------- *) type opmatch = [ | `Op of EcPath.path * EcTypes.ty list | `Lc of EcIdent.t | `Var of EcTypes.prog_var | `Proj of EcTypes.prog_var * EcTypes.ty * (int * int) ] type mismatch_funsig = | MF_targs of ty * ty (* expected, got *) | MF_tres of ty * ty (* expected, got *) | MF_restr of EcEnv.env * [`Eq of Sx.t * Sx.t | `Sub of Sx.t ] type tymod_cnv_failure = | E_TyModCnv_ParamCountMismatch | E_TyModCnv_ParamTypeMismatch of EcIdent.t | E_TyModCnv_MissingComp of symbol | E_TyModCnv_MismatchFunSig of symbol * mismatch_funsig | E_TyModCnv_SubTypeArg of EcIdent.t * module_type * module_type * tymod_cnv_failure type modapp_error = | MAE_WrongArgCount of int * int (* expected, got *) | MAE_InvalidArgType of EcPath.mpath * tymod_cnv_failure | MAE_AccesSubModFunctor type modtyp_error = | MTE_IncludeFunctor | MTE_InnerFunctor | MTE_DupProcName of symbol type modsig_error = | MTS_DupProcName of symbol | MTS_DupArgName of symbol * symbol type funapp_error = | FAE_WrongArgCount type mem_error = | MAE_IsConcrete type filter_error = | FE_InvalidIndex of int | FE_NoMatch type tyerror = | UniVarNotAllowed | FreeTypeVariables | TypeVarNotAllowed | OnlyMonoTypeAllowed of symbol option | UnboundTypeParameter of symbol | UnknownTypeName of qsymbol | UnknownTypeClass of qsymbol | UnknownRecFieldName of qsymbol | UnknownInstrMetaVar of symbol | UnknownMetaVar of symbol | UnknownProgVar of qsymbol * EcMemory.memory | DuplicatedRecFieldName of symbol | MissingRecField of symbol | MixingRecFields of EcPath.path tuple2 | UnknownProj of qsymbol | AmbiguousProj of qsymbol | AmbiguousProji of int * ty | InvalidTypeAppl of qsymbol * int * int | DuplicatedTyVar | DuplicatedLocal of symbol | DuplicatedField of symbol | NonLinearPattern | LvNonLinear | NonUnitFunWithoutReturn | TypeMismatch of (ty * ty) * (ty * ty) | TypeClassMismatch | TypeModMismatch of mpath * module_type * tymod_cnv_failure | NotAFunction | AbbrevLowArgs | UnknownVarOrOp of qsymbol * ty list | MultipleOpMatch of qsymbol * ty list * (opmatch * EcUnify.unienv) list | UnknownModName of qsymbol | UnknownTyModName of qsymbol | UnknownFunName of qsymbol | UnknownModVar of qsymbol | UnknownMemName of symbol | InvalidFunAppl of funapp_error | InvalidModAppl of modapp_error | InvalidModType of modtyp_error | InvalidModSig of modsig_error | InvalidMem of symbol * mem_error | InvalidFilter of filter_error | FunNotInModParam of qsymbol | NoActiveMemory | PatternNotAllowed | MemNotAllowed | UnknownScope of qsymbol | FilterMatchFailure | LvMapOnNonAssign exception TyError of EcLocation.t * EcEnv.env * tyerror let tyerror loc env e = raise (TyError (loc, env, e)) (* -------------------------------------------------------------------- *) type restriction_who = | RW_mod of EcPath.mpath | RW_fun of EcPath.xpath type restriction_err = | RE_UseVariable of EcPath.xpath | RE_UseVariableViaModule of EcPath.xpath * EcPath.mpath | RE_UseModule of EcPath.mpath | RE_VMissingRestriction of EcPath.xpath * EcPath.mpath pair | RE_MMissingRestriction of EcPath.mpath * EcPath.mpath pair type restriction_error = restriction_who * restriction_err exception RestrictionError of EcEnv.env * restriction_error (* -------------------------------------------------------------------- *) type ptnmap = ty EcIdent.Mid.t ref type metavs = EcFol.form Msym.t (* -------------------------------------------------------------------- *) let ident_of_osymbol x = omap unloc x |> odfl "_" |> EcIdent.create (* -------------------------------------------------------------------- *) module UE = EcUnify.UniEnv let unify_or_fail (env : EcEnv.env) ue loc ~expct:ty1 ty2 = try EcUnify.unify env ue ty1 ty2 with EcUnify.UnificationFailure pb -> match pb with | `TyUni (t1, t2)-> let tyinst = Tuni.offun (UE.assubst ue) in tyerror loc env (TypeMismatch ((tyinst ty1, tyinst ty2), (tyinst t1, tyinst t2))) | `TcCtt _ -> tyerror loc env TypeClassMismatch (* -------------------------------------------------------------------- *) let e_inuse = let rec inuse (map : Sx.t) (e : expr) = match e.e_node with | Evar p -> begin match p.pv_kind with | PVglob -> Sx.add p.pv_name map | _ -> map end | _ -> e_fold inuse map e in fun e -> inuse Sx.empty e (* -------------------------------------------------------------------- *) let empty_uses : uses = mk_uses [] Sx.empty Sx.empty let add_call (u : uses) p : uses = mk_uses (p::u.us_calls) u.us_reads u.us_writes let add_read (u : uses) p : uses = if is_glob p then mk_uses u.us_calls (Sx.add p.pv_name u.us_reads) u.us_writes else u let add_write (u : uses) p : uses = if is_glob p then mk_uses u.us_calls u.us_reads (Sx.add p.pv_name u.us_writes) else u let (_i_inuse, s_inuse, se_inuse) = let rec lv_inuse (map : uses) (lv : lvalue) = match lv with | LvVar (p,_) -> add_write map p | LvTuple ps -> List.fold_left (fun map (p, _) -> add_write map p) map ps and i_inuse (map : uses) (i : instr) = match i.i_node with | Sasgn (lv, e) -> let map = lv_inuse map lv in let map = se_inuse map e in map | Srnd (lv, e) -> let map = lv_inuse map lv in let map = se_inuse map e in map | Scall (lv, p, es) -> begin let map = List.fold_left se_inuse map es in let map = add_call map p in let map = lv |> ofold ((^~) lv_inuse) map in map end | Sif (e, s1, s2) -> let map = se_inuse map e in let map = s_inuse map s1 in let map = s_inuse map s2 in map | Swhile (e, s) -> let map = se_inuse map e in let map = s_inuse map s in map | Sassert e -> se_inuse map e | Sabstract _ -> assert false (* FIXME *) and s_inuse (map : uses) (s : stmt) = List.fold_left i_inuse map s.s_node and se_inuse (u : uses) (e : expr) = mk_uses u.us_calls (Sx.union u.us_reads (e_inuse e)) u.us_writes in (i_inuse empty_uses, s_inuse empty_uses, se_inuse) (* -------------------------------------------------------------------- *) let select_local env (qs,s) = if qs = [] then EcEnv.Var.lookup_local_opt s env else None (* -------------------------------------------------------------------- *) let select_pv env side name ue tvi psig = if tvi <> None then [] else try let pvs = EcEnv.Var.lookup_progvar ?side name env in let select (pv,ty) = let subue = UE.copy ue in let texpected = EcUnify.tfun_expected subue psig in try EcUnify.unify env subue ty texpected; [(pv, ty, subue)] with EcUnify.UnificationFailure _ -> [] in select pvs with EcEnv.LookupFailure _ -> [] (* -------------------------------------------------------------------- *) module OpSelect = struct type pvsel = [ | `Proj of EcTypes.prog_var * EcTypes.ty * (int * int) | `Var of EcTypes.prog_var ] type opsel = [ | `Pv of EcMemory.memory option * pvsel | `Op of (EcPath.path * ty list) | `Lc of EcIdent.ident | `Nt of EcUnify.sbody ] type mode = [`Form | `Expr of [`InProc | `InOp]] type gopsel = opsel * EcTypes.ty * EcUnify.unienv * opmatch end let gen_select_op ~(actonly : bool) ~(mode : OpSelect.mode) (opsc : path option) (tvi : EcUnify.tvi) (env : EcEnv.env) (name : EcSymbols.qsymbol) (ue : EcUnify.unienv) (psig : EcTypes.dom) : OpSelect.gopsel list = let fpv me (pv, ty, ue) = (`Pv (me, pv), ty, ue, (pv :> opmatch)) and fop (op, ty, ue, bd) = match bd with | None -> (`Op op, ty, ue, (`Op op :> opmatch)) | Some bd -> (`Nt bd, ty, ue, (`Op op :> opmatch)) and flc (lc, ty, ue) = (`Lc lc, ty, ue, (`Lc lc :> opmatch)) in let ue_filter = match mode with | `Expr _ -> fun op -> not (EcDecl.is_pred op) | `Form -> fun _ -> true in let by_scope opsc ((p, _), _, _, _) = EcPath.p_equal opsc (oget (EcPath.prefix p)) and by_current ((p, _), _, _, _) = EcPath.isprefix (oget (EcPath.prefix p)) (EcEnv.root env) and by_tc ((p, _), _, _, _) = match oget (EcEnv.Op.by_path_opt p env) with | { op_kind = OB_oper (Some OP_TC) } -> false | _ -> true in match (if tvi = None then select_local env name else None) with | Some (id, ty) -> [ flc (id, ty, ue) ] | None -> let ops () = let ops = EcUnify.select_op ~filter:ue_filter tvi env name ue psig in let ops = opsc |> ofold (fun opsc -> List.mbfilter (by_scope opsc)) ops in let ops = match List.mbfilter by_current ops with [] -> ops | ops -> ops in let ops = match List.mbfilter by_tc ops with [] -> ops | ops -> ops in (List.map fop ops) and pvs () = let me, pvs = match EcEnv.Memory.get_active env, actonly with | None, true -> (None, []) | me , _ -> ( me, select_pv env me name ue tvi psig) in List.map (fpv me) pvs in match mode with | `Expr `InOp -> ops () | `Form -> (match pvs () with [] -> ops () | pvs -> pvs) | `Expr `InProc -> (match pvs () with [] -> ops () | pvs -> pvs) (* -------------------------------------------------------------------- *) let select_exp_op env mode opsc name ue tvi psig = gen_select_op ~actonly:false ~mode:(`Expr mode) opsc tvi env name ue psig (* -------------------------------------------------------------------- *) let select_form_op env opsc name ue tvi psig = gen_select_op ~actonly:true ~mode:`Form opsc tvi env name ue psig (* -------------------------------------------------------------------- *) let select_proj env opsc name ue tvi recty = let filter = (fun op -> EcDecl.is_proj op) in let ops = EcUnify.select_op ~filter tvi env name ue [recty] in let ops = List.map (fun (p, ty, ue, _) -> (p, ty, ue)) ops in match ops, opsc with | _ :: _ :: _, Some opsc -> List.filter (fun ((p, _), _, _) -> EcPath.p_equal opsc (oget (EcPath.prefix p))) ops | _, _ -> ops (* -------------------------------------------------------------------- *) let lookup_scope env popsc = match unloc popsc with | ([], x) when x = EcCoreLib.i_top -> EcCoreLib.p_top | _ -> begin match EcEnv.Theory.lookup_opt (unloc popsc) env with | None -> tyerror popsc.pl_loc env (UnknownScope (unloc popsc)) | Some opsc -> fst opsc end (* -------------------------------------------------------------------- *) type typolicy = { tp_uni : bool; (* "_" (Tuniar) allowed *) tp_tvar : bool; (* type variable allowed *) } let tp_tydecl = { tp_uni = false; tp_tvar = true ; } (* type decl. *) let tp_relax = { tp_uni = true ; tp_tvar = true ; } (* ops/forms/preds *) let tp_nothing = { tp_uni = false; tp_tvar = false; } (* module type annot. *) let tp_uni = { tp_uni = true ; tp_tvar = false; } (* params/local vars. *) (* -------------------------------------------------------------------- *) type ismap = (instr list) Mstr.t (* -------------------------------------------------------------------- *) let transtcs (env : EcEnv.env) tcs = let for1 tc = match EcEnv.TypeClass.lookup_opt (unloc tc) env with | None -> tyerror tc.pl_loc env (UnknownTypeClass (unloc tc)) | Some (p, _) -> p (* FIXME: TC HOOK *) in Sp.of_list (List.map for1 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 tyerror loc env DuplicatedTyVar; List.map for1 tparams) in EcUnify.UniEnv.create tparams (* -------------------------------------------------------------------- *) exception TymodCnvFailure of tymod_cnv_failure let tymod_cnv_failure e = raise (TymodCnvFailure e) let tysig_item_name = function | Tys_function (f, _) -> f.fs_name let tysig_item_kind = function | Tys_function _ -> `Function let rec check_sig_cnv mode (env:EcEnv.env) (sin:module_sig) (sout:module_sig) = (* Check parameters for compatibility. Parameters names may be * different, hence, substitute in [tin.tym_params] types the names * of [tout.tym_params] *) if List.length sin.mis_params <> List.length sout.mis_params then tymod_cnv_failure E_TyModCnv_ParamCountMismatch; let bsubst = List.fold_left2 (fun subst (xin, tyin) (xout, tyout) -> let tyout = EcSubst.subst_modtype subst tyout in begin try check_modtype_cnv ~mode env tyout tyin with TymodCnvFailure err -> tymod_cnv_failure (E_TyModCnv_SubTypeArg(xin, tyout, tyin, err)) end; EcSubst.add_module subst xout (EcPath.mident xin)) EcSubst.empty sin.mis_params sout.mis_params in (* Check for body inclusion (w.r.t the parameters names substitution). * This includes: * - functions inclusion with equal signatures + included use modifiers. *) let tin = sin.mis_body and tout = EcSubst.subst_modsig_body bsubst sout.mis_body in let env = List.fold_left (fun env (xin,tyin) -> EcEnv.Mod.bind_local xin tyin (EcPath.Sx.empty, EcPath.Sm.empty) env) env sin.mis_params in let check_item_compatible = let check_fun_compatible (fin,oin) (fout,oout) = assert (fin.fs_name = fout.fs_name); let (iargs, oargs) = (fin.fs_arg, fout.fs_arg) in let (ires , ores ) = (fin.fs_ret, fout.fs_ret) in if not (EqTest.for_type env iargs oargs) then tymod_cnv_failure (E_TyModCnv_MismatchFunSig(fin.fs_name,MF_targs(oargs,iargs))); if not (EqTest.for_type env ires ores) then tymod_cnv_failure (E_TyModCnv_MismatchFunSig(fin.fs_name,MF_tres(ores,ires))); let norm oi = List.fold_left (fun s f -> EcPath.Sx.add (EcEnv.NormMp.norm_xfun env f) s) EcPath.Sx.empty oi.oi_calls in let icalls = norm oin in let ocalls = norm oout in match mode with | `Sub -> if not (Sx.subset icalls ocalls) then let sx = Sx.diff icalls ocalls in tymod_cnv_failure (E_TyModCnv_MismatchFunSig(fin.fs_name, MF_restr(env, `Sub sx))) | `Eq -> if not (Sx.equal icalls ocalls) then tymod_cnv_failure (E_TyModCnv_MismatchFunSig(fin.fs_name, MF_restr(env, `Eq(ocalls, icalls)))) in fun i_item o_item -> match i_item, o_item with | Tys_function (fin,oin), Tys_function (fout,oout) -> check_fun_compatible (fin,oin) (fout,oout) in let check_for_item (o_item : module_sig_body_item) = let o_name = tysig_item_name o_item and o_kind = tysig_item_kind o_item in let i_item = List.ofind (fun i_item -> (tysig_item_name i_item) = o_name && (tysig_item_kind i_item) = o_kind) tin in match i_item with | None -> tymod_cnv_failure (E_TyModCnv_MissingComp o_name) | Some i_item -> check_item_compatible i_item o_item in List.iter check_for_item tout; if mode = `Eq then begin List.iter (fun i_item -> let i_name = tysig_item_name i_item and i_kind = tysig_item_kind i_item in let b = List.exists (fun o_item -> (tysig_item_name o_item) = i_name && (tysig_item_kind o_item) = i_kind) tout in if not b then tymod_cnv_failure (E_TyModCnv_MissingComp i_name)) tin end and check_modtype_cnv ?(mode = `Eq) env (tyin:module_type) (tyout:module_type) = let sin = EcEnv.ModTy.sig_of_mt env tyin in let sout = EcEnv.ModTy.sig_of_mt env tyout in check_sig_cnv mode env sin sout let check_sig_mt_cnv env sin tyout = let sout = EcEnv.ModTy.sig_of_mt env tyout in check_sig_cnv `Sub env sin sout (* -------------------------------------------------------------------- *) let check_restrictions env who use restr = let re_error = fun env x -> raise (RestrictionError (env, (who, x))) in let restr = NormMp.norm_restr env restr in let check_xp xp _ = (* We check that the variable is not a variable in restr *) if NormMp.use_mem_xp xp restr then re_error env (RE_UseVariable xp); (* We check that the variable is in the restriction of the * abstract module in restr. *) let check id2 = let mp2 = EcPath.mident id2 in let r2 = NormMp.get_restr env mp2 in if not (NormMp.use_mem_xp xp r2) then re_error env (RE_UseVariableViaModule (xp, mp2)); in EcIdent.Sid.iter check restr.EcEnv.us_gl in EcPath.Mx.iter check_xp (use.EcEnv.us_pv); let check_gl id = let mp1 = EcPath.mident id in if NormMp.use_mem_gl mp1 restr then re_error env (RE_UseModule mp1); let r1 = NormMp.get_restr env mp1 in let check_v xp2 _ = if not (NormMp.use_mem_xp xp2 r1) then re_error env (RE_VMissingRestriction (xp2, (xp2.x_top, mp1))) in Mx.iter check_v restr.EcEnv.us_pv; let check_g id2 = let mp2 = EcPath.mident id2 in if not (NormMp.use_mem_gl mp2 r1) then let r2 = NormMp.get_restr env mp2 in if not (NormMp.use_mem_gl mp1 r2) then re_error env (RE_MMissingRestriction (mp1, (mp1, mp2))); in EcIdent.Sid.iter check_g restr.EcEnv.us_gl in EcIdent.Sid.iter check_gl use.EcEnv.us_gl let check_restrictions_fun env xp use restr = check_restrictions env (RW_fun xp) use restr (* -------------------------------------------------------------------- *) let check_modtype_with_restrictions env mp mt i restr = check_sig_mt_cnv env mt i; let use = NormMp.mod_use env mp in check_restrictions env (RW_mod mp) use restr (* -------------------------------------------------------------------- *) let split_msymb (env : EcEnv.env) (msymb : pmsymbol located) = let (top, args, sm) = try let (r, (x, args), sm) = List.find_pivot (fun (_,args) -> args <> None) msymb.pl_desc in (List.rev_append r [x, None], args, sm) with Not_found -> (msymb.pl_desc, None, []) in let (top, sm) = let ca (x, args) = if args <> None then tyerror msymb.pl_loc env (InvalidModAppl (MAE_WrongArgCount(0, List.length (oget args)))); x in (List.map ca top, List.map ca sm) in (top, args, sm) (* -------------------------------------------------------------------- *) let rec trans_msymbol (env : EcEnv.env) (msymb : pmsymbol located) = let loc = msymb.pl_loc in let (top, args, sm) = split_msymb env msymb in let to_qsymbol l = match List.rev l with | [] -> assert false | x::qn -> { pl_desc = (List.rev_map unloc qn, unloc x); pl_loc = x.pl_loc; } in let top_qname = to_qsymbol (top@sm) in let (top_path, {EcEnv.sp_target = mod_expr; EcEnv.sp_params = (spi, params)}) = match EcEnv.Mod.sp_lookup_opt top_qname.pl_desc env with | None -> tyerror top_qname.pl_loc env (UnknownModName top_qname.pl_desc) | Some me -> me in let (params, istop) = match top_path.EcPath.m_top with | `Concrete (_, Some sub) -> if mod_expr.me_sig.mis_params <> [] then assert false; if args <> None then if not (EcPath.p_size sub = List.length sm) then tyerror loc env (InvalidModAppl (MAE_WrongArgCount(EcPath.p_size sub, List.length sm))); (params, false) | `Concrete (p, None) -> if (params <> []) || ((spi+1) <> EcPath.p_size p) then assert false; (mod_expr.me_sig.mis_params, true) | `Local _m -> if (params <> []) || spi <> 0 then assert false; (mod_expr.me_sig.mis_params, true) in let args = args |> omap (List.map (trans_msymbol env)) in match args with | None -> if not istop && params <> [] then tyerror loc env (InvalidModAppl MAE_AccesSubModFunctor); ((top_path,loc), mod_expr.me_sig) | Some args -> let lena = List.length args in let lenp = List.length params in if lena > lenp then tyerror loc env (InvalidModAppl (MAE_WrongArgCount(lenp, lena))); let params, remn = List.takedrop lena params in let args = List.map2 (fun (_,tp) ((a,loc),ta) -> try check_sig_mt_cnv env ta tp; a with TymodCnvFailure error -> tyerror loc env (InvalidModAppl (MAE_InvalidArgType(a, error)))) params args in let subst = List.fold_left2 (fun s (x,_) a -> EcSubst.add_module s x a) EcSubst.empty params args in let keepcall = let used = EcIdent.Sid.of_list (List.map fst params) in fun xp -> match xp.EcPath.x_top.EcPath.m_top with | `Local id -> not (EcIdent.Sid.mem id used) | _ -> true in let body = List.map (fun (Tys_function (s, oi)) -> Tys_function(s, { oi_calls = List.filter keepcall oi.oi_calls; oi_in = oi.oi_in; })) mod_expr.me_sig.mis_body in let body = EcSubst.subst_modsig_body subst body in ((EcPath.mpath top_path.EcPath.m_top args, loc), {mis_params = remn; mis_body = body}) let trans_msymbol env msymb = let ((m,_),mt) = trans_msymbol env msymb in (m,mt) (* -------------------------------------------------------------------- *) let rec transty (tp : typolicy) (env : EcEnv.env) ue ty = match ty.pl_desc with | PTunivar -> if tp.tp_uni then UE.fresh ue else tyerror ty.pl_loc env UniVarNotAllowed | PTvar s -> if tp.tp_tvar then try tvar (UE.getnamed ue s.pl_desc) with _ -> tyerror s.pl_loc env (UnboundTypeParameter s.pl_desc) else tyerror s.pl_loc env TypeVarNotAllowed; | PTtuple tys -> ttuple (transtys tp env ue tys) | PTnamed { pl_desc = name } -> begin match EcEnv.Ty.lookup_opt name env with | None -> tyerror ty.pl_loc env (UnknownTypeName name) | Some (p, tydecl) -> if tydecl.tyd_params <> [] then begin let nargs = List.length tydecl.tyd_params in tyerror ty.pl_loc env (InvalidTypeAppl (name, nargs, 0)) end; tconstr p [] end | PTfun(ty1,ty2) -> tfun (transty tp env ue ty1) (transty tp env ue ty2) | PTapp ({ pl_desc = name }, tyargs) -> begin match EcEnv.Ty.lookup_opt name env with | None -> tyerror ty.pl_loc env (UnknownTypeName name) | Some (p, tydecl) -> let nargs = List.length tyargs in let expected = List.length tydecl.tyd_params in if nargs <> expected then tyerror ty.pl_loc env (InvalidTypeAppl (name, expected, nargs)); let tyargs = transtys tp env ue tyargs in tconstr p tyargs end | PTglob gp -> let m,_ = trans_msymbol env gp in tglob m and transtys tp (env : EcEnv.env) ue tys = List.map (transty tp env ue) tys let transty_for_decl env ty = let ue = UE.create (Some []) in transty tp_nothing env ue ty (* -------------------------------------------------------------------- *) let transpattern1 env ue (p : EcParsetree.plpattern) = match p.pl_desc with | LPSymbol { pl_desc = x } -> let ty = UE.fresh ue in let x = EcIdent.create x in (LSymbol (x,ty), ty) | LPTuple xs -> let xs = unlocs xs in if not (List.is_unique xs) then tyerror p.pl_loc env NonLinearPattern else let xs = List.map ident_of_osymbol xs in let subtys = List.map (fun _ -> UE.fresh ue) xs in (LTuple (List.combine xs subtys), ttuple subtys) | LPRecord fields -> let xs = List.map (unloc |- snd) fields in if not (List.is_unique xs) then tyerror p.pl_loc env NonLinearPattern; let fields = let for1 (name, v) = let filter = fun op -> EcDecl.is_proj op in let fds = EcUnify.select_op ~filter None env (unloc name) ue [] in match List.ohead fds with | None -> let exn = UnknownRecFieldName (unloc name) in tyerror name.pl_loc env exn | Some ((fp, _tvi), opty, subue, _) -> let field = oget (EcEnv.Op.by_path_opt fp env) in let (recp, fieldidx, _) = EcDecl.operator_as_proj field in EcUnify.UniEnv.restore ~src:subue ~dst:ue; ((recp, fieldidx), opty, (name, v)) in List.map for1 fields in let recp = Sp.of_list (List.map (fst |- proj3_1) fields) in let recp = match Sp.elements recp with | [] -> assert false | [recp] -> recp | p1::p2::_ -> tyerror p.pl_loc env (MixingRecFields (p1, p2)) in let recty = oget (EcEnv.Ty.by_path_opt recp env) in let rec_ = snd (EcDecl.tydecl_as_record recty) in let reccty = tconstr recp (List.map (tvar |- fst) recty.tyd_params) in let reccty, rectvi = EcUnify.UniEnv.openty ue recty.tyd_params None reccty in let fields = List.fold_left (fun map (((_, idx), _, _) as field) -> if Mint.mem idx map then let name = fst (List.nth rec_ idx) in let exn = DuplicatedRecFieldName name in tyerror p.pl_loc env exn else Mint.add idx field map) Mint.empty fields in let fields = List.init (List.length rec_) (fun i -> match Mint.find_opt i fields with | None -> let pty = EcUnify.UniEnv.fresh ue in let fty = snd (List.nth rec_ i) in let fty, _ = EcUnify.UniEnv.openty ue recty.tyd_params (Some (EcUnify.TVIunamed rectvi)) fty in (try EcUnify.unify env ue pty fty with EcUnify.UnificationFailure _ -> assert false); (None, pty) | Some (_, opty, (_, v)) -> let pty = EcUnify.UniEnv.fresh ue in (try EcUnify.unify env ue (tfun reccty pty) opty with EcUnify.UnificationFailure _ -> assert false); (Some (EcIdent.create (unloc v)), pty)) in (LRecord (recp, fields), reccty) let transpattern env ue (p : EcParsetree.plpattern) = match transpattern1 env ue p with | (LSymbol (x, ty)) as p, _ -> (EcEnv.Var.bind_local x ty env, p, ty) | LTuple xs as p, ty -> (EcEnv.Var.bind_locals xs env, p, ty) | LRecord (_, xs) as p, ty -> let xs = List.pmap (function | (None, _) -> None | (Some x, ty) -> Some (x, ty)) xs in (EcEnv.Var.bind_locals xs env, p, ty) (* -------------------------------------------------------------------- *) let transtvi env ue tvi = match tvi.pl_desc with | TVIunamed lt -> EcUnify.TVIunamed (List.map (transty tp_relax env ue) lt) | TVInamed lst -> let add locals (s, t) = if List.exists (fun (s', _) -> unloc s = unloc s') locals then tyerror tvi.pl_loc env DuplicatedTyVar; (s, transty tp_relax env ue t) :: locals in let lst = List.fold_left add [] lst in EcUnify.TVInamed (List.rev_map (fun (s,t) -> unloc s, t) lst) let rec destr_tfun env ue tf = match tf.ty_node with | Tunivar id -> begin let tf' = UE.repr ue tf in match tf == tf' with | false -> destr_tfun env ue tf' | true -> let ty1 = UE.fresh ue in let ty2 = UE.fresh ue in EcUnify.unify env ue (tuni id) (tfun ty1 ty2); Some (ty1, ty2) end | Tfun (ty1, ty2) -> Some (ty1, ty2) | Tconstr (p, tys) when EcEnv.Ty.defined p env -> destr_tfun env ue (EcEnv.Ty.unfold p tys env) | _ -> None let rec ty_fun_app loc env ue tf targs = match targs with | [] -> tf | t1 :: targs -> begin match destr_tfun env ue tf with | None -> tyerror loc env NotAFunction | Some (dom, codom) -> unify_or_fail env ue t1.pl_loc ~expct:dom t1.pl_desc; let loc = EcLocation.merge loc t1.pl_loc in ty_fun_app loc env ue codom targs end (* -------------------------------------------------------------------- *) let trans_binding env ue bd = let trans_bd1 env (xs, pty) = let ty = transty tp_relax env ue pty in let xs = List.map (fun x -> ident_of_osymbol (unloc x), ty) xs in let env = EcEnv.Var.bind_locals xs env in env, xs in let env, bd = List.map_fold trans_bd1 env bd in let bd = List.flatten bd in env, bd (* -------------------------------------------------------------------- *) let trans_record env ue (subtt, proj) (loc, b, fields) = let fields = let for1 rf = let filter = fun op -> EcDecl.is_proj op in let tvi = rf.rf_tvi |> omap (transtvi env ue) in let fds = EcUnify.select_op ~filter tvi env (unloc rf.rf_name) ue [] in match List.ohead fds with | None -> let exn = UnknownRecFieldName (unloc rf.rf_name) in tyerror rf.rf_name.pl_loc env exn | Some ((fp, _tvi), opty, subue, _) -> let field = oget (EcEnv.Op.by_path_opt fp env) in let (recp, fieldidx, _) = EcDecl.operator_as_proj field in EcUnify.UniEnv.restore ~src:subue ~dst:ue; ((recp, fieldidx), opty, rf) in List.map for1 fields in let recp = Sp.of_list (List.map (fst |- proj3_1) fields) in let recp = match Sp.elements recp with | [] -> assert false | [recp] -> recp | p1::p2::_ -> tyerror loc env (MixingRecFields (p1, p2)) in let recty = oget (EcEnv.Ty.by_path_opt recp env) in let rec_ = snd (EcDecl.tydecl_as_record recty) in let reccty = tconstr recp (List.map (tvar |- fst) 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 fields = List.fold_left (fun map (((_, idx), _, _) as field) -> if Mint.mem idx map then let name = fst (List.nth rec_ idx) in let exn = DuplicatedRecFieldName name in tyerror loc env exn else Mint.add idx field map) Mint.empty fields in let dflrec = let doit f = let (dfl, dflty) = subtt f in unify_or_fail env ue f.pl_loc ~expct:reccty dflty; dfl in b |> omap doit in let fields = let get_field i name rty = match Mint.find_opt i fields with | Some (_, opty, rf) -> `Set (opty, rf.rf_value) | None -> match dflrec with | None -> tyerror loc env (MissingRecField name) | Some _ -> `Dfl (Tvar.subst tysopn rty, name) in List.mapi (fun i (name, rty) -> get_field i name rty) rec_ in let fields = let for1 = function | `Set (opty, value) -> let pty = EcUnify.UniEnv.fresh ue in (try EcUnify.unify env ue (tfun reccty pty) opty with EcUnify.UnificationFailure _ -> assert false); let e, ety = subtt value in unify_or_fail env ue value.pl_loc ~expct:pty ety; (e, pty) | `Dfl (rty, name) -> let nm = oget (EcPath.prefix recp) in (proj (nm, name, (rtvi, reccty), rty, oget dflrec), rty) in List.map for1 fields in let ctor = EcPath.pqoname (EcPath.prefix recp) (Printf.sprintf "mk_%s" (EcPath.basename recp)) in (ctor, fields, (rtvi, reccty)) (*-------------------------------------------------------------------- *) 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 = { EcTypes.e_subst_id with es_freshen = true; } in let subst = { subst with es_loc = Mid.of_list lcmap; } in let body = EcTypes.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, `Var pv) -> e_var pv ty | `Pv (_me, `Proj (pv, _ , (0, 1))) -> e_var pv ty | `Pv (_me, `Proj (pv, ty', (i, _))) -> e_proj (e_var pv ty') i 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 esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) 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 esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) 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) | 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 | [] -> let ty = Tuni.offun (EcUnify.UniEnv.assubst ue) ety in let me = EcFol.mhr in let mp = match ty.ty_node with | Tglob mp -> mp | _ -> tyerror x.pl_loc env (UnknownProj (unloc x)) in let f = NormMp.norm_glob env me mp in let lf = match f.f_node with | Ftuple l -> l | _ -> tyerror x.pl_loc env (UnknownProj (unloc x)) in let vx,ty = match EcEnv.Var.lookup_progvar_opt ~side:me (unloc x) env with | None -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) | Some (x1, ty) -> match x1 with | `Var x -> NormMp.norm_pvar env x, ty | _ -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) in let find f1 = match f1.f_node with | Fpvar (x1, _) -> EcTypes.pv_equal vx (NormMp.norm_pvar env x1) | _ -> false in let i = match List.oindex find lf with | None -> tyerror x.pl_loc env (UnknownProj (unloc x)) | Some i -> i in e_proj sube i ty, ty | _::_::_ -> 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 ty = Tuni.offun (EcUnify.UniEnv.assubst ue) 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 | None -> tyerror name.pl_loc env (UnknownTyModName (unloc name)) | Some x -> x let lookup_fun env name = try EcEnv.Fun.lookup name.pl_desc env with EcEnv.LookupFailure _ -> tyerror name.pl_loc env (UnknownFunName name.pl_desc) (* -------------------------------------------------------------------- *) let transmodtype (env : EcEnv.env) (modty : pmodule_type) = let (p, sig_) = lookup_module_type env modty in let modty = { (* eta-normal form *) mt_params = sig_.mis_params; mt_name = p; mt_args = List.map (EcPath.mident -| fst) sig_.mis_params; } in (modty, sig_) let transcall transexp env ue loc fsig args = let targ = fsig.fs_arg in let process_args tys = if List.length args <> List.length tys then tyerror loc env (InvalidFunAppl FAE_WrongArgCount); List.map2 (fun a ty -> let loc = a.pl_loc in let a, aty = transexp a in unify_or_fail env ue loc ~expct:ty aty; a) args tys in let args = match List.length args with | 0 -> if not (EcReduction.EqTest.for_type env targ tunit) then tyerror loc env (InvalidFunAppl FAE_WrongArgCount); [] | _ when EcReduction.EqTest.for_type env targ tunit -> tyerror loc env (InvalidFunAppl FAE_WrongArgCount); | 1 -> process_args [targ] | _ -> let lty = match (EcEnv.Ty.hnorm targ env).ty_node with | Ttuple lty -> lty | _ -> [targ] in process_args lty in (args, fsig.fs_ret) (* -------------------------------------------------------------------- *) let trans_gamepath (env : EcEnv.env) gp = let loc = gp.pl_loc in let modsymb = List.map (unloc -| fst) (fst (unloc gp)) and funsymb = unloc (snd (unloc gp)) in let xp = match EcEnv.Fun.sp_lookup_opt (modsymb, funsymb) env with | None -> tyerror gp.pl_loc env (UnknownFunName (modsymb, funsymb)) | Some (xp,_) -> xp in match modsymb with | [] -> xp | _ -> let (mpath, _sig) = trans_msymbol env (mk_loc loc (fst (unloc gp))) in if _sig.mis_params <> [] then tyerror gp.pl_loc env (UnknownFunName (modsymb, funsymb)); EcPath.xpath_fun mpath funsymb (* -------------------------------------------------------------------- *) let rec transmodsig (env : EcEnv.env) (name : symbol) (modty : pmodule_sig) = let Pmty_struct modty = modty in let margs = List.map (fun (x, i) -> (EcIdent.create (unloc x), fst (transmodtype env i))) modty.pmsig_params in let sa = List.fold_left (fun sa (x,_) -> Sm.add (EcPath.mident x) sa) Sm.empty margs in let env = EcEnv.Mod.enter name margs env in let body = transmodsig_body env sa modty.pmsig_body in { mis_params = margs; mis_body = body; } (* -------------------------------------------------------------------- *) and transmodsig_body (env : EcEnv.env) (sa : Sm.t) (is : pmodule_sig_struct_body) = let names = ref [] in let mk_calls = function | None -> let do_one mp calls = let sig_ = (EcEnv.Mod.by_mpath mp env).me_sig in if sig_.mis_params <> [] then calls else let fs = List.map (fun (Tys_function (fsig, _)) -> EcPath.xpath_fun mp fsig.fs_name) sig_.mis_body in fs@calls in Sm.fold do_one sa [] | Some pfd_uses -> List.map (fun name -> let f = fst (lookup_fun env name) in let p = f.EcPath.x_top in if not (Sm.mem p sa) then tyerror name.pl_loc env (FunNotInModParam name.pl_desc); f) pfd_uses in let transsig1 = function | `FunctionDecl f -> let name = f.pfd_name in names := name::!names; let tyarg, tyargs = match f.pfd_tyargs with | Fparams_exp args -> let tyargs = List.map (* FIXME: continuation *) (fun (x, ty) -> { v_name = x.pl_desc; v_type = transty_for_decl env ty}) args in Msym.odup unloc (List.map fst args) |> oiter (fun (_, a) -> tyerror name.pl_loc env (InvalidModSig (MTS_DupArgName (unloc name, unloc a)))); let tyarg = ttuple (List.map (fun vd -> vd.v_type) tyargs) in tyarg, Some tyargs | Fparams_imp ty -> let tyarg = transty_for_decl env ty in tyarg, None in let resty = transty_for_decl env f.pfd_tyresult in let (uin, calls) = (fst f.pfd_uses, mk_calls (snd f.pfd_uses)) in let sig_ = { fs_name = name.pl_desc; fs_arg = tyarg; fs_anames = tyargs; fs_ret = resty; } and oi = { oi_calls = calls; oi_in = uin; } in [Tys_function (sig_, oi)] | `Include (i,proc,restr) -> let (_modty,sig_) = transmodtype env i in if sig_.mis_params <> [] then tyerror i.pl_loc env (InvalidModType MTE_IncludeFunctor); let check_xs xs = List.iter (fun x -> let s = unloc x in if not (List.exists (fun (Tys_function(fs,_)) -> sym_equal fs.fs_name s) sig_.mis_body) then let modsymb = fst (unloc i) @ [snd (unloc i)] in let funsymb = unloc x in tyerror (loc x) env (UnknownFunName (modsymb,funsymb))) xs in let in_xs (Tys_function(fs,_oi)) xs = List.exists (fun x -> sym_equal fs.fs_name (unloc x)) xs in let calls = mk_calls restr in let add (Tys_function(fs,oi)) = names := mk_loc (loc i) fs.fs_name :: !names; Tys_function( fs, {oi with oi_calls = calls} ) in match proc with | None -> List.map add sig_.mis_body | Some (`MInclude xs) -> check_xs xs; List.pmap (fun fs -> if in_xs fs xs then Some (add fs) else None) sig_.mis_body | Some (`MExclude xs) -> check_xs xs; List.pmap (fun fs -> if not (in_xs fs xs) then Some (add fs) else None) sig_.mis_body in let items = List.flatten (List.map transsig1 is) in let names = List.rev !names in Msym.odup unloc names |> oiter (fun (_, x) -> tyerror (loc x) env (InvalidModSig (MTS_DupProcName (unloc x)))); items (* -------------------------------------------------------------------- *) (* LvMap (op, x, e, ty) * - op is the map-set operator * - x is the map to be updated * - e is the index to update * - ty is the type of the value [x] *) type lvmap = (path * ty list) * prog_var * expr * ty type lVAl = | Lval of lvalue | LvMap of lvmap let i_asgn_lv (_loc : EcLocation.t) (_env : EcEnv.env) lv e = match lv with | Lval lv -> i_asgn (lv, e) | LvMap ((op,tys), x, ei, ty) -> let op = e_op op tys (toarrow [ty; ei.e_ty; e.e_ty] ty) in i_asgn (LvVar (x,ty), e_app op [e_var x ty; ei; e] ty) let i_rnd_lv loc env lv e = match lv with | Lval lv -> i_rnd (lv, e) | LvMap _ -> tyerror loc env LvMapOnNonAssign let i_call_lv loc env lv f args = match lv with | Lval lv -> i_call (Some lv, f, args) | LvMap _ -> tyerror loc env LvMapOnNonAssign (* -------------------------------------------------------------------- *) let rec transmod ~attop (env : EcEnv.env) (me : pmodule_def) = snd (transmod_header ~attop env me.ptm_header [] me.ptm_body) (* -------------------------------------------------------------------- *) and transmod_header ~attop (env : EcEnv.env) (mh:pmodule_header) params (me:pmodule_expr) = match mh with | Pmh_ident x -> 0, transmod_body ~attop env x params me | Pmh_params {pl_desc = (mh,params')} -> let n, me = transmod_header ~attop env mh (params' @ params) me in n + List.length params', me | Pmh_cast(mh, mts) -> let n, me = transmod_header ~attop env mh params me in (* Compute the signature at the given position, i.e: remove the n first argument *) let rm,mis_params = List.takedrop n me.me_sig.mis_params in let torm = List.fold_left (fun mparams (id,_) -> Sm.add (EcPath.mident id) mparams) Sm.empty rm in let filter f = let ftop = EcPath.m_functor f.EcPath.x_top in not (Sm.mem ftop torm) in let clear (Tys_function(fsig,oi)) = Tys_function(fsig, {oi with oi_calls = List.filter filter oi.oi_calls}) in let mis_body = List.map clear me.me_sig.mis_body in let tymod = { mis_params; mis_body } in (* Check that the signature is a subtype *) let check s = let (aty, _asig) = transmodtype env s in try check_sig_mt_cnv env tymod aty with TymodCnvFailure err -> let args = List.map (fun (id,_) -> EcPath.mident id) rm in let mp = mpath_crt (psymbol me.me_name) args None in tyerror s.pl_loc env (TypeModMismatch(mp, aty, err)) in List.iter check mts; n,me (* -------------------------------------------------------------------- *) and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = (* Check parameters types *) (* FIXME: dup names *) let stparams = List.map (* FIXME: exn *) (fun (a, aty) -> (EcIdent.create a.pl_desc, fst (transmodtype env aty))) params in let env = EcEnv.Mod.enter x.pl_desc stparams env in match me.pl_desc with | Pm_ident m -> let (mp, sig_) = trans_msymbol env {pl_desc = m; pl_loc = me.pl_loc} in let extraparams = sig_.mis_params in let allparams = stparams @ extraparams in if allparams <> [] && not attop then tyerror me.pl_loc env (InvalidModAppl (MAE_WrongArgCount(0,List.length allparams))); let me = EcEnv.Mod.by_mpath mp env in let arity = List.length stparams in let me = { me with me_name = x.pl_desc; me_body = ME_Alias (arity,mp); me_sig = { sig_ with mis_params = allparams }; } in me | Pm_struct ps -> transstruct ~attop env x.pl_desc stparams (mk_loc me.pl_loc ps) (* -------------------------------------------------------------------- *) and transstruct ~attop (env : EcEnv.env) (x : symbol) stparams (st:pstructure located) = let { pl_loc = loc; pl_desc = st; } = st in if not attop && stparams <> [] then tyerror loc env (InvalidModType MTE_InnerFunctor); let (envi, items) = let tydecl1 (x, obj) = match obj with | MI_Module m -> (x, `Module m) | MI_Variable v -> (x, `Variable (EcTypes.PVglob, v.v_type)) | MI_Function f -> (x, `Function f) in List.fold_left (fun (env, acc) item -> let imports, newitems = transstruct1 env item in let env = EcEnv.bindall (List.map tydecl1 newitems) env in let env = List.fold_left EcEnv.Mod.import_vars env imports in (env, acc @ newitems)) (env, []) st in let items = List.map snd items in (* Generate structure signature *) let tymod = let mparams = List.fold_left (fun mparams (id,_) -> Sm.add (EcPath.mident id) mparams) Sm.empty stparams in let tymod1 = function | MI_Module _ -> None | MI_Variable _ -> None | MI_Function f -> let rec f_call c f = let f = EcEnv.NormMp.norm_xfun envi f in if EcPath.Sx.mem f c then c else let c = EcPath.Sx.add f c in match (EcEnv.Fun.by_xpath f envi).f_def with | FBalias _ -> assert false | FBdef def -> List.fold_left f_call c def.f_uses.us_calls | FBabs oi -> List.fold_left f_call c oi.oi_calls in let all_calls = match f.f_def with | FBalias f -> f_call EcPath.Sx.empty f | FBdef def -> List.fold_left f_call EcPath.Sx.empty def.f_uses.us_calls | FBabs _ -> assert false in let filter f = let ftop = EcPath.m_functor f.EcPath.x_top in Sm.mem ftop mparams in let calls = List.filter filter (EcPath.Sx.elements all_calls) in Some (Tys_function (f.f_sig, { oi_calls = calls; oi_in = true; })) in let sigitems = List.pmap tymod1 items in { mis_params = stparams; mis_body = sigitems; }; in (* Construct structure representation *) let me = { me_name = x; me_body = ME_Structure { ms_body = items; }; me_comps = items; me_sig = tymod; } in me (* -------------------------------------------------------------------- *) and transstruct1 (env : EcEnv.env) (st : pstructure_item located) = match unloc st with | Pst_mod (x,cast, me) -> let pe = { ptm_header = if List.is_empty cast then Pmh_ident x else Pmh_cast(Pmh_ident x, cast); ptm_body = me; ptm_local = true } in let me = transmod ~attop:false env pe in [], [me.me_name, MI_Module me] | Pst_var (xs, ty) -> let ty = transty_for_decl env ty in let items = List.map (fun { pl_desc = x } -> (x, MI_Variable { v_name = x; v_type = ty; })) xs in [], items | Pst_fun (decl, body) -> begin let ue = UE.create (Some []) in let env = EcEnv.Fun.enter decl.pfd_name.pl_desc env in let symbols = ref Sstr.empty and env = ref env in (* Type-check function parameters / check for dups *) let dtyargs = match decl.pfd_tyargs with | Fparams_imp _ -> assert false | Fparams_exp l -> l in let params = let params = ref [] in let add_param (x, pty) = let ty = transty tp_uni !env ue pty in let pr = (unloc x, `Variable (PVloc, ty)) in fundef_add_symbol !env symbols x; params := ({ v_name = unloc x; v_type = ty }, pty.pl_loc) :: !params; env := EcEnv.bindall [pr] !env in List.iter add_param dtyargs; List.rev !params in (* Type-check body *) let retty = transty tp_uni !env ue decl.pfd_tyresult in let (env, stmt, result, prelude, locals) = transbody ue symbols !env retty (mk_loc st.pl_loc body) in (* Close all types *) let su = Tuni.offun (UE.assubst ue) in let retty = fundef_check_type su env None (retty, decl.pfd_tyresult.pl_loc) in let params = List.map (fundef_check_decl su env) params in let locals = List.map (fundef_check_decl su env) locals in let prelude = List.map (fundef_check_iasgn su env) prelude in if not (UE.closed ue) then tyerror st.pl_loc env (OnlyMonoTypeAllowed None); let clsubst = { EcTypes.e_subst_id with es_ty = su } in let stmt = s_subst clsubst stmt and result = result |> omap (e_subst clsubst) in let stmt = EcModules.stmt (List.flatten prelude @ stmt.s_node) in (* Computes reads/writes/calls *) let uses = result |> ofold ((^~) se_inuse) (s_inuse stmt) in (* Compose all results *) let fun_ = { f_name = decl.pfd_name.pl_desc; f_sig = { fs_name = decl.pfd_name.pl_desc; fs_arg = ttuple (List.map (fun vd -> vd.v_type) params); fs_anames = Some params; fs_ret = retty; }; f_def = FBdef { f_locals = locals; f_body = stmt; f_ret = result; f_uses = uses; }; } in [], [(decl.pfd_name.pl_desc, MI_Function fun_)] end | Pst_alias ({pl_desc = name},f) -> [], [transstruct1_alias env name f] | Pst_include (m, imp, procs) -> begin let (mo, ms) = trans_msymbol env m in if ms.mis_params <> [] then tyerror (loc m) env (InvalidModType MTE_InnerFunctor); let check_procs = let check_proc { pl_loc = ploc; pl_desc = name; } = let check (Tys_function (fs, _)) = sym_equal fs.fs_name name in if not (List.exists check ms.mis_body) then begin let modsymb = List.map (unloc -| fst) (unloc m) in tyerror ploc env (UnknownFunName (modsymb, name)) end in List.iter check_proc in let in_procs (Tys_function (fs, _)) procs = List.exists (fun x -> sym_equal fs.fs_name (unloc x)) procs in let mk_fun (Tys_function (fs, _)) = (fs.fs_name, MI_Function { f_name = fs.fs_name; f_sig = fs; f_def = FBalias (EcPath.xpath_fun mo fs.fs_name) }) in let items = match procs with | None -> List.map mk_fun ms.mis_body | Some (`MInclude procs) -> check_procs procs; List.pmap (fun fs -> if in_procs fs procs then Some (mk_fun fs) else None) ms.mis_body | Some (`MExclude procs) -> check_procs procs; List.pmap (fun fs -> if not (in_procs fs procs) then Some (mk_fun fs) else None) ms.mis_body in (if imp then [mo] else []), items end | Pst_import ms -> (List.map (fst |- trans_msymbol env) ms), [] and transstruct1_alias env name f = let f = trans_gamepath env f in let sig_ = (EcEnv.Fun.by_xpath f env).f_sig in let fun_ = { f_name = name; f_sig = { sig_ with fs_name = name }; f_def = FBalias f; } in (name, MI_Function fun_) (* -------------------------------------------------------------------- *) and transbody ue symbols (env : EcEnv.env) retty pbody = let { pl_loc = loc; pl_desc = pbody; } = pbody in let env = ref env and prelude = ref [] and locals = ref [] in let mpath = oget (EcEnv.xroot !env) in (* Type-check local variables / check for dups *) let add_local local = List.iter (fundef_add_symbol !env symbols) (snd (unloc local.pfl_names)); let xs = snd (unloc local.pfl_names) in let mode = fst (unloc local.pfl_names) in let init = local.pfl_init |> omap (fst -| transexp !env `InProc ue) in let ty = local.pfl_type |> omap (transty tp_uni !env ue) in let ty = match ty, init with | None , None -> None | Some ty, None -> Some ty | None , Some e -> Some e.e_ty | Some ty, Some e -> begin let loc = (oget local.pfl_init).pl_loc in unify_or_fail !env ue loc ~expct:ty e.e_ty; Some ty end in let xsvars = List.map (fun _ -> UE.fresh ue) xs in begin ty |> oiter (fun ty -> match mode with | `Single -> List.iter (fun a -> EcUnify.unify !env ue a ty) xsvars | `Tuple -> unify_or_fail !env ue local.pfl_names.pl_loc ~expct:ty (ttuple xsvars)) end; env := begin let topr = fun x xty -> (unloc x, `Variable (PVloc, xty)) in EcEnv.bindall (List.map2 topr xs xsvars) !env end; let mylocals = List.map2 (fun { pl_desc = x; pl_loc = loc; } xty -> ({ v_name = x; v_type = xty }, pv_loc mpath x, xty, loc)) xs xsvars in locals := List.rev_append (List.map (fun (v, _, _, pl) -> (v, pl)) mylocals) !locals; init |> oiter (fun init -> let iasgn = List.map (fun (_, v, xty, _) -> (v, xty)) mylocals in prelude := ((mode, iasgn), init, _dummy) :: !prelude) in List.iter add_local pbody.pfb_locals; let body = transstmt !env ue pbody.pfb_body in let result = match pbody.pfb_return with | None -> begin try EcUnify.unify !env ue tunit retty with EcUnify.UnificationFailure _ -> tyerror loc !env NonUnitFunWithoutReturn end; None | Some pe -> let (e, ety) = transexp !env `InProc ue pe in unify_or_fail !env ue pe.pl_loc ~expct:retty ety; Some e in (!env, body, result, List.rev !prelude, List.rev !locals) (* -------------------------------------------------------------------- *) and fundef_add_symbol env symbols x = (* for locals dup check *) if Sstr.mem x.pl_desc !symbols then tyerror x.pl_loc env (DuplicatedLocal x.pl_desc); symbols := Sstr.add x.pl_desc !symbols and fundef_check_type subst_uni env os (ty, loc) = let ty = subst_uni ty in if not (EcUid.Suid.is_empty (Tuni.fv ty)) then tyerror loc env (OnlyMonoTypeAllowed os); ty and fundef_check_decl subst_uni env (decl, loc) = { decl with v_type = fundef_check_type subst_uni env (Some decl.v_name) (decl.v_type, loc) } and fundef_check_iasgn subst_uni env ((mode, pl), init, loc) = let pl = List.map (fun (p, ty) -> (p, fundef_check_type subst_uni env None (ty, loc))) pl in let pl = match mode with | `Single -> List.map (fun xty -> LvVar xty) pl | `Tuple -> [LvTuple pl] in let clsubst = { EcTypes.e_subst_id with es_ty = subst_uni } in let init = e_subst clsubst init in List.map (fun lv -> i_asgn (lv, init)) pl (* -------------------------------------------------------------------- *) and transstmt ?(map : ismap = Mstr.empty) (env : EcEnv.env) ue (stmt : pstmt) : stmt = let l_start = Mstr.find_def [] EcTransMatching.default_start_name map in let l_end = Mstr.find_def [] EcTransMatching.default_end_name map in let instr_list_list = List.map (transinstr ~map env ue) stmt in let instr_list_list = instr_list_list @ [l_end] in let instr_list_list = l_start :: instr_list_list in EcModules.stmt (List.flatten instr_list_list) (* -------------------------------------------------------------------- *) and transinstr ?(map : ismap = Mstr.empty) (env : EcEnv.env) ue (i : pinstr) = let transcall name args = let fpath = trans_gamepath env name in let fsig = (EcEnv.Fun.by_xpath fpath env).f_sig in let (args, ty) = transcall (transexp env `InProc ue) env ue name.pl_loc fsig args in (fpath, args, ty) in match i.pl_desc with | PSident x -> begin match Mstr.find_opt (unloc x) map with | Some x -> x | None -> tyerror (loc x) env (UnknownInstrMetaVar (unloc x)) end | PSasgn (plvalue, prvalue) -> begin match unloc prvalue with | PEapp ( { pl_desc = PEident (f, None) }, [{ pl_desc = PEtuple es; pl_loc = les; }]) when EcEnv.Fun.lookup_opt (unloc f) env <> None -> let fident { pl_loc = loc; pl_desc = (nm, x); } = let nm = List.map (fun x -> (mk_loc loc x, None)) nm in mk_loc loc (nm, mk_loc loc x) in let call = PScall (Some plvalue, fident f, mk_loc les es) in transinstr env ue (mk_loc i.pl_loc call) | _ -> let lvalue, lty = translvalue ue env plvalue in let rvalue, rty = transexp env `InProc ue prvalue in unify_or_fail env ue prvalue.pl_loc ~expct:lty rty; [ i_asgn_lv i.pl_loc env lvalue rvalue ] end | PSrnd (plvalue, prvalue) -> let lvalue, lty = translvalue ue env plvalue in let rvalue, rty = transexp env `InProc ue prvalue in unify_or_fail env ue prvalue.pl_loc ~expct:(tdistr lty) rty; [ i_rnd_lv i.pl_loc env lvalue rvalue ] | PScall (None, name, args) -> let (fpath, args, _rty) = transcall name (unloc args) in [ i_call (None, fpath, args) ] | PScall (Some lvalue, name, args) -> let lvalue, lty = translvalue ue env lvalue in let (fpath, args, rty) = transcall name (unloc args) in unify_or_fail env ue name.pl_loc ~expct:lty rty; [ i_call_lv i.pl_loc env lvalue fpath args ] | PSif ((pe, s), cs, sel) -> begin let rec for1_i (pe, s) sel = let e, ety = transexp env `InProc ue pe in let s = transstmt env ue s in unify_or_fail env ue pe.pl_loc ~expct:tbool ety; i_if (e, s, sel) and for1_s (pe, s) sel = stmt [for1_i (pe, s) sel] in [ for1_i (pe, s) (List.fold_right for1_s cs (transstmt env ue sel)) ] end | PSwhile (pe, pbody) -> let e, ety = transexp env `InProc ue pe in let body = transstmt env ue pbody in unify_or_fail env ue pe.pl_loc ~expct:tbool ety; [ i_while (e, body) ] | PSassert pe -> let e, ety = transexp env `InProc ue pe in unify_or_fail env ue pe.pl_loc ~expct:tbool ety; [ i_assert e ] (* -------------------------------------------------------------------- *) and trans_pv env { pl_desc = x; pl_loc = loc } = let side = EcEnv.Memory.get_active env in match EcEnv.Var.lookup_progvar_opt ?side x env with | None -> tyerror loc env (UnknownModVar x) | Some(pv,xty) -> match pv with | `Var pv -> pv, xty | `Proj _ -> assert false and translvalue ue (env : EcEnv.env) lvalue = match lvalue.pl_desc with | PLvSymbol x -> let pty = trans_pv env x in Lval (LvVar pty), snd pty | PLvTuple xs -> let xs = List.map (trans_pv env) xs in if not (List.is_unique ~eq:(EqTest.for_pv env) (List.map fst xs)) then tyerror lvalue.pl_loc env LvNonLinear; let ty = ttuple (List.map snd xs) in Lval (LvTuple xs), ty | PLvMap (x, tvi, e) -> let tvi = tvi |> omap (transtvi env ue) in let codomty = UE.fresh ue in let pv, xty = trans_pv env x in let e, ety = transexp env `InProc ue e in let name = ([], EcCoreLib.s_set) in let esig = [xty; ety; codomty] in let ops = select_exp_op env `InProc None name ue tvi esig in match ops with | [] -> let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in tyerror x.pl_loc env (UnknownVarOrOp (name, esig)) | [`Op (p, tys), opty, subue, _] -> EcUnify.UniEnv.restore ~src:subue ~dst:ue; let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in let esig = toarrow esig xty in unify_or_fail env ue lvalue.pl_loc ~expct:esig opty; LvMap ((p, tys), pv, e, xty), codomty | [_] -> let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in tyerror x.pl_loc env (UnknownVarOrOp (name, esig)) | _ -> let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in tyerror x.pl_loc env (MultipleOpMatch (name, esig, matches)) (* -------------------------------------------------------------------- *) let transmem env m = match EcEnv.Memory.lookup (unloc m) env with | None -> tyerror m.pl_loc env (UnknownMemName (unloc m)) | Some me -> (* if (EcMemory.memtype me) <> None then tyerror m.pl_loc env (InvalidMem (unloc m, MAE_IsConcrete)); *) (fst me) (* -------------------------------------------------------------------- *) let transpvar env side p = match EcEnv.Var.lookup_progvar_opt ~side (unloc p) env with | Some (`Var p, _) -> p | _ -> tyerror p.pl_loc env (UnknownProgVar (unloc p, side)) (* -------------------------------------------------------------------- *) let trans_topmsymbol env gp = (* FIXME *) let (mp,_) = trans_msymbol env gp in let top = EcPath.m_functor mp in let mp = EcPath.m_apply top mp.EcPath.m_args in mp (* -------------------------------------------------------------------- *) module PFS : sig type pfstate val create : unit -> pfstate val set_memused : pfstate -> unit val get_memused : pfstate -> bool val new_memused : ('a -> 'b) -> pfstate -> 'a -> bool * 'b end = struct type pfstate = { mutable pfa_memused : bool; } let create () = { pfa_memused = true; } let set_memused state = state.pfa_memused <- true let get_memused state = state.pfa_memused let new_memused f state x = let old = state.pfa_memused in let aout = (state.pfa_memused <- false; f x) in let new_ = state.pfa_memused in state.pfa_memused <- old; (new_, aout) end (* -------------------------------------------------------------------- *) let form_of_opselect (env, ue) loc ((sel, ty, subue, _) : OpSelect.gopsel) args = EcUnify.UniEnv.restore ~src:subue ~dst:ue; let esig = List.map (lmap f_ty) args in let args = List.map 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), flam) = 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 f_local) xs, []), xs) in let flam = List.map (snd_map gtty) flam in let me = odfl mhr (EcEnv.Memory.get_active env) in let body = form_of_expr me body in let lcmap = List.map2 (fun (x, _) y -> (x, y)) bds tosub in let subst = Fsubst.f_subst_init ~freshen:true () in let subst = List.fold_left (fun s -> curry (Fsubst.f_bind_local s)) subst lcmap in (f_lambda flam (Fsubst.f_subst subst body), args) | (`Op _ | `Lc _ | `Pv _) as sel -> let op = match sel with | `Op (p, tys) -> f_op p tys ty | `Lc id -> f_local id ty | `Pv (me, `Var pv) -> f_pvar pv ty (oget me) | `Pv (me, `Proj (pv, _ , (0, 1))) -> f_pvar pv ty (oget me) | `Pv (me, `Proj (pv, ty', (i, _))) -> f_proj (f_pvar pv ty' (oget me)) i ty in (op, args) in f_app op args codom (* -------------------------------------------------------------------- *) let trans_gbinding env ue decl = let trans1 env (xs, pgty) = match pgty with | PGTY_Type ty -> let ty = transty tp_relax env ue ty in let xs = List.map (fun x -> ident_of_osymbol (unloc x), ty) xs in let env = EcEnv.Var.bind_locals xs env in let xs = List.map (fun (x,ty) -> x,GTty ty) xs in (env, xs) | PGTY_ModTy (mi, restr) -> let mi = fst (transmodtype env mi) in let restr = Sm.of_list (List.map (trans_topmsymbol env) restr) in let restr = Sx.empty, restr in let ty = GTmodty (mi, restr) in let add1 env x = let x = ident_of_osymbol (unloc x) in let env = EcEnv.Mod.bind_local x mi restr env in (env, (x, ty)) in List.map_fold add1 env xs | PGTY_Mem -> let add1 env x = let x = ident_of_osymbol (unloc x) in let env = EcEnv.Memory.push (EcMemory.abstract x) env in (env, (x, GTmem None)) in List.map_fold add1 env xs in snd_map List.flatten (List.map_fold trans1 env decl) (* -------------------------------------------------------------------- *) let rec trans_form_or_pattern env ?mv ?ps ue pf tt = let state = PFS.create () in let rec transf_r opsc env f = let transf = transf_r opsc in match f.pl_desc with | PFhole -> begin match ps with | None -> tyerror f.pl_loc env PatternNotAllowed | Some ps -> let x = EcIdent.create (Printf.sprintf "?%d" (EcUid.unique ())) in let ty = UE.fresh ue in ps := Mid.add x ty !ps; f_local x ty end | PFref ({ pl_desc = name; pl_loc = loc }, filters) -> begin match Msym.find_opt name (odfl Msym.empty mv) with | None -> tyerror loc env (UnknownMetaVar name) | Some f -> (* FIXME: refresh *) let rec flatten deep f = try let (f1, f2) = EcFol.destr_and f in (if deep then flatten deep f1 else [f1]) @ (flatten deep f2) with DestrError _ -> [f] in let trans_idx (f : form list) (idx : pfindex) = match idx with | `Index i -> i | `Match (ppt, off) -> let ps = ref Mid.empty in let ue = EcUnify.UniEnv.create None in let pt = trans_pattern env ps ue ppt in let ev = EcMatching.MEV.of_idents (Mid.keys !ps) `Form in let mode = EcMatching.fmrigid in let hyps = EcEnv.LDecl.init env [] in let test (_ : int) f = try ignore (EcMatching.f_match mode hyps (ue, ev) ~ptn:pt f); true with EcMatching.MatchFailure -> false in match List.Exceptionless.findi test f with | Some (i, _) -> (i+1) + (odfl 0 off) | None -> tyerror loc env (InvalidFilter (FE_NoMatch)) in let trans_rg (f : form list) (rg : pfrange) = match rg with | `Single idx -> `Single (trans_idx f idx) | `Range (i1, i2) -> let i1 = omap (trans_idx f) i1 in let i2 = omap (trans_idx f) i2 in `Range (i1, i2) in let filter1 (fs : form list) ij = let n = List.length fs in let norm (x as ox) = let x = match x with | x when 0 < x && x <= n -> Some (x - 1) | x when x < 0 && -n <= x -> Some (n + x) | _ -> None in match x with | None -> tyerror loc env (InvalidFilter (FE_InvalidIndex ox)) | Some x -> x in match match ij with | `Single i -> `Single (norm i) | `Range (i, j) -> let i = odfl 0 (omap norm i) in let j = odfl n (omap norm j) in `Range (i, j) with | `Single k -> [List.nth fs k] | `Range (k1, k2) -> List.take (k2 - k1) (List.drop k1 fs) in let filter f pf = match pf with | PFRange (deep, rgs) -> let f = flatten deep f in let rgs = List.map (trans_rg f) rgs in let f = List.map (filter1 f) rgs in f_ands (List.flatten f) | PFMatch (deep, x, ppt) -> let f = f_ands (flatten deep f) in let x = EcIdent.create (unloc x) in let lenv = EcEnv.Var.bind_local x tbool env in let ps = ref Mid.empty in let ue = EcUnify.UniEnv.create None in let pt = trans_pattern lenv ps ue ppt in let ev = EcMatching.MEV.of_idents (x :: Mid.keys !ps) `Form in let mode = EcMatching.fmrigid in let hyps = EcEnv.LDecl.init lenv [] in let (ue, _, ev) = try EcMatching.f_match mode hyps (ue, ev) ~ptn:pt f with EcMatching.MatchFailure -> tyerror ppt.pl_loc env FilterMatchFailure in let subst = EcMatching.MEV.assubst ue ev in Fsubst.f_subst subst (f_local x tbool) | PFMatchBuild (deep, xs, ptg, ppt) -> let f = f_ands (flatten deep f) in let xs = List.map (EcIdent.create |- unloc) xs in let xst = List.map (fun x -> (x, tbool)) xs in let lenv = EcEnv.Var.bind_locals xst env in let tg = trans_prop lenv ue ptg in let ps = ref Mid.empty in let ue = EcUnify.UniEnv.create None in let pt = trans_pattern lenv ps ue ppt in let ev = EcMatching.MEV.of_idents (xs @ Mid.keys !ps) `Form in let mode = EcMatching.fmrigid in let hyps = EcEnv.LDecl.init lenv [] in let (ue, _, ev) = try EcMatching.f_match mode hyps (ue, ev) ~ptn:pt f with EcMatching.MatchFailure -> tyerror ppt.pl_loc env FilterMatchFailure in let subst = EcMatching.MEV.assubst ue ev in Fsubst.f_subst subst tg | PFKeep (deep, rooted, exclude, ppt) -> let f = flatten deep f in let ps = ref Mid.empty in let module E = struct exception MatchFound end in let test = match ppt with | `Pattern ppt -> let ue = EcUnify.UniEnv.create None in let pt = trans_pattern env ps ue ppt in let ev = EcMatching.MEV.of_idents (Mid.keys !ps) `Form in let mode = EcMatching.fmrigid in let hyps = EcEnv.LDecl.init env [] in let test target = try ignore (EcMatching.f_match mode hyps (ue, ev) ~ptn:pt target); raise E.MatchFound with EcMatching.MatchFailure -> `Continue in let test target = if rooted then test target else try ignore (EcMatching.f_match mode hyps (ue, ev) ~ptn:pt target); raise E.MatchFound with EcMatching.MatchFailure -> `Continue in test | `VarSet xs -> let trans1 (x, s) = let mem = match s with | None -> odfl mhr (EcEnv.Memory.get_active env) | Some s -> transmem env s in (transpvar env mem x, mem) in let xs = List.map trans1 xs in let test target = match target.f_node with | Fpvar (p, m) -> if (List.exists (fun (p', m') -> EcMemory.mem_equal m m' && EcEnv.NormMp.pv_equal env p p') xs) then raise E.MatchFound else `Continue | _ -> `Continue in test in let test target = try ignore (EcMatching.FPosition.select (fun _ -> test) target); false with E.MatchFound -> true in let test target = let b = test target in if exclude then not b else b in f_ands (List.filter test f) in List.fold_left filter f filters end | PFcast (pf, pty) -> let ty = transty tp_relax env ue pty in let aout = transf env pf in unify_or_fail env ue pf.pl_loc ~expct:ty aout.f_ty; aout | PFmem _ -> tyerror f.pl_loc env MemNotAllowed | PFscope (popsc, f) -> let opsc = lookup_scope env popsc in transf_r (Some opsc) env f | PFglob gp -> let mp = fst (trans_msymbol env gp) in let me = match EcEnv.Memory.current env with | None -> tyerror f.pl_loc env NoActiveMemory | Some me -> EcMemory.memory me in PFS.set_memused state; f_glob mp me | PFint n -> f_int n | PFdecimal (n, f) -> f_decimal (n, f) | PFtuple args -> begin let args = List.map (transf env) args in match args with | [] -> f_tt | [f] -> f | fs -> f_tuple fs end | PFident ({ pl_desc = name; pl_loc = loc }, tvi) -> let tvi = tvi |> omap (transtvi env ue) in let ops = select_form_op env opsc name ue tvi [] in begin match ops with | [] -> tyerror loc env (UnknownVarOrOp (name, [])) | [sel] -> begin let op = form_of_opselect (env, ue) loc sel [] in let inmem = match op.f_node with | Fpvar _ | Fproj ({ f_node = Fpvar _ }, _) -> true | _ -> false in if inmem then PFS.set_memused state; op end | _ -> let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in tyerror loc env (MultipleOpMatch (name, [], matches)) end | PFside (f, side) -> begin let (sloc, side) = (side.pl_loc, unloc side) in let me = match EcEnv.Memory.lookup side env with | None -> tyerror sloc env (UnknownMemName side) | Some me -> EcMemory.memory me in let used, aout = PFS.new_memused (transf (EcEnv.Memory.set_active me env)) state f in if not used then begin let ppe = EcPrinting.PPEnv.ofenv env in EcEnv.notify ~immediate:false env `Warning "unused memory `%s', while typing %a" side (EcPrinting.pp_form ppe) aout end; aout end | PFeqveq (xs, om) -> 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, [])) | Some (x, ty) -> match x with | `Var x -> f_pvar x ty me | `Proj (x, ty', (i, n)) -> if i = 0 && n = 1 then f_pvar x ty me else f_proj (f_pvar x ty' me) i ty in let check_mem loc me = match EcEnv.Memory.byid me env with | None -> tyerror loc env (UnknownMemName (EcIdent.name me)) | Some _ -> () in let qual (mq : pmsymbol option) (x : pqsymbol) = match mq with | None -> x | Some qs -> let (nm, name) = x.pl_desc in { x with pl_desc = ((List.map (unloc |- fst) qs)@nm, name) } in let do1 = function | GVvar x -> let x1 = lookup EcFol.mleft (qual (om |> omap fst) x) in let x2 = lookup EcFol.mright (qual (om |> omap snd) x) in unify_or_fail env ue x.pl_loc ~expct:x1.f_ty x2.f_ty; f_eq x1 x2 | GVglob (gp, ex) -> let (m, _) = trans_msymbol env gp in let ex = List.map (trans_pv env) ex in let filter_pv (xp, _) = let xp = pv_glob xp in let for1 (ex1, _) = not (EcEnv.NormMp.pv_equal env xp ex1) in List.for_all for1 ex in let create mem = if List.is_empty ex then f_glob m mem else let use = EcEnv.NormMp.mod_use env m in let gl = Sid.elements use.us_gl in let pv = List.filter filter_pv (Mx.bindings use.us_pv) in let res = List.map (fun mid -> f_glob (EcPath.mident mid) mem) gl @ List.map (fun (xp, ty) -> f_pvar (EcTypes.pv_glob xp) ty mem) pv in f_tuple res in let x1 = create EcFol.mleft in let x2 = create EcFol.mright in unify_or_fail env ue gp.pl_loc ~expct:x1.f_ty x2.f_ty; f_eq x1 x2 in check_mem f.pl_loc EcFol.mleft; check_mem f.pl_loc EcFol.mright; EcFol.f_ands (List.map do1 xs) | PFeqf fs -> let check_mem loc me = match EcEnv.Memory.byid me env with | None -> tyerror loc env (UnknownMemName (EcIdent.name me)) | Some _ -> () and do1 (me1, me2) f = let _, f1 = PFS.new_memused (transf (EcEnv.Memory.set_active me1 env)) state f in let _, f2 = PFS.new_memused (transf (EcEnv.Memory.set_active me2 env)) state f in unify_or_fail env ue f.pl_loc ~expct:f1.f_ty f2.f_ty; f_eq f1 f2 in check_mem f.pl_loc EcFol.mleft; check_mem f.pl_loc EcFol.mright; EcFol.f_ands (List.map (do1 (EcFol.mleft, EcFol.mright)) fs) | PFapp ({pl_desc = PFident ({ pl_desc = name; pl_loc = loc }, tvi)}, pes) -> let tvi = tvi |> omap (transtvi env ue) in let es = List.map (transf env) pes in let esig = List.map EcFol.f_ty es in let ops = select_form_op env opsc name ue tvi esig in begin match ops with | [] -> let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) 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 form_of_opselect (env, ue) loc sel es | _ -> let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in tyerror loc env (MultipleOpMatch (name, esig, matches)) end | PFapp (e, pes) -> let es = List.map (transf env) pes in let esig = List.map2 (fun f l -> mk_loc l.pl_loc f.f_ty) es pes in let op = transf env e in let codom = ty_fun_app e.pl_loc env ue op.f_ty esig in f_app op es codom | PFif (pf1, pf2, pf3) -> let f1 = transf env pf1 in let f2 = transf env pf2 in let f3 = transf env pf3 in unify_or_fail env ue pf1.pl_loc ~expct:tbool f1.f_ty; unify_or_fail env ue pf3.pl_loc ~expct:f2.f_ty f3.f_ty; f_if f1 f2 f3 | PFlet (lp, (pf1, paty), f2) -> let (penv, p, pty) = transpattern env ue lp in let aty = paty |> omap (transty tp_uni env ue) in let f1 = transf env pf1 in unify_or_fail env ue pf1.pl_loc ~expct:pty f1.f_ty; aty |> oiter (fun aty-> unify_or_fail env ue pf1.pl_loc ~expct:pty aty); let f2 = transf penv f2 in f_let p f1 f2 | PFforall (xs, pf) -> let env, xs = trans_gbinding env ue xs in let f = transf env pf in unify_or_fail env ue pf.pl_loc ~expct:tbool f.f_ty; f_forall xs f | PFexists (xs, f1) -> let env, xs = trans_gbinding env ue xs in let f = transf env f1 in unify_or_fail env ue f1.pl_loc ~expct:tbool f.f_ty; f_exists xs f | PFlambda (xs, f1) -> let env, xs = trans_binding env ue xs in let f = transf env f1 in f_lambda (List.map (fun (x,ty) -> (x,GTty ty)) xs) f | PFrecord (b, fields) -> let (ctor, fields, (rtvi, reccty)) = let proj (recp, name, (rtvi, reccty), pty, arg) = let proj = EcPath.pqname recp name in let proj = f_op proj rtvi (tfun reccty pty) in f_app proj [arg] pty in trans_record env ue ((fun f -> let f = transf env f in (f, f.f_ty)), proj) (f.pl_loc, b, fields) in let ctor = f_op ctor rtvi (toarrow (List.map snd fields) reccty) in f_app ctor (List.map fst fields) reccty | PFproj (subf, x) -> begin let subf = transf env subf in match select_proj env opsc (unloc x) ue None subf.f_ty with | [] -> let ty = Tuni.offun (EcUnify.UniEnv.assubst ue) subf.f_ty in let lf = let mp = match ty.ty_node with | Tglob mp -> mp | _ -> tyerror x.pl_loc env (UnknownProj (unloc x)) in match NormMp.norm_glob env EcFol.mhr mp with | { f_node = Ftuple xs } -> xs | _ -> tyerror x.pl_loc env (UnknownProj (unloc x)) in let (vx, ty) = match EcEnv.Var.lookup_progvar_opt ~side:EcFol.mhr (unloc x) env with | None -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) | Some (`Var x, ty) -> (NormMp.norm_pvar env x, ty) | Some (_, _) -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) in let find = function | { f_node = Fpvar (x, _) } -> EcTypes.pv_equal vx (NormMp.norm_pvar env x) | _ -> false in let i = match List.oindex find lf with | None -> tyerror x.pl_loc env (UnknownProj (unloc x)) | Some i -> i in f_proj subf i ty | _ :: _ :: _ -> 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 subf.f_ty rty) pty with EcUnify.UnificationFailure _ -> assert false); f_app (f_op op tvi pty) [subf] rty end | PFproji (psubf, i) -> begin let subf = transf env psubf in let ty = Tuni.offun (EcUnify.UniEnv.assubst ue) subf.f_ty in match (EcEnv.ty_hnorm ty env).ty_node with | Ttuple l when i < List.length l -> f_proj subf i (List.nth l i) | _ -> tyerror psubf.pl_loc env (AmbiguousProji (i, ty)) end | PFprob (gp, args, m, event) -> let fpath = trans_gamepath env gp in let fun_ = EcEnv.Fun.by_xpath fpath env in let args,_ = transcall (fun f -> let f = transf env f in f, f.f_ty) env ue f.pl_loc fun_.f_sig args in let memid = transmem env m in let env = EcEnv.Fun.prF fpath env in let event' = transf env event in unify_or_fail env ue event.pl_loc ~expct:tbool event'.f_ty; f_pr memid fpath (f_tuple args) event' | PFhoareF (pre, gp, post) -> let fpath = trans_gamepath env gp in let penv, qenv = EcEnv.Fun.hoareF fpath env in let pre' = transf penv pre in let post' = transf qenv post in 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' | PFBDhoareF (pre, gp, post, hcmp, bd) -> let fpath = trans_gamepath env gp in let penv, qenv = EcEnv.Fun.hoareF fpath env in let pre' = transf penv pre in let post' = transf qenv post in let bd' = transf penv bd in (* FIXME: check that there are not pvars in bd *) 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; unify_or_fail env ue bd .pl_loc ~expct:treal bd' .f_ty; f_bdHoareF pre' fpath post' hcmp bd' | PFlsless gp -> let fpath = trans_gamepath env gp in f_losslessF fpath | PFequivF (pre, (gp1, gp2), post) -> let fpath1 = trans_gamepath env gp1 in let fpath2 = trans_gamepath env gp2 in let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in let pre' = transf penv pre in let post' = transf qenv post in 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_equivF pre' fpath1 fpath2 post' | PFeagerF (pre, (s1,gp1,gp2,s2), post) -> let fpath1 = trans_gamepath env gp1 in let fpath2 = trans_gamepath env gp2 in let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in let pre' = transf penv pre in let post' = transf qenv post in let s1 = transstmt env ue s1 in let s2 = transstmt env ue s2 in 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_eagerF pre' s1 fpath1 fpath2 s2 post' in let f = transf_r None env pf in tt |> oiter (fun tt -> unify_or_fail env ue pf.pl_loc ~expct:tt f.f_ty); f (* -------------------------------------------------------------------- *) and trans_form_opt env ?mv ue pf oty = trans_form_or_pattern env ?mv ue pf oty (* -------------------------------------------------------------------- *) and trans_form env ?mv ue pf ty = trans_form_opt env ?mv ue pf (Some ty) (* -------------------------------------------------------------------- *) and trans_prop env ?mv ue pf = trans_form env ?mv ue pf tbool (* -------------------------------------------------------------------- *) and trans_pattern env ps ue pf = trans_form_or_pattern env ~ps ue pf None (* -------------------------------------------------------------------- *) let get_instances (tvi, bty) env = let inst = List.pmap (function | (_, (`Ring _ | `Field _)) as x -> Some x | _ -> None) (EcEnv.TypeClass.get_instances env) in List.pmap (fun ((typ, gty), cr) -> let ue = EcUnify.UniEnv.create (Some tvi) in let (gty, _typ) = EcUnify.UniEnv.openty ue typ None gty in try EcUnify.unify env ue bty gty; Some (inst, Tuni.offun (EcUnify.UniEnv.close ue) gty, cr) with EcUnify.UnificationFailure _ -> None) inst let get_ring (typ, ty) env = let module E = struct exception Found of ring end in try List.iter (fun (_, _, cr) -> match cr with | `Ring cr -> raise (E.Found cr) | _ -> ()) (get_instances (typ, ty) env); None with E.Found cr -> Some cr let get_field (typ, ty) env = let module E = struct exception Found of field end in try List.iter (fun (_, _, cr) -> match cr with | `Field cr -> raise (E.Found cr) | _ -> ()) (get_instances (typ, ty) env); None with E.Found cr -> Some cr