Asts generalized: a lot of tactics where restricted to identifiers in place

of patterns or terms.

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 669d7b62f182adf55dbc4d9c7f753d66b725a58a..522a5157053161e990ebdef8172cef7070e2b5a7 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -77,11 +77,11 @@ let tactic_of_ast = function
         EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
       else
         EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
-  | TacticAst.FwdSimpl (_, name) -> 
-     Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ())
-  | TacticAst.LApply (_, term, substs) ->
+  | TacticAst.FwdSimpl (_, term) -> 
+     Tactics.fwd_simpl ~term ~dbd:(MatitaDb.instance ())
+  | TacticAst.LApply (_, term) ->
      let f (name, term) = Cic.Name name, term in
-     Tactics.lapply ~substs:(List.map f substs) term
+     Tactics.lapply term
 
 let eval_tactical status tac =
   let apply_tactic tactic =
@@ -404,10 +404,11 @@ let disambiguate_tactic status = function
       let status, cic1 = disambiguate_term status what in
       let status, cic2 = disambiguate_term status with_what in
       status, TacticAst.Replace (loc, cic1, cic2)
-  | TacticAst.Change (loc, what, with_what, ident) -> 
+  | TacticAst.Change (loc, what, with_what, pattern) -> 
       let status, cic1 = disambiguate_term status what in
       let status, cic2 = disambiguate_term status with_what in
-      status, TacticAst.Change (loc, cic1, cic2, ident)
+      let pattern = disambiguate_pattern status.aliases pattern in
+      status, TacticAst.Change (loc, cic1, cic2, pattern)
   | TacticAst.Generalize (loc,term,pattern) ->
       let status,term = disambiguate_term status term in
       let pattern = disambiguate_pattern status.aliases pattern in
@@ -448,15 +449,12 @@ let disambiguate_tactic status = function
   | TacticAst.Split loc -> status, TacticAst.Split loc
   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
-  | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name)  
-  | TacticAst.LApply (loc, term, substs) ->
-     let f (status, substs) (name, term) =
-        let status, term = disambiguate_term status term in
-       status, (name, term) :: substs
-     in
+  | TacticAst.FwdSimpl (loc, term) ->
+     let status, term = disambiguate_term status term in
+     status, TacticAst.FwdSimpl (loc, term)  
+  | TacticAst.LApply (loc, term) ->
      let status, term = disambiguate_term status term in
-     let status, substs = List.fold_left f (status, []) substs in 
-     status, TacticAst.LApply (loc, term, substs)
+     status, TacticAst.LApply (loc, term)
 
 let rec disambiguate_tactical status = function 
   | TacticAst.Tactic (loc, tactic) -> 

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 737673e143f45949ebec70a2cbb23ac434662ce9..e54185a1b2fd9e368673caa9f923c30c12bbfe4a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -312,16 +312,10 @@ EXTEND
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
-  tactic_where: [
-    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
-  ];
   tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
-  ident_list1: [
-    [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
-  ];
   reduction_kind: [
     [ [ IDENT "reduce" ] -> `Reduce
     | [ IDENT "simplify" ] -> `Simpl
@@ -355,8 +349,7 @@ EXTEND
     | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> 
           TacticAst.Auto (loc,num)
     | [ IDENT "change" ];
-      t1 = tactic_term; "with"; t2 = tactic_term;
-      where = tactic_where ->
+      t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec ->
         TacticAst.Change (loc, t1, t2, where)
     (* TODO Change_pattern *)
     | [ IDENT "contradiction" ] ->
@@ -364,9 +357,8 @@ EXTEND
     | [ IDENT "cut" ];
       t = tactic_term ->
         TacticAst.Cut (loc, t)
-    | [ IDENT "decompose" ];
-      principles = ident_list1; where = IDENT ->
-        TacticAst.Decompose (loc, where, principles)
+    | [ IDENT "decompose" ]; where = term ->
+        TacticAst.Decompose (loc, where)
     | [ IDENT "discriminate" ];
       t = tactic_term ->
         TacticAst.Discriminate (loc, t)
@@ -386,8 +378,8 @@ EXTEND
     | [ IDENT "fourier" ] ->
         TacticAst.Fourier loc
     | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
-    | [ IDENT "injection" ]; ident = IDENT ->
-        TacticAst.Injection (loc, ident)
+    | [ IDENT "injection" ]; t = term ->
+        TacticAst.Injection (loc, t)
     | [ IDENT "intros" ];
       num = OPT [ num = int -> num ];
       idents = OPT ident_list0 ->
@@ -423,10 +415,10 @@ EXTEND
     | [ IDENT "transitivity" ];
       t = tactic_term ->
         TacticAst.Transitivity (loc, t)
-    | [ IDENT "fwd" ]; name = IDENT ->
-        TacticAst.FwdSimpl (loc, name)
+    | [ IDENT "fwd" ]; t = term ->
+        TacticAst.FwdSimpl (loc, t)
     | [ IDENT "lapply" ]; t = term ->
-        TacticAst.LApply (loc, t, [])
+        TacticAst.LApply (loc, t)
     ]
   ];
   tactical:

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 12b7774cd32938f9141e9e332f6e315d155d2f13..269ba553a22467ae74bec15eda5229154ce71e87 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -36,10 +36,10 @@ type ('term, 'ident) tactic =
   | Apply of loc * 'term
   | Auto of loc * int option
   | Assumption of loc
-  | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
+  | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *)
   | Contradiction of loc
   | Cut of loc * 'term
-  | Decompose of loc * 'ident * 'ident list (* where, which principles *)
+  | Decompose of loc * 'term
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
   | ElimType of loc * 'term
@@ -49,7 +49,7 @@ type ('term, 'ident) tactic =
   | Fourier of loc
   | Generalize of loc * 'term * ('term, 'ident) pattern
   | Goal of loc * int (* change current goal, argument is goal number 1-based *)
-  | Injection of loc * 'ident
+  | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
   | Left of loc
   | LetIn of loc * 'term * 'ident
@@ -62,8 +62,8 @@ type ('term, 'ident) tactic =
   | Split of loc
   | Symmetry of loc
   | Transitivity of loc * 'term
-  | FwdSimpl of loc * 'ident
-  | LApply of loc * 'term * ('ident * 'term) list
+  | FwdSimpl of loc * 'term
+  | LApply of loc * 'term
 
 type thm_flavour =
   [ `Definition

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index f43091c755a012cd059cfd64d52c289151013e06..1c6723186ca6e1aeb70606e15dbcbb3487559b91 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -44,18 +44,18 @@ let rec count_tactic current_size tac =
     | Auto _ -> current_size + 4
     | Assumption _ -> current_size + 10
     | Change (_, t1, t2, where) ->
+(*
        let size1 = countterm (current_size + 12) t1 in (* change, with *)
        let size2 = countterm size1 t2 in
         (match where with 
             None -> size2
           | Some ident -> size2 + 3 + String.length ident)
+*) assert false
 (*     | Change_pattern _ -> assert false  (* TODO *) *)
     | Contradiction _ -> current_size + 13
     | Cut (_, term) -> countterm (current_size + 4) term
-    | Decompose (_, ident, principles) ->
-       List.fold_left
-         (fun size s -> size + (String.length s))
-         (current_size + 11 + String.length ident) principles
+    | Decompose (_, term) ->
+       countterm (current_size + 11) term
     | Discriminate (_, term) -> countterm (current_size + 12) term
     | Elim (_, term, using) ->
        let size1 = countterm (current_size + 5) term in
@@ -70,7 +70,8 @@ let rec count_tactic current_size tac =
     | Fourier _ -> current_size + 7
     | Generalize (_,term,pattern) -> assert false (* TODO *)
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
-    | Injection (_, ident) -> current_size + 10 + (String.length ident)
+    | Injection (_, term) ->
+       countterm (current_size + 10) term
     | Intros (_, num, idents) ->
        List.fold_left 
          (fun size s -> size + (String.length s))
@@ -137,6 +138,7 @@ and big_tactic2box = function
   | Assumption _ -> Box.Text([],"assumption")
   | Auto _ -> Box.Text([],"auto")
   | Change (_, t1, t2, where) ->
+(*
       let where =
        (match where with 
             None -> []
@@ -151,19 +153,15 @@ and big_tactic2box = function
              (pretty_append 
                 [Box.Text([],"with")]
                 t2)@where)
+*) assert false
 (*   | Change_pattern _ -> assert false  (* TODO *) *)
   | Contradiction _ -> Box.Text([],"contradiction")
   | Cut (_, term) -> 
       Box.V([],[Box.Text([],"cut");
                Box.indent(ast2astBox term)])
-  | Decompose (_, ident, principles) ->
-      let principles =
-       List.map (fun x -> Box.Text([],x)) principles in
+  | Decompose (_, term) ->
       Box.V([],[Box.Text([],"decompose");
-               Box.H([],[Box.Text([],"[");
-                         Box.V([],principles);
-                         Box.Text([],"]")]);
-               Box.Text([],ident)])
+               Box.indent(ast2astBox term)])
   | Discriminate (_, term) -> 
       Box.V([],pretty_append [Box.Text([],"discriminate")] term)
   | Elim (_, term, using) ->
@@ -193,9 +191,7 @@ and big_tactic2box = function
   | Fourier _ -> Box.Text([],"fourier")
   | Generalize _ -> assert false  (* TODO *)
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
-  | Injection (_, ident) -> 
-      Box.V([],[Box.Text([],"transitivity");
-               Box.indent (Box.Text([],ident))])
+  | Injection (_, term) -> assert false (* TODO *)
   | Intros (_, num, idents) ->
       let num =
        (match num with 

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 52f7b1ab20099709575e37bcbd18eb61f2b96116..263382ef10cfbd2b9aa9c3c3cc885b1092cede61 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -57,7 +57,8 @@ let pp_pattern (hyp, goal) =
   let separator = 
     if hyp <> [] then " \vdash " else " "
   in
-  pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal
+   "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal
+
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term
   | Apply (_, term) -> "apply " ^ pp_term_ast term
@@ -65,12 +66,12 @@ let rec pp_tactic = function
   | Assumption _ -> "assumption"
   | Change (_, t1, t2, where) ->
       sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2)
-        (match where with None -> "" | Some ident -> "in " ^ ident)
+       (pp_pattern where)
 (*   | Change_pattern (_, _, _, _) -> assert false  (* TODO *) *)
   | Contradiction _ -> "contradiction"
   | Cut (_, term) -> "cut " ^ pp_term_ast term
-  | Decompose (_, ident, principles) ->
-      sprintf "decompose %s %s" (pp_idents principles) ident
+  | Decompose (_, term) ->
+      sprintf "decompose %s" (pp_term_ast term)
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
   | Elim (_, term, using) ->
       sprintf "elim " ^ pp_term_ast term ^
@@ -84,7 +85,7 @@ let rec pp_tactic = function
      sprintf "generalize %s %s" (pp_term_ast term) (pp_pattern pattern)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
-  | Injection (_, ident) -> "injection " ^ ident
+  | Injection (_, term) -> "injection " ^ pp_term_ast term
   | Intros (_, None, []) -> "intro"
   | Intros (_, num, idents) ->
       sprintf "intros%s%s"
@@ -103,13 +104,13 @@ let rec pp_tactic = function
 (*       sprintf "%s in hyp %s" (pp_reduction_kind kind) *)
 (*         (String.concat ", " (List.map pp_term_ast terms)) *)
   | Reduce (_, kind, pat) ->
-      sprintf "%s in %s" (pp_reduction_kind kind) (pp_pattern pat)
+      sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat)
   | Reflexivity _ -> "reflexivity"
   | Replace (_, t1, t2) ->
       sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
 (*   | Replace_pattern (_, _, _) -> assert false  (* TODO *) *)
   | Rewrite (_, pos, t, pattern) -> 
-      sprintf "rewrite %s %s in %s" 
+      sprintf "rewrite %s %s %s" 
         (if pos = `Left then "left" else "right") (pp_term_ast t)
         (pp_pattern pattern)
   | Right _ -> "right"
@@ -117,7 +118,7 @@ let rec pp_tactic = function
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
-  | FwdSimpl (_, ident) -> sprintf "fwd %s" ident
+  | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term)
 
 let pp_flavour = function
   | `Definition -> "Definition"

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 7981ac8753727962ad64f8443c13385a642b6e77..98125f5e738d447986bdb88f74aed4825ef646e6 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -30,24 +30,13 @@ module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
 
-(*
-let module R = CicReduction
-*)
-
-let fail_msg0 = "not a declaration of the current context"
 let fail_msg1 = "no applicable simplification"
 
 let error msg = raise (PET.Fail msg)
 
-let rec declaration name = function 
-   | []                                           -> error fail_msg0
-   | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty
-   | _ :: tail                                    -> declaration name tail 
-
 (* lapply *******************************************************************)
 
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-               ?(substs = []) what =
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) what =
    let rec strip_dependent_prods metasenv context ss = function
       | Cic.Prod (name, t1, t2) as t -> 
         if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else 
@@ -74,12 +63,14 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
 
 (* fwd **********************************************************************)
 
-let fwd_simpl_tac ~hyp ~dbd =
+let fwd_simpl_tac ~term ~dbd =
    let fwd_simpl_tac status =
       let (proof, goal) = status in
       let _,metasenv,_,_ = proof in
       let _,context,ty = CicUtil.lookup_meta goal metasenv in
-      let major = declaration hyp context in 
+      let major,_ =
+       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+      in 
       match  MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg1
          | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])  

diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli
index 0b065f92096f8818377395bef5e22fc843c0ae82..705569fdca06a06dd93055714faa8dcf29317395 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.mli
+++ b/helm/ocaml/tactics/fwdSimplTactic.mli
@@ -25,8 +25,7 @@
 
 val lapply_tac:
    ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-   ?substs:(Cic.name * Cic.term) list -> Cic.term -> 
-   ProofEngineTypes.tactic
+   Cic.term -> ProofEngineTypes.tactic
 
 val fwd_simpl_tac:
-   hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+   term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index b656fe58cc6af392219b12843d3f42c4cd6d6670..cddc6d3b2bc7bacc761de5cf6e1993941979d11c 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -23,8 +23,8 @@ val decompose :
                          list) ->
   Cic.term -> ProofEngineTypes.tactic
 val discriminate : term:Cic.term -> ProofEngineTypes.tactic
-val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros : term:Cic.term -> ProofEngineTypes.tactic
+val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
 val elim_type : term:Cic.term -> ProofEngineTypes.tactic
 val exact : term:Cic.term -> ProofEngineTypes.tactic
 val exists : ProofEngineTypes.tactic
@@ -32,29 +32,33 @@ val fold :
   reduction:(Cic.context -> Cic.term -> Cic.term) ->
   also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic
 val fourier : ProofEngineTypes.tactic
+val fwd_simpl : term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   unit -> ProofEngineTypes.tactic
+val lapply :
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  Cic.term -> ProofEngineTypes.tactic
 val left : ProofEngineTypes.tactic
 val letin :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic
+val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val reflexivity : ProofEngineTypes.tactic
 val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back :
+val rewrite :
   ?where:ProofEngineTypes.pattern ->
   term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl :
+val rewrite_back :
   ?where:ProofEngineTypes.pattern ->
   term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite :
+val rewrite_back_simpl :
   ?where:ProofEngineTypes.pattern ->
   term:Cic.term -> unit -> ProofEngineTypes.tactic
 val rewrite_simpl :
@@ -62,13 +66,9 @@ val rewrite_simpl :
   term:Cic.term -> unit -> ProofEngineTypes.tactic
 val right : ProofEngineTypes.tactic
 val ring : ProofEngineTypes.tactic
+val set_goal : int -> ProofEngineTypes.tactic
 val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val split : ProofEngineTypes.tactic
 val symmetry : ProofEngineTypes.tactic
 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
-val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
-val lapply :
-  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic