let get_type msg st t = H.get_type msg st.context (H.cic t)
+let clear_absts m =
+ let rec aux k n = function
+ | C.ALambda (id, s, v, t) when k > 0 ->
+ C.ALambda (id, s, v, aux (pred k) n t)
+ | C.ALambda (_, _, _, t) when n > 0 ->
+ aux 0 (pred n) (Cn.lift 1 (-1) t)
+ | t when n > 0 ->
+ Printf.eprintf "A2P.clear_absts: %u %s\n" n (Pp.ppterm (H.cic t));
+ assert false
+ | t -> t
+ in
+ aux m
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "UNNAMED"
in
mk_preamble st what script
+and proc_case st what uri tyno u v ts =
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let synth, classes = I.S.empty, Cl.make ts in
+ let names = H.get_ind_names uri tyno in
+ let qs = proc_bkd_proofs (next st) synth names classes ts in
+ let lpsno, _ = H.get_ind_type uri tyno in
+ let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in
+ let _, rps = HEL.split_nth lpsno ps in
+ let rpsno = List.length rps in
+ let predicate = clear_absts rpsno (1 - sort_disp) u in
+ let e = Cn.mk_pattern rpsno predicate in
+ let text = "" in
+ let script = List.rev (mk_arg st v) in
+ script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_preamble st what script
+
and proc_other st what =
let _, dtext = test_depth st in
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
{st with context = context}
in
match t with
- | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t
- | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
- | C.ARel _ as what -> proc_rel (f st) what
- | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
- | C.AConst _ as what -> proc_const (f st) what
- | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
- | what -> proc_other (f st) what
+ | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t
+ | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
+ | C.ARel _ as what -> proc_rel (f st) what
+ | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
+ | C.AConst _ as what -> proc_const (f st) what
+ | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
+ | C.AMutCase (_, uri, i, u, v, ts) as what -> proc_case (f st) what uri i u v ts
+ | what -> proc_other (f st) what
and proc_bkd_proofs st synth names classes ts =
try
Array.iteri map b;
prerr_newline ()
+(* dummy dependences ********************************************************)
+
+let make l =
+ let map _ = I.S.empty, false in
+ List.rev_map map l
+
(* classification ***********************************************************)
let classify_conclusion vs =
type conclusion = (int * int * UriManager.uri * int) option
+val make: 'a list -> dependences
+
val classify: Cic.context -> Cic.term -> dependences * conclusion
val adjust: Cic.context -> Cic.annterm list -> ?goal:Cic.term -> dependences -> dependences
| (_, hd) :: _, _ -> hd
| _ -> assert false
-let is_proof c t =
- match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
+let is_prop c t =
+ match get_tail c (get_type "is_prop" c t) with
| C.Sort C.Prop -> true
| C.Sort _ -> false
| _ -> assert false
+let is_proof c t =
+ is_prop c (get_type "is_prop" c t)
+
let is_sort = function
| C.Sort _ -> true
| _ -> false
Cic.context -> Cic.term -> Cic.term
val get_type:
string -> Cic.context -> Cic.term -> Cic.term
+val is_prop:
+ Cic.context -> Cic.term -> bool
val is_proof:
Cic.context -> Cic.term -> bool
val is_sort:
opt_proof g (info st "Optimizer: remove 3") es c x
and opt_mutcase_plain g st es c uri tyno outty arg cases =
- let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in
- g st arg cases
+ let g st v =
+ let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ let map h v (st, vs) =
+ let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+ in
+ if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+ in
+ if es then opt_proof g st es c arg else g st arg
and opt_mutcase g =
if !critical then opt_mutcase_critical g else opt_mutcase_plain g
val optimize_term: Cic.context -> Cic.term -> Cic.term * string
+val critical: bool ref
+
val debug: bool ref
| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
| Elim of what * using option * pattern * note
+ | Cases of what * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| Clear of hyp list * note
let tactic = G.Elim (floc, what, using, pattern, (Some 0, [])) in
mk_tactic tactic punctation
+let mk_cases what pattern punctation =
+ let pattern = None, [], Some pattern in
+ let tactic = G.Cases (floc, what, pattern, (Some 0, [])) in
+ mk_tactic tactic punctation
+
let mk_apply t punctation =
let tactic = G.ApplyP (floc, t) in
mk_tactic tactic punctation
| LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
| Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
| Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
+ | Cases (t, e, s) -> mk_cases t 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
| Apply (t, _) -> I.count_nodes a (H.cic t)
| Rewrite (_, t, _, p, _)
| Elim (t, _, p, _)
+ | Cases (t, p, _)
| Change (t, _, _, p, _) ->
let a = I.count_nodes a (H.cic t) in
I.count_nodes a (H.cic p)
| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
| Elim of what * using option * pattern * note
+ | Cases of what * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| Clear of hyp list * note
| AutoBatch (_,params) -> "autobatch " ^
pp_auto_params ~term_pp params
| Assumption _ -> "assumption"
- | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
- pp_tactic_pattern pattern ^
- pp_intros_specs "names " specs
+ | Cases (_, term, pattern, specs) ->
+ Printf.sprintf "cases %s %s%s"
+ (term_pp term)
+ (pp_tactic_pattern pattern)
+ (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)
GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
- (num, idents) = intros_spec ->
+ ispecs = intros_spec ->
let pattern = match pattern with
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
in
- GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
+ GrafiteAst.Elim (loc, what, using, pattern, ispecs)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, (num, idents))
||I||
||T|| HELM is free software; you can redistribute it and/or
||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
(* $Id$ *)
apply cic:/Coq/Init/Logic/f_equal.con.
assumption.
qed.
+
+alias id "land" = "cic:/matita/procedural/Coq/Init/Logic/and.ind#xpointer(1/1)".
projects / helm.git / commitdiff