diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-15 14:40:26 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-15 14:40:26 +0000 |
commit | 87953e62b73ed431521b0167fb3f2ee8768cae8b (patch) | |
tree | 628483c2ae51e2fc3278ca9a36d11cdbc21c0c83 /kernel/environ.ml | |
parent | 5bf9e67bbee3cee047ad8bfb7fd3c3ffae5f1245 (diff) |
Revert "Fast lookup_named in environments, based on maps instead of lists."
Contrarily to my machine results, it seems that it tore down the performance of
Coq on benchmarks.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17091 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r-- | kernel/environ.ml | 79 |
1 files changed, 35 insertions, 44 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 8c94451d0..9f1868004 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -48,7 +48,7 @@ let empty_env = empty_env let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context -let named_context_val env = env.env_named_context,env.env_named_context_map,env.env_named_vals +let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context let empty_context env = @@ -90,17 +90,16 @@ let fold_rel_context f env ~init = (* Named context *) -let named_context_of_val (ctxt, _, _) = ctxt -let named_vals_of_val (_, _, vals) = vals +let named_context_of_val = fst +let named_vals_of_val = snd (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f (ctxt,map,ctxtv) = - let map_decl (id,body,typ) = (id, Option.map f body, f typ) in - let ctxt = List.map map_decl ctxt in - let map = Id.Map.map map_decl map in - (ctxt,map,ctxtv) +let map_named_val f (ctxt,ctxtv) = + let ctxt = + List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in + (ctxt,ctxtv) let empty_named_context = empty_named_context @@ -112,8 +111,8 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Id.Map.find id env.env_named_context_map -let lookup_named_val id (_,map,_) = Id.Map.find id map +let lookup_named id env = Context.lookup_named id env.env_named_context +let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt let eq_named_context_val c1 c2 = c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) @@ -131,10 +130,9 @@ let evaluable_named id env = | Some _ -> true | _ -> false -let reset_with_named_context (ctxt,map,ctxtv) env = +let reset_with_named_context (ctxt,ctxtv) env = { env with env_named_context = ctxt; - env_named_context_map = map; env_named_vals = ctxtv; env_rel_context = empty_rel_context; env_rel_val = []; @@ -146,11 +144,9 @@ let fold_named_context f env ~init = let rec fold_right env = match env.env_named_context with | [] -> init - | (id, _, _ as d)::ctxt -> - let vals = List.tl env.env_named_vals in - let map = Id.Map.remove id env.env_named_context_map in + | d::ctxt -> let env = - reset_with_named_context (ctxt,map,vals) env in + reset_with_named_context (ctxt,List.tl env.env_named_vals) env in f env d (fold_right env) in fold_right env @@ -323,63 +319,58 @@ let compile_constant_body = Cbytegen.compile_constant_body exception Hyp_not_found -let apply_to_hyp (ctxt,map,vals) id f = - let rec aux rtail ctxt map vals = +let apply_to_hyp (ctxt,vals) id f = + let rec aux rtail ctxt vals = match ctxt, vals with | (idc,c,ct as d)::ctxt, v::vals -> - let map = Id.Map.remove idc map in if Id.equal idc id then - let (nid, _, _ as d) = f ctxt d rtail in - d::ctxt, Id.Map.add nid d map, v::vals + (f ctxt d rtail)::ctxt, v::vals else - let ctxt',map',vals' = aux (d::rtail) ctxt map vals in - d::ctxt', Id.Map.add idc d map', v::vals' + let ctxt',vals' = aux (d::rtail) ctxt vals in + d::ctxt', v::vals' | [],[] -> raise Hyp_not_found | _, _ -> assert false - in aux [] ctxt map vals + in aux [] ctxt vals -let apply_to_hyp_and_dependent_on (ctxt,map,vals) id f g = - let rec aux ctxt map vals = +let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = + let rec aux ctxt vals = match ctxt,vals with | (idc,c,ct as d)::ctxt, v::vals -> - let map = Id.Map.remove idc map in if Id.equal idc id then - let sign = ctxt,map,vals in + let sign = ctxt,vals in push_named_context_val (f d sign) sign else - let (ctxt,map,vals as sign) = aux ctxt map vals in + let (ctxt,vals as sign) = aux ctxt vals in push_named_context_val (g d sign) sign | [],[] -> raise Hyp_not_found | _,_ -> assert false - in aux ctxt map vals + in aux ctxt vals -let insert_after_hyp (ctxt,map,vals) id d check = - let rec aux ctxt map vals = +let insert_after_hyp (ctxt,vals) id d check = + let rec aux ctxt vals = match ctxt, vals with - | (idc, c, ct) :: _, v :: _ -> + | (idc,c,ct)::ctxt', v::vals' -> if Id.equal idc id then begin check ctxt; - push_named_context_val d (ctxt,map,vals) + push_named_context_val d (ctxt,vals) end else - let ctxt,map,vals = aux ctxt map vals in - let (id, _, _) = d in - d::ctxt, Id.Map.add id d map, v::vals + let ctxt,vals = aux ctxt vals in + d::ctxt, v::vals | [],[] -> raise Hyp_not_found | _, _ -> assert false - in aux ctxt map vals + in aux ctxt vals (* To be used in Logic.clear_hyps *) -let remove_hyps ids check_context check_value (ctxt, map, vals) = - List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,map,vals) -> +let remove_hyps ids check_context check_value (ctxt, vals) = + List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) -> if Id.Set.mem id ids then - (ctxt,map,vals) + (ctxt,vals) else let nd = check_context d in - let (nid, _, _) = nd in let nv = check_value v in - (nd::ctxt,Id.Map.add nid nd map,(id',nv)::vals)) - ctxt vals ([],Id.Map.empty,[]) + (nd::ctxt,(id',nv)::vals)) + ctxt vals ([],[]) |