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