diff --git a/src/ecSection.ml b/src/ecSection.ml index 3534ea58e..8f54c0bc0 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -91,325 +91,386 @@ let hierror fmt = bfmt fmt (* -------------------------------------------------------------------- *) -let rec on_mp (cb : cb) (mp : mpath) = - let f = m_functor mp in - cb (`Module f); - List.iter (on_mp cb) mp.m_args +type aenv = { + env : EcEnv.env; (* Global environment for dep. analysis *) + cb : cb; (* Dep. analysis callback *) + cache : acache ref; (* Dep. analysis cache *) +} -let on_xp (cb : cb) (xp : xpath) = - on_mp cb xp.x_top +and acache = { + op : Sp.t; (* Operator declaration already handled *) +} -let rec on_ty (cb : cb) (ty : ty) = - match ty.ty_node with - | Tunivar _ -> () - | Tvar _ -> () - | Tglob _ -> () - | Ttuple tys -> List.iter (on_ty cb) tys - | Tconstr (p, tys) -> cb (`Type p); List.iter (on_ty cb) tys - | Tfun (ty1, ty2) -> List.iter (on_ty cb) [ty1; ty2] +(* -------------------------------------------------------------------- *) +let empty_acache : acache = + { op = Sp.empty; } + +(* -------------------------------------------------------------------- *) +let mkaenv (env : EcEnv.env) (cb : cb) : aenv = + { env; cb; cache = ref empty_acache; } + +(* -------------------------------------------------------------------- *) +let rec on_mp (aenv : aenv) (mp : mpath) = + aenv.cb (`Module (m_functor mp)); + List.iter (on_mp aenv) mp.m_args + +(* -------------------------------------------------------------------- *) +and on_xp (aenv : aenv) (xp : xpath) = + on_mp aenv xp.x_top + +(* -------------------------------------------------------------------- *) +and on_memtype (aenv : aenv) (mt : EcMemory.memtype) = + EcMemory.mt_iter_ty (on_ty aenv) mt + +(* -------------------------------------------------------------------- *) +and on_memenv (aenv : aenv) (m : EcMemory.memenv) = + on_memtype aenv (snd m) -let on_pv (cb : cb) (pv : prog_var)= +(* -------------------------------------------------------------------- *) +and on_pv (aenv : aenv) (pv : prog_var)= match pv with - | PVglob xp -> on_xp cb xp + | PVglob xp -> on_xp aenv xp | _ -> () -let on_lp (cb : cb) (lp : lpattern) = +(* -------------------------------------------------------------------- *) +and on_lp (aenv : aenv) (lp : lpattern) = match lp with - | LSymbol (_, ty) -> on_ty cb ty - | LTuple xs -> List.iter (fun (_, ty) -> on_ty cb ty) xs - | LRecord (_, xs) -> List.iter (on_ty cb |- snd) xs + | LSymbol (_, ty) -> on_ty aenv ty + | LTuple xs -> List.iter (fun (_, ty) -> on_ty aenv ty) xs + | LRecord (_, xs) -> List.iter (on_ty aenv |- snd) xs + +(* -------------------------------------------------------------------- *) +and on_binding (aenv : aenv) ((_, ty) : (EcIdent.t * ty)) = + on_ty aenv ty + +(* -------------------------------------------------------------------- *) +and on_bindings (aenv : aenv) (bds : (EcIdent.t * ty) list) = + List.iter (on_binding aenv) bds -let on_binding (cb : cb) ((_, ty) : (EcIdent.t * ty)) = - on_ty cb ty +(* -------------------------------------------------------------------- *) +and on_ty (aenv : aenv) (ty : ty) = + match ty.ty_node with + | Tunivar _ -> () + | Tvar _ -> () + | Tglob _ -> () + | Ttuple tys -> List.iter (on_ty aenv) tys + | Tconstr (p, tys) -> aenv.cb (`Type p); List.iter (on_ty aenv) tys + | Tfun (ty1, ty2) -> List.iter (on_ty aenv) [ty1; ty2] -let on_bindings (cb : cb) (bds : (EcIdent.t * ty) list) = - List.iter (on_binding cb) bds +(* -------------------------------------------------------------------- *) +and on_opname (aenv : aenv) (p : EcPath.path) = + aenv.cb (`Op p); + if not (Sp.mem p !(aenv.cache).op) then begin + let cache = { !(aenv.cache) with op = Sp.add p !(aenv.cache).op } in + aenv.cache := cache; + on_opdecl aenv (EcEnv.Op.by_path p aenv.env); + end -let rec on_expr (cb : cb) (e : expr) = - let cbrec = on_expr cb in +(* -------------------------------------------------------------------- *) +and on_expr (aenv : aenv) (e : expr) = + let cbrec = on_expr aenv in let fornode () = match e.e_node with | Eint _ -> () | Elocal _ -> () - | Equant (_, bds, e) -> on_bindings cb bds; cbrec e - | Evar pv -> on_pv cb pv - | Elet (lp, e1, e2) -> on_lp cb lp; List.iter cbrec [e1; e2] + | Equant (_, bds, e) -> on_bindings aenv bds; cbrec e + | Evar pv -> on_pv aenv pv + | Elet (lp, e1, e2) -> on_lp aenv lp; List.iter cbrec [e1; e2] | Etuple es -> List.iter cbrec es - | Eop (p, tys) -> cb (`Op p); List.iter (on_ty cb) tys | Eapp (e, es) -> List.iter cbrec (e :: es) | Eif (c, e1, e2) -> List.iter cbrec [c; e1; e2] - | Ematch (e, es, ty) -> on_ty cb ty; List.iter cbrec (e :: es) + | Ematch (e, es, ty) -> on_ty aenv ty; List.iter cbrec (e :: es) | Eproj (e, _) -> cbrec e - in on_ty cb e.e_ty; fornode () + | Eop (p, tys) -> begin + on_opname aenv p; + List.iter (on_ty aenv) tys; + end + + in on_ty aenv e.e_ty; fornode () -let on_lv (cb : cb) (lv : lvalue) = - let for1 (pv, ty) = on_pv cb pv; on_ty cb ty in +(* -------------------------------------------------------------------- *) +and on_lv (aenv : aenv) (lv : lvalue) = + let for1 (pv, ty) = on_pv aenv pv; on_ty aenv ty in match lv with | LvVar pv -> for1 pv | LvTuple pvs -> List.iter for1 pvs -let rec on_instr (cb : cb) (i : instr)= +(* -------------------------------------------------------------------- *) +and on_instr (aenv : aenv) (i : instr)= match i.i_node with | Srnd (lv, e) | Sasgn (lv, e) -> - on_lv cb lv; - on_expr cb e + on_lv aenv lv; + on_expr aenv e | Sassert e -> - on_expr cb e + on_expr aenv e | Scall (lv, f, args) -> - lv |> oiter (on_lv cb); - on_xp cb f; - List.iter (on_expr cb) args + oiter (on_lv aenv) lv; + on_xp aenv f; + List.iter (on_expr aenv) args | Sif (e, s1, s2) -> - on_expr cb e; - List.iter (on_stmt cb) [s1; s2] + on_expr aenv e; + List.iter (on_stmt aenv) [s1; s2] | Swhile (e, s) -> - on_expr cb e; - on_stmt cb s + on_expr aenv e; + on_stmt aenv s | Smatch (e, b) -> let forb (bs, s) = - List.iter (on_ty cb |- snd) bs; - on_stmt cb s - in on_expr cb e; List.iter forb b + List.iter (on_ty aenv |- snd) bs; + on_stmt aenv s + in on_expr aenv e; List.iter forb b | Sabstract _ -> () -and on_stmt (cb : cb) (s : stmt) = - List.iter (on_instr cb) s.s_node - -let on_memtype cb mt = - EcMemory.mt_iter_ty (on_ty cb) mt - -let on_memenv cb (m : EcMemory.memenv) = - on_memtype cb (snd m) +(* -------------------------------------------------------------------- *) +and on_stmt (aenv : aenv) (s : stmt) = + List.iter (on_instr aenv) s.s_node -let rec on_form (cb : cb) (f : EcFol.form) = - let cbrec = on_form cb in +(* -------------------------------------------------------------------- *) +and on_form (aenv : aenv) (f : EcFol.form) = + let cbrec = on_form aenv in let rec fornode () = match f.EcAst.f_node with | EcAst.Fint _ -> () | EcAst.Flocal _ -> () - | EcAst.Fquant (_, b, f) -> on_gbindings cb b; cbrec f + | EcAst.Fquant (_, b, f) -> on_gbindings aenv b; cbrec f | EcAst.Fif (f1, f2, f3) -> List.iter cbrec [f1; f2; f3] - | EcAst.Fmatch (b, fs, ty) -> on_ty cb ty; List.iter cbrec (b :: fs) - | EcAst.Flet (lp, f1, f2) -> on_lp cb lp; List.iter cbrec [f1; f2] - | EcAst.Fop (p, tys) -> cb (`Op p); List.iter (on_ty cb) tys + | EcAst.Fmatch (b, fs, ty) -> on_ty aenv ty; List.iter cbrec (b :: fs) + | EcAst.Flet (lp, f1, f2) -> on_lp aenv lp; List.iter cbrec [f1; f2] | EcAst.Fapp (f, fs) -> List.iter cbrec (f :: fs) | EcAst.Ftuple fs -> List.iter cbrec fs | EcAst.Fproj (f, _) -> cbrec f - | EcAst.Fpvar (pv, _) -> on_pv cb pv + | EcAst.Fpvar (pv, _) -> on_pv aenv pv | EcAst.Fglob _ -> () - | EcAst.FhoareF hf -> on_hf cb hf - | EcAst.FhoareS hs -> on_hs cb hs - | EcAst.FeHoareF hf -> on_ehf cb hf - | EcAst.FeHoareS hs -> on_ehs cb hs - | EcAst.FequivF ef -> on_ef cb ef - | EcAst.FequivS es -> on_es cb es - | EcAst.FeagerF eg -> on_eg cb eg - | EcAst.FbdHoareS bhs -> on_bhs cb bhs - | EcAst.FbdHoareF bhf -> on_bhf cb bhf - | EcAst.Fpr pr -> on_pr cb pr - - and on_hf cb hf = - on_form cb (hf_pr hf).inv; - on_form cb (hf_po hf).inv; - on_xp cb hf.EcAst.hf_f - - and on_hs cb hs = - on_form cb (hs_pr hs).inv; - on_form cb (hs_po hs).inv; - on_stmt cb hs.EcAst.hs_s; - on_memenv cb hs.EcAst.hs_m - - and on_ef cb ef = - on_form cb (EcAst.ef_pr ef).inv; - on_form cb (EcAst.ef_po ef).inv; - on_xp cb ef.EcAst.ef_fl; - on_xp cb ef.EcAst.ef_fr - - and on_es cb es = - on_form cb (EcAst.es_pr es).inv; - on_form cb (EcAst.es_po es).inv; - on_stmt cb es.EcAst.es_sl; - on_stmt cb es.EcAst.es_sr; - on_memenv cb es.EcAst.es_ml; - on_memenv cb es.EcAst.es_mr - - and on_eg cb eg = - on_form cb (EcAst.eg_pr eg).inv; - on_form cb (EcAst.eg_po eg).inv; - on_xp cb eg.EcAst.eg_fl; - on_xp cb eg.EcAst.eg_fr; - on_stmt cb eg.EcAst.eg_sl; - on_stmt cb eg.EcAst.eg_sr; - - and on_ehf cb hf = - on_form cb (EcAst.ehf_pr hf).inv; - on_form cb (EcAst.ehf_po hf).inv; - on_xp cb hf.EcAst.ehf_f - - and on_ehs cb hs = - on_form cb (EcAst.ehs_pr hs).inv; - on_form cb (EcAst.ehs_po hs).inv; - on_stmt cb hs.EcAst.ehs_s; - on_memenv cb hs.EcAst.ehs_m - - and on_bhf cb bhf = - on_form cb (EcAst.bhf_pr bhf).inv; - on_form cb (EcAst.bhf_po bhf).inv; - on_form cb (EcAst.bhf_bd bhf).inv; - on_xp cb bhf.EcAst.bhf_f - - and on_bhs cb bhs = - on_form cb (EcAst.bhs_pr bhs).inv; - on_form cb (EcAst.bhs_po bhs).inv; - on_form cb (EcAst.bhs_bd bhs).inv; - on_stmt cb bhs.EcAst.bhs_s; - on_memenv cb bhs.EcAst.bhs_m - - - and on_pr cb pr = - on_xp cb pr.EcAst.pr_fun; - List.iter (on_form cb) [pr.EcAst.pr_event.inv; pr.EcAst.pr_args] + | EcAst.FhoareF hf -> on_hf aenv hf + | EcAst.FhoareS hs -> on_hs aenv hs + | EcAst.FeHoareF hf -> on_ehf aenv hf + | EcAst.FeHoareS hs -> on_ehs aenv hs + | EcAst.FequivF ef -> on_ef aenv ef + | EcAst.FequivS es -> on_es aenv es + | EcAst.FeagerF eg -> on_eg aenv eg + | EcAst.FbdHoareS bhs -> on_bhs aenv bhs + | EcAst.FbdHoareF bhf -> on_bhf aenv bhf + | EcAst.Fpr pr -> on_pr aenv pr + + | EcAst.Fop (p, tys) -> begin + on_opname aenv p; + List.iter (on_ty aenv) tys; + end + + and on_hf (aenv : aenv) hf = + on_form aenv (hf_pr hf).inv; + on_form aenv (hf_po hf).inv; + on_xp aenv hf.EcAst.hf_f + + and on_hs (aenv : aenv) hs = + on_form aenv (hs_pr hs).inv; + on_form aenv (hs_po hs).inv; + on_stmt aenv hs.EcAst.hs_s; + on_memenv aenv hs.EcAst.hs_m + + and on_ef (aenv : aenv) ef = + on_form aenv (EcAst.ef_pr ef).inv; + on_form aenv (EcAst.ef_po ef).inv; + on_xp aenv ef.EcAst.ef_fl; + on_xp aenv ef.EcAst.ef_fr + + and on_es (aenv : aenv) es = + on_form aenv (EcAst.es_pr es).inv; + on_form aenv (EcAst.es_po es).inv; + on_stmt aenv es.EcAst.es_sl; + on_stmt aenv es.EcAst.es_sr; + on_memenv aenv es.EcAst.es_ml; + on_memenv aenv es.EcAst.es_mr + + and on_eg (aenv : aenv) eg = + on_form aenv (EcAst.eg_pr eg).inv; + on_form aenv (EcAst.eg_po eg).inv; + on_xp aenv eg.EcAst.eg_fl; + on_xp aenv eg.EcAst.eg_fr; + on_stmt aenv eg.EcAst.eg_sl; + on_stmt aenv eg.EcAst.eg_sr; + + and on_ehf (aenv : aenv) hf = + on_form aenv (EcAst.ehf_pr hf).inv; + on_form aenv (EcAst.ehf_po hf).inv; + on_xp aenv hf.EcAst.ehf_f + + and on_ehs (aenv : aenv) hs = + on_form aenv (EcAst.ehs_pr hs).inv; + on_form aenv (EcAst.ehs_po hs).inv; + on_stmt aenv hs.EcAst.ehs_s; + on_memenv aenv hs.EcAst.ehs_m + + and on_bhf (aenv : aenv) bhf = + on_form aenv (EcAst.bhf_pr bhf).inv; + on_form aenv (EcAst.bhf_po bhf).inv; + on_form aenv (EcAst.bhf_bd bhf).inv; + on_xp aenv bhf.EcAst.bhf_f + + and on_bhs (aenv : aenv) bhs = + on_form aenv (EcAst.bhs_pr bhs).inv; + on_form aenv (EcAst.bhs_po bhs).inv; + on_form aenv (EcAst.bhs_bd bhs).inv; + on_stmt aenv bhs.EcAst.bhs_s; + on_memenv aenv bhs.EcAst.bhs_m + + + and on_pr (aenv : aenv) pr = + on_xp aenv pr.EcAst.pr_fun; + List.iter (on_form aenv) [pr.EcAst.pr_event.inv; pr.EcAst.pr_args] in - on_ty cb f.EcAst.f_ty; fornode () + on_ty aenv f.EcAst.f_ty; fornode () -and on_restr (cb : cb) (restr : mod_restr) = - let doit (xs, ms) = Sx.iter (on_xp cb) xs; Sm.iter (on_mp cb) ms in +(* -------------------------------------------------------------------- *) +and on_restr (aenv : aenv) (restr : mod_restr) = + let doit (xs, ms) = Sx.iter (on_xp aenv) xs; Sm.iter (on_mp aenv) ms in oiter doit restr.ur_pos; doit restr.ur_neg -and on_modty cb (mty : module_type) = - cb (`ModuleType mty.mt_name); - List.iter (fun (_, mty) -> on_modty cb mty) mty.mt_params; - List.iter (on_mp cb) mty.mt_args +(* -------------------------------------------------------------------- *) +and on_modty (aenv : aenv) (mty : module_type) = + aenv.cb (`ModuleType mty.mt_name); + List.iter (fun (_, mty) -> on_modty aenv mty) mty.mt_params; + List.iter (on_mp aenv) mty.mt_args -and on_mty_mr (cb : cb) ((mty, mr) : mty_mr) = - on_modty cb mty; on_restr cb mr +(* -------------------------------------------------------------------- *) +and on_mty_mr (aenv : aenv) ((mty, mr) : mty_mr) = + on_modty aenv mty; on_restr aenv mr -and on_gbinding (cb : cb) (b : gty) = +(* -------------------------------------------------------------------- *) +and on_gbinding (aenv : aenv) (b : gty) = match b with | EcAst.GTty ty -> - on_ty cb ty + on_ty aenv ty | EcAst.GTmodty mty -> - on_mty_mr cb mty + on_mty_mr aenv mty | EcAst.GTmem m -> - on_memtype cb m + on_memtype aenv m -and on_gbindings (cb : cb) (b : (EcIdent.t * gty) list) = - List.iter (fun (_, b) -> on_gbinding cb b) b +(* -------------------------------------------------------------------- *) +and on_gbindings (aenv : aenv) (b : (EcIdent.t * gty) list) = + List.iter (fun (_, b) -> on_gbinding aenv b) b -and on_module (cb : cb) (me : module_expr) = +(* -------------------------------------------------------------------- *) +and on_module (aenv : aenv) (me : module_expr) = match me.me_body with - | ME_Alias (_, mp) -> on_mp cb mp - | ME_Structure st -> on_mstruct cb st - | ME_Decl mty -> on_mty_mr cb mty + | ME_Alias (_, mp) -> on_mp aenv mp + | ME_Structure st -> on_mstruct aenv st + | ME_Decl mty -> on_mty_mr aenv mty -and on_mstruct (cb : cb) (st : module_structure) = - List.iter (on_mpath_mstruct1 cb) st.ms_body +(* -------------------------------------------------------------------- *) +and on_mstruct (aenv : aenv) (st : module_structure) = + List.iter (on_mpath_mstruct1 aenv) st.ms_body -and on_mpath_mstruct1 (cb : cb) (item : module_item) = +(* -------------------------------------------------------------------- *) +and on_mpath_mstruct1 (aenv : aenv) (item : module_item) = match item with - | MI_Module me -> on_module cb me - | MI_Variable x -> on_ty cb x.v_type - | MI_Function f -> on_fun cb f + | MI_Module me -> on_module aenv me + | MI_Variable x -> on_ty aenv x.v_type + | MI_Function f -> on_fun aenv f -and on_fun (cb : cb) (fun_ : function_) = - on_fun_sig cb fun_.f_sig; - on_fun_body cb fun_.f_def +(* -------------------------------------------------------------------- *) +and on_fun (aenv : aenv) (fun_ : function_) = + on_fun_sig aenv fun_.f_sig; + on_fun_body aenv fun_.f_def -and on_fun_sig (cb : cb) (fsig : funsig) = - on_ty cb fsig.fs_arg; - on_ty cb fsig.fs_ret +(* -------------------------------------------------------------------- *) +and on_fun_sig (aenv : aenv) (fsig : funsig) = + on_ty aenv fsig.fs_arg; + on_ty aenv fsig.fs_ret -and on_fun_body (cb : cb) (fbody : function_body) = +(* -------------------------------------------------------------------- *) +and on_fun_body (aenv : aenv) (fbody : function_body) = match fbody with - | FBalias xp -> on_xp cb xp - | FBdef fdef -> on_fun_def cb fdef - | FBabs oi -> on_oi cb oi + | FBalias xp -> on_xp aenv xp + | FBdef fdef -> on_fun_def aenv fdef + | FBabs oi -> on_oi aenv oi -and on_fun_def (cb : cb) (fdef : function_def) = - List.iter (fun v -> on_ty cb v.v_type) fdef.f_locals; - on_stmt cb fdef.f_body; - fdef.f_ret |> oiter (on_expr cb); - on_uses cb fdef.f_uses +(* -------------------------------------------------------------------- *) +and on_fun_def (aenv : aenv) (fdef : function_def) = + List.iter (fun v -> on_ty aenv v.v_type) fdef.f_locals; + on_stmt aenv fdef.f_body; + fdef.f_ret |> oiter (on_expr aenv); + on_uses aenv fdef.f_uses -and on_uses (cb : cb) (uses : uses) = - List.iter (on_xp cb) uses.us_calls; - Sx.iter (on_xp cb) uses.us_reads; - Sx.iter (on_xp cb) uses.us_writes +(* -------------------------------------------------------------------- *) +and on_uses (aenv : aenv) (uses : uses) = + List.iter (on_xp aenv) uses.us_calls; + Sx.iter (on_xp aenv) uses.us_reads; + Sx.iter (on_xp aenv) uses.us_writes -and on_oi (cb : cb) (oi : OI.t) = - List.iter (on_xp cb) (OI.allowed oi) +(* -------------------------------------------------------------------- *) +and on_oi (aenv : aenv) (oi : OI.t) = + List.iter (on_xp aenv) (OI.allowed oi) (* -------------------------------------------------------------------- *) -let on_typeclasses cb s = - Sp.iter (fun p -> cb (`Typeclass p)) s +and on_typeclasses (aenv : aenv) s = + Sp.iter (fun p -> aenv.cb (`Typeclass p)) s -let on_typarams cb typarams = - List.iter (fun (_,s) -> on_typeclasses cb s) typarams +and on_typarams (aenv : aenv) typarams = + List.iter (fun (_,s) -> on_typeclasses aenv s) typarams (* -------------------------------------------------------------------- *) -let on_tydecl (cb : cb) (tyd : tydecl) = - on_typarams cb tyd.tyd_params; +and on_tydecl (aenv : aenv) (tyd : tydecl) = + on_typarams aenv tyd.tyd_params; match tyd.tyd_type with - | `Concrete ty -> on_ty cb ty - | `Abstract s -> on_typeclasses cb s + | `Concrete ty -> on_ty aenv ty + | `Abstract s -> on_typeclasses aenv s | `Record (f, fds) -> - on_form cb f; - List.iter (on_ty cb |- snd) fds + on_form aenv f; + List.iter (on_ty aenv |- snd) fds | `Datatype dt -> - List.iter (List.iter (on_ty cb) |- snd) dt.tydt_ctors; - List.iter (on_form cb) [dt.tydt_schelim; dt.tydt_schcase] + List.iter (List.iter (on_ty aenv) |- snd) dt.tydt_ctors; + List.iter (on_form aenv) [dt.tydt_schelim; dt.tydt_schcase] -let on_typeclass cb tc = - oiter (fun p -> cb (`Typeclass p)) tc.tc_prt; - List.iter (fun (_,ty) -> on_ty cb ty) tc.tc_ops; - List.iter (fun (_,f) -> on_form cb f) tc.tc_axs +and on_typeclass (aenv : aenv) tc = + oiter (fun p -> aenv.cb (`Typeclass p)) tc.tc_prt; + List.iter (fun (_,ty) -> on_ty aenv ty) tc.tc_ops; + List.iter (fun (_,f) -> on_form aenv f) tc.tc_axs (* -------------------------------------------------------------------- *) -let on_opdecl (cb : cb) (opdecl : operator) = - on_typarams cb opdecl.op_tparams; +and on_opdecl (aenv : aenv) (opdecl : operator) = + on_typarams aenv opdecl.op_tparams; let for_kind () = match opdecl.op_kind with | OB_pred None -> () | OB_pred (Some (PR_Plain f)) -> - on_form cb f + on_form aenv f | OB_pred (Some (PR_Ind pri)) -> - on_bindings cb pri.pri_args; + on_bindings aenv pri.pri_args; List.iter (fun ctor -> - on_gbindings cb ctor.prc_bds; - List.iter (on_form cb) ctor.prc_spec) + on_gbindings aenv ctor.prc_bds; + List.iter (on_form aenv) ctor.prc_spec) pri.pri_ctors | OB_nott nott -> - List.iter (on_ty cb |- snd) nott.ont_args; - on_ty cb nott.ont_resty; - on_expr cb nott.ont_body + List.iter (on_ty aenv |- snd) nott.ont_args; + on_ty aenv nott.ont_resty; + on_expr aenv nott.ont_body | OB_oper None -> () | OB_oper Some b -> match b with - | OP_Constr _ | OP_Record _ | OP_Proj _ -> assert false - | OP_TC -> assert false - | OP_Plain f -> on_form cb f + | OP_Constr _ | OP_Record _ | OP_Proj _ | OP_TC -> () + | OP_Plain f -> on_form aenv f | OP_Fix f -> let rec on_mpath_branches br = match br with | OPB_Leaf (bds, e) -> - List.iter (on_bindings cb) bds; - on_expr cb e + List.iter (on_bindings aenv) bds; + on_expr aenv e | OPB_Branch br -> Parray.iter on_mpath_branch br @@ -418,45 +479,48 @@ let on_opdecl (cb : cb) (opdecl : operator) = in on_mpath_branches f.opf_branches - in on_ty cb opdecl.op_ty; for_kind () + in on_ty aenv opdecl.op_ty; for_kind () (* -------------------------------------------------------------------- *) -let on_axiom (cb : cb) (ax : axiom) = - on_typarams cb ax.ax_tparams; - on_form cb ax.ax_spec +and on_axiom (aenv : aenv) (ax : axiom) = + on_typarams aenv ax.ax_tparams; + on_form aenv ax.ax_spec (* -------------------------------------------------------------------- *) -let on_modsig (cb:cb) (ms:module_sig) = - List.iter (fun (_,mt) -> on_modty cb mt) ms.mis_params; +and on_modsig (aenv : aenv) (ms:module_sig) = + List.iter (fun (_,mt) -> on_modty aenv mt) ms.mis_params; List.iter (fun (Tys_function fs) -> - on_ty cb fs.fs_arg; - List.iter (fun x -> on_ty cb x.ov_type) fs.fs_anames; - on_ty cb fs.fs_ret;) ms.mis_body; - Msym.iter (fun _ oi -> on_oi cb oi) ms.mis_oinfos - -let on_ring cb r = - on_ty cb r.r_type; - let on_p p = cb (`Op p) in + on_ty aenv fs.fs_arg; + List.iter (fun x -> on_ty aenv x.ov_type) fs.fs_anames; + on_ty aenv fs.fs_ret;) ms.mis_body; + Msym.iter (fun _ oi -> on_oi aenv oi) ms.mis_oinfos + +(* -------------------------------------------------------------------- *) +and on_ring (aenv : aenv) (r : ring) = + on_ty aenv r.r_type; + let on_p p = on_opname aenv p in List.iter on_p [r.r_zero; r.r_one; r.r_add; r.r_mul]; List.iter (oiter on_p) [r.r_opp; r.r_exp; r.r_sub]; match r.r_embed with | `Direct | `Default -> () | `Embed p -> on_p p -let on_field cb f = - on_ring cb f.f_ring; - let on_p p = cb (`Op p) in +(* -------------------------------------------------------------------- *) +and on_field (aenv : aenv) (f : field) = + on_ring aenv f.f_ring; + let on_p p = on_opname aenv p in on_p f.f_inv; oiter on_p f.f_div -let on_instance cb ty tci = - on_typarams cb (fst ty); - on_ty cb (snd ty); +(* -------------------------------------------------------------------- *) +and on_instance (aenv : aenv) ty tci = + on_typarams aenv (fst ty); + on_ty aenv (snd ty); match tci with - | `Ring r -> on_ring cb r - | `Field f -> on_field cb f + | `Ring r -> on_ring aenv r + | `Field f -> on_field aenv f | `General p -> (* FIXME section: ring/field use type class that do not exists *) - cb (`Typeclass p) + aenv.cb (`Typeclass p) (* -------------------------------------------------------------------- *) type sc_name = @@ -973,7 +1037,7 @@ let generalize_module to_gen prefix me = | _ -> () in try - on_mp check_gen mp; + on_mp (mkaenv to_gen.tg_env.sc_env check_gen) mp; to_gen, Some (Th_module me) with Inline -> @@ -1159,27 +1223,7 @@ let check_tyd scenv prefix name tyd = d_modty = []; d_tc = [`Global]; } in - on_tydecl (cb scenv from cd) tyd - -(* -let cb_glob scenv (who:cbarg) = - match who with - | `Type p -> - if is_local scenv who then - hierror "global definition can't depend of local type %s" - (EcPath.tostring p) - | `Module mp -> - check_glob_mp scenv mp - | `Op p -> - if is_local scenv who then - hierror "global definition can't depend of local op %s" - (EcPath.tostring p) - | `ModuleType p -> - if is_local scenv who then - hierror "global definition can't depend of local module type %s" - (EcPath.tostring p) - | `Ax _ | `Typeclass _ -> assert false -*) + on_tydecl (mkaenv scenv.sc_env (cb scenv from cd)) tyd let is_abstract_op op = match op.op_kind with @@ -1205,7 +1249,7 @@ let check_op scenv prefix name op = d_modty = []; d_tc = [`Global]; } in - on_opdecl (cb scenv from cd) op + on_opdecl (mkaenv scenv.sc_env (cb scenv from cd)) op | `Global -> let cd = { @@ -1217,7 +1261,7 @@ let check_op scenv prefix name op = d_modty = []; d_tc = [`Global]; } in - on_opdecl (cb scenv from cd) op + on_opdecl (mkaenv scenv.sc_env (cb scenv from cd)) op let is_inth scenv = match scenv.sc_name with @@ -1236,7 +1280,7 @@ let check_ax (scenv : scenv) (prefix : path) (name : symbol) (ax : axiom) = d_modty = [`Global]; d_tc = [`Global]; } in - let doit = on_axiom (cb scenv from cd) in + let doit = on_axiom (mkaenv scenv.sc_env (cb scenv from cd)) in let error b s1 s = if b then hierror "%s %a %s" s1 (pp_axname scenv) path s in @@ -1268,7 +1312,7 @@ let check_modtype scenv prefix name ms = | `Local -> check_section scenv from | `Global -> if scenv.sc_insec then - on_modsig (cb scenv from cd_glob) ms.tms_sig + on_modsig (mkaenv scenv.sc_env (cb scenv from cd_glob)) ms.tms_sig let check_module scenv prefix tme = @@ -1288,7 +1332,7 @@ let check_module scenv prefix tme = d_modty = [`Global]; d_tc = [`Global]; } in - on_module (cb scenv from cd) me + on_module (mkaenv scenv.sc_env (cb scenv from cd)) me | `Declare -> (* Should be SC_decl_mod ... *) assert false @@ -1297,7 +1341,7 @@ let check_typeclass scenv prefix name tc = let from = ((tc.tc_loca :> locality), `Typeclass path) in if tc.tc_loca = `Local then check_section scenv from else - on_typeclass (cb scenv from cd_glob) tc + on_typeclass (mkaenv scenv.sc_env (cb scenv from cd_glob)) tc let check_instance scenv ty tci lc = let from = (lc :> locality), `Instance tci in @@ -1305,10 +1349,11 @@ let check_instance scenv ty tci lc = else if scenv.sc_insec then match tci with - | `Ring _ | `Field _ -> on_instance (cb scenv from cd_glob) ty tci + | `Ring _ | `Field _ -> + on_instance (mkaenv scenv.sc_env (cb scenv from cd_glob) )ty tci | `General _ -> let cd = { cd_glob with d_ty = [`Declare; `Global]; } in - on_instance (cb scenv from cd) ty tci + on_instance (mkaenv scenv.sc_env (cb scenv from cd)) ty tci (* -----------------------------------------------------------*) let enter_theory (name:symbol) (lc:is_local) (mode:thmode) scenv : scenv = @@ -1527,7 +1572,7 @@ let add_decl_mod id mt scenv = d_tc = [`Global]; } in let from = `Declare, `Module (mpath_abs id []) in - on_mty_mr (cb scenv from cd) mt; + on_mty_mr (mkaenv scenv.sc_env (cb scenv from cd)) mt; { scenv with sc_env = EcEnv.Mod.declare_local id mt scenv.sc_env; sc_items = SC_decl_mod (id, mt) :: scenv.sc_items }