diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-30 16:22:33 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-30 16:40:17 +0200 |
commit | b5f07be9fdcd41fdaf73503e5214e766bf6a303b (patch) | |
tree | af2013ee5efc9aed41e5961c87f99b337aa4361a /engine | |
parent | bf0e0e7c9c07982c25057653f29dacbe28a7d743 (diff) |
Specially crafted EConstr.kind to be more efficient.
We do one step of loop unrolling, limit the number of allocations and
mark the function as inline.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.ml | 56 |
1 files changed, 49 insertions, 7 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index f50a8b850..68ef37226 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -41,8 +41,8 @@ let safe_evar_value sigma ev = let rec whd_evar sigma c = match Constr.kind c with - | Evar (evk, args) -> - (match safe_evar_value sigma (evk, args) with + | Evar ev -> + (match safe_evar_value sigma ev with Some c -> whd_evar sigma c | None -> c) | Sort (Type u) -> @@ -57,16 +57,58 @@ let rec whd_evar sigma c = | Construct (co, u) when not (Univ.Instance.is_empty u) -> let u' = Evd.normalize_universe_instance sigma u in if u' == u then c else mkConstructU (co, u') - | App (f, args) when isEvar f -> + | App (f, args) -> (** Enforce smart constructor invariant on applications *) - let ev = destEvar f in + begin match Constr.kind f with + | Evar ev -> + begin match safe_evar_value sigma ev with + | None -> c + | Some f -> whd_evar sigma (mkApp (f, args)) + end + | _ -> c + end + | _ -> c + +(** Loop unrolling to ensure efficiency *) +let kind sigma c = + let c = Constr.kind c in + match c with + | Evar ev -> begin match safe_evar_value sigma ev with + | Some c -> Constr.kind (whd_evar sigma c) | None -> c - | Some f -> whd_evar sigma (mkApp (f, args)) end - | _ -> c + | Sort (Type u) -> + let u' = Evd.normalize_universe sigma u in + if u' == u then c else Sort (Sorts.sort_of_univ u') + | Const (c', u) -> + if Univ.Instance.is_empty u then c + else + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else Const (c', u') + | Ind (i, u) -> + if Univ.Instance.is_empty u then c + else + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else Ind (i, u') + | Construct (co, u) -> + if Univ.Instance.is_empty u then c + else + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else Construct (co, u') + | App (f, args) -> + (** Enforce smart constructor invariant on applications *) + begin match Constr.kind f with + | Evar ev -> + begin match safe_evar_value sigma ev with + | None -> c + | Some f -> Constr.kind (whd_evar sigma (mkApp (f, args))) + end + | _ -> c + end + | c -> c +[@@ocaml.inline] -let kind sigma c = Constr.kind (whd_evar sigma c) let kind_upto = kind let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind |