X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=eeda7a862a83ce2d9a6771ff5d3c7d6f57f14e07;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=537ef3f5d986f06286ca7ea341cb9d2c750bed0f;hpb=17f33fa8cb65de1f3edcba6ac750bbdb4d061117;p=helm.git diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 537ef3f5d..eeda7a862 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -597,7 +597,7 @@ let tac_zero_inf_pos (n,d) ~status = let pall str ~status:(proof,goal) t = debug ("tac "^str^" :\n" ); let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm t ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); in @@ -678,7 +678,7 @@ let tac_zero_inf_false gl (n,d) ~status= (debug "2\n";let r = (Tacticals.then_ ~start:( fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in - let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " ^ CicPp.ppterm ty ^"\n"); let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in @@ -698,7 +698,7 @@ let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= debug("stat tac_zero_infeq_false\n"); let r = let curi,metasenv,pbo,pty = proof in - let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("faccio fold di " ^ CicPp.ppterm (Cic.Appl @@ -736,7 +736,7 @@ let r = let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -757,7 +757,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = let my_cut ~term:c ~status:(proof,goal)= let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("my_cut di "^CicPp.ppterm c^"\n"); @@ -784,7 +784,7 @@ let exact = PrimitiveTactics.exact_tac;; let tac_use h ~status:(proof,goal as status) = debug("Inizio TC_USE\n"); let curi,metasenv,pbo,pty = proof in -let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -899,7 +899,7 @@ debug("inizio EQ\n"); let module C = Cic in let proof,goal = status in let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = @@ -925,7 +925,7 @@ let tcl_fail a ~status:(proof,goal) = (* Galla: moved in variousTactics.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 metano,context,ty = CicUtil.lookup_meta goal metasenv in let num = ref 0 in let tac_list = List.map ( fun x -> num := !num + 1; @@ -955,9 +955,7 @@ let contradiction_tac ~status:(proof,goal)= let rec fourier ~status:(s_proof,s_goal)= let s_curi,s_metasenv,s_pbo,s_pty = s_proof in - let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) - s_metasenv in - + let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); debug_pcontext s_context; @@ -998,7 +996,7 @@ theoreme,so let's parse our thesis *) (* now we have all the right environment *) let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* now we want to convert hp to inequations, but first we must lift @@ -1087,8 +1085,7 @@ theoreme,so let's parse our thesis *) fun ~status -> debug ("inizio t1 strict\n"); let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find - (function (m,_,_) -> m=goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) @@ -1124,8 +1121,7 @@ theoreme,so let's parse our thesis *) fun ~status -> debug("INIZIO TAC 1 2\n"); let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) - metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) @@ -1163,8 +1159,7 @@ theoreme,so let's parse our thesis *) ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ ~start:(fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) - metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status) ~continuation:(Tacticals.then_ @@ -1203,8 +1198,7 @@ theoreme,so let's parse our thesis *) ( fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m= - goal) metasenv in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* check if ty is of type *) let w1 = debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");