diff options
| -rw-r--r-- | lib/util.ml | 33 | ||||
| -rw-r--r-- | lib/util.mli | 15 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 31 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 19 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 14 |
5 files changed, 83 insertions, 29 deletions
diff --git a/lib/util.ml b/lib/util.ml index 172d8d911..57fea3808 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1359,6 +1359,39 @@ let pr_located pr (loc,x) = let surround p = hov 1 (str"(" ++ p ++ str")") +(*s Memoization *) + +let memo1_eq eq f = + let m = ref None in + fun x -> + match !m with + Some(x',y') when eq x x' -> y' + | _ -> let y = f x in m := Some(x,y); y + +let memo1_1 f = memo1_eq (==) f +let memo1_2 f = + let f' = + memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in + (fun x y -> f'(x,y)) + +(* Memorizes the last n distinct calls to f. Since there is no hash, + Efficient only for small n. *) +let memon_eq eq n f = + let cache = ref [] in (* the cache: a stack *) + let m = ref 0 in (* usage of the cache *) + let rec find x = function + | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *) + | [] -> (* we assume n>0, so creating one memo cell is OK *) + incr m; (f x, []) + | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *) + | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l') + in + (fun x -> + let (y,l) = find x !cache in + cache := (x,y)::l; + y) + + (*s Size of ocaml values. *) module Size = struct diff --git a/lib/util.mli b/lib/util.mli index 023b8a15e..1be7f807a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -298,6 +298,21 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val surround : std_ppcmds -> std_ppcmds +(*s Memoization. *) + +(* General comments on memoization: + - cache is created whenever the function is supplied (because of + ML's polymorphic value restriction). + - cache is never flushed (unless the memoized fun is GC'd) + *) +(* One cell memory: memorizes only the last call *) +val memo1_1 : ('a -> 'b) -> ('a -> 'b) +val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c) +(* with custom equality (used to deal with various arities) *) +val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b) + +(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *) +val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b) (*s Size of an ocaml value (in words, bytes and kilobytes). *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aba6e2e19..d7da100ab 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -164,18 +164,25 @@ let rec evar_conv_x env evd pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term evd term1 && is_ground_term evd term2 - && is_ground_env evd env - then (evd, is_fconv pbty env (evars_of evd) term1 term2) - else - let term1 = apprec_nohdbeta env evd term1 in - let term2 = apprec_nohdbeta env evd term2 in - if is_undefined_evar evd term1 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) - else if is_undefined_evar evd term2 then - solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) - else - evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) + let ground_test = + if is_ground_term evd term1 && is_ground_term evd term2 then + if is_fconv pbty env (evars_of evd) term1 term2 then + Some true + else if is_ground_env evd env then Some false + else None + else None in + match ground_test with + Some b -> (evd,b) + | None -> + let term1 = apprec_nohdbeta env evd term1 in + let term2 = apprec_nohdbeta env evd term2 in + if is_undefined_evar evd term1 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + else if is_undefined_evar evd term2 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + else + evar_eqappr_x env evd pbty + (decompose_app term1) (decompose_app term2) and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fee8e29f5..37288d394 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -962,9 +962,19 @@ and evar_define env (evk,_ as ev) rhs evd = (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_undefined_evars evd t = - try let _ = local_strong whd_ise (evars_of evd) t in false - with Uninstantiated_evar _ -> true +let has_undefined_evars evd t = + let evm = evars_of evd in + let rec has_ev t = + match kind_of_term t with + Evar (ev,args) -> + (match evar_body (Evd.find evm ev) with + | Evar_defined c -> + has_ev c; Array.iter has_ev args + | Evar_empty -> + raise NotInstantiatedEvar) + | _ -> iter_constr has_ev t in + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true let is_ground_term evd t = not (has_undefined_evars evd t) @@ -975,6 +985,9 @@ let is_ground_env evd env = | _ -> true in List.for_all is_ground_decl (rel_context env) && List.for_all is_ground_decl (named_context env) +(* Memoization is safe since evar_map and environ are applicative + structures *) +let is_ground_env = memo1_2 is_ground_env let head_evar = let rec hrec c = match kind_of_term c with diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8a40361d3..38ac3485b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -598,20 +598,6 @@ let pb_equal = function let sort_cmp = sort_cmp - -let nf_red_env sigma env = - let nf_decl = function - (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty) - | d -> d in - let sign = named_context env in - let ctxt = rel_context env in - let env = reset_context env in - let env = Sign.fold_named_context - (fun d env -> push_named (nf_decl d) env) ~init:env sign in - Sign.fold_rel_context - (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt - - let test_conversion (f:?evars:'a->'b) env sigma x y = try let _ = f ~evars:(safe_evar_value sigma) env x y in true |