]> matita.cs.unibo.it Git - helm.git/commitdiff
Added Decompose tactic
authorMichele Galatà <??>
Fri, 24 Jan 2003 11:15:57 +0000 (11:15 +0000)
committerMichele Galatà <??>
Fri, 24 Jan 2003 11:15:57 +0000 (11:15 +0000)
helm/gTopLevel/eliminationTactics.ml
helm/gTopLevel/eliminationTactics.mli
helm/gTopLevel/equalityTactics.ml
helm/gTopLevel/esempi/decompose.cic [new file with mode: 0644]
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/introductionTactics.ml
helm/gTopLevel/negationTactics.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/proofEngine.mli
helm/gTopLevel/tacticals.ml
helm/gTopLevel/variousTactics.ml

index d2ed7481023158d4a9b6586e27c6a1f794c9bda2..fc6906cbc9c9662e655c3ba324b008747ed47949 100644 (file)
@@ -30,38 +30,20 @@ let induction_tac ~term ~status:((proof,goal) as status) =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
   let module S = ProofEngineStructuralRules in
-  let module U = UriManager in
+  let module U = UriManager in 
    let (_,metasenv,_,_) = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-     let termty = T.type_of_aux' metasenv context term in
-     let uri,exp_named_subst,typeno,args =
-      match termty with
-         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
-       | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args)
-       | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate")
-     in
-      let eliminator_uri =
-       let base = U.buri_of_uri uri in
-       let name =
-        match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (tys,_,_) ->
-            let (name,_,_,_) = List.nth tys typeno in
-             name
-         | _ -> assert false
-       in
-       let ext =
-        match T.type_of_aux' metasenv context ty with
-           C.Sort C.Prop -> "_ind"
-         | C.Sort C.Set  -> "_rec"
-         | C.Sort C.Type -> "_rect"
-         | _ -> assert false
-       in
-        U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con")
-      in 
-       apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst))    (* come mi devo comportare con gli args??? *)
+     let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
+
+     T.then_ ~start:(T.repeat_tactic 
+                       ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *)
+                       ~continuation:(P.intros))
+             ~continuation:(P.elim_intros_simpl ~term)
+             ~status
 ;;
 *)
 
+
 let elim_type_tac ~term ~status =
   let module C = Cic in
   let module P = PrimitiveTactics in
@@ -80,111 +62,159 @@ let elim_type_tac ~term ~status =
 *)
 
 
-(* PROVE DI DECOMPOSE
+(* PROVE DI DECOMPOSE *)
+(* guardare quali sono i tipi induttivi decomponibili presenti in
+profondita' nel term; chiamare una funzione di call-back passando questa
+lista e ritornando la lista di termini che l'utente vuole decomporre;
+decomporre. *)
 
-(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
-let decompose_tac ~what ~where ~status:((proof,goal) as status) =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-  let module S = ProofEngineStructuralRules in
 
-   let rec decomposing ty what =
-    match (what) with
-       [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
-     | hd::tl as what ->
-        match ty with
-           (C.Appl (hd::_)) -> hd
-         | _ -> decomposing ty tl
-    in
+exception InteractiveUserUriChoiceNotRegistered
 
-   let (_,metasenv,_,_) = proof in
-    let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
-     T.repeat_tactic
-       ~tactic:(T.then_
-                   ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
-                   ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where))))                (* ma che ipotesi sto cancellando??? *)
-               )
-       ~status
+let interactive_user_uri_choice =
+ (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) :
+  (selection_mode:[`SINGLE | `EXTENDED] ->
+      ?ok:string ->
+      ?enable_button_for_non_vars:bool ->
+      title:string -> msg:string -> string list -> string list) ref)
+;;
+
+exception IllFormedUri of string
+
+let cic_textual_parser_uri_of_string uri' =
+ try
+  (* Constant *)
+  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+  else
+   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+   else
+    (try
+      (* Inductive Type *)
+      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+       CicTextualParser0.IndTyUri (uri'',typeno)
+     with
+      _ ->
+       (* Constructor of an Inductive Type *)
+       let uri'',typeno,consno =
+        CicTextualLexer.indconuri_of_uri uri'
+       in
+        CicTextualParser0.IndConUri (uri'',typeno,consno)
+    )
+ with
+  _ -> raise (IllFormedUri uri')
+;;
+
+let constructor_uri_of_string uri = 
+  match cic_textual_parser_uri_of_string uri with
+     CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
+   | _ -> assert false
+;;
+
+let call_back uris = 
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+  let module U = UriManager in 
+   List.map 
+    (constructor_uri_of_string)
+    (!interactive_user_uri_choice 
+      ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
+      ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
+      (List.map 
+        (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)) 
+        uris)
+    ) 
 ;;
 
 
-let decompose_tac ~clist ~status:((proof,goal) as status) =
+let decompose_tac ~term ~status:((proof,goal) as status) =
   let module C = Cic in
   let module R = CicReduction in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
   let module S = ProofEngineStructuralRules in
-   let (_,metasenv,_,_) = proof in
+   let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-     let rec repeat_elim ~term ~status =                (* term -> status -> proof * (goal list) *)
-      try
-       let (proof, goallist) =
-        T.then_
-           ~start:(P.elim_simpl_intros_tac ~term)
-           ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty))))                (* non so che ipotesi sto cancellando??? *)
-           ~status
+     let old_context_len = List.length context in
+(*     let nr_of_hyp_still_to_elim = ref 1 in *)
+     let termty = CicTypeChecker.type_of_aux' metasenv context term in
+
+      let rec make_list termty = 
+(* altamente inefficente? *)
+       let rec search_inductive_types urilist termty =
+        (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
+        match termty with
+           (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> 
+               (uri,typeno,exp_named_subst)::urilist
+         | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> 
+               (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist)
+         | _ -> urilist
+         (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *)
+       in 
+       let rec purge_duplicates urilist = 
+        let rec aux triple urilist =
+         match urilist with 
+            [] -> []
+          | hd::tl -> 
+             if (hd = triple) 
+              then aux triple tl
+              else hd::(aux triple tl)
         in
-         let rec step proof goallist =
-          match goallist with
-             [] -> (proof, [])
-           | hd::tl ->
-              let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
-               let (proof'', goallist'') = step proof' tl in
-                proof'', goallist'@goallist''
-          in
-           step proof goallist
-       with
-        (Fail _) -> T.id_tac
-
-    in
-                                                                  let rec decomposing ty clist =             (* term -> (term list) -> bool *)
-      match (clist) with
-        [] -> false
-      | hd::tl as clist ->
-         match ty with
-           (C.Appl (hd::_)) -> true
-         | _ -> decomposing ty tl
-
+        match urilist with
+           [] -> []
+         | hd::tl -> hd::(purge_duplicates (aux hd tl))
+       in
+        purge_duplicates (search_inductive_types [] termty) 
       in
-       let term = decomposing (R.whd context ty) clist in
-        if (term == C.Implicit)
-         then (Fail "Decompose: nothing to decompose or no application")
-         else repeat_elim ~term ~status
-;;
-*)
 
-let decompose_tac ~clist ~status =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-  let module S = ProofEngineStructuralRules in
+       let urilist =  
+          (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *)
+          (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *)
+         call_back (make_list termty) in
+
+        let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) =
+prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
+         if nr_of_hyp_still_to_elim <> 0 then
+          let _,metasenv,_,_ = proof in
+           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+            let old_context_len = List.length context in
+            let termty = CicTypeChecker.type_of_aux' metasenv context term' in
+prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty);
+             match termty with
+                C.MutInd (uri,typeno,exp_named_subst)
+              | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) 
+                 when (List.mem (uri,typeno,exp_named_subst) urilist) ->
+prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty);
+                   T.then_ 
+                      ~start:(P.elim_intros_simpl_tac ~term:term')
+                      ~continuation:(
+                        (* clear the hyp that has just been eliminated *)
+                        (fun ~status:((proof,goal) as status) -> 
+                          let _,metasenv,_,_ = proof in
+                           let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+                            let new_context_len = List.length context in   
+prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
+                             let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
+                             T.then_ 
+                                ~start:(
+                                  if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *) 
+                                   then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
+                                   else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
+                                ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)
+                                ~status
+                        ))
+                      ~status
+              | _ ->
+                   let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in 
+prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
+                    elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status
+         else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status
 
-   let rec choose ty =
-    function
-       [] -> C.Implicit (* a cosa serve? *)
-     | hd::tl ->
-        match ty with
-           (C.Appl (hd::_)) -> hd
-         | _ -> choose ty tl
-     in
-
-    let decompose_one_tac ~clist ~status:((proof,goal) as status) =
-     let (_,metasenv,_,_) = proof in
-      let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-       let term = choose (R.whd context ty) clist in
-        if (term == C.Implicit)
-         then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
-         else T.then_
-                 ~start:(P.elim_intros_simpl_tac ~term)
-                 ~continuation:(S.clear ~hyp:(List.hd context))
-(*                             (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty))))                (* ma che ipotesi sto cancellando??? *)*)
-                 ~status
-     in
-      T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
+        in
+(*         T.repeat_tactic ~tactic: *)
+              (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1)
+            ~status
 ;;
 
 
+
index 00ccedd64efe99bbed7a4e4389ca43c8973675b5..a49c771585dee99989e0a910f64869c18b742d28 100644 (file)
@@ -25,4 +25,9 @@
 
 val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
 
-val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic
+val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] ->
+      ?ok:string ->
+      ?enable_button_for_non_vars:bool ->
+      title:string -> msg:string -> string list -> string list) ref
+
+val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic
index afa210119fe9ce50304b53b90a2820d800290e7c..79b5b1dbe499e50a6b2d26788a023bcf30081554 100644 (file)
@@ -182,6 +182,8 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
 ;;
 
 
+(* All these tacs do is applying the right constructor/theorem *)
+
 let reflexivity_tac =
   IntroductionTactics.constructor_tac ~n:1
 ;;
diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
new file mode 100644 (file)
index 0000000..f03d410
--- /dev/null
@@ -0,0 +1,5 @@
+!A:Prop.!B:Prop.!C:Prop.(and (or A C) (and (or A B) (or B C))) -> True
+
+!A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
+
+!A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True
index ebe26c3e350a915089f1dbe229547d1620bdee0d..f590481baf7ed79d7a9acd70a807bd3467c7958e 100644 (file)
@@ -352,6 +352,9 @@ let
    raise NoChoice
 ;;
 
+EliminationTactics.interactive_user_uri_choice :=
+ (fun ~selection_mode -> interactive_user_uri_choice ~selection_mode:selection_mode);;
+
 let interactive_interpretation_choice interpretations =
  let chosen = ref None in
  let window =
@@ -2148,9 +2151,7 @@ let assumption = call_tactic ProofEngine.assumption;;
 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
-(* Galla chiede: come dare alla tattica la lista di termini da decomporre?
-let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
-*)
+let decompose = call_tactic_with_input ProofEngine.decompose;;
 
 let whd_in_scratch scratch_window =
  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
@@ -3083,6 +3084,9 @@ object(self)
    let searchpatternb =
     GButton.button ~label:"SearchPattern_Apply"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let decomposeb =
+    GButton.button ~label:"Decompose"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 
    ignore(exactb#connect#clicked exact) ;
    ignore(applyb#connect#clicked apply) ;
@@ -3118,6 +3122,7 @@ object(self)
    ignore(introsb#connect#clicked intros) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+   ignore(decomposeb#connect#clicked decompose) ;
   ))
 end
 ;;
index bd29f4f5a147ed59f7f33472725f2ea03aa929e6..bc28c41709c92719a143d40506a9db6860a2f8e5 100644 (file)
@@ -34,7 +34,7 @@ let constructor_tac ~n ~status:(proof, goal) =
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
          PrimitiveTactics.apply_tac ~status:(proof, goal)
           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-      | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
+      | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
 ;;
 
 
index d55f04556cb249cfb52d89f76f779c837e006522..2b87bb911d7ebc28160cb147318ea9e72b6839c9 100644 (file)
@@ -30,7 +30,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) =
   let module P = PrimitiveTactics in
    let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-     if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
+     if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
       then P.apply_tac 
               ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
@@ -42,7 +42,8 @@ let contradiction_tac ~status =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-   T.then_
+   try
+    T.then_
       ~start: P.intros_tac
       ~continuation:(
         T.then_
@@ -50,6 +51,9 @@ let contradiction_tac ~status =
                      ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
            ~continuation: VariousTactics.assumption_tac)
     ~status
+   with 
+    (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption")
+    (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
 ;;
 
 (* Questa era in fourierR.ml
index 7d637551fdc693fef96b6ce9f2b4d3b7e7e02071..379007021595618f5edaec3142fe9638918aed9c 100644 (file)
@@ -231,7 +231,7 @@ let generalize term = apply_tactic (VariousTactics.generalize_tac ~term)
 let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
 let contradiction () = apply_tactic NegationTactics.contradiction_tac
 
-let decompose ~clist = apply_tactic (EliminationTactics.decompose_tac ~clist)
+let decompose term = apply_tactic (EliminationTactics.decompose_tac ~term)
 
 (*
 let decide_equality () = apply_tactic VariousTactics.decide_equality_tac
index ab1b0285e978ce81cd2e762f0dea22562c7c189e..0263fd1e7c31e8e07fb5bc23335905fb051ba1cd 100644 (file)
@@ -81,7 +81,7 @@ val generalize : Cic.term -> unit
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit
 
-val decompose : clist:(Cic.term list) -> unit
+val decompose : Cic.term -> unit
 
 (*
 val decide_equality : unit -> unit
index d48b6a02c28dc5e2ca60876aeaa26a93f288c351..1319c13ca2dc34fa1e20299f0be540fab22c6df0 100644 (file)
@@ -103,7 +103,8 @@ let then_ ~start ~continuation ~status =
 
 
 (* Galla *)
-(* si suppone che tutte le tattiche sollevano solamente Fail? *)
+(* si suppone che tutte le tattiche sollevino solamente Fail? *)
+
 
 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
 
@@ -201,6 +202,10 @@ let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
 
 
 
+
+
+
+
   (** tattica di prova per debuggare i tatticali *)
 (*
 let thens' ~start ~continuations ~status =
index 604307cd35cb662b16631efb40cc16044b3d7a00..1df9128c168ca1fad6e9213be480e0c45e78a7d7 100644 (file)
  *)
 
 
-(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
+(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
+chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
+funzione di callback che restituisce la (sola) hyp da applicare *)
+
 let assumption_tac ~status:((proof,goal) as status) =
   let module C = Cic in
   let module R = CicReduction in
@@ -67,13 +70,56 @@ let assumption_tac ~status:(proof,goal)=
 
 (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
-contesto e si lifta *)
+contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
+
 let generalize_tac ~term ~status:((proof,goal) as status) =
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+(*
+     let found = false in
+     let rec new_context context ty = 
+      if ty == term then let found = true in context
+       else match ty with
+             C.Rel _
+           | C.Var _ 
+           | C.Meta _ (* ???? *)
+           | C.Sort s 
+           | C.Implicit -> context                   
+           | C.Cast (val,typ) -> 
+              let tmp_context = new_context context val in 
+               tmp_context @ (new_context tmp_context typ)
+           | C.Prod (binder, source, target) -> 
+           | C.Lambda (binder, source, target) -> 
+              let tmp_context = new_context context source in 
+               tmp_context @ (new_context tmp_context binder)
+           | C.LetIn (binder, term, target) ->
+           | C.Appl applist -> 
+              let rec aux context = 
+               match applist with 
+                  [] -> context
+                | hd::tl -> 
+                   let tmp_context = (new_context context hd)
+                   in aux tmp_context tl 
+              in aux context applist
+           | C.Const (uri, exp_named_subst)
+           | C.MutInd (uri, typeno, exp_named_subst)
+           | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> 
+              match exp_named_subst with
+                 [] -> context
+               | (uri,t)::_ -> new_context context (type_of_aux' context t)
+               | _ -> assert false
+           | C.MutCase (uri, typeno, outtype, iterm, patterns) 
+           | C.Fix (funno, funlist) 
+           | C.CoFix (funno, funlist) ->
+              match funlist with
+                 [] -> context (* caso possibile? *)
+               | (name, index, type, body)::_ -> 
+                  let tmp_context = ~
+     in
+*)
      T.thens 
       ~start:(P.cut_tac 
        ~term:(
@@ -94,24 +140,67 @@ let generalize_tac ~term ~status:((proof,goal) as status) =
 (* IN FASE DI IMPLEMENTAZIONE *)
 
 let decide_equality_tac =
+(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza
+e' vera o no e lo risolve *)
   Tacticals.id_tac
 ;;
 
-(*
-let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
+
+let compare_tac ~term ~status:((proof, goal) as status) =
+(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to          *)
+(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2  *)
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
     let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
-     if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
-       (* controllo che i due termini siano comparabili *)
-      then
-       T.thens 
-         ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
-         ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]  
-      else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types") 
+     let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
+      match termty with
+         (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
+          
+          let term' = (* (t1=t2)\/~(t1=t2) *)
+           C.Appl [
+            (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; 
+            term ; 
+            C.Appl [
+             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; 
+             t1 ; 
+             C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
+            ]
+           ] 
+          in
+            T.thens 
+               ~start:(P.cut_tac ~term:term')
+               ~continuations:[
+                 T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
+                 decide_equality_tac]  
+      | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
+          let term' = (* (t1=t2) \/ ~(t1=t2) *)
+           C.Appl [
+            (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; 
+            term ; 
+            C.Appl [
+             (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; 
+             t1 ; 
+             C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2]
+            ]
+           ] 
+          in
+            T.thens 
+               ~start:(P.cut_tac ~term:term')
+               ~continuations:[
+                 T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; 
+                 decide_equality_tac]  
+      | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") 
+;;
+
+
+let discriminate_tac ~term ~status:((proof, goal) as status) =
+  let module C = Cic in
+  let module U = UriManager in
+  let module P = PrimitiveTactics in
+  let module T = Tacticals in
+   T.id_tac 
 ;;
-*)