X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fdeclarative.ml;h=a136a51dd88afc306661a18aee087139dadaf99f;hp=ac521186a4db80d0c6190d9b39c4ba547406a718;hb=784f0d4d7cff3700363affe647f7b8b218726fcb;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index ac521186a..a136a51dd 100644
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -1,14 +1,14 @@
 (* Copyright (C) 2019, HELM Team.
- * 
+ *
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
  * Department, University of Bologna, Italy.
- * 
+ *
  * HELM is free software; you can redistribute it and/or
  * modify it under the terms of the GNU General Public License
  * as published by the Free Software Foundation; either version 2
  * of the License, or (at your option) any later version.
- * 
+ *
  * HELM is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
@@ -18,327 +18,623 @@
  * along with HELM; if not, write to the Free Software
  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  * MA  02111-1307, USA.
- * 
+ *
  * For details, see the HELM World-Wide-Web page,
  * http://cs.unibo.it/helm/.
- *)
+*)
 
+open Continuationals.Stack
 module Ast = NotationPt
 open NTactics
 open NTacStatus
 
 type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
 
-let mk_just =
-    function
-          `Auto (l,params) -> distribute_tac (fun status goal -> NnAuto.auto_lowtac
-          ~params:(l,params) status goal)
-        | `Term t -> apply_tac t
+let mk_just status goal =
+  function
+    `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal
+  | `Term t -> apply_tac t
 
 exception NotAProduct
 exception FirstTypeWrong
 exception NotEquivalentTypes
 
+let extract_first_goal_from_status status =
+  let s = status#stack in
+  match s with
+  | [] -> fail (lazy "There's nothing to prove")
+  | (g1, _, _k, _tag1, _) :: _tl ->
+    let goals = filter_open g1 in
+    match goals with
+      [] -> fail (lazy "No goals under focus")
+    | loc::_tl -> 
+      let goal = goal_of_loc (loc) in
+      goal ;;
+
 let extract_conclusion_type status goal =
-    let gty = get_goalty status goal in
-    let ctx = ctx_of gty in
-    let status,gty = term_of_cic_term status gty ctx in
-    gty
+  let gty = get_goalty status goal in
+  let ctx = ctx_of gty in
+  term_of_cic_term status gty ctx
 ;;
 
-let same_type_as_conclusion ty t status goal =
-    let gty = get_goalty status goal in
-    let ctx = ctx_of gty in
-    let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
-    let (_,_,metasenv,subst,_) = status#obj in
-    let status,ty = term_of_cic_term status cicterm ctx in
-    if NCicReduction.alpha_eq status metasenv subst ctx t ty then
-        true
-    else
-        false
+let alpha_eq_tacterm_kerterm ty t status goal =
+  let gty = get_goalty status goal in
+  let ctx = ctx_of gty in
+  let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
+  let (_,_,metasenv,subst,_) = status#obj in
+  let status,ty = term_of_cic_term status cicterm ctx in
+  if NCicReduction.alpha_eq status metasenv subst ctx t ty then
+    true
+  else
+    false
 ;;
 
 let are_convertible ty1 ty2 status goal =
-    let gty = get_goalty status goal in
-    let ctx = ctx_of gty in
-    let status,cicterm1 = disambiguate status ctx ty1 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
-    let status,cicterm2 = disambiguate status ctx ty2 `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
-    NTacStatus.are_convertible status ctx cicterm1 cicterm2
+  let gty = get_goalty status goal in
+  let ctx = ctx_of gty in
+  let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
+  let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
+  NTacStatus.are_convertible status ctx cicterm1 cicterm2
+
+let clear_volatile_params_tac status =
+  match status#stack with
+    [] -> fail (lazy "Empty stack")
+  | (g,t,k,tag,p)::tl -> 
+    let rec remove_volatile = function
+        [] -> []
+      | (k,_v as hd')::tl' ->
+        let re = Str.regexp "volatile_.*" in
+        if Str.string_match re k 0 then
+          remove_volatile tl'
+        else
+          hd'::(remove_volatile tl')
+    in
+    let newp = remove_volatile p in
+    status#set_stack ((g,t,k,tag,newp)::tl)
+;;
+
+let add_parameter_tac key value status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+;;
+
 
 (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
-the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
-\lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
+   the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
+   \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
 *)
-let lambda_abstract_tac id t1 t2 status goal =
-    match extract_conclusion_type status goal with
-    | NCic.Prod (_,t,_) -> 
-        if same_type_as_conclusion t1 t status goal then
-            match t2 with
-            | None -> 
-                    let (_,_,t1) = t1 in
-                    exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
-                    `JustOne)))) status goal
-
-            | Some t2 -> 
-                let status,res = are_convertible t1 t2 status goal in
-                if res then
-                let (_,_,t2) = t2 in
-                    exec (exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t2),Ast.Implicit
-                    `JustOne)))) status goal
-                else
-                    raise NotEquivalentTypes
-        else
-            raise FirstTypeWrong
-    | _ -> raise NotAProduct
-
-let assume name ty eqty =
-    distribute_tac (fun status goal ->
-        try lambda_abstract_tac name ty eqty status goal
-        with
-        | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
-        | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
-        | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
-     )
+let lambda_abstract_tac id t1 status goal =
+  match extract_conclusion_type status goal with
+  | status,NCic.Prod (_,t,_) ->
+    if alpha_eq_tacterm_kerterm t1 t status goal then
+      let (_,_,t1) = t1 in
+      block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+                                                `JustOne))); clear_volatile_params_tac;
+                 add_parameter_tac "volatile_newhypo" id] status
+    else
+      raise FirstTypeWrong
+  | _ -> raise NotAProduct
+
+let assume name ty status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac name ty status goal
+  with
+  | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
+  | FirstTypeWrong ->  fail (lazy "The assumed type is wrong")
+  | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
 ;;
 
-let suppose t1 id t2 =
-    distribute_tac (fun status goal ->
-        try lambda_abstract_tac id t1 t2 status goal
-        with
-        | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
-        | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
-        | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
-     )
+let suppose t1 id status =
+  let goal = extract_first_goal_from_status status in
+  try lambda_abstract_tac id t1 status goal
+  with
+  | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
+  | FirstTypeWrong ->  fail (lazy "The supposed proposition is different from the premise")
+  | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
 ;;
 
 let assert_tac t1 t2 status goal continuation =
-    let t = extract_conclusion_type status goal in
-    if same_type_as_conclusion t1 t status goal then
-        match t2 with
-        | None -> exec continuation status goal
-        | Some t2 ->
-            let status,res = are_convertible t1 t2 status goal in
-            if res then
-                exec continuation status goal
-            else
-                raise NotEquivalentTypes
+  let status,t = extract_conclusion_type status goal in
+  if alpha_eq_tacterm_kerterm t1 t status goal then
+    match t2 with
+    | None -> continuation
+    | Some t2 ->
+      let _status,res = are_convertible t1 t2 status goal in
+      if res then continuation
+      else
+        raise NotEquivalentTypes
+  else
+    raise FirstTypeWrong
+
+let branch_dot_tac status =
+  match status#stack with 
+    ([],t,k,tag,p) :: tl ->
+    if List.length t > 0 then
+      status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
     else
-        raise FirstTypeWrong
-
-let we_need_to_prove t id t1 =
-    distribute_tac (fun status goal ->
-        match id with
-        | None -> 
-            (
-                match t1 with
-                | None ->  (* We need to prove t *)
-                    (
-                    try
-                        assert_tac t None status goal id_tac
-                    with
-                    | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-                    )
-                | Some t1 -> (* We need to prove t or equivalently t1 *)
-                    (
-                        try
-                            assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1)
-                        with
-                        | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-                        | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-                    )
-            )
-        | Some id -> 
-            (
-                match t1 with
-                | None -> (* We need to prove t (id) *)
-                    exec (block_tac [cut_tac t; branch_tac ~force:false; shift_tac; intro_tac id;
-                    (*merge_tac*)]) status goal
-                | Some t1 -> (* We need to prove t (id) or equivalently t1 *)
-                    exec (block_tac [cut_tac t; branch_tac ~force:false; change_tac ~where:("",0,(None,[],Some Ast.UserInput))
-                    ~with_what:t1; shift_tac; intro_tac id; merge_tac]) status goal
-            )
+      status
+  | _ -> status
+;;
+
+let status_parameter key status =
+  match status#stack with
+    [] -> ""
+  | (_g,_t,_k,_tag,p)::_ -> try List.assoc key p with _ -> ""
+;;
+
+let beta_rewriting_step t status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx <> "beta_rewrite" then 
+    (
+      let newhypo = status_parameter "volatile_newhypo" status in
+      if newhypo = "" then
+        fail (lazy "Invalid use of 'that is equivalent to'")
+      else
+        change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
+    )
+  else
+    change_tac ~where:("",0,(None,[],Some
+                               Ast.UserInput)) ~with_what:t status
+;;
+
+let done_continuation status =
+  let rec continuation l =
+    match l with
+      [] -> []
+    | (_,t,_,tag,p)::tl ->
+      if tag = `BranchTag then
+        if List.length t > 0 then
+          let continue =
+            let ctx =
+              try List.assoc "context" p
+              with Not_found -> ""
+            in
+              ctx <> "induction" && ctx <> "cases"
+          in
+          if continue then [clear_volatile_params_tac;branch_dot_tac] else
+            [clear_volatile_params_tac]
+        else 
+          [merge_tac] @ (continuation tl)
+      else
+        []
+  in
+    continuation status#stack
+;;
+
+let bydone just status =
+  let goal = extract_first_goal_from_status status in
+  let continuation = done_continuation status in
+  let l = [mk_just status goal just] @ continuation in
+  block_tac l status
+;;
+
+let push_goals_tac status = 
+  match status#stack with
+    [] -> fail (lazy "Error pushing goals")
+  | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
+    if List.length g2 > 0 then
+      status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
+    else status (* Nothing to push *)
+  | _ -> status
+
+let we_need_to_prove t id status =
+  let goal = extract_first_goal_from_status status in
+  match id with
+  | None ->
+    (
+      try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
+      with
+      | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
+    )
+  | Some id ->
+    (
+      block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+                 push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite"
+                          ] status
     )
 ;;
 
-let by_just_we_proved just ty id ty' = 
-    distribute_tac (fun status goal -> 
-        let just = mk_just just in
-            match id with
-            | None ->
-                (match ty' with
-                     | None -> (* just we proved P done *)
-                        (
-                            try
-                                assert_tac ty None status goal just
-                            with
-                            | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
-                            | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-                        )
-                     | Some ty' -> (* just we proved P that is equivalent to P' done *)
-                        (
-                            try
-                                assert_tac ty' (Some ty) status goal (block_tac [change_tac
-                                ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:ty; just])
-                            with
-                            | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
-                            | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
-                        )
-                 )
-            | Some id ->
-                (
-                    match ty' with
-                    | None -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
-                    id; merge_tac ]) status goal
-                    | Some ty' -> exec (block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac
-                    id; change_tac ~where:("",0,(None,[id,Ast.UserInput],None))
-                    ~with_what:ty'; merge_tac]) status goal
-                )
+let by_just_we_proved just ty id status =
+  let goal = extract_first_goal_from_status status in
+  let just = mk_just status goal just in
+  match id with
+  | None ->
+    assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
+                                                 "volatile_context" "beta_rewrite"] status)
+  | Some id ->
+    (
+      block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+                 clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status
     )
 ;;
 
-let thesisbecomes t1 t2 = we_need_to_prove t1 None t2 ;;
+let existselim just id1 t1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
+      cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
+                                                                                 (id1,None), Some t1),t2)]));
+      branch_tac ~force:false;
+      just;
+      shift_tac;
+      case1_tac "_";
+      intros_tac ~names_ref:(ref []) [id1;id2];
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
+;;
 
-let bydone just =
-    mk_just just
+let andelim just t1 id1 t2 id2 status =
+  let goal = extract_first_goal_from_status status in
+  let (_,_,t1) = t1 in
+  let (_,_,t2) = t2 in
+  let just = mk_just status goal just in
+  (block_tac [
+      cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
+      branch_tac ~force:false;
+      just;
+      shift_tac;
+      case1_tac "_";
+      intros_tac ~names_ref:(ref []) [id1;id2];
+      merge_tac;
+      clear_volatile_params_tac
+    ]) status
 ;;
 
-let existselim just id1 t1 t2 id2 =
-    let (_,_,t1) = t1 in
-    let (_,_,t2) = t2 in
-    let just = mk_just just in
-    block_tac [
-        cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
-        (id1,None), Some t1),t2)])); 
-        branch_tac ~force:false;
-        just; 
-        shift_tac; 
-        case1_tac "_";
-        intros_tac ~names_ref:(ref []) [id1;id2]; 
-        merge_tac
-    ]
-
-let andelim just t1 id1 t2 id2 = 
-    let (_,_,t1) = t1 in
-    let (_,_,t2) = t2 in
-    let just = mk_just just in
-    block_tac [
-        cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2])); 
-        branch_tac ~force:false;
-        just; 
-        shift_tac; 
-        case1_tac "_";
-        intros_tac ~names_ref:(ref []) [id1;id2]; 
-        merge_tac
-    ]
+let type_of_tactic_term status ctx t =
+  let status,cicterm = disambiguate status ctx t `XTNone in
+  let (_,cicty) = typeof status ctx cicterm in
+  cicty
+
+let swap_first_two_goals_tac status =
+  let gstatus =
+    match status#stack with
+    | [] -> assert false
+    | (g,t,k,tag,p) :: s ->
+      match g with
+      | (loc1) :: (loc2) :: tl ->
+        ([loc2;loc1] @+ tl,t,k,tag,p) :: s
+      | _ -> assert false
+  in
+  status#set_stack gstatus
+
+let thesisbecomes t1 = we_need_to_prove t1 None
 ;;
 
+let obtain id t1 status =
+  let goal = extract_first_goal_from_status status in
+  let cicgty = get_goalty status goal in
+  let ctx = ctx_of cicgty in
+  let cicty = type_of_tactic_term status ctx t1 in
+  let _,ty = term_of_cic_term status cicty ctx in
+  let (_,_,t1) = t1 in
+  block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
+                                         `JustOne]));
+              swap_first_two_goals_tac;
+              branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+              add_parameter_tac "volatile_context" "rewrite"
+            ]
+    status
+;;
 
+let conclude t1 status =
+  let goal = extract_first_goal_from_status status in
+  let cicgty = get_goalty status goal in
+  let ctx = ctx_of cicgty in
+  let _,gty = term_of_cic_term status cicgty ctx in
+  match gty with
+    (* The first term of this Appl should probably be "eq" *)
+    NCic.Appl [_;_;plhs;_] ->
+    if alpha_eq_tacterm_kerterm t1 plhs status goal then
+      add_parameter_tac "volatile_context" "rewrite" status
+    else
+      fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+  | _ -> fail (lazy "Your conclusion needs to be an equality")
+;;
 
-let rewritingstep lhs rhs just last_step = fail (lazy "Not implemented");
- (*
- let aux ((proof,goal) as status) =
-  let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
-  let _,context,gty = CicUtil.lookup_meta goal metasenv in
-  let eq,trans =
-   match LibraryObjects.eq_URI () with
-      None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
-    | Some uri ->
-      Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
+let rewritingstep rhs just last_step status =
+  let ctx = status_parameter "volatile_context" status in
+  if ctx = "rewrite" then 
+    (
+      let goal = extract_first_goal_from_status status in
+      let cicgty = get_goalty status goal in
+      let ctx = ctx_of cicgty in
+      let _,gty = term_of_cic_term status cicgty ctx in
+      let cicty = type_of_tactic_term status ctx rhs in
+      let _,ty = term_of_cic_term status cicty ctx in
+      let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+        match just with
+          `Auto (univ, params) ->
+          let params =
+            if not (List.mem_assoc "timeout" params) then
+              ("timeout","3")::params
+            else params
+          in
+          let params' =
+            if not (List.mem_assoc "paramodulation" params) then
+              ("paramodulation","1")::params
+            else params
+          in
+          if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+          else
+            first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+                         ~params:(univ, params') status goal]
+        | `Term just -> apply_tac just
+        | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+        | `Proof -> id_tac
+      in
+      let plhs,prhs,prepare =
+        match gty with (* Extracting the lhs and rhs of the previous equality *)
+          NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+        | _ -> fail (lazy "You are not building an equaility chain")
+      in
+      let continuation =
+        if last_step then
+          let todo = [just'] @ (done_continuation status) in
+          block_tac todo
+        else
+          let (_,_,rhs) = rhs in
+          block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+                                               rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
+      in
+      prepare continuation
+    )
+  else
+    fail (lazy "You are not building an equality chain")
+;;
+
+let rec pp_metasenv_names (metasenv:NCic.metasenv) =
+  match metasenv with
+    [] -> ""
+  | hd :: tl ->
+    let n,conj = hd in
+    let meta_attrs,_,_ = conj in
+    let rec find_name_aux meta_attrs = match meta_attrs with
+        [] -> "Anonymous"
+      | hd :: tl -> match hd with
+          `Name n -> n
+        | _ -> find_name_aux tl
+    in
+    let name = find_name_aux meta_attrs
+    in
+    "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
+;;
+
+let print_goals_names_tac s (status:#NTacStatus.tac_status) =
+  let (_,_,metasenv,_,_) = status#obj in
+  prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
+
+(* Useful as it does not change the order in the list *)
+let rec list_change_assoc k v = function
+    [] -> []
+  | (k',_v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+;;
+
+let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
+  let add_name_to_goal name goal metasenv =
+    let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in
+    let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+    let newconj = (mattrs,ctx,t) in
+    list_change_assoc goal newconj metasenv
   in
-  let ty,_ =
-   CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
-  let just' =
-   match just with
-      `Auto (univ, params) ->
-        let params =
-         if not (List.exists (fun (k,_) -> k = "timeout") params) then
-          ("timeout","3")::params
-         else params
-        in
-        let params' =
-         if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
-          ("paramodulation","1")::params
-         else params
-        in
-         if params = params' then
-          Tactics.auto ~dbd ~params:(univ, params) ~automation_cache
-         else
-          Tacticals.first
-           [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
-            Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
-    | `Term just -> Tactics.apply just
-    | `SolveWith term -> 
-                    Tactics.demodulate ~automation_cache ~dbd
-                    ~params:(Some [term],
-                      ["all","1";"steps","1"; "use_context","false"])
-    | `Proof ->
-        Tacticals.id_tac
+  let new_goals =
+    (* It's important that this tactic is called before branching and right after the creation of
+     * the new goals, when they are still under focus *)
+    match status#stack with
+      [] -> fail (lazy "Can not add names to an empty stack")
+    | (g,_,_,_,_) :: _tl -> 
+      let rec sublist n = function
+          [] -> []
+        | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+      in
+      List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+  in
+  let rec add_names_to_goals g cl metasenv =
+    match g,cl with
+      [],[] -> metasenv
+    | hd::tl, (_,consname,_)::tl' -> 
+      add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+    | _,_ -> fail (lazy "There are less goals than constructors")
   in
-   let plhs,prhs,prepare =
-    match lhs with
-       None ->
-        let plhs,prhs =
-         match gty with 
-            Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
-          | _ -> assert false
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let newmetasenv = add_names_to_goals new_goals !cl metasenv
+  in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+;;
+(*
+  let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+  let remove_name_from_metaattrs =
+   List.filter (function `Name _ -> false | _ -> true) in
+  let rec add_names_to_metasenv cl metasenv =
+    match cl,metasenv with
+      [],_ -> metasenv
+    | hd :: tl, mhd :: mtl ->
+      let _,consname,_ = hd in
+        let gnum,conj = mhd in
+        let mattrs,ctx,t = conj in
+        let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
         in
-         plhs,prhs,
-          (fun continuation ->
-            ProofEngineTypes.apply_tactic continuation status)
-     | Some (None,lhs) ->
-        let plhs,prhs =
-         match gty with 
-            Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
-          | _ -> assert false
+        let newconj = mattrs,ctx,t in
+        let newmeta = gnum,newconj in
+        newmeta :: (add_names_to_metasenv tl mtl)
+    | _,[] -> assert false
+  in
+  let newmetasenv = add_names_to_metasenv !cl metasenv in
+  status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+*)
+
+let unfocus_branch_tac status =
+  match status#stack with
+    [] -> status
+  | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+;;
+
+let we_proceed_by_induction_on t1 t2 status =
+  let goal = extract_first_goal_from_status status in
+  let txt,len,t1 = t1 in
+  let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let sort = ref (NCic.Rel 1) in
+  let cl = ref [] in (* this is a ref on purpose, as the block of code after sort_of_goal_tac in
+  block_tac acts as a block of asynchronous code, in which cl gets modified with the info retrieved
+  with analize_indty_tac, and later used to label each new goal with a costructor name. Using a
+  plain list this doesn't seem to work, as add_names_to_goals_tac would immediately act on an empty
+  list, instead of acting on the list of constructors *)
+  try
+    assert_tac t2 None status goal (block_tac [
+        analyze_indty_tac ~what:t1 indtyinfo;
+        sort_of_goal_tac sort;
+        (fun status ->
+           let ity = HExtlib.unopt !indtyinfo in
+           let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
+           let name =
+             NUri.name_of_uri uri ^ "_" ^
+             snd (NCicElim.ast_of_sort
+                    (match !sort with NCic.Sort x -> x | _ -> assert false))
+           in
+           let eliminator =
+             let l = [Ast.Ident (name,None)] in
+             (* Generating an implicit for each argument of the inductive type, plus one the
+              * predicate, plus an implicit for each constructor of the inductive type *)
+             let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
+             let _,_,t1 = t1 in
+             let l = l @ [t1] in
+             Ast.Appl l
+           in
+           cl := ity.cl;
+           exact_tac ("",0,eliminator) status);
+        add_names_to_goals_tac cl; 
+        branch_tac; 
+        push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "induction"
+      ] status)
+  with
+  | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let we_proceed_by_cases_on ((txt,len,ast1) as t1)  t2 status =
+  let goal = extract_first_goal_from_status status in
+  let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let cl = ref [] in
+  try
+    assert_tac t2 None status goal (block_tac [
+        analyze_indty_tac ~what:npt1 indtyinfo;
+        cases_tac ~what:t1 ~where:("",0,(None,[],Some
+                                           Ast.UserInput));
+        (
+          fun status ->
+            let ity = HExtlib.unopt !indtyinfo in
+            cl := ity.cl; add_names_to_goals_tac cl status
+        );
+        branch_tac; push_goals_tac;
+        unfocus_branch_tac;
+        add_parameter_tac "context" "cases"
+      ] status)
+  with
+  | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+;;
+
+let byinduction t1 id status =
+  let ctx = status_parameter "context" status in
+  if ctx <> "induction" then fail (lazy "You can't use this tactic outside of an induction context")
+  else suppose t1 id status
+;;
+
+let name_of_conj conj =
+  let mattrs,_,_ = conj in
+  let rec search_name mattrs =
+    match mattrs with
+      [] -> "Anonymous"
+    | hd::tl ->
+      match hd with
+        `Name n -> n
+      | _ -> search_name tl
+  in
+  search_name mattrs
+
+let rec loc_of_goal goal l =
+  match l with
+    [] -> fail (lazy "Reached the end")
+  | hd :: tl ->
+    let _,sw = hd in
+    let g = goal_of_switch sw in
+    if g = goal then hd
+    else loc_of_goal goal tl
+;;
+
+let has_focused_goal status =
+  match status#stack with
+    [] -> false
+  | ([],_,_,_,_) :: _tl -> false
+  | _ -> true
+;;
+
+let focus_on_case_tac case status =
+  let (_,_,metasenv,_,_) = status#obj in
+  let rec goal_of_case case metasenv =
+    match metasenv with
+      [] -> fail (lazy "The given case does not exist")
+    | (goal,conj) :: tl ->
+      if name_of_conj conj = case then goal
+      else goal_of_case case tl
+  in
+  let goal_to_focus = goal_of_case case metasenv in
+  let gstatus =
+    match status#stack with
+      [] -> fail (lazy "There is nothing to prove")
+    | (g,t,k,tag,p) :: s ->
+      let loc = 
+        try 
+          loc_of_goal goal_to_focus t 
+        with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+        context")
+      in
+      let curloc = if has_focused_goal status then 
+          let goal = extract_first_goal_from_status status in
+          [loc_of_goal goal g]
+        else []
+      in
+      (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+  in 
+  status#set_stack gstatus
+;;
+
+let case id l status =
+  let ctx = status_parameter "context" status in
+  if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+  induction/cases analysis context")
+else
+  (
+    if has_focused_goal status then fail (lazy "Finish the current case before switching")
+    else
+      (
+(*
+        let goal = extract_first_goal_from_status status in
+        let (_,_,metasenv,_,_) = status#obj in
+        let conj = NCicUtils.lookup_meta goal metasenv in
+        let name = name_of_conj conj in
+*)
+        let continuation =
+          let rec aux l =
+            match l with
+              [] -> [id_tac]
+            | (id,ty)::tl ->
+              (try_tac (assume id ("",0,ty))) :: (aux tl)
+          in
+          aux l
         in
-         (*CSC: manca check plhs convertibile con lhs *)
-         plhs,prhs,
-          (fun continuation ->
-            ProofEngineTypes.apply_tactic continuation status)
-     | Some (Some name,lhs) ->
-        let newmeta = CicMkImplicit.new_meta metasenv [] in
-        let irl =
-         CicMkImplicit.identity_relocation_list_for_metavariable context in
-        let plhs = lhs in
-        let prhs = Cic.Meta(newmeta,irl) in
-         plhs,prhs,
-          (fun continuation ->
-            let metasenv = (newmeta, context, ty)::metasenv in
-            let mk_fresh_name_callback =
-             fun metasenv context _ ~typ ->
-	      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
-               (Cic.Name name) ~typ
-	    in
-            let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
-            let proof,goals =
-             ProofEngineTypes.apply_tactic
-              (Tacticals.thens
-                ~start:(Tactics.cut ~mk_fresh_name_callback
-                 (Cic.Appl [eq ; ty ; lhs ; prhs]))
-                ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
-            in
-             let goals =
-              match just,goals with
-                 `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
-               | _, [g1;g2] -> [g2;newmeta;g1]
-               | _, l -> 
-                 prerr_endline (String.concat "," (List.map string_of_int l));
-                 prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
-                 assert false
-             in
-              proof,goals)
-   in
-    let continuation =
-     if last_step then
-      (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
-      just'
-     else
-      Tacticals.thens
-       ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
-       ~continuations:[just' ; Tacticals.id_tac]
-    in
-     prepare continuation
- in
-  ProofEngineTypes.mk_tactic aux
+(*         if name = id then block_tac continuation status *)
+(*         else  *)
+          block_tac ([focus_on_case_tac id] @ continuation) status
+      )
+  )
 ;;
-  *)
+
+let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
+
+(* vim: ts=2: sw=0: et:
+ * *)