From 4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Mar 2006 14:44:00 +0000 Subject: [PATCH] #### 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). --- .../components/cic_proof_checking/cicReduction.ml | 15 +++++++++++++++ .../cic_proof_checking/cicSubstitution.ml | 13 ++++++++++++- .../cic_proof_checking/cicSubstitution.mli | 9 ++++++--- .../cic_proof_checking/cicTypeChecker.ml | 5 +++-- .../cic_proof_checking/freshNamesGenerator.ml | 2 +- 5 files changed, 37 insertions(+), 7 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 18259a004..0bc05674b 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/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/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml index a30a036cb..a4340583e 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.ml +++ b/helm/software/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/helm/software/components/cic_proof_checking/cicSubstitution.mli b/helm/software/components/cic_proof_checking/cicSubstitution.mli index 21a1f5d0e..36291fb18 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.mli +++ b/helm/software/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/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index c67dc5343..531705a3c 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/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/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 99c9e4d76..5f3bfdbbd 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/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,_) -- 2.39.2