From 21478bf4534374bb3c2c131acb096c7d3ffc2058 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Oct 2009 18:18:00 +0000
Subject: [PATCH] Performance improvement by preserving more sharing. Visible
in Oliboni's development. But still slower then old matita (but pheraps on
different data...)
---
.../components/ng_kernel/nCicReduction.ml | 64 ++++++++-----------
1 file changed, 25 insertions(+), 39 deletions(-)
diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index e1e5bc7cb..2417f718b 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -141,46 +141,32 @@ module Reduction(RS : Strategy) = struct
(Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config ->
config, true
| (_, _, (C.Const (Ref.Ref
- (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config ->
- (match
- try
- let recarg = RS.from_stack ~delta:max_int (List.nth s recindex) in
- let fixes,(_,_,pragma),_ =
+ (_,Ref.Fix (fixno,recindex,height)) as refer)),s) as config ->
+ (let arg = try Some (List.nth s recindex) with Failure _ -> None in
+ match arg with
+ None -> config, true
+ | Some arg ->
+ let fixes,(_,_,pragma),_ =
NCicEnvironment.get_checked_fixes_or_cofixes refer in
- Some (recarg, fixes, pragma)
- with Failure _ -> None
- with
- | None -> config, true
- | Some((_,_,C.Const(Ref.Ref(_,Ref.Con _)),_::_ as c),fs,`Projection) ->
- let new_s =
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- let _,_,_,_,body = List.nth fs fixno in
- aux (0, [], body, new_s)
- | Some (recparam, fixes, pragma) ->
- match reduce ~delta:0 ~subst context recparam with
- | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _
- when delta >= height ->
- let new_s =
- (* FIXME, we should push on the stack
- * c for CBV and recparam for CBN *)
- if pragma = `Projection then
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind recparam)
- else
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- (0, [], head, new_s), false
- | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ ->
- let new_s =
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- let _,_,_,_,body = List.nth fixes fixno in
- aux (0, [], body, new_s)
- | _ -> config, true)
+ if delta >= height then
+ match pragma with
+ | `Projection ->
+ (match RS.from_stack ~delta:max_int arg with
+ | _,_,C.Const(Ref.Ref(_,Ref.Con _)),_::_ ->
+ let _,_,_,_,body = List.nth fixes fixno in
+ aux (0, [], body, s)
+ | _ -> config,false)
+ | _ -> config,false
+ else
+ match RS.from_stack ~delta:0 arg with
+ | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
+ let new_s =
+ replace recindex s
+ (RS.compute_to_stack ~reduce:(reduce ~subst context)
+ ~unwind c) in
+ let _,_,_,_,body = List.nth fixes fixno in
+ aux (0, [], body, new_s)
+ | _ -> config, true)
| (k, e, C.Match (_,_,term,pl),s) as config ->
let decofix = function
| (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)->
--
2.39.2