From ed9af5a10b66343f817a1f9eac3add29e4b2baae Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jun 2005 14:03:41 +0000 Subject: [PATCH] * (Head) beta reduction functions factorized * the type inferred for a match both in the kernel and in the refiner are now beta reduced --- helm/ocaml/cic_proof_checking/cicReduction.ml | 16 ++++++++++ .../ocaml/cic_proof_checking/cicReduction.mli | 2 ++ .../cic_proof_checking/cicTypeChecker.ml | 18 ++++++----- helm/ocaml/cic_unification/cicMetaSubst.ml | 24 +------------- helm/ocaml/cic_unification/cicRefine.ml | 9 ++++-- helm/ocaml/cic_unification/cicUnification.ml | 31 +++---------------- 6 files changed, 39 insertions(+), 61 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 63a8f5503..14b858491 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -1086,3 +1086,19 @@ let normalize ?delta ?subst ctx term = t +(* performs an head beta/cast reduction *) +let rec head_beta_reduce = + function + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce he''' + | Cic.Cast (te,_) -> head_beta_reduce te + | t -> t diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli index cd48a025b..e3619053d 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.mli +++ b/helm/ocaml/cic_proof_checking/cicReduction.mli @@ -38,3 +38,5 @@ val are_convertible : val normalize: ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term +(* performs an head beta/cast reduction *) +val head_beta_reduce: Cic.term -> Cic.term diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index fbcf25f91..6789c4dff 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1766,12 +1766,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if not branches_ok then raise (TypeCheckerFailure "Case analysys: wrong branch type"); - if not need_dummy then - (C.Appl ((outtype::arguments)@[term])),ugraph5 - else if arguments = [] then - outtype,ugraph5 - else - (C.Appl (outtype::arguments)),ugraph5 + let arguments = + if not need_dummy then outtype::arguments@[term] + else outtype::arguments in + let outtype = + if arguments = [] then outtype + else CicReduction.head_beta_reduce (C.Appl arguments) + in + outtype,ugraph5 | C.Fix (i,fl) -> let types_times_kl,ugraph1 = (* WAS: list rev list map *) @@ -2117,9 +2119,9 @@ let typecheck uri ugraph = (** wrappers which instantiate fresh loggers *) -let type_of_aux' ?(subst = []) metasenv context t = +let type_of_aux' ?(subst = []) metasenv context t ugraph = let logger = new CicLogger.logger in - type_of_aux' ~logger ~subst metasenv context t + type_of_aux' ~logger ~subst metasenv context t ugraph let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) = let logger = new CicLogger.logger in diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 768255a14..3b8e4ad22 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -232,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term = ;; let apply_subst = -(* CSC: old code that never performs beta reduction - let appl_fun um_aux he tl = - let tl' = List.map um_aux tl in - begin - match um_aux he with - Cic.Appl l -> Cic.Appl (l@tl') - | he' -> Cic.Appl (he'::tl') - end - in - apply_subst_gen ~appl_fun -*) let appl_fun um_aux he tl = let tl' = List.map um_aux tl in let t' = @@ -252,18 +241,7 @@ let apply_subst = in begin match he with - Cic.Meta (m,_) -> - let rec beta_reduce = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - beta_reduce (Cic.Appl(he''::tl')) - | t -> t - in - beta_reduce t' + Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' | _ -> t' end in diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a9593c67f..76642ee3d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -559,7 +559,9 @@ and type_of_aux' metasenv context t ugraph = candidate outtype ugraph5 in C.MutCase (uri, i, outtype, term', pl'), - (Cic.Appl (outtype::right_args@[term'])), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) let _,_, subst, metasenv,ugraph5 = @@ -584,8 +586,9 @@ and type_of_aux' metasenv context t ugraph = (subst,metasenv,ugraph5) outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), - CicReduction.whd ~subst context - (C.Appl(outtype::right_args@[term])), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (C.Appl(outtype::right_args@[term]))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> let fl_ty',subst,metasenv,types,ugraph1 = diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 5e2eaba00..7a67c8248 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -50,29 +50,6 @@ let type_of_aux' metasenv subst context term ugraph = let exists_a_meta l = List.exists (function Cic.Meta _ -> true | _ -> false) l -let rec beta_reduce = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - beta_reduce (Cic.Appl(he''::tl')) - | t -> t -(* -let rec deref subst = - let snd (_,a,_) = a in - function - Cic.Meta(n,l) as t -> - (try - deref subst - (CicSubstitution.subst_meta - l (snd (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | t -> t -;; *) - let rec deref subst t = let snd (_,a,_) = a in match t with @@ -86,10 +63,10 @@ let rec deref subst t = | Cic.Appl(Cic.Meta(n,l)::args) -> (match deref subst (Cic.Meta(n,l)) with | Cic.Lambda _ as t -> - deref subst (beta_reduce (Cic.Appl(t::args))) + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) | r -> Cic.Appl(r::args)) | Cic.Appl(((Cic.Lambda _) as t)::args) -> - deref subst (beta_reduce (Cic.Appl(t::args))) + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) | t -> t ;; @@ -481,7 +458,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (try let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.subst_meta l t in - let reduced = beta_reduce (Cic.Appl (lifted::args)) in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only subst context metasenv reduced t2 ugraph @@ -496,7 +473,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (* (try let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.subst_meta l t in - let reduced = beta_reduce (Cic.Appl (lifted::args)) in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only subst context metasenv t1 reduced ugraph -- 2.39.2