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