diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.ml | 36 | ||||
-rw-r--r-- | engine/evarutil.ml | 3 | ||||
-rw-r--r-- | engine/evd.ml | 12 | ||||
-rw-r--r-- | engine/termops.ml | 21 |
4 files changed, 38 insertions, 34 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 2ab545612..6810626ad 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -285,7 +285,7 @@ let map sigma f c = match kind sigma c with else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,t) -> @@ -293,23 +293,23 @@ let map sigma f c = match kind sigma c with if t' == t then c else mkProj (p, t') | Evar (e,l) -> - let l' = Array.smartmap f l in + let l' = Array.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,p,b,bl) -> let b' = f b in let p' = f p in - let bl' = Array.smartmap f bl in + let bl' = Array.Smart.map f bl in if b'==b && p'==p && bl'==bl then c else mkCase (ci, p', b', bl') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap f tl in - let bl' = Array.smartmap f bl in + let tl' = Array.Smart.map f tl in + let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) @@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.smartmap f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.smartmap f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.smartmap f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.smartmap f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) let iter sigma f c = match kind sigma c with @@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c = | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; @@ -783,7 +783,7 @@ let of_existential : Constr.existential -> existential = let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) -let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) +let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e) let map_rel_context_in_env f env sign = let rec aux env acc = function diff --git a/engine/evarutil.ml b/engine/evarutil.ml index cb2d01bdf..afedfe180 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Pre_env open Environ open Evd open Termops @@ -214,7 +213,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta()) let non_instantiated sigma = let listev = Evd.undefined_map sigma in - Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev (************************) (* Manipulating filters *) diff --git a/engine/evd.ml b/engine/evd.ml index 03b843655..78d5d4c8f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -510,8 +510,8 @@ let raw_map f d = in ans in - let defn_evars = EvMap.smartmapi f d.defn_evars in - let undf_evars = EvMap.smartmapi f d.undf_evars in + let defn_evars = EvMap.Smart.mapi f d.defn_evars in + let undf_evars = EvMap.Smart.mapi f d.undf_evars in { d with defn_evars; undf_evars; } let raw_map_undefined f d = @@ -524,7 +524,7 @@ let raw_map_undefined f d = in ans in - { d with undf_evars = EvMap.smartmapi f d.undf_evars; } + { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; } let is_evar = mem @@ -1040,11 +1040,11 @@ let map_metas_fvalue f evd = | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ) | x -> x in - set_metas evd (Metamap.smartmap map evd.metas) + set_metas evd (Metamap.Smart.map map evd.metas) let map_metas f evd = let map cl = map_clb f cl in - set_metas evd (Metamap.smartmap map evd.metas) + set_metas evd (Metamap.Smart.map map evd.metas) let meta_opt_fvalue evd mv = match Metamap.find mv evd.metas with @@ -1120,7 +1120,7 @@ let retract_coercible_metas evd = Cltyp (na, typ) | v -> v in - let metas = Metamap.smartmapi map evd.metas in + let metas = Metamap.Smart.mapi map evd.metas in !mc, set_metas evd metas let evar_source_of_meta mv evd = diff --git a/engine/termops.ml b/engine/termops.ml index c271d9d99..c52f96079 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -98,7 +98,10 @@ let rec pr_constr c = match kind c with let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) let print_constr_env env sigma t = !term_printer env sigma t -let print_constr t = !term_printer (Global.env()) Evd.empty t +let print_constr t = + let env = Global.env () in + let evd = Evd.from_env env in + !term_printer env evd t let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -340,7 +343,7 @@ let pr_evar_constraints sigma pbs = str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ protect (print_constr_env env Evd.empty) t2 + spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2 in prlist_with_sep fnl pr_evconstr pbs @@ -434,27 +437,29 @@ let pr_metaset metas = let pr_var_decl env decl = let open NamedDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -931,7 +936,7 @@ let dependent_main noevar sigma m t = match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); - CArray.Fun1.iter deprec m + Array.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) | _, Cast (c,_,_) when noevar && isMeta sigma c -> () @@ -1374,7 +1379,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false + try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false let map_rel_decl f = function | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t) |