module Pp = CicPp
module PEH = ProofEngineHelpers
module HEL = HExtlib
+module DTI = DoubleTypeInference
module Cl = ProceduralClassify
module T = ProceduralTypes
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
}
(* 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) =
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
| 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 =
[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
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
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
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"
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
module UM = UriManager
module Rd = CicReduction
+module DTI = DoubleTypeInference
+
(* helpers ******************************************************************)
let cic = D.deannotate_term
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
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
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 =
(****************************************************************************)
-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
| 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 *****************************************************)
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)))
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
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 =
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
| 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
(****************************************************************************)
-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
| 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
| `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
| 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
| 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
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
| 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)
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)
"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 "")
(* $Id$ *)
-open Printf
-
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
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
| 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
| 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
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
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
| 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
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) &&
| 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 ->
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)
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 ]
];
| 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 ->
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
| 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" ->
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";
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))
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
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
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
ProofEngineTypes.tactic
val cases_intros_tac:
+ ?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term -> ProofEngineTypes.tactic
-(* 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 :
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 :
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
~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));
projects / helm.git / commitdiff