]> matita.cs.unibo.it Git - helm.git/commitdiff
PrimitiveTactics: intros _ now aveilable
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 9 May 2007 19:36:00 +0000 (19:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 9 May 2007 19:36:00 +0000 (19:36 +0000)
GrafiteAst      : some refactoring

16 files changed:
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralConversion.ml
helm/software/components/acic_procedural/proceduralConversion.mli
helm/software/components/acic_procedural/proceduralOptimizer.ml
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/tactics.mli
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/matita/matitaGui.ml

index ff8aaea883c2541af693c5b19057e5ecb07074b7..95c4c1a9a7825182daf0dcab6313c2eef0d707b9 100644 (file)
@@ -38,6 +38,7 @@ module E    = CicEnvironment
 module Pp   = CicPp
 module PEH  = ProofEngineHelpers
 module HEL  = HExtlib
+module DTI  = DoubleTypeInference
 
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
@@ -50,7 +51,9 @@ type status = {
    max_depth: int option;
    depth: int;
    context: C.context;
-   intros: string list;
+   intros: string option list;
+   clears: string list;
+   clears_note: string;
    case: int list
 }
 
@@ -175,8 +178,6 @@ with Invalid_argument _ -> failwith "A2P.get_ind_names"
 
 (* proof construction *******************************************************)
 
-let unused_premise = "UNUSED"
-
 let mk_exp_args hd tl classes synth =
    let meta id = C.AImplicit (id, None) in
    let map v (cl, b) =
@@ -207,17 +208,23 @@ let convert st ?name v =
                     if Ut.alpha_equivalence csty w then [] 
                     else 
                     [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w);
-                    T.Change (sty, ety, Some (id, id), e, "")] 
+                    T.Change (sty, ety, Some (id, Some id), e, "")] 
               end
 
 let get_intro = function 
-   | C.Anonymous -> unused_premise
-   | C.Name s    -> s
+   | C.Anonymous -> None
+   | C.Name s    -> Some s
 
 let mk_intros st script =
-   if st.intros = [] then script else
-   let count = List.length st.intros in
-   T.Intros (Some count, List.rev st.intros, "") :: script
+   let intros st script =
+      if st.intros = [] then script else
+      let count = List.length st.intros in
+      T.Intros (Some count, List.rev st.intros, "") :: script
+   in
+   let clears st script =
+      if st.clears = [] then script else T.Clear (st.clears, st.clears_note) :: script
+   in
+   intros st (clears st script)   
 
 let mk_arg st = function
    | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
@@ -231,7 +238,8 @@ let mk_fwd_rewrite st dtext name tl direction =
       | C.ARel (_, _, _, premise) ->
          let script = mk_arg st what in
          let where = Some (premise, name) in
-        T.Rewrite (direction, what, where, e, dtext) :: script
+        let st = {st with context = Cn.clear st.context premise} in 
+        st, T.Rewrite (direction, what, where, e, dtext) :: script
       | _                         -> assert false
 
 let mk_rewrite st dtext what qs tl direction = 
@@ -241,6 +249,13 @@ let mk_rewrite st dtext what qs tl direction =
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
+   let dno = DTI.does_not_occur 1 (cic t) in
+   let dno = dno && match get_inner_types st v with
+      | None          -> true
+      | Some (it, et) -> 
+         DTI.does_not_occur 1 (cic it) && DTI.does_not_occur 1 (cic et)
+   in
+   let name = if dno then C.Anonymous else name in  
    let entry = Some (name, C.Decl (cic v)) in
    let intro = get_intro name in
    proc_proof (add st entry intro) t
@@ -249,20 +264,20 @@ and proc_letin st what name v t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
-      let hyp, rqv = match get_inner_types st v with
+      let st, hyp, rqv = match get_inner_types st v with
          | Some (ity, _) ->
-           let rqv = match v with
+           let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
                  mk_fwd_rewrite st dtext intro tl true
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
                  mk_fwd_rewrite st dtext intro tl false
               | v                                                     ->
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+                 st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
-           C.Decl (cic ity), rqv
+           st, C.Decl (cic ity), rqv
         | None          ->
-           C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
+           st, C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -333,13 +348,23 @@ and proc_other st what =
    let script = [T.Note text] in
    mk_intros st script
 
-and proc_proof st = function
-   | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
-   | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t
-   | C.ARel _ as what                 -> proc_rel st what
-   | C.AMutConstruct _ as what        -> proc_mutconstruct st what
-   | C.AAppl (_, hd :: tl) as what    -> proc_appl st what hd tl
-   | what                             -> proc_other st what
+and proc_proof st t = 
+   let f st =
+      let xet = match get_inner_types st t with
+         | Some (_, et) -> Some (cic et)
+         | None         -> None
+      in
+      let context, clears = Cn.get_clears st.context (cic t) xet in
+      let note = Pp.ppcontext st.context in
+      {st with context = context; clears = clears; clears_note = note}
+   in
+   match t with
+      | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
+      | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t
+      | C.ARel _ as what                 -> proc_rel (f st) what
+      | C.AMutConstruct _ as what        -> proc_mutconstruct (f st) what
+      | C.AAppl (_, hd :: tl) as what    -> proc_appl (f st) what hd tl
+      | what                             -> proc_other (f st) what
 
 and proc_bkd_proofs st synth names classes ts =
 try 
@@ -377,7 +402,7 @@ let proc_obj st = function
       let ast = proc_proof st v in
       let count = T.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
-      T.Theorem (s, t, "") :: ast @ [T.Qed text]
+      T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 
@@ -385,14 +410,16 @@ let proc_obj st = function
 
 let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = 
    let st = {
-      sorts     = ids_to_inner_sorts;
-      types     = ids_to_inner_types;
-      prefix    = prefix;
-      max_depth = depth;
-      depth     = 0;
-      context   = [];
-      intros    = [];
-      case      = []
+      sorts       = ids_to_inner_sorts;
+      types       = ids_to_inner_types;
+      prefix      = prefix;
+      max_depth   = depth;
+      depth       = 0;
+      context     = [];
+      intros      = [];
+      clears      = [];
+      clears_note = "";
+      case        = []
    } in
    HLog.debug "Procedural: level 2 transformation";
    let steps = proc_obj st aobj in
index 80aae9e7f3668b83fcee3378d7cb148174b5c31c..68b47341c05caff79f8972eb645c16c8fef30d73 100644 (file)
@@ -31,6 +31,8 @@ module D    = Deannotate
 module UM   = UriManager
 module Rd   = CicReduction
 
+module DTI  = DoubleTypeInference
+
 (* helpers ******************************************************************)
 
 let cic = D.deannotate_term
@@ -142,3 +144,51 @@ let generalize n =
 let mk_pattern psno predicate =
    let body = generalize psno predicate in
    clear_absts 0 psno body
+
+let get_clears c p xet = 
+   let meta = C.Implicit None in
+   let rec aux c names p et = function
+      | []                                                -> 
+         List.rev c, List.rev names         
+      | Some (C.Name name as n, C.Decl v) as hd :: tl     ->
+         let hd, names, v = 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+              Some (C.Anonymous, C.Decl v), name :: names, meta 
+           else 
+              hd, names, v
+        in
+        let p = C.Lambda (n, v, p) in
+        let et = C.Prod (n, v, et) in
+        aux (hd :: c) names p et tl
+      | Some (C.Name name as n, C.Def (v, x)) as hd :: tl ->
+         let hd, names, v = 
+           if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then 
+              Some (C.Anonymous, C.Def (v, x)), name :: names, meta
+           else 
+              hd, names, v
+        in
+        let p = C.LetIn (n, v, p) in
+        let et = C.LetIn (n, v, et) in
+        aux (hd :: c) names p et tl
+      | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
+        let p = C.Lambda (n, meta, p) in
+        let et = C.Lambda (n, meta, et) in
+        aux (hd :: c) names p et tl
+      | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
+        let p = C.LetIn (n, meta, p) in
+        let et = C.LetIn (n, meta, et) in
+        aux (hd :: c) names p et tl
+      | None :: tl                                        -> assert false
+   in
+   match xet with 
+      | Some et -> aux [] [] p et c
+      | None    -> c, []
+
+let clear c hyp =
+   let rec aux c = function
+      | []            -> List.rev c
+      | Some (C.Name name, entry) :: tail when name = hyp ->
+        aux (Some (C.Anonymous, entry) :: c) tail
+      | entry :: tail -> aux (entry :: c) tail
+   in
+   aux [] c
index 769cf3b9d08428baabf72ce7cd719ddc36f44d2c..f41f8e56c3f2d425d1e93b313de237d5cb9818c0 100644 (file)
@@ -30,3 +30,8 @@ val hole: Cic.id -> Cic.annterm
 val lift: int -> int -> Cic.annterm -> Cic.annterm
 
 val mk_pattern: int -> Cic.annterm -> Cic.annterm
+
+val get_clears: 
+   Cic.context -> Cic.term -> Cic.term option -> Cic.context * string list
+
+val clear: Cic.context -> string -> Cic.context
index 9d95d100ba83c375d1ba9f35d17d8ca73268b90c..ab15d70872aeccf94f99493eabc8511a577dbfb1 100644 (file)
@@ -82,10 +82,7 @@ let rec opt1_letin g es c name v t =
 and opt1_lambda g es c name w t =
    let name = H.mk_fresh_name c name in
    let entry = Some (name, C.Decl w) in
-   let g t = 
-      let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
-      g (C.Lambda (name, w, t))
-   in
+   let g t = g (C.Lambda (name, w, t)) in
    if es then opt1_proof g es (entry :: c) t else g t
 
 and opt1_appl g es c t vs =
index a1d120f807a161ac7aeb472e17d5518a63f28dcf..bc725d118f1124d3d2d3adf22492677a20a797cc 100644 (file)
@@ -51,13 +51,14 @@ let list_init f i =
 
 (****************************************************************************)
 
-type name     = string
+type name     = string option
+type hyp      = string
 type what     = Cic.annterm
 type how      = bool
 type using    = Cic.annterm
 type count    = int
 type note     = string
-type where    = (name * name) option
+type where    = (hyp * name) option
 type inferred = Cic.annterm
 type pattern  = Cic.annterm
 
@@ -72,7 +73,8 @@ type step = Note of note
          | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note 
-         | ClearBody of name * note
+         | Clear of hyp list * note
+         | ClearBody of hyp * note
          | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -94,7 +96,8 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_theorem name t = 
+let mk_theorem name t =
+   let name = match name with Some name -> name | None -> assert false in
    let obj = N.Theorem (`Theorem, name, t, None) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
@@ -111,15 +114,17 @@ let mk_id punctation =
    let tactic = G.IdTac floc in
    mk_tactic tactic punctation
 
-let mk_intros xi ids punctation =
-   let tactic = G.Intros (floc, xi, ids) in
+let mk_intros xi xids punctation =
+   let tactic = G.Intros (floc, (xi, xids)) in
    mk_tactic tactic punctation
 
 let mk_cut name what punctation =
+   let name = match name with Some name -> name | None -> assert false in
    let tactic = G.Cut (floc, Some name, what) in
    mk_tactic tactic punctation
 
 let mk_letin name what punctation =
+   let name = match name with Some name -> name | None -> assert false in
    let tactic = G.LetIn (floc, what, name) in
    mk_tactic tactic punctation
 
@@ -134,7 +139,7 @@ let mk_rewrite direction what where pattern punctation =
 
 let mk_elim what using pattern punctation =
    let pattern = None, [], Some pattern in
-   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
+   let tactic = G.Elim (floc, what, using, pattern, (Some 0, [])) in
    mk_tactic tactic punctation
 
 let mk_apply t punctation =
@@ -149,6 +154,10 @@ let mk_change t where pattern punctation =
    let tactic = G.Change (floc, pattern, t) in
    mk_tactic tactic punctation
 
+let mk_clear ids punctation =
+   let tactic = G.Clear (floc, ids) in
+   mk_tactic tactic punctation
+
 let mk_clearbody id punctation =
    let tactic = G.ClearBody (floc, id) in
    mk_tactic tactic punctation
@@ -179,6 +188,7 @@ let rec render_step sep a = function
    | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_tacnote s a
    | Apply (t, s)            -> mk_apply t sep :: mk_tacnote s a
    | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_tacnote s a
+   | Clear (ns, s)           -> mk_clear ns sep :: mk_tacnote s a
    | ClearBody (n, s)        -> mk_clearbody n sep :: mk_tacnote s a
    | Branch ([], s)          -> a
    | Branch ([ps], s)        -> render_steps sep a ps
index 9659a94ecca3ab9ae514d50244bfdf3708cdd495..cc5d75caf2918cec3f10beffe680905441b135eb 100644 (file)
@@ -33,13 +33,14 @@ val mk_arel: int -> string -> Cic.annterm
 
 (****************************************************************************)
 
-type name     = string
+type name     = string option
+type hyp      = string
 type what     = Cic.annterm
 type how      = bool
 type using    = Cic.annterm
 type count    = int
 type note     = string
-type where    = (name * name) option
+type where    = (hyp * name) option
 type inferred = Cic.annterm
 type pattern  = Cic.annterm
 
@@ -48,19 +49,20 @@ type step = Note of note
           | Qed of note
          | Id of note
          | Intros of count option * name list * note
-          | Cut of name * what * note
-          | LetIn of name * what * note
+         | Cut of name * what * note
+         | LetIn of name * what * note
          | Rewrite of how * what * where * pattern * note
          | Elim of what * using option * pattern * note
          | Apply of what * note
-         | Change of inferred * what * where * pattern * note
-         | ClearBody of name * note
+         | Change of inferred * what * where * pattern * note 
+         | Clear of hyp list * note
+         | ClearBody of hyp * note
          | Branch of step list list * note
 
 val render_steps: 
-   (what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> 
+   (what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, hyp) GrafiteAst.statement list -> 
    step list -> 
-   (what, inferred, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
+   (what, inferred, 'b, what CicNotationPt.obj, hyp) GrafiteAst.statement list
 
 val count_steps:
    int -> step list -> int
index d7b929de323fa12c0d6be8e37e4890ddeb8d5b02..fea24e42bc8b30249adfd7ddcbea4cc43d1a25c6 100644 (file)
@@ -39,6 +39,8 @@ type 'lazy_term reduction =
   | `Unfold of 'lazy_term option
   | `Whd ]
 
+type 'ident intros_spec = int option * 'ident option list
+
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Higher order tactics (i.e. tacticals) *)
   | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic
@@ -59,28 +61,28 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | ApplyS of loc * 'term * (string * string) list
   | Assumption of loc
   | Auto of loc * (string * string) list
-  | Cases of loc * 'term * 'ident list
+  | Cases of loc * 'term * 'ident intros_spec
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident list
   | ClearBody of loc * 'ident
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
-  | Decompose of loc * 'ident list
+  | Decompose of loc * 'ident option list
   | Demodulate of loc
   | Destruct of loc * 'term
   | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
-           int option * 'ident list
-  | ElimType of loc * 'term * 'term option * int option * 'ident list
+           'ident intros_spec
+  | ElimType of loc * 'term * 'term option * 'ident intros_spec
   | Exact of loc * 'term
   | Exists of loc
   | Fail of loc
   | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern
   | Fourier of loc
-  | FwdSimpl of loc * string * 'ident list
+  | FwdSimpl of loc * string * 'ident option list
   | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
   | IdTac of loc
-  | Intros of loc * int option * 'ident list
+  | Intros of loc * 'ident intros_spec
   | Inversion of loc * 'term
   | LApply of loc * bool * int option * 'term list * 'term * 'ident option
   | Left of loc
@@ -89,7 +91,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Reflexivity of loc
   | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Rewrite of loc * direction * 'term *
-      ('term, 'lazy_term, 'ident) pattern * 'ident list
+      ('term, 'lazy_term, 'ident) pattern * 'ident option list
   | Right of loc
   | Ring of loc
   | Split of loc
index 1b73d62de66dc638df803e136309da1e7fc645d3..521db02f3d28d3655d55e35bfc8613aa32869583 100644 (file)
@@ -31,7 +31,9 @@ let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
-let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
+let pp_idents idents = 
+   let map = function Some s -> s | None -> "_" in
+   "(" ^ String.concat " " (List.map map idents) ^ ")"
 let pp_hyps idents = String.concat " " idents
 
 let pp_reduction_kind ~term_pp = function
@@ -57,11 +59,11 @@ let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) =
     | Some t -> Printf.sprintf "\\vdash (%s)" (term_pp t) in
   Printf.sprintf "%sin %s%s" what_text hyp_text goal_text
 
-let pp_intros_specs = function
+let pp_intros_specs = function
    | None, []         -> ""
-   | Some num, []     -> Printf.sprintf " names %i" num
-   | None, idents     -> Printf.sprintf " names %s" (pp_idents idents)
-   | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
+   | Some num, []     -> Printf.sprintf " %s%i" s num
+   | None, idents     -> Printf.sprintf " %s%s" s (pp_idents idents)
+   | Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents)
 
 let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
 
@@ -98,8 +100,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
-  | Cases (_, term, idents) -> Printf.sprintf "cases " ^ term_pp term ^
-      pp_intros_specs (None, idents) 
+  | Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^
+      pp_intros_specs "names " specs 
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
@@ -110,39 +112,36 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
      "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Decompose (_, names) ->
-      Printf.sprintf "decompose%s" (pp_intros_specs (None, names)) 
+      Printf.sprintf "decompose%s" 
+      (pp_intros_specs "names " (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
-  | Elim (_, what, using, pattern, num, idents) ->
+  | Elim (_, what, using, pattern, specs) ->
       Printf.sprintf "elim %s%s %s%s" 
       (term_pp what)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
       (pp_tactic_pattern pattern)
-      (pp_intros_specs (num, idents)) 
-  | ElimType (_, term, using, num, idents) ->
-      Printf.sprintf "elim type " ^ term_pp term ^
+      (pp_intros_specs "names " specs) 
+  | ElimType (_, term, using, specs) ->
+      Printf.sprintf "elim type %s%s%s" 
+      (term_pp term)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
-      ^ pp_intros_specs (num, idents)
+      (pp_intros_specs "names " specs)
   | Exact (_, term) -> "exact " ^ term_pp term
   | Exists _ -> "exists"
   | Fold (_, kind, term, pattern) ->
       Printf.sprintf "fold %s %s %s" (pp_reduction_kind kind)
        (lazy_term_pp term) (pp_tactic_pattern pattern)
-  | FwdSimpl (_, hyp, idents) -> 
-      Printf.sprintf "fwd %s%s" hyp 
-        (match idents with [] -> "" | idents -> " as " ^ pp_idents idents)
+  | FwdSimpl (_, hyp, names) -> 
+      Printf.sprintf "fwd %s%s" hyp (pp_intros_specs "names " (None, names))
   | Generalize (_, pattern, ident) ->
      Printf.sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Fail _ -> "fail"
   | Fourier _ -> "fourier"
   | IdTac _ -> "id"
-  | Intros (_, None, []) -> "intros"
+  | Intros (_, specs) -> Printf.sprintf "intros%s" (pp_intros_specs "" specs)
   | Inversion (_, term) -> "inversion " ^ term_pp term
-  | Intros (_, num, idents) ->
-      Printf.sprintf "intros%s%s"
-        (match num with None -> "" | Some num -> " " ^ string_of_int num)
-        (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
   | LApply (_, linear, level_opt, terms, term, ident_opt) -> 
       Printf.sprintf "lapply %s%s%s%s%s" 
         (if linear then " linear " else "")
index 08b88b95fbc1b5e32ce1c883b2f5a4ed1d2053d3..296625a1dbc43a7284a3f9d730cf671aa01db5e3 100644 (file)
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-open Printf
-
 exception Drop
 (* mo file name, ma file name *)
 exception IncludedFileNotCompiled of string * string 
@@ -50,7 +48,10 @@ let namer_of names =
   let count = ref 0 in
   fun metasenv context name ~typ ->
     if !count < len then begin
-      let name = Cic.Name (List.nth names !count) in
+      let name = match List.nth names !count with
+         | Some s -> Cic.Name s
+        | None   -> Cic.Anonymous
+      in
       incr count;
       name
     end else
@@ -88,8 +89,8 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
        ~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Cases (_, what, names) ->
-      Tactics.cases_intros ~mk_fresh_name_callback:(namer_of names)
+  | GrafiteAst.Cases (_, what, (howmany, names)) ->
+      Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
         what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
@@ -98,7 +99,7 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
-     let names = match ident with None -> [] | Some id -> [id] in
+     let names = match ident with None -> [] | Some id -> [Some id] in
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
   | GrafiteAst.Decompose (_, names) ->
       let mk_fresh_name_callback = namer_of names in
@@ -107,10 +108,10 @@ let rec tactic_of_ast status ast =
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
-  | GrafiteAst.Elim (_, what, using, pattern, depth, names) ->
+  | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         ~pattern what
-  | GrafiteAst.ElimType (_, what, using, depth, names) ->
+  | GrafiteAst.ElimType (_, what, using, (depth, names)) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
   | GrafiteAst.Exact (_, term) -> Tactics.exact term
@@ -139,23 +140,21 @@ let rec tactic_of_ast status ast =
      Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
       ~dbd:(LibraryDb.instance ()) hyp
   | GrafiteAst.Generalize (_,pattern,ident) ->
-     let names = match ident with None -> [] | Some id -> [id] in
+     let names = match ident with None -> [] | Some id -> [Some id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
   | GrafiteAst.IdTac _ -> Tactics.id
-  | GrafiteAst.Intros (_, None, names) ->
-      PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-  | GrafiteAst.Intros (_, Some num, names) ->
-      PrimitiveTactics.intros_tac ~howmany:num
+  | GrafiteAst.Intros (_, (howmany, names)) ->
+      PrimitiveTactics.intros_tac ?howmany
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
   | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
-      let names = match ident with None -> [] | Some id -> [id] in
+      let names = match ident with None -> [] | Some id -> [Some id] in
       Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
         ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
-      Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
+      Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
         | `Normalize -> Tactics.normalize ~pattern
@@ -167,7 +166,9 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Replace (_, pattern, with_what) ->
      Tactics.replace ~pattern ~with_what
   | GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
-     EqualityTactics.rewrite_tac ~direction ~pattern t names
+     EqualityTactics.rewrite_tac ~direction ~pattern t 
+(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *)
+     (List.map (function Some s -> s | None -> assert false) names)
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring
   | GrafiteAst.Split _ -> Tactics.split
@@ -721,7 +722,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           with Not_found -> v
         in
         if Http_getter_storage.is_read_only value then begin
-          HLog.error (sprintf "uri %s belongs to a read-only repository" value);
+          HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" value);
           raise (ReadOnlyUri value)
         end;
         if not (Http_getter_storage.is_empty value) && 
index 912abbcc38d0eadb1dc1235d35010309e719d3e8..fd1849760f986010be8a950833a5bf8eb47aca11 100644 (file)
@@ -212,22 +212,22 @@ let rec disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents) ->
+    | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
        let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
        let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, pattern, depth, idents) ->
+        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
+    | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
        let metasenv,what = disambiguate_term context metasenv what in
        let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Elim (loc, what, None, pattern, depth, idents)
-    | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+        metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
+    | GrafiteAst.ElimType (loc, what, Some using, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
-    | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+        metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
+    | GrafiteAst.ElimType (loc, what, None, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.ElimType (loc, what, None, specs)
     | GrafiteAst.Exists loc ->
         metasenv,GrafiteAst.Exists loc 
     | GrafiteAst.Fail loc ->
@@ -246,8 +246,8 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
     | GrafiteAst.IdTac loc ->
         metasenv,GrafiteAst.IdTac loc
-    | GrafiteAst.Intros (loc, num, names) ->
-        metasenv,GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.Intros (loc, specs) ->
+        metasenv,GrafiteAst.Intros (loc, specs)
     | GrafiteAst.Inversion (loc, term) ->
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
index 63df8ab7f37d1b6a208e89bd16b599ec67da2512..05504f511f3c149913256f7740cffb861b231730 100644 (file)
@@ -65,7 +65,11 @@ EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
-  ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+  new_name: [
+    [ id = IDENT -> Some id
+    | SYMBOL "_" -> None ]
+    ];
+  ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
   tactic_term_list1: [
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
@@ -144,8 +148,8 @@ EXTEND
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
     | IDENT "cases"; what = tactic_term;
-      (num, idents) = intros_spec ->
-       GrafiteAst.Cases (loc, what, idents)
+      specs = intros_spec ->
+       GrafiteAst.Cases (loc, what, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
@@ -158,7 +162,7 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
@@ -171,10 +175,10 @@ EXTEND
           | None         -> None, [], Some Ast.UserInput
           | Some pattern -> pattern   
        in
-       GrafiteAst.Elim (loc, what, using, pattern, num, idents)
+       GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
-       GrafiteAst.ElimType (loc, what, using, num, idents)
+       GrafiteAst.ElimType (loc, what, using, (num, idents))
     | IDENT "exact"; t = tactic_term ->
         GrafiteAst.Exact (loc, t)
     | IDENT "exists" ->
@@ -190,17 +194,17 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
        GrafiteAst.Generalize (loc,p,id)
     | IDENT "id" -> GrafiteAst.IdTac loc
     | IDENT "intro"; ident = OPT IDENT ->
-        let idents = match ident with None -> [] | Some id -> [id] in
-        GrafiteAst.Intros (loc, Some 1, idents)
-    | IDENT "intros"; (num, idents) = intros_spec ->
-        GrafiteAst.Intros (loc, num, idents)
+        let idents = match ident with None -> [] | Some id -> [Some id] in
+        GrafiteAst.Intros (loc, (Some 1, idents))
+    | IDENT "intros"; specs = intros_spec ->
+        GrafiteAst.Intros (loc, specs)
     | IDENT "inversion"; t = tactic_term ->
         GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
index 64db996667879cd10efb1adf0ad83b7032fd2a94..c5aab0f5ff45eeebb63f608195552302d799df26 100644 (file)
@@ -52,9 +52,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
       match ty with 
         C.Cast (te,_)   -> collect_context context howmany do_whd te 
       | C.Prod (n,s,t)  ->
-         let n' = mk_fresh_name metasenv context n ~typ:s in
+        let n' = mk_fresh_name metasenv context n ~typ:s in
           let (context',ty,bo) =
-           let ctx = (Some (n',(C.Decl s)))::context in
+           let entry = match n' with
+             | C.Name _    -> Some (n',(C.Decl s))
+             | C.Anonymous -> None
+          in
+          let ctx = entry :: context in
            collect_context ctx (howmany - 1) do_whd t 
           in
            (context',ty,C.Lambda(n',s,bo))
@@ -365,9 +369,7 @@ let apply_tac ~term =
   PET.mk_tactic (apply_tac ~term)
 
 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
- let intros_tac
-  ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) ()
-  (proof, goal)
+ let intros_tac (proof, goal)
  =
   let module C = Cic in
   let module R = CicReduction in
@@ -383,7 +385,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
       in
        (newproof, [newmeta])
  in
-  PET.mk_tactic (intros_tac ~mk_fresh_name_callback ())
+  PET.mk_tactic intros_tac
   
 let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cut_tac
@@ -706,7 +708,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
    PET.mk_tactic elim_tac
 ;;
 
-let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cases_tac ~term (proof, goal) =
   let module TC = CicTypeChecker in
   let module U = UriManager in
index 863df5eeea2872ef08d48c01348c2c25974072f0..577ed753575a0da5dd6ecfd78b3cbdcb3e08481c 100644 (file)
@@ -82,6 +82,7 @@ val elim_intros_tac:
   ProofEngineTypes.tactic 
 
 val cases_intros_tac:
+  ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic 
 
index 2ad12d22ada36508a5f786ab048ee60794ab80ce..6cc96c74b4751c0c3881c38e5e72372cbfc1de73 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Sat Apr 28 12:11:33 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed May  9 13:55:06 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -11,6 +11,7 @@ val auto :
   params:(string * string) list ->
   dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
 val cases_intros :
+  ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic
 val change :
index 3ed457d958dd64d25ee7d29ab111ad53574563c2..fa280b3f8adcd864496eb94af4440d1a445aa324 100644 (file)
@@ -247,7 +247,7 @@ let convert_ast statements context = function
           statements @ [
             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
             GA.Executable(floc,GA.Tactic(floc, Some
-             (GA.Intros (floc,None,[])),GA.Dot(floc)))] @
+             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
           (if fv <> [] then     
             (List.flatten
               (List.map 
index 55db1774cde3e4818ae5bf468082b046a95afe8e..30d6dbd2051e38db13a773ee825f5228cea9f41e 100644 (file)
@@ -986,14 +986,14 @@ class gui () =
               ~lazy_term_pp:CicNotationPp.pp_term ast)
       in
       let tbar = main in
-      connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
+      connect_button tbar#introsButton (tac (A.Intros (loc, (None, []))));
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
       connect_button tbar#elimButton (tac_w_term
         (let pattern = None, [], Some CicNotationPt.UserInput in
-       A.Elim (loc, hole, None, pattern, None, [])));
+       A.Elim (loc, hole, None, pattern, (None, []))));
       connect_button tbar#elimTypeButton (tac_w_term
-        (A.ElimType (loc, hole, None, None, [])));
+        (A.ElimType (loc, hole, None, (None, []))));
       connect_button tbar#splitButton (tac (A.Split loc));
       connect_button tbar#leftButton (tac (A.Left loc));
       connect_button tbar#rightButton (tac (A.Right loc));