X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=dd2e68d09e8afcaf582ee88f10a7481cc63cfd0d;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=5523c137ce80c3f539b632ef41580a60e9b690f5;hpb=d651bf2e3d560e194fbe948dd950dd600a40eab6;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 5523c137c..dd2e68d09 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,7 +25,8 @@ 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 @@ -71,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 @@ -147,7 +149,8 @@ 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 = CicUtil.lookup_meta goal metasenv in prerr_endline ("XXXX goal " ^ string_of_int goal) ; @@ -178,7 +181,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ); t1] ) - ~status + status ) ~continuation: (T.then_ @@ -186,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") @@ -199,7 +202,8 @@ 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 @@ -284,7 +288,7 @@ 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'] -> @@ -326,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") @@ -335,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 ;; @@ -352,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 *) @@ -382,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 [ @@ -400,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") *) ;; @@ -411,11 +415,12 @@ 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,_ = CicUtil.lookup_meta goal metasenv in let termty = (CicTypeChecker.type_of_aux' metasenv context term) in @@ -497,7 +502,7 @@ 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'] -> @@ -543,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")