From: Claudio Sacerdoti Coen Date: Fri, 18 Jun 2004 11:26:45 +0000 (+0000) Subject: - In the case (?i args) vs term the term is now eta-expanded w.r.t. args. X-Git-Tag: pre_subst_in_kernel~23 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb0f22004d533abca8d157ed89665dbf1041e0e2;p=helm.git - In the case (?i args) vs term the term is now eta-expanded w.r.t. args. This allows to easily implement elim using apply and it makes the auto tactic much more powerful. - CicMetaSubst.apply_subst semantics changed: it now always performs beta-reduction when a meta in head-position in an application is istantiated with a lambda-abstraction. - CicMetaSubst.apply_subst_reducing no longer in use: removed. --- diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 457286589..4f19b765f 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -5,8 +5,8 @@ PREDICATES = INTERFACE_FILES = \ cicMkImplicit.mli \ cicMetaSubst.mli \ - cicUnification.mli \ freshNamesGenerator.mli \ + cicUnification.mli \ cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 9695d714b..512c65d98 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -96,6 +96,7 @@ 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 @@ -105,19 +106,7 @@ let apply_subst = end in apply_subst_gen ~appl_fun -;; - -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [meta_to_reduce]) that, once unwinding is performed, creates *) -(* a new beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* eta-expansions have been performed and the head of the new *) -(* application has been unified with (META [meta_to_reduce]): *) -(* during the unwinding the eta-expansions are undone. *) - -let apply_subst_reducing meta_to_reduce = +*) let appl_fun um_aux he tl = let tl' = List.map um_aux tl in let t' = @@ -126,23 +115,24 @@ let apply_subst_reducing meta_to_reduce = | he' -> Cic.Appl (he'::tl') in begin - match meta_to_reduce, he with - Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr -> + match he with + Cic.Meta (m,_) -> let rec beta_reduce = function - (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 -> + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> let he'' = CicSubstitution.subst he' t in if tl' = [] then he'' else - beta_reduce (n-1,Cic.Appl(he''::tl')) - | (_,t) -> t + beta_reduce (Cic.Appl(he''::tl')) + | t -> t in - beta_reduce (reductions_no,t') - | _,_ -> t' + beta_reduce t' + | _ -> t' end in apply_subst_gen ~appl_fun +;; let rec apply_subst_context subst context = List.fold_right diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index b1e34757e..4f055f1f8 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -36,19 +36,6 @@ type substitution = (int * Cic.term) list (* [subst] must be already unwinded *) val apply_subst : substitution -> Cic.term -> Cic.term -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [mtr]) that, once unwinding is performed, creates a new *) -(* beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* eta-expansions have been performed and the head of the new *) -(* application has been unified with (META [meta_to_reduce]): *) -(* during the unwinding the eta-expansions are undone. *) -(* [subst] must be already unwinded *) -val apply_subst_reducing : - (int * int) option -> substitution -> Cic.term -> Cic.term - val apply_subst_context : substitution -> Cic.context -> Cic.context val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 395799b31..c239f8e1f 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -29,7 +29,7 @@ exception AssertFailure of string;; (* type_of_aux' metasenv context term *) (* refines [term] and returns the refined form of [term], *) -(* its type, the computed substitution and the new metasenv. *) +(* its type the new metasenv. *) val type_of_aux': Cic.metasenv -> Cic.context -> Cic.term -> Cic.term * Cic.term * Cic.metasenv diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 35eb18f45..8a1f4c43e 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -43,6 +43,134 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv metasenv subst) msg))) +let rec eta_expand test_equality_only metasenv subst context t arg = + let module T = CicTypeChecker in + let module S = CicSubstitution in + let module C = Cic in + let rec aux metasenv subst n context t' = + try + let subst,metasenv = + fo_unif_subst test_equality_only subst context metasenv arg t' + in + subst,metasenv,C.Rel (1 + n) + with + Uncertain _ + | UnificationFailure _ -> + match t' with + | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1) + | C.Var (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.Var (uri,exp_named_subst') + | C.Meta (i,l) as t-> + (try + let t' = List.assoc i subst in + aux metasenv subst n context t' + with + Not_found -> subst,metasenv,t) + | C.Sort _ + | C.Implicit _ as t -> subst,metasenv,t + | C.Cast (te,ty) -> + let subst,metasenv,te' = aux metasenv subst n context te in + let subst,metasenv,ty' = aux metasenv subst n context ty in + subst,metasenv,C.Cast (te', ty') + | C.Prod (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + in + subst,metasenv,C.Prod (nn, s', t') + | C.Lambda (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + in + subst,metasenv,C.Lambda (nn, s', t') + | C.LetIn (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t + in + subst,metasenv,C.LetIn (nn, s', t') + | C.Appl l -> + let subst,metasenv,revl' = + List.fold_left + (fun (subst,metasenv,appl) t -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,t'::appl + ) (subst,metasenv,[]) l + in + subst,metasenv,C.Appl (List.rev revl') + | C.Const (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + let subst,metasenv,outt' = aux metasenv subst n context outt in + let subst,metasenv,t' = aux metasenv subst n context t in + let subst,metasenv,revpl' = + List.fold_left + (fun (subst,metasenv,pl) t -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,t'::pl + ) (subst,metasenv,[]) pl + in + subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl') + | C.Fix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) +*) subst,metasenv,CicMetaSubst.lift subst 1 t' + | C.CoFix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) +*) subst,metasenv,CicMetaSubst.lift subst 1 t' + + and aux_exp_named_subst metasenv subst n context ens = + List.fold_right + (fun (uri,t) (subst,metasenv,l) -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) + in + let argty = + T.type_of_aux' metasenv context arg + in + let fresh_name = + FreshNamesGenerator.mk_fresh_name + metasenv context (Cic.Name "Heta") ~typ:argty + in + let subst,metasenv,t' = aux metasenv subst 0 context t in + subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + +and eta_expand_many test_equality_only metasenv subst context t = + List.fold_left + (fun (subst,metasenv,t) arg -> + eta_expand test_equality_only metasenv subst context t arg + ) (subst,metasenv,t) + (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a metavariable i with its body. @@ -52,7 +180,7 @@ let type_of_aux' metasenv subst context term = a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 = +and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in let module R = CicMetaSubst in let module S = CicSubstitution in @@ -203,25 +331,48 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_l test_equality_only subst metasenv = - function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_subst test_equality_only subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> - fo_unif_subst - test_equality_only subst context metasenv h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_subst test_equality_only subst context metasenv h1 h2 - in - fo_unif_l test_equality_only subst' metasenv' (l1,l2) + let subst,metasenv,t1',t2' = + match l1,l2 with + (* In the first two cases when we reach the next begin ... end + section useless work is done since, by construction, the list + of arguments will be equal. + *) + C.Meta (i,l)::args, _ -> + let subst,metasenv,t2' = + eta_expand_many test_equality_only metasenv subst context t2 args + in + subst,metasenv,t1,t2' + | _, C.Meta (i,l)::args -> + let subst,metasenv,t1' = + eta_expand_many test_equality_only metasenv subst context t1 args + in + subst,metasenv,t1',t2 + | _,_ -> subst,metasenv,t1,t2 in - fo_unif_l test_equality_only subst metasenv (lr1, lr2) + begin + match t1',t2' with + C.Appl l1, C.Appl l2 -> + let lr1 = List.rev l1 in + let lr2 = List.rev l2 in + let rec fo_unif_l test_equality_only subst metasenv = + function + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_subst test_equality_only subst context metasenv h1 h2 + | ([h],l) + | (l,[h]) -> + fo_unif_subst + test_equality_only subst context metasenv h (C.Appl (List.rev l)) + | ((h1::l1),(h2::l2)) -> + let subst', metasenv' = + fo_unif_subst test_equality_only subst context metasenv h1 h2 + in + fo_unif_l test_equality_only subst' metasenv' (l1,l2) + in + fo_unif_l test_equality_only subst metasenv (lr1, lr2) + | _ -> assert false + end | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv' = fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in