X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=dd2e68d09e8afcaf582ee88f10a7481cc63cfd0d;hb=e4b873cd8511753e65319d02fcdd5473214f42a5;hp=9e91eeb07fad9f5f58a20bd3b94c873660397cff;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 9e91eeb07..dd2e68d09 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,18 +25,18 @@ open HelmLibraryObjects -let rec injection_tac ~term ~status:((proof, goal) as status) = +let rec injection_tac ~term status = + let (proof, goal) = status in 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,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) - or (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -72,10 +72,11 @@ let rec injection_tac ~term ~status:((proof, goal) as status) = | _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ) | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation") - ) ~status + ) status -and injection1_tac ~term ~i ~status:((proof, goal) as status) = +and injection1_tac ~term ~i status = +let (proof, goal) = status in (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *) let module C = Cic in let module S = CicSubstitution in @@ -83,12 +84,11 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) or - (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -149,9 +149,10 @@ prerr_endline ("XXXX cominciamo!") ; ; T.then_ ~start: - (fun ~status:((proof,goal) as status) -> + (fun status -> + let (proof, goal) = status in let _,metasenv,_,_ = proof in - let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,gty = CicUtil.lookup_meta goal metasenv in prerr_endline ("XXXX goal " ^ string_of_int goal) ; prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; @@ -180,7 +181,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ); t1] ) - ~status + status ) ~continuation: (T.then_ @@ -188,7 +189,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ~continuation:EqualityTactics.reflexivity_tac ) ] - ~status + status | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") @@ -201,17 +202,18 @@ exception TwoDifferentSubtermsFound of int (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) -let discriminate'_tac ~term ~status:((proof, goal) as status) = +let discriminate'_tac ~term status = + let (proof, goal) = status in 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,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -286,26 +288,14 @@ prerr_endline ("XXXX nth funzionano ") ; let (proof',goals') = EliminationTactics.elim_type_tac ~term:(C.MutInd(Logic.false_URI,0,[])) - ~status + status in (match goals' with [goal'] -> let _,metasenv',_,_ = proof' in - let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in -prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ; -prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; -prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; -ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ; -prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); t2])) ; + let _,context',gty' = + CicUtil.lookup_meta goal' metasenv' + in T.then_ ~start: (P.change_tac @@ -340,7 +330,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) ) - ~status:(proof',goal') + (proof',goal') | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") @@ -349,11 +339,11 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ;; -let discriminate_tac ~term ~status = +let discriminate_tac ~term status = Tacticals.then_ ~start:(* (injection_tac ~term) *) Tacticals.id_tac ~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *) - ~status + status ;; @@ -366,7 +356,7 @@ e' vera o no e lo risolve *) -let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~status +let compare_tac ~term status = Tacticals.id_tac status (* (* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) (* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) @@ -375,7 +365,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat 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 + let _,context,gty = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> @@ -396,7 +386,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat ~continuations:[ T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; decide_equality_tac] - ~status + status | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> let term' = (* (t1=t2) \/ ~(t1=t2) *) C.Appl [ @@ -414,7 +404,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat ~continuations:[ T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; decide_equality_tac] - ~status + status | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") *) ;; @@ -425,13 +415,14 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int) -let discriminate_tac ~term ~status:((proof, goal) as status) = +let discriminate_tac ~term status = let module C = Cic in let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in + let (proof, goal) = status in let _,metasenv,_,_ = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -511,26 +502,14 @@ prerr_endline ("XXXX nth funzionano ") ; let (proof',goals') = EliminationTactics.elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) - ~status + status in (match goals' with [goal'] -> let _,metasenv',_,_ = proof' in - let _,context',gty' = List.find (function (m,_,_) -> m=goal') metasenv' in -prerr_endline ("XXXX gty " ^ CicPp.ppterm gty') ; -prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; -prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; -ignore (List.map (fun t -> prerr_endline ("XXXX t " ^ CicPp.ppterm t)) pattern) ; -prerr_endline ("XXXX case " ^ CicPp.ppterm (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); t2'])) ; + let _,context',gty' = + CicUtil.lookup_meta goal' metasenv' + in T.then_ ~start: (P.change_tac @@ -569,7 +548,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) ) - ~status:(proof',goal') + (proof',goal') | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")