#### 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 18259a00441873ea85ea755e3a06e891de291872..0bc05674bced1f7ccf563c06532ab5cedb272b3a 100644 (file)
--- 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 a30a036cb42dc7726c1720906d706f903b0fcf30..a4340583efc8b1f98cbacfdb58a7f94efa8249a9 100644 (file)
--- 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 21a1f5d0e579d775c9e1ea2117b56898506f1990..36291fb184b284971cf8e81c36cb1aaf09fc124d 100644 (file)
--- 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 c67dc5343f622b0ce215c28c0ed5fa4dee3e99d8..531705a3c2d40abf7d2699291e683b5da0b2e70f 100644 (file)
--- 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 99c9e4d76c9d93f51e070fce5aca31487c6099af..5f3bfdbbd01a284190f10d6e618ed002981f8de5 100755 (executable)
--- 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,_)