diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 4a28057e3..cd32c69e5 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -334,11 +334,15 @@ let select_pv env side name ue tvi (psig, retty) try let (pv, ty) = EcEnv.Var.lookup_progvar ?side name env in let subue = UE.copy ue in - match EcUnify.classify_application env subue ty psig retty with - | None -> ([(pv, ty, subue)], []) - | Some f -> - let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in - ([], [(`Pv (pv0, ty), f)]) + let expected = toarrow psig (ofdfl (fun () -> UE.fresh subue) retty) in + try + EcUnify.unify env subue ty expected; + ([(pv, ty, subue)], []) + with EcUnify.UnificationFailure _ -> + let subue = UE.copy ue in + let f = oget (EcUnify.classify_application env subue ty psig retty) in + let pv0 = match pv with `Var p -> p | `Proj (p, _) -> p in + ([], [(`Pv (pv0, ty), f)]) with EcEnv.LookupFailure _ -> ([], []) (* -------------------------------------------------------------------- *) @@ -374,11 +378,9 @@ let gen_select_op (ue : EcUnify.unienv) (psig : EcTypes.dom * EcTypes.ty option) - : OpSelect.gopsel list * OpSelect.opfailure list + : OpSelect.gopsel list * OpSelect.opfailure list Lazy.t = - let opfailures = ref [] in - let fpv me (pv, ty, ue) : OpSelect.gopsel = (`Pv (me, pv), ty, ue, (pv :> opmatch)) @@ -417,30 +419,22 @@ let gen_select_op |> Option.to_list else [] in + let pvfailures = ref [] in + let ops () : OpSelect.gopsel list = - let outcomes = - EcUnify.select_op_outcomes ~filter:ue_filter tvi env name ue psig in - let ops = - List.filter_map - (function EcUnify.OK r -> Some r | EcUnify.KO _ -> None) outcomes in - opfailures := !opfailures @ - List.filter_map - (function - | EcUnify.KO (p, inst, ty, f) -> Some (`Op (p, inst, ty), f) - | EcUnify.OK _ -> None) - outcomes; + 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 () : OpSelect.gopsel list = - let me, (pvs, pvfailures) = + let me, (pvs, pvf) = match EcEnv.Memory.get_active_ss env, actonly with | None, true -> (None, ([], [])) | me , _ -> ( me, select_pv env me name ue tvi psig) in - opfailures := !opfailures @ pvfailures; + pvfailures := pvf; List.map (fpv me) pvs in @@ -460,7 +454,15 @@ let gen_select_op else select [locals; pvs; ops] in - (selected, !opfailures) + + let opfailures = lazy ( + !pvfailures + @ List.map + (fun (p, inst, ty, f) -> (`Op (p, inst, ty), f)) + (EcUnify.select_op_failures ~filter:ue_filter tvi env name ue psig) + ) in + + (selected, opfailures) (* -------------------------------------------------------------------- *) let select_exp_op env mode opsc name ue tvi psig = @@ -475,10 +477,11 @@ let select_form_op env mode ~forcepv opsc name ue tvi psig = (* -------------------------------------------------------------------- *) (* [UnappliedOp] when candidates of that name exist but fail, else [UnknownVarOrOp]. *) -let tyerror_noop env loc name esig retty (opfailures : OpSelect.opfailure list) = - match opfailures with +let tyerror_noop env loc name esig retty + (opfailures : OpSelect.opfailure list Lazy.t) = + match Lazy.force opfailures with | [] -> tyerror loc env (UnknownVarOrOp (name, esig)) - | _ -> tyerror loc env (UnappliedOp (name, esig, retty, opfailures)) + | opfailures -> tyerror loc env (UnappliedOp (name, esig, retty, opfailures)) (* -------------------------------------------------------------------- *) let select_proj env opsc name ue tvi recty = diff --git a/src/ecUnify.ml b/src/ecUnify.ml index ea387a03b..55a9a0f67 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -342,7 +342,7 @@ type op_instance = (EcIdent.t * ty) list type select_outcome = | OK of select_result - | KO of EcPath.path * op_instance * ty * op_failure + | KO of (EcPath.path * op_instance * ty * op_failure) Lazy.t (* operator path, partial instantiation, declared operator type, reason *) (* -------------------------------------------------------------------- *) @@ -434,7 +434,23 @@ let select_op_outcomes filter oppath op && filter_on_tvi op in - let select (path, op) = + let mk_ok (path, op) tip tvs top subue = + let bd = + match op.D.op_kind with + | OB_nott nt -> + let substnt () = + let xs = List.map (snd_map (ty_subst tip)) nt.D.ont_args in + let es = e_subst tip in + let bd = es nt.D.ont_body in + (xs, bd) + in Some (Lazy.from_fun substnt) + + | _ -> None + + in OK ((path, tvs), top, subue, bd) + in + + let classify (path, op) = let subue = UniEnv.copy ue in let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in @@ -442,32 +458,29 @@ let select_op_outcomes let resolve ty = ty_subst (Tuni.subst (UniEnv.assubst subue)) ty in - let failure = classify_application env subue top psig retty in + (* [select] builds a [KO] only after unification rejected the candidate. *) + let f = oget (classify_application env subue top psig retty) in + let instance = + List.combine op.D.op_tparams tvs + |> List.filter_map (fun (tp, tv) -> + match (resolve tv).ty_node with + | Tunivar _ -> None + | _ -> Some (tp, resolve tv)) + in + (path, instance, op.D.op_ty, f) + in - match failure with - | Some f -> - let instance = - List.combine op.D.op_tparams tvs - |> List.filter_map (fun (tp, tv) -> - match (resolve tv).ty_node with - | Tunivar _ -> None - | _ -> Some (tp, resolve tv)) - in - KO (path, instance, op.D.op_ty, f) - | None -> - let bd = - match op.D.op_kind with - | OB_nott nt -> - let substnt () = - let xs = List.map (snd_map (ty_subst tip)) nt.D.ont_args in - let es = e_subst tip in - let bd = es nt.D.ont_body in - (xs, bd) - in Some (Lazy.from_fun substnt) + let select (path, op) = + let subue = UniEnv.copy ue in - | _ -> None + let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in + let top = ty_subst tip op.D.op_ty in + + let texpected = tfun_expected subue ?retty psig in - in OK ((path, tvs), top, subue, bd) + match unify env subue top texpected with + | () -> mk_ok (path, op) tip tvs top subue + | exception UnificationFailure _ -> KO (lazy (classify (path, op))) in List.map select (EcEnv.Op.all ~check:filter ~name env) @@ -482,3 +495,15 @@ let select_op List.filter_map (function OK r -> Some r | KO _ -> None) (select_op_outcomes ?hidden ?filter tvi env name ue sig_) + +(* -------------------------------------------------------------------- *) +(* The candidates of that name that fail to apply, with the reason why. *) +let select_op_failures + ?hidden ?filter (tvi : tvar_inst option) + (env : EcEnv.env) (name : qsymbol) (ue : unienv) + (sig_ : ty list * ty option) + : (EcPath.path * op_instance * ty * op_failure) list += + List.filter_map + (function KO lz -> Some (Lazy.force lz) | OK _ -> None) + (select_op_outcomes ?hidden ?filter tvi env name ue sig_) diff --git a/src/ecUnify.mli b/src/ecUnify.mli index 6713131e4..31d9a658a 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -50,11 +50,6 @@ type op_failure = (* Constrained type parameters of an operator (those bound while applying it). *) type op_instance = (EcIdent.t * ty) list -type select_outcome = - | OK of select_result - | KO of EcPath.path * op_instance * ty * op_failure - (* operator path, partial instantiation, declared operator type, reason *) - (* [None] if [top] applies to [psig] (and [retty]), updating [ue]; otherwise [Some] of the first argument/result/arity failure. *) val classify_application : @@ -70,7 +65,7 @@ val select_op : -> dom * ty option -> select_result list -val select_op_outcomes : +val select_op_failures : ?hidden:bool -> ?filter:(path -> operator -> bool) -> tvi @@ -78,4 +73,4 @@ val select_op_outcomes : -> qsymbol -> unienv -> dom * ty option - -> select_outcome list + -> (path * op_instance * ty * op_failure) list