From: Ferruccio Guidi Date: Wed, 9 May 2007 19:36:00 +0000 (+0000) Subject: PrimitiveTactics: intros _ now aveilable X-Git-Tag: 0.4.95@7852~481 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8254cf86275b9d78b30a0b14974a6f23ad9be24;p=helm.git PrimitiveTactics: intros _ now aveilable GrafiteAst : some refactoring --- diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index ff8aaea88..95c4c1a9a 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -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 diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index 80aae9e7f..68b47341c 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -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 diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli index 769cf3b9d..f41f8e56c 100644 --- a/components/acic_procedural/proceduralConversion.mli +++ b/components/acic_procedural/proceduralConversion.mli @@ -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 diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml index 9d95d100b..ab15d7087 100644 --- a/components/acic_procedural/proceduralOptimizer.ml +++ b/components/acic_procedural/proceduralOptimizer.ml @@ -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 = diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index a1d120f80..bc725d118 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -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 diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index 9659a94ec..cc5d75caf 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -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 diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index d7b929de3..fea24e42b 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -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 diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 1b73d62de..521db02f3 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -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 s = 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 "") diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 08b88b95f..296625a1d 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -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) && diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 912abbcc3..fd1849760 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -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) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 63df8ab7f..05504f511 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -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"; diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 64db99666..c5aab0f5f 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -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 diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli index 863df5eee..577ed7535 100644 --- a/components/tactics/primitiveTactics.mli +++ b/components/tactics/primitiveTactics.mli @@ -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 diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 2ad12d22a..6cc96c74b 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -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 : diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml index 3ed457d95..fa280b3f8 100644 --- a/components/tptp_grafite/tptp2grafite.ml +++ b/components/tptp_grafite/tptp2grafite.ml @@ -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 diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 55db1774c..30d6dbd20 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -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));