From 5d1cece5f42866b34566a0f616aa3b46a77359a3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jun 2007 12:20:18 +0000 Subject: [PATCH] new more flexible compose, see matita/tests/compose.ma for a sample --- .../software/components/grafite/grafiteAst.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 6 +- .../grafite_engine/grafiteEngine.ml | 4 +- .../grafite_parser/grafiteDisambiguate.ml | 12 +- .../grafite_parser/grafiteParser.ml | 7 +- .../components/tactics/closeCoercionGraph.ml | 14 +- helm/software/components/tactics/compose.ml | 130 ++++++++++++++++-- helm/software/components/tactics/compose.mli | 3 +- helm/software/components/tactics/tactics.mli | 4 +- helm/software/matita/Makefile | 39 +++--- helm/software/matita/tests/compose.ma | 53 +++++++ 11 files changed, 226 insertions(+), 48 deletions(-) create mode 100644 helm/software/matita/tests/compose.ma diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 9a453ae42..0b54b68a4 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -65,7 +65,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident list | ClearBody of loc * 'ident - | Compose of loc * 'term * 'term * 'ident intros_spec + | Compose of loc * 'term * 'term option * int * 'ident intros_spec | Constructor of loc * int | Contradiction of loc | Cut of loc * 'ident option * 'term diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 51b002de9..f689ff101 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -107,8 +107,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids) | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id]) | Constructor (_,n) -> "constructor " ^ string_of_int n - | Compose (_,t1, t2, intro_specs) -> - Printf.sprintf "compose %s %s%s" (term_pp t1) (term_pp t1) + | Compose (_,t1, t2, times, intro_specs) -> + Printf.sprintf "compose %s%s %s%s" + (if times > 0 then string_of_int times ^ " " else "") + (term_pp t1) (match t2 with None -> "" | Some t2 -> "with "^term_pp t2) (pp_intros_specs " as " intro_specs) | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6b34c687c..ad4ae40c6 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -96,8 +96,8 @@ let rec tactic_of_ast status ast = Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id - | GrafiteAst.Compose (_,t1,t2,(howmany, names)) -> - Tactics.compose t1 t2 ?howmany + | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> + Tactics.compose times t1 t2 ?howmany ~mk_fresh_name_callback:(namer_of names) | GrafiteAst.Contradiction _ -> Tactics.contradiction | GrafiteAst.Constructor (_, n) -> Tactics.constructor n diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 31b881988..ececcf967 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -195,10 +195,16 @@ let rec disambiguate_tactic metasenv,GrafiteAst.Clear (loc,id) | GrafiteAst.ClearBody (loc,id) -> metasenv,GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compose (loc, t1, t2, spec) -> + | GrafiteAst.Compose (loc, t1, t2, times, spec) -> let metasenv,t1 = disambiguate_term context metasenv t1 in - let metasenv,t2 = disambiguate_term context metasenv t2 in - metasenv, GrafiteAst.Compose (loc, t1, t2, spec) + let metasenv,t2 = + match t2 with + | None -> metasenv, None + | Some t2 -> + let m, t2 = disambiguate_term context metasenv t2 in + m, Some t2 + in + metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec) | GrafiteAst.Constructor (loc,n) -> metasenv,GrafiteAst.Constructor (loc,n) | GrafiteAst.Contradiction loc -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 10a841e2e..45a71f174 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -156,9 +156,10 @@ EXTEND GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Change (loc, what, t) - | IDENT "compose"; t1 = tactic_term; t2 = tactic_term; - specs = intros_spec -> - GrafiteAst.Compose (loc, t1, t2, specs) + | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = + OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec -> + let times = match times with None -> 1 | Some i -> i in + GrafiteAst.Compose (loc, t1, t2, times, specs) | IDENT "constructor"; n = int -> GrafiteAst.Constructor (loc, n) | IDENT "contradiction" -> diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 4f1d1b182..3e6411098 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -78,6 +78,7 @@ exception UnableToCompose * both living in the same context and metasenv *) let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = let module RT = RefinementTool in + let original_metasenv = metasenv in let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in let rec mk_implicits = function @@ -177,8 +178,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = List.sort (fun (i,ctx1,ty1) (j,ctx1,ty1) -> try List.assoc i meta2no - List.assoc j meta2no - with Not_found -> - assert false) + with Not_found -> assert false) body_metasenv in let namer l n = @@ -221,6 +221,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = let subst = create_subst_from_metas_to_rels spline_len body_metasenv in debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst)); let term = CicMetaSubst.apply_subst subst term in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term)); let term, ty, metasenv, ugraph = CicRefine.type_of_aux' metasenv context term ugraph @@ -229,6 +230,15 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = split_metasenv metasenv (spline_len + List.length context) in let term = purge_unused_lambdas lambdas_metasenv term in + let metasenv = + List.filter + (fun (i,_,_) -> + List.for_all + (fun (j,_,_) -> + i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv) + lambdas_metasenv) + metasenv + in debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term)); debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); term, metasenv, ugraph diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml index f090c3dbf..137e919b0 100644 --- a/helm/software/components/tactics/compose.ml +++ b/helm/software/components/tactics/compose.ml @@ -23,30 +23,78 @@ * http://helm.cs.unibo.it/ *) -let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) = +let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;; + +let compose_core t2 t1 (proof, goal) = let _,metasenv,_subst,_,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let ty1,_ = CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph in - let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 in - let rec generate arity menv acc = - if arity < 0 then acc, menv - else + let ty2,_ = + CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph + in + let saturated_ty2, menv_for_saturated_ty2 = + let maxm = CicMkImplicit.new_meta metasenv [] in + let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in + ty2, menv + in + (* unifies t with saturated_ty2 and gives back a fresh meta of type t *) + let unif menv t = + let m, menv2 = + let n = CicMkImplicit.new_meta menv [] in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + Cic.Meta (n,irl), ((n,context,t)::menv) + in + try + let _ = + CicUnification.fo_unif menv context t saturated_ty2 + CicUniv.oblivion_ugraph + in + true, menv2, m + with + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> false, menv2, m + in + (* check which "positions" in the input arrow unifies with saturated_ty2 *) + let rec positions menv cur arity = function + | Cic.Prod (n,s,t) -> + let b, newmenv, sb = unif menv s in + if b then + (arity - cur - 1) :: + (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)) + else + positions newmenv (cur + 1) arity (CicSubstitution.subst sb t) + | _ -> [] + in + (* position is a list of arities, that is if t1 : a -> b -> c and arity is + * 0 then the computed term will be (t1 ? t2) of type a -> c + * if arity is 1 then (t1 t2 ?) of type b -> c *) + let rec generate positions menv acc = + match positions with + | [] -> acc, menv + | arity::tl -> try - let t, menv, _ = - CloseCoercionGraph.generate_composite t1 t2 context menv + let t, menv1, _ = + CloseCoercionGraph.generate_composite t2 t1 context menv CicUniv.oblivion_ugraph arity false in - generate (arity - 1) menv (t::acc) + assert (List.length menv1 = List.length menv); + generate tl menv (t::acc) with - | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc + | CloseCoercionGraph.UnableToCompose -> generate tl menv acc + in + let terms, metasenv = + generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv [] in - let terms, metasenv = generate (count_pi ty1) metasenv [] in + (* the new proof has the resulting metasenv (shouldn't it be the same?) *) let proof = let uri, _, _subst, bo, ty, attrs = proof in uri, metasenv, _subst, bo, ty, attrs in + (* now we have the terms, we generalize them and intros them *) let proof, goal = List.fold_left (fun (proof,goal) t -> @@ -62,12 +110,64 @@ let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) = proof,List.hd gl) (proof,goal) terms in - ProofEngineTypes.apply_tactic - (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ()) - (proof,goal) + (proof, goal), List.length terms +;; + +let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus = + let ((proof, goal), k), n = + match t2 with + | Some t2 -> compose_core t1 t2 proofstatus, n-1 + | None -> + let k = + let proof, goal = proofstatus in + let _,metasenv,subst,_,_,_ = proof in + let _,_,ty = CicUtil.lookup_meta goal metasenv in + count_pi (CicMetaSubst.apply_subst subst ty) + in + (proofstatus, k), n + in + let (proof, goal), k = + (* fix iterates n times the composition *) + let rec fix proofstatus k t = function + | 0 -> proofstatus, k + | n -> + let t = CicSubstitution.lift k t in + let proof, gl = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.intros_tac + ~howmany:k ?mk_fresh_name_callback ()) proofstatus + in + assert (List.length gl = 1); + let goal = List.hd gl in + let k, proofstatus = + (* aux compose t with every previous result *) + let rec aux k proofstatus = function + | 0 -> k, proofstatus + | n -> + let (proof, goal), k1 = + compose_core t (Cic.Rel n) proofstatus + in + aux (k+k1) (proof, goal) (n-1) + in + aux 0 (proof, goal) k + in + fix proofstatus k t (n-1) + in + fix (proof, goal) k t1 n + in + let howmany = + match howmany with + | None -> None + | Some i -> + if i - k < 0 then (* we should generalize back and clear *) Some 0 + else Some (i - k) + in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ()) + (proof,goal) ;; -let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 = +let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 = ProofEngineTypes.mk_tactic - (compose_tac ?howmany ?mk_fresh_name_callback t1 t2) + (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2) ;; diff --git a/helm/software/components/tactics/compose.mli b/helm/software/components/tactics/compose.mli index 37e69d42f..44db74b76 100644 --- a/helm/software/components/tactics/compose.mli +++ b/helm/software/components/tactics/compose.mli @@ -26,4 +26,5 @@ val compose_tac: ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> Cic.term -> ProofEngineTypes.tactic + int (* times *) -> + Cic.term -> Cic.term option -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index d63e8805c..16c668266 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun 1 17:03:59 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun 4 13:44:18 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -105,4 +105,4 @@ val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val compose : ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> Cic.term -> ProofEngineTypes.tactic + int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 81e67db64..1e940c3b8 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -86,11 +86,6 @@ CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) $(CMOS) : $(LIB_DEPS) $(CMXOS): $(LIBX_DEPS) -ifeq ($(MAKECMDGOALS),opt) - $(MLI:%.mli=%.cmi): $(LIBX_DEPS) -else - $(MLI:%.mli=%.cmi): $(LIB_DEPS) -endif LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) @@ -404,21 +399,31 @@ depend.opt: $(H)echo " OCAMLDEP -native" $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt -ifeq ($(MAKECMDGOALS),) - include .depend -endif - -ifeq ($(MAKECMDGOALS), all) - include .depend +# this should be sligtly better, since should work with 'make all opt' +ifneq (,$(findstring all,$(MAKECMDGOALS))) + # if we 'make all opt' the deps for 'all' should be fine also for opt + # if we 'make opt all' it should not work... + TO_INCLUDE+=.depend + TO_DEPEND_ON=$(LIB_DEPS) +else ifneq (,$(findstring opt,$(MAKECMDGOALS))) + TO_INCLUDE+=.depend.opt + TO_DEPEND_ON=$(LIBX_DEPS) +else ifneq (,$(findstring world,$(MAKECMDGOALS))) + ifeq ($(HAVE_OCAMLOPT),yes) + TO_INCLUDE+=.depend.opt + TO_DEPEND_ON=$(LIBX_DEPS) + else + TO_INCLUDE+=.depend + TO_DEPEND_ON=$(LIB_DEPS) + endif +else + TO_INCLUDE+=.depend + TO_DEPEND_ON=$(LIB_DEPS) endif -ifeq ($(MAKECMDGOALS), opt) - include .depend.opt -endif +$(MLI:%.mli=%.cmi): $(TO_DEPEND_ON) -ifeq ($(MAKECMDGOALS), world) - include .depend.opt -endif +include $(TO_INCLUDE) %.cmi: %.mli $(H)echo " OCAMLC $<" diff --git a/helm/software/matita/tests/compose.ma b/helm/software/matita/tests/compose.ma new file mode 100644 index 000000000..5d6035777 --- /dev/null +++ b/helm/software/matita/tests/compose.ma @@ -0,0 +1,53 @@ +set "baseuri" "cic:/matita/tests/compose/LCL002-1". +include "logic/equality.ma". + +theorem an_1: +∀ Univ:Set. +∀ a:Univ. +∀ is_a_theorem:Univ → Prop. +∀ not:Univ → Univ. +∀ or:Univ → Univ → Univ. +∀ H0:∀ U:Univ.∀ V:Univ.∀ X:Univ.∀ Y:Univ.∀ Z:Univ. + is_a_theorem + (or (not (or (not (or (not X) Y)) (or Z (or U V)))) + (or (not (or (not U) X)) (or Z (or V X)))). +∀ H1:∀ X:Univ.∀ Y:Univ. + is_a_theorem (or (not X) Y) → is_a_theorem X → is_a_theorem Y. +∀ ABS:∀ X.is_a_theorem X. +True. +. +intros 5. +intros (H H1 ABS). + +(* H1 o H *) +compose (H) with (H1) (primo secondo). +letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H ? ? ? ? ?)); +try assumption; [1,2: apply ABS] +letin verifica_secondo ≝ (secondo ? ? ? ? ? ? ? = H1 ? ? (H ? ? ? ? ?) ?); +try assumption; [1,2: apply ABS] +clear verifica_primo verifica_secondo. +compose (H) with (primo) (terzo). +compose (H) with (secondo) (quarto). +letin verifica_terzo_quarto ≝ (terzo ? ? ? ? ? = quarto ? ? ? ? ?); +try assumption. +clear verifica_terzo_quarto. +clear primo secondo terzo quarto. + +(* H1 o H1 *) +compose (H1) with (H1) (primo secondo). +letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H1 ? ? ? ?)); +try assumption; [1,2,3,4,5,6: apply ABS] +letin verifica_secondo ≝ (secondo ? ? ? ? ? ? = H1 ? ? (H1 ? ? ? ?) ?); +try assumption; [1,2,3,4,5,6: apply ABS] +clear verifica_primo verifica_secondo. +clear primo secondo. + +(* close H1 o H1 with H *) +compose H1 with H1 0. +(* +leaving the result under the sequent line and calling compose without +the with parameter, will compose H with all the stuff under the sequent line +*) +compose 3 (H) (i1 i2 p1 p2 p3 p4 p5 p6 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12). +exact I. +qed. -- 2.39.2