From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Mar 2006 14:44:00 +0000 (+0000)
Subject: #### EXPERIMENTAL COMMIT ####
X-Git-Tag: 0.4.95@7852~1545
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=730824d3dc60ff3d6d7cff3f5d11c3621eb0f552;p=helm.git

#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).
---

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index 18259a004..0bc05674b 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -1072,3 +1072,18 @@ let rec head_beta_reduce =
          head_beta_reduce he'''
   | Cic.Cast (te,_) -> head_beta_reduce te
   | t -> t
+
+(*Debugging code
+let are_convertible ?subst ?metasenv context t1 t2 ugraph =
+ let before = Unix.gettimeofday () in
+ let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
+ let after = Unix.gettimeofday () in
+ let diff = after -. before in
+  if diff > 0.1 then
+   begin
+    let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
+     prerr_endline
+      ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
+   end;
+  res
+*)
diff --git a/components/cic_proof_checking/cicSubstitution.ml b/components/cic_proof_checking/cicSubstitution.ml
index a30a036cb..a4340583e 100644
--- a/components/cic_proof_checking/cicSubstitution.ml
+++ b/components/cic_proof_checking/cicSubstitution.ml
@@ -108,7 +108,12 @@ let lift n t =
    lift_from 1 n t
 ;;
 
-let subst arg =
+(* subst t1 t2                                                         *)
+(* substitutes [t1] for [Rel 1] in [t2]                                *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes  *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true.                          *)
+let rec subst ?(avoid_beta_redexes=false) arg =
  let rec substaux k =
   let module C = Cic in
    function
@@ -144,6 +149,12 @@ let subst arg =
         begin
          match substaux k he with
             C.Appl l -> C.Appl (l@tl')
+            (* Experimental *)
+          | C.Lambda (_,_,bo) when avoid_beta_redexes ->
+             (match tl' with
+                 [] -> assert false
+               | [he] -> subst ~avoid_beta_redexes he bo
+               | he::tl -> C.Appl (subst he bo::tl))
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false
diff --git a/components/cic_proof_checking/cicSubstitution.mli b/components/cic_proof_checking/cicSubstitution.mli
index 21a1f5d0e..36291fb18 100644
--- a/components/cic_proof_checking/cicSubstitution.mli
+++ b/components/cic_proof_checking/cicSubstitution.mli
@@ -40,9 +40,12 @@ val lift : int -> Cic.term -> Cic.term
 (* as lift but lifts only indexes >= from *)
 val lift_from: int -> int -> Cic.term -> Cic.term
 
-(* subst t1 t2                          *)
-(* substitutes [t1] for [Rel 1] in [t2] *)
-val subst : Cic.term -> Cic.term -> Cic.term
+(* subst t1 t2                                                         *)
+(* substitutes [t1] for [Rel 1] in [t2]                                *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes  *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true.                          *)
+val subst : ?avoid_beta_redexes:bool -> Cic.term -> Cic.term -> Cic.term
 
 (* subst_vars exp_named_subst t2     *)
 (* applies [exp_named_subst] to [t2] *)
diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index c67dc5343..531705a3c 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -1569,7 +1569,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 type_of_aux ~logger 
 	   ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 
        in
-       (CicSubstitution.subst s ty1),ugraph2
+       (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
    | C.Appl (he::tl) when List.length tl > 0 ->
        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
        let tlbody_and_type,ugraph2 = 
@@ -1963,7 +1963,8 @@ end;
 		    begin
 		      CicReduction.fdebug := -1 ;
 		      eat_prods ~subst context 
-			(CicSubstitution.subst hete t) tl ugraph1
+			(CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+                         tl ugraph1
 			(*TASSI: not sure *)
 		    end
 		  else
diff --git a/components/cic_proof_checking/freshNamesGenerator.ml b/components/cic_proof_checking/freshNamesGenerator.ml
index 99c9e4d76..5f3bfdbbd 100755
--- a/components/cic_proof_checking/freshNamesGenerator.ml
+++ b/components/cic_proof_checking/freshNamesGenerator.ml
@@ -61,7 +61,7 @@ let rec guess_a_name context ty =
   | Cic.Cast (t1,t2) -> guess_a_name context t1
   | Cic.Prod (na_,_,t) -> higher_name 1 t
   | Cic.Lambda _ -> assert false                   
-  | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
+  | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
   | Cic.Appl [] -> assert false
   | Cic.Appl (he::_) -> guess_a_name context he 
   | Cic.Const (uri,_)