From 06fb3694ba485d761586c1a90f97f15b8915a277 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 16:54:44 +0000 Subject: [PATCH] Generalize now works on a list of convertible terms, generalizing all of them at once. --- helm/gTopLevel/gTopLevel.ml | 2 +- helm/gTopLevel/proofEngine.ml | 2 +- helm/gTopLevel/proofEngine.mli | 2 +- helm/ocaml/tactics/proofEngineReduction.ml | 168 +++++++++++--------- helm/ocaml/tactics/proofEngineReduction.mli | 2 +- helm/ocaml/tactics/variousTactics.ml | 66 +++----- helm/ocaml/tactics/variousTactics.mli | 5 +- 7 files changed, 115 insertions(+), 132 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 293bed93c..27c6ca17b 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -2292,7 +2292,7 @@ let split = call_tactic ProofEngine.split;; let left = call_tactic ProofEngine.left;; let right = call_tactic ProofEngine.right;; let assumption = call_tactic ProofEngine.assumption;; -let generalize = call_tactic_with_goal_input ProofEngine.generalize;; +let generalize = call_tactic_with_goal_inputs ProofEngine.generalize;; let absurd = call_tactic_with_input ProofEngine.absurd;; let contradiction = call_tactic ProofEngine.contradiction;; let decompose = diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 4751cb23f..313790a7f 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -229,7 +229,7 @@ let right () = apply_tactic IntroductionTactics.right_tac let assumption () = apply_tactic VariousTactics.assumption_tac -let generalize term = apply_tactic (VariousTactics.generalize_tac ~term) +let generalize terms = apply_tactic (VariousTactics.generalize_tac ~terms) let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) let contradiction () = apply_tactic NegationTactics.contradiction_tac diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index 8f8b1261d..59ed974ca 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -79,7 +79,7 @@ val right : unit -> unit val assumption : unit -> unit -val generalize : Cic.term -> unit +val generalize : Cic.term list -> unit val absurd : Cic.term -> unit val contradiction : unit -> unit diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index a51ab3909..5cc513deb 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -261,88 +261,98 @@ let replace_lifting ~equality ~what ~with_what ~where = substaux 1 what where ;; -(* replaces in a term a term with another one. *) -(* Lifting are performed as usual. *) +(* replaces in a term a list of terms with other ones. *) +(* Lifting are performed as usual. *) let replace_lifting_csc nnn ~equality ~what ~with_what ~where = - let rec substaux k = - let module C = Cic in - let module S = CicSubstitution in - function - t when (equality t what) -> S.lift (k-1) with_what - | C.Rel n as t -> - if n < k then C.Rel n else C.Rel (n + nnn) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l) as t -> - let l' = - List.map - (function - None -> None - | Some t -> Some (substaux k t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) - | C.Prod (n,s,t) -> - C.Prod (n, substaux k s, substaux (k + 1) t) - | C.Lambda (n,s,t) -> - C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> - C.LetIn (n, substaux k s, substaux (k + 1) t) - | C.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k) tl in - begin - match substaux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k outt, substaux k t, - List.map (substaux k) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> - (name, i, substaux k ty, substaux (k+len) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> - (name, substaux k ty, substaux (k+len) bo)) - fl - in - C.CoFix (i, substitutedfl) + let module C = Cic in + let module S = CicSubstitution in + let find_image t = + let rec find_image_aux = + function + [],[] -> raise Not_found + | what::tl1,with_what::tl2 -> + if equality t what then with_what else find_image_aux (tl1,tl2) + | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength + in + find_image_aux (what,with_what) + in + let rec substaux k t = + try + S.lift (k-1) (find_image t) + with Not_found -> + match t with + C.Rel n as t -> + if n < k then C.Rel n else C.Rel (n + nnn) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> + (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) in -let res = substaux 1 where -in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res ;; (* Takes a well-typed term and fully reduces it. *) diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli index 2c210b677..e3bdfd49e 100644 --- a/helm/ocaml/tactics/proofEngineReduction.mli +++ b/helm/ocaml/tactics/proofEngineReduction.mli @@ -43,6 +43,6 @@ val replace_lifting : what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term val replace_lifting_csc : int -> equality:(Cic.term -> Cic.term -> bool) -> - what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term + what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index f0a3070f7..f24f7904c 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -50,68 +50,40 @@ let assumption_tac ~status:((proof,goal) as status) = (* ANCORA DA DEBUGGARE *) +exception AllSelectedTermsMustBeConvertible;; + (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda e li aggiunga nel context, poi si conta la lunghezza di questo nuovo contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) -let generalize_tac ~term ~status:((proof,goal) as status) = +let generalize_tac ~terms ~status:((proof,goal) as status) = let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in -(* - let found = false in - let rec new_context context ty = - if ty == term then let found = true in context - else match ty with - C.Rel _ - | C.Var _ - | C.Meta _ (* ???? *) - | C.Sort s - | C.Implicit -> context - | C.Cast (val,typ) -> - let tmp_context = new_context context val in - tmp_context @ (new_context tmp_context typ) - | C.Prod (binder, source, target) -> - | C.Lambda (binder, source, target) -> - let tmp_context = new_context context source in - tmp_context @ (new_context tmp_context binder) - | C.LetIn (binder, term, target) -> - | C.Appl applist -> - let rec aux context = - match applist with - [] -> context - | hd::tl -> - let tmp_context = (new_context context hd) - in aux tmp_context tl - in aux context applist - | C.Const (uri, exp_named_subst) - | C.MutInd (uri, typeno, exp_named_subst) - | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> - match exp_named_subst with - [] -> context - | (uri,t)::_ -> new_context context (type_of_aux' context t) - | _ -> assert false - | C.MutCase (uri, typeno, outtype, iterm, patterns) - | C.Fix (funno, funlist) - | C.CoFix (funno, funlist) -> - match funlist with - [] -> context (* caso possibile? *) - | (name, index, type, body)::_ -> - let tmp_context = ~ - in -*) + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let typ = + match terms with + [] -> assert false + | he::tl -> + (* We need to check that all the convertibility of all the terms *) + List.iter + (function t -> + if not (CicReduction.are_convertible context he t) then + raise AllSelectedTermsMustBeConvertible + ) tl ; + (CicTypeChecker.type_of_aux' metasenv context he) + in T.thens ~start: (P.cut_tac (C.Prod( (C.Name "dummy_for_gen"), - (CicTypeChecker.type_of_aux' metasenv context term), + typ, (ProofEngineReduction.replace_lifting_csc 1 ~equality:(==) - ~what:term - ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) + ~what:terms + ~with_what:(List.map (function _ -> C.Rel 1) terms) ~where:ty) ))) ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index 27b59682f..b08b33fac 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -23,9 +23,10 @@ * http://cs.unibo.it/helm/. *) -val assumption_tac: ProofEngineTypes.tactic +exception AllSelectedTermsMustBeConvertible;; -val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic +val assumption_tac: ProofEngineTypes.tactic +val generalize_tac: terms:Cic.term list -> ProofEngineTypes.tactic (* val decide_equality_tac: ProofEngineTypes.tactic -- 2.39.2