From: Claudio Sacerdoti Coen Date: Mon, 4 Jul 2005 12:30:36 +0000 (+0000) Subject: All the tactics have been ported to use the objects in LibraryObjects. X-Git-Tag: PRE_GETTER_STORAGE~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8ac0d11d5cd4083838a3848fce68683a518b54a;p=helm.git All the tactics have been ported to use the objects in LibraryObjects. --- diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml index d9fb88f6b..f7613fe19 100644 --- a/helm/ocaml/cic/libraryObjects.ml +++ b/helm/ocaml/cic/libraryObjects.ml @@ -57,3 +57,7 @@ let trans_eq_URI = something_URI HelmLibraryObjects.Logic.trans_eq_URI MatitaLibraryObjects.Equality.trans_eq_URI + +let true_URI = MatitaLibraryObjects.Logic.true_URI +let false_URI = MatitaLibraryObjects.Logic.false_URI +let absurd_URI = MatitaLibraryObjects.Logic.absurd_URI diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli index 6a7bb1833..859b4e732 100644 --- a/helm/ocaml/cic/libraryObjects.mli +++ b/helm/ocaml/cic/libraryObjects.mli @@ -34,3 +34,8 @@ val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri + + +val false_URI : UriManager.uri +val true_URI : UriManager.uri +val absurd_URI : UriManager.uri diff --git a/helm/ocaml/cic/matitaLibraryObjects.ml b/helm/ocaml/cic/matitaLibraryObjects.ml index 33129ce4c..0a4b4f11e 100644 --- a/helm/ocaml/cic/matitaLibraryObjects.ml +++ b/helm/ocaml/cic/matitaLibraryObjects.ml @@ -33,3 +33,10 @@ module Equality = let sym_eq_URI = uri "cic:/matita/equality/sym_eq.con" let trans_eq_URI = uri "cic:/matita/equality/trans_eq.con" end + +module Logic = + struct + let true_URI = uri "cic:/matita/logic/True.ind" + let false_URI = uri "cic:/matita/logic/False.ind" + let absurd_URI = uri "cic:/matita/logic/absurd.ind" + end diff --git a/helm/ocaml/cic/matitaLibraryObjects.mli b/helm/ocaml/cic/matitaLibraryObjects.mli index fd254622d..57311fde7 100644 --- a/helm/ocaml/cic/matitaLibraryObjects.mli +++ b/helm/ocaml/cic/matitaLibraryObjects.mli @@ -31,3 +31,10 @@ module Equality : val sym_eq_URI : UriManager.uri val trans_eq_URI : UriManager.uri end + +module Logic : + sig + val true_URI : UriManager.uri + val false_URI : UriManager.uri + val absurd_URI : UriManager.uri + end diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index cf0db10e6..21fc2b33c 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -39,7 +39,7 @@ let rec injection_tac ~term = ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -95,7 +95,7 @@ and injection1_tac ~term ~i = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -217,7 +217,7 @@ let discriminate'_tac ~term = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -276,8 +276,8 @@ let discriminate'_tac ~term = C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[])) - else (C.MutInd(HelmLibraryObjects.Logic.true_URI,0,[])) + then (C.MutInd(LibraryObjects.false_URI,0,[])) + else (C.MutInd(LibraryObjects.true_URI,0,[])) in aux red_ty 1 ) constructor_list @@ -287,7 +287,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[]))) + ~term:(C.MutInd(LibraryObjects.false_URI,0,[]))) status in (match goals' with diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index c8c9785da..b86cf43d6 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -37,7 +37,7 @@ let absurd_tac ~term = then ProofEngineTypes.apply_tactic (P.apply_tac ~term:( - C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; + C.Appl [(C.Const (LibraryObjects.absurd_URI , [] )) ; term ; ty]) ) status @@ -61,7 +61,7 @@ let contradiction_tac = ~start: (EliminationTactics.elim_type_tac ~term: - (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []))) + (C.MutInd (LibraryObjects.false_URI, 0, []))) ~continuation: VariousTactics.assumption_tac)) status with