matita/components/ng_tactics/declarative.ml

   1 (* Copyright (C) 2019, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24 *)
  25
  26 open Continuationals.Stack
  27 module Ast = NotationPt
  28 open NTactics
  29 open NTacStatus
  30
  31 type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
  32
  33 let mk_just status goal =
  34   function
  35     `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal
  36   | `Term t -> apply_tac t
  37
  38 exception NotAProduct
  39 exception FirstTypeWrong
  40 exception NotEquivalentTypes
  41
  42 let extract_first_goal_from_status status =
  43   let s = status#stack in
  44   match s with
  45   | [] -> fail (lazy "There's nothing to prove")
  46   | (g1, _, k, tag1, _) :: tl ->
  47     let goals = filter_open g1 in
  48     match goals with
  49       [] -> fail (lazy "No goals under focus")
  50     | loc::tl ->
  51       let goal = goal_of_loc (loc) in
  52       goal ;;
  53
  54 let extract_conclusion_type status goal =
  55   let gty = get_goalty status goal in
  56   let ctx = ctx_of gty in
  57   let status,gty = term_of_cic_term status gty ctx in
  58   gty
  59 ;;
  60
  61 let alpha_eq_tacterm_kerterm ty t status goal =
  62   let gty = get_goalty status goal in
  63   let ctx = ctx_of gty in
  64   let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
  65   let (_,_,metasenv,subst,_) = status#obj in
  66   let status,ty = term_of_cic_term status cicterm ctx in
  67   if NCicReduction.alpha_eq status metasenv subst ctx t ty then
  68     true
  69   else
  70     false
  71 ;;
  72
  73 let are_convertible ty1 ty2 status goal =
  74   let gty = get_goalty status goal in
  75   let ctx = ctx_of gty in
  76   let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
  77   let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
  78   NTacStatus.are_convertible status ctx cicterm1 cicterm2
  79
  80 let clear_volatile_params_tac status =
  81   match status#stack with
  82     [] -> fail (lazy "Empty stack")
  83   | (g,t,k,tag,p)::tl ->
  84     let rec remove_volatile = function
  85         [] -> []
  86       | (k,v as hd')::tl' ->
  87         let re = Str.regexp "volatile_.*" in
  88         if Str.string_match re k 0 then
  89           remove_volatile tl'
  90         else
  91           hd'::(remove_volatile tl')
  92     in
  93     let newp = remove_volatile p in
  94     status#set_stack ((g,t,k,tag,newp)::tl)
  95 ;;
  96
  97 let add_parameter_tac key value status =
  98   match status#stack with
  99     [] -> status
 100   | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
 101 ;;
 102
 103
 104 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
 105    the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
 106    \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
 107 *)
 108 let lambda_abstract_tac id t1 status goal =
 109   match extract_conclusion_type status goal with
 110   | NCic.Prod (_,t,_) ->
 111     if alpha_eq_tacterm_kerterm t1 t status goal then
 112       let (_,_,t1) = t1 in
 113       block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
 114                                                 `JustOne))); clear_volatile_params_tac;
 115                  add_parameter_tac "volatile_newhypo" id] status
 116 (*
 117       match t2 with
 118       | None ->
 119         let (_,_,t1) = t1 in
 120         block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
 121                                                   `JustOne))); clear_volatile_params_tac] status
 122       | Some t2 ->
 123         let status,res = are_convertible t1 t2 status goal in
 124         if res then
 125           let (_,_,t2) = t2 in
 126           block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
 127                                                     `JustOne))); clear_volatile_params_tac] status
 128         else
 129           raise NotEquivalentTypes
 130 *)
 131     else
 132       raise FirstTypeWrong
 133   | _ -> raise NotAProduct
 134
 135 let assume name ty status =
 136   let goal = extract_first_goal_from_status status in
 137   try lambda_abstract_tac name ty status goal
 138   with
 139   | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
 140   | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
 141   | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 142 ;;
 143
 144 let suppose t1 id status =
 145   let goal = extract_first_goal_from_status status in
 146   try lambda_abstract_tac id t1 status goal
 147   with
 148   | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
 149   | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
 150   | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 151 ;;
 152
 153 let assert_tac t1 t2 status goal continuation =
 154   let t = extract_conclusion_type status goal in
 155   if alpha_eq_tacterm_kerterm t1 t status goal then
 156     match t2 with
 157     | None -> continuation
 158     | Some t2 ->
 159       let status,res = are_convertible t1 t2 status goal in
 160       if res then continuation
 161       else
 162         raise NotEquivalentTypes
 163   else
 164     raise FirstTypeWrong
 165
 166 let branch_dot_tac status =
 167   match status#stack with
 168     ([],t,k,tag,p) :: tl ->
 169     if List.length t > 0 then
 170       status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
 171     else
 172       status
 173   | _ -> status
 174 ;;
 175
 176 let status_parameter key status =
 177   match status#stack with
 178     [] -> ""
 179   | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
 180 ;;
 181
 182 let beta_rewriting_step t status =
 183   let ctx = status_parameter "volatile_context" status in
 184   if ctx <> "beta_rewrite" then
 185     (
 186       let newhypo = status_parameter "volatile_newhypo" status in
 187       if newhypo = "" then
 188         fail (lazy "Invalid use of 'or equivalently'")
 189       else
 190         change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
 191     )
 192   else
 193     change_tac ~where:("",0,(None,[],Some
 194                                Ast.UserInput)) ~with_what:t status
 195 ;;
 196
 197 let done_continuation status =
 198   let rec continuation l =
 199     match l with
 200       [] -> []
 201     | (_,t,_,tag,p)::tl ->
 202       if tag = `BranchTag then
 203         if List.length t > 0 then
 204           let continue =
 205             let ctx =
 206               try List.assoc "context" p
 207               with Not_found -> ""
 208             in
 209               ctx <> "induction" && ctx <> "cases"
 210           in
 211           if continue then [clear_volatile_params_tac;branch_dot_tac] else
 212             [clear_volatile_params_tac]
 213         else
 214           [merge_tac] @ (continuation tl)
 215       else
 216         []
 217   in
 218     continuation status#stack
 219 ;;
 220
 221 let bydone just status =
 222   let goal = extract_first_goal_from_status status in
 223   let continuation = done_continuation status in
 224   let l = [mk_just status goal just] @ continuation in
 225   block_tac l status
 226 ;;
 227
 228 let push_goals_tac status =
 229   match status#stack with
 230     [] -> fail (lazy "Error pushing goals")
 231   | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
 232     if List.length g2 > 0 then
 233       status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
 234     else status (* Nothing to push *)
 235   | _ -> status
 236
 237 let we_need_to_prove t id status =
 238   let goal = extract_first_goal_from_status status in
 239   match id with
 240   | None ->
 241     (
 242       try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
 243       with
 244       | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
 245     )
 246   | Some id ->
 247     (
 248       block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
 249                  push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite"
 250                           ] status
 251     )
 252 ;;
 253
 254 let by_just_we_proved just ty id status =
 255   let goal = extract_first_goal_from_status status in
 256   let wrappedjust = just in
 257   let just = mk_just status goal just in
 258   match id with
 259   | None ->
 260     assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
 261                                                  "volatile_context" "beta_rewrite"] status)
 262   | Some id ->
 263     (
 264       block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
 265                  clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status
 266     )
 267 ;;
 268
 269 let existselim just id1 t1 t2 id2 status =
 270   let goal = extract_first_goal_from_status status in
 271   let (_,_,t1) = t1 in
 272   let (_,_,t2) = t2 in
 273   let just = mk_just status goal just in
 274   (block_tac [
 275       cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
 276                                                                                  (id1,None), Some t1),t2)]));
 277       branch_tac ~force:false;
 278       just;
 279       shift_tac;
 280       case1_tac "_";
 281       intros_tac ~names_ref:(ref []) [id1;id2];
 282       merge_tac;
 283       clear_volatile_params_tac
 284     ]) status
 285 ;;
 286
 287 let andelim just t1 id1 t2 id2 status =
 288   let goal = extract_first_goal_from_status status in
 289   let (_,_,t1) = t1 in
 290   let (_,_,t2) = t2 in
 291   let just = mk_just status goal just in
 292   (block_tac [
 293       cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
 294       branch_tac ~force:false;
 295       just;
 296       shift_tac;
 297       case1_tac "_";
 298       intros_tac ~names_ref:(ref []) [id1;id2];
 299       merge_tac;
 300       clear_volatile_params_tac
 301     ]) status
 302 ;;
 303
 304 let type_of_tactic_term status ctx t =
 305   let status,cicterm = disambiguate status ctx t `XTNone in
 306   let (_,cicty) = typeof status ctx cicterm in
 307   cicty
 308
 309 let swap_first_two_goals_tac status =
 310   let gstatus =
 311     match status#stack with
 312     | [] -> assert false
 313     | (g,t,k,tag,p) :: s ->
 314       match g with
 315       | (loc1) :: (loc2) :: tl ->
 316         ([loc2;loc1] @+ tl,t,k,tag,p) :: s
 317       | _ -> assert false
 318   in
 319   status#set_stack gstatus
 320
 321 let thesisbecomes t1 = we_need_to_prove t1 None
 322 ;;
 323
 324 let obtain id t1 status =
 325   let goal = extract_first_goal_from_status status in
 326   let cicgty = get_goalty status goal in
 327   let ctx = ctx_of cicgty in
 328   let cicty = type_of_tactic_term status ctx t1 in
 329   let _,ty = term_of_cic_term status cicty ctx in
 330   let (_,_,t1) = t1 in
 331   block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
 332                                          `JustOne]));
 333               swap_first_two_goals_tac;
 334               branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
 335               add_parameter_tac "volatile_context" "rewrite"
 336             ]
 337     status
 338 ;;
 339
 340 let conclude t1 status =
 341   let goal = extract_first_goal_from_status status in
 342   let cicgty = get_goalty status goal in
 343   let ctx = ctx_of cicgty in
 344   let _,gty = term_of_cic_term status cicgty ctx in
 345   match gty with
 346     NCic.Appl [_;_;plhs;_] ->
 347     if alpha_eq_tacterm_kerterm t1 plhs status goal then
 348       add_parameter_tac "volatile_context" "rewrite" status
 349     else
 350       fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
 351   | _ -> fail (lazy "Your conclusion needs to be an equality")
 352 ;;
 353
 354 let rewritingstep rhs just last_step status =
 355   let ctx = status_parameter "volatile_context" status in
 356   if ctx = "rewrite" then
 357     (
 358       let goal = extract_first_goal_from_status status in
 359       let cicgty = get_goalty status goal in
 360       let ctx = ctx_of cicgty in
 361       let _,gty = term_of_cic_term status cicgty ctx in
 362       let cicty = type_of_tactic_term status ctx rhs in
 363       let _,ty = term_of_cic_term status cicty ctx in
 364       let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
 365         match just with
 366           `Auto (univ, params) ->
 367           let params =
 368             if not (List.mem_assoc "timeout" params) then
 369               ("timeout","3")::params
 370             else params
 371           in
 372           let params' =
 373             if not (List.mem_assoc "paramodulation" params) then
 374               ("paramodulation","1")::params
 375             else params
 376           in
 377           if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
 378           else
 379             first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
 380                          ~params:(univ, params') status goal]
 381         | `Term just -> apply_tac just
 382         | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
 383         | `Proof -> id_tac
 384       in
 385       let plhs,prhs,prepare =
 386         match gty with (* Extracting the lhs and rhs of the previous equality *)
 387           NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
 388         | _ -> fail (lazy "You are not building an equaility chain")
 389       in
 390       let continuation =
 391         if last_step then
 392           (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
 393           let todo = [just'] @ (done_continuation status) in
 394           (*       let todo = if mustdot status then List.append todo [dot_tac] else todo *)
 395           (*       in *)
 396           block_tac todo
 397         else
 398           let (_,_,rhs) = rhs in
 399           block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
 400                                                rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
 401       in
 402       prepare continuation
 403     )
 404   else
 405     fail (lazy "You are not building an equality chain")
 406 ;;
 407
 408 let rec pp_metasenv_names (metasenv:NCic.metasenv) =
 409   match metasenv with
 410     [] -> ""
 411   | hd :: tl ->
 412     let n,conj = hd in
 413     let meta_attrs,_,_ = conj in
 414     let rec find_name_aux meta_attrs = match meta_attrs with
 415         [] -> "Anonymous"
 416       | hd :: tl -> match hd with
 417           `Name n -> n
 418         | _ -> find_name_aux tl
 419     in
 420     let name = find_name_aux meta_attrs
 421     in
 422     "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
 423 ;;
 424
 425 let print_goals_names_tac s (status:#NTacStatus.tac_status) =
 426   let (_,_,metasenv,_,_) = status#obj in
 427   prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
 428
 429 (* Useful as it does not change the order in the list *)
 430 let rec list_change_assoc k v = function
 431     [] -> []
 432   | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
 433 ;;
 434
 435 let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
 436   let add_name_to_goal name goal metasenv =
 437     let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
 438     let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
 439     let newconj = (mattrs,ctx,t) in
 440     list_change_assoc goal newconj metasenv
 441   in
 442   let new_goals =
 443     (* It's important that this tactic is called before branching and right after the creation of
 444      * the new goals, when they are still under focus *)
 445     match status#stack with
 446       [] -> fail (lazy "Can not add names to an empty stack")
 447     | (g,_,_,_,_) :: tl ->
 448       let rec sublist n = function
 449           [] -> []
 450         | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
 451       in
 452       List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
 453   in
 454   let rec add_names_to_goals g cl metasenv =
 455     match g,cl with
 456       [],[] -> metasenv
 457     | hd::tl, (_,consname,_)::tl' ->
 458       add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
 459     | _,_ -> fail (lazy "There are less goals than constructors")
 460   in
 461   let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
 462   let newmetasenv = add_names_to_goals new_goals !cl metasenv
 463   in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
 464 ;;
 465 (*
 466   let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
 467   let remove_name_from_metaattrs =
 468    List.filter (function `Name _ -> false | _ -> true) in
 469   let rec add_names_to_metasenv cl metasenv =
 470     match cl,metasenv with
 471       [],_ -> metasenv
 472     | hd :: tl, mhd :: mtl ->
 473       let _,consname,_ = hd in
 474         let gnum,conj = mhd in
 475         let mattrs,ctx,t = conj in
 476         let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
 477         in
 478         let newconj = mattrs,ctx,t in
 479         let newmeta = gnum,newconj in
 480         newmeta :: (add_names_to_metasenv tl mtl)
 481     | _,[] -> assert false
 482   in
 483   let newmetasenv = add_names_to_metasenv !cl metasenv in
 484   status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
 485 *)
 486
 487 let unfocus_branch_tac status =
 488   match status#stack with
 489     [] -> status
 490   | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
 491 ;;
 492
 493 let we_proceed_by_induction_on t1 t2 status =
 494   let goal = extract_first_goal_from_status status in
 495   let txt,len,t1 = t1 in
 496   let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
 497   let indtyinfo = ref None in
 498   let sort = ref (NCic.Rel 1) in
 499   let cl = ref [] in
 500   try
 501     assert_tac t2 None status goal (block_tac [
 502         analyze_indty_tac ~what:t1 indtyinfo;
 503         sort_of_goal_tac sort;
 504         (fun status ->
 505            let ity = HExtlib.unopt !indtyinfo in
 506            let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
 507            let name =
 508              NUri.name_of_uri uri ^ "_" ^
 509              snd (NCicElim.ast_of_sort
 510                     (match !sort with NCic.Sort x -> x | _ -> assert false))
 511            in
 512            let eliminator =
 513              let l = [Ast.Ident (name,None)] in
 514              (* Generating an implicit for each argument of the inductive type, plus one the
 515               * predicate, plus an implicit for each constructor of the inductive type *)
 516              let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
 517              let _,_,t1 = t1 in
 518              let l = l @ [t1] in
 519              Ast.Appl l
 520            in
 521            cl := ity.cl;
 522            exact_tac ("",0,eliminator) status);
 523         add_names_to_goals_tac cl;
 524         branch_tac;
 525         push_goals_tac;
 526         unfocus_branch_tac;
 527         add_parameter_tac "context" "induction"
 528       ] status)
 529   with
 530   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 531 ;;
 532
 533 let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
 534   let goal = extract_first_goal_from_status status in
 535   let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
 536   let indtyinfo = ref None in
 537   let cl = ref [] in
 538   try
 539     assert_tac t2 None status goal (block_tac [
 540         analyze_indty_tac ~what:npt1 indtyinfo;
 541         cases_tac ~what:t1 ~where:("",0,(None,[],Some
 542                                            Ast.UserInput));
 543         (
 544           fun status ->
 545             let ity = HExtlib.unopt !indtyinfo in
 546             cl := ity.cl; add_names_to_goals_tac cl status
 547         );
 548         branch_tac; push_goals_tac;
 549         unfocus_branch_tac;
 550         add_parameter_tac "context" "cases"
 551       ] status)
 552   with
 553   | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
 554 ;;
 555
 556 let byinduction t1 id = suppose t1 id ;;
 557
 558 let name_of_conj conj =
 559   let mattrs,_,_ = conj in
 560   let rec search_name mattrs =
 561     match mattrs with
 562       [] -> "Anonymous"
 563     | hd::tl ->
 564       match hd with
 565         `Name n -> n
 566       | _ -> search_name tl
 567   in
 568   search_name mattrs
 569
 570 let rec loc_of_goal goal l =
 571   match l with
 572     [] -> fail (lazy "Reached the end")
 573   | hd :: tl ->
 574     let _,sw = hd in
 575     let g = goal_of_switch sw in
 576     if g = goal then hd
 577     else loc_of_goal goal tl
 578 ;;
 579
 580 let has_focused_goal status =
 581   match status#stack with
 582     [] -> false
 583   | ([],_,_,_,_) :: tl -> false
 584   | _ -> true
 585 ;;
 586
 587 let focus_on_case_tac case status =
 588   let (_,_,metasenv,_,_) = status#obj in
 589   let rec goal_of_case case metasenv =
 590     match metasenv with
 591       [] -> fail (lazy "The given case does not exist")
 592     | (goal,conj) :: tl ->
 593       if name_of_conj conj = case then goal
 594       else goal_of_case case tl
 595   in
 596   let goal_to_focus = goal_of_case case metasenv in
 597   let gstatus =
 598     match status#stack with
 599       [] -> fail (lazy "There is nothing to prove")
 600     | (g,t,k,tag,p) :: s ->
 601       let loc =
 602         try
 603           loc_of_goal goal_to_focus t
 604         with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
 605         context")
 606       in
 607       let curloc = if has_focused_goal status then
 608           let goal = extract_first_goal_from_status status in
 609           [loc_of_goal goal g]
 610         else []
 611       in
 612       (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
 613   in
 614   status#set_stack gstatus
 615 ;;
 616
 617 let case id l status =
 618   let ctx = status_parameter "context" status in
 619   if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
 620   induction/cases analysis context")
 621 else
 622   (
 623     if has_focused_goal status then fail (lazy "Finish the current case before switching")
 624     else
 625       (
 626 (*
 627         let goal = extract_first_goal_from_status status in
 628         let (_,_,metasenv,_,_) = status#obj in
 629         let conj = NCicUtils.lookup_meta goal metasenv in
 630         let name = name_of_conj conj in
 631 *)
 632         let continuation =
 633           let rec aux l =
 634             match l with
 635               [] -> [id_tac]
 636             | (id,ty)::tl ->
 637               (try_tac (assume id ("",0,ty))) :: (aux tl)
 638           in
 639           aux l
 640         in
 641 (*         if name = id then block_tac continuation status *)
 642 (*         else  *)
 643           block_tac ([focus_on_case_tac id] @ continuation) status
 644       )
 645   )
 646 ;;
 647
 648 let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
 649
 650 (* vim: ts=2: sw=0: et:
 651  * *)