X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FvariousTactics.ml;h=615cf43b4930c954b4fc3f187138610d7c9c8091;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=d2f168ce9ac36478bc51de9c1a51d0e208a83ea8;hpb=373eaf73bebec626e031a4a534ddfdd4f1c1b474;p=helm.git diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index d2f168ce9..615cf43b4 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -24,132 +24,91 @@ *) -let constructor_tac ~n ~status:(proof, goal) = - let module C = Cic in - let module R = CicReduction in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.MutInd (uri,typeno,exp_named_subst)) - | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::_)) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) - | _ -> raise (ProofEngineTypes.Fail "Constructor failed") -;; - - -let exists_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let split_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let left_tac ~status = - constructor_tac ~n:1 ~status -;; - - -let right_tac ~status = - constructor_tac ~n:2 ~status -;; - - -let reflexivity_tac = - constructor_tac ~n:1 -;; - - -let symmetry_tac ~status:(proof, goal) = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/sym_eq.con", [])) - - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con", [])) - - | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") -;; - - -let transitivity_tac ~term ~status:((proof, goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let module Tl = Tacticals in - let (_,metasenv,_,_) = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> - Tl.thens - ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", []))) - ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] - ~status - - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - Tl.thens - ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", []))) - ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] - ~status - - | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") -;; - - (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *) - let assumption_tac ~status:((proof,goal) as status) = let module C = Cic in let module R = CicReduction in - let module T = CicTypeChecker in + let module S = CicSubstitution in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let rec find n = function hd::tl -> -(* (let hdd = hd in - match hdd with - Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine) - | None -> prerr_endline("#### None") - ); -*) (match hd with - (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n - | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n + (match hd with + (Some (_, C.Decl t)) when + (R.are_convertible context (S.lift n t) ty) -> n + | (Some (_, C.Def t)) when + (R.are_convertible context + (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n | _ -> find (n+1) tl ) - | [] -> raise (ProofEngineTypes.Fail "No such assumption") + | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption") in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context)) ;; -(* +(* Questa invece era in fourierR.ml +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref 0 in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; +*) + + +(* ANCORA DA DEBUGGARE *) + let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in - let module R = CicReduction in - let module T = CicTypeChecker in let module P = PrimitiveTactics in - let module Tl = Tacticals in + let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in - Tl.thens - ~start:(P.cut_tac ~term:(C.Lambda ("dummy_for_gen", (T.type_of_aux' metasenv context term), (R.replace ?????? (C.Name "dummy_for_gen") term ))) - ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac] (* in quest'ordine o viceversa? provare *) + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + T.thens + ~start:(P.cut_tac + ~term:( + C.Prod( + (C.Name "dummy_for_gen"), + (CicTypeChecker.type_of_aux' metasenv context term), + (ProofEngineReduction.replace_lifting_csc 1 + ~equality:(==) + ~what:term + ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) + ~where:ty) + ))) + ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] ~status ;; -let absurd_tac ~term ~status:((proof,goal) as status) = - PrimitiveTactics.cut_tac +(* IN FASE DI IMPLEMENTAZIONE *) + +let decide_equality_tac = + Tacticals.id_tac +;; + +(* +let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2)) + (* controllo che i due termini siano comparabili *) + then + T.thens + ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *) + ~continuations:[split_tac ; P.intros_tac ~name:"FOO"] + else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types") ;; *)