From 5b45f78ed4293ebbe8cc73ad925bca11a300d021 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 17 Feb 2009 19:37:22 +0000 Subject: [PATCH] - Coq/preamble: missing alias added - nUri: head comment fixed - Procedural: the cases tactic is now detected and generated but does not compile :)) - grafiteAstPp: output syntax of the cases tactic fixed - grafiteParser: impovement in the code for the elim tactic --- .../acic_procedural/acic2Procedural.ml | 48 ++++++++++++++++--- .../acic_procedural/proceduralClassify.ml | 6 +++ .../acic_procedural/proceduralClassify.mli | 2 + .../acic_procedural/proceduralHelpers.ml | 7 ++- .../acic_procedural/proceduralHelpers.mli | 2 + .../acic_procedural/proceduralOptimizer.ml | 10 +++- .../acic_procedural/proceduralOptimizer.mli | 2 + .../acic_procedural/proceduralTypes.ml | 8 ++++ .../acic_procedural/proceduralTypes.mli | 1 + .../components/grafite/grafiteAstPp.ml | 8 ++-- .../grafite_parser/grafiteParser.ml | 4 +- helm/software/components/ng_kernel/nUri.ml | 4 +- .../contribs/procedural/Coq/preamble.ma | 2 + 13 files changed, 86 insertions(+), 18 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index b65d131e6..ae64d1f19 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -174,6 +174,19 @@ let get_sub_names head l = 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" @@ -380,6 +393,26 @@ and proc_appl st what hd tl = 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 @@ -398,13 +431,14 @@ and proc_proof st t = {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 diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 981acc969..53c363a42 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -56,6 +56,12 @@ let out_table b = 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 = diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli index 6a93a1fda..d4662764e 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.mli +++ b/helm/software/components/acic_procedural/proceduralClassify.mli @@ -27,6 +27,8 @@ type dependences = (CicInspect.S.t * bool) list 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 diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 5807e185a..a9fa6473f 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -127,12 +127,15 @@ let get_tail c t = | (_, 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 diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 69df6d797..6d4ef50da 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -41,6 +41,8 @@ val refine: 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: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index f1840cf7c..a05bbd26d 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -209,8 +209,14 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases = 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 diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.mli b/helm/software/components/acic_procedural/proceduralOptimizer.mli index 1e7bdada2..522860df3 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.mli +++ b/helm/software/components/acic_procedural/proceduralOptimizer.mli @@ -27,4 +27,6 @@ val optimize_obj: Cic.obj -> Cic.obj * string val optimize_term: Cic.context -> Cic.term -> Cic.term * string +val critical: bool ref + val debug: bool ref diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index b194fbfa9..3b6afc4c3 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -79,6 +79,7 @@ type step = Note of note | 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 @@ -194,6 +195,11 @@ let mk_elim what using pattern punctation = 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 @@ -239,6 +245,7 @@ let rec render_step sep a = function | 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 @@ -287,6 +294,7 @@ let rec count_node a = function | 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) diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index 3cc482a8c..aa6ad3aa5 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -58,6 +58,7 @@ type step = Note of note | 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 9e3ea3b5a..1fdc87b41 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -121,9 +121,11 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = | 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) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 4da1d4477..44dec6d32 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -227,12 +227,12 @@ EXTEND 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)) diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml index 592403684..e94ee9037 100644 --- a/helm/software/components/ng_kernel/nUri.ml +++ b/helm/software/components/ng_kernel/nUri.ml @@ -5,8 +5,8 @@ ||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$ *) diff --git a/helm/software/matita/contribs/procedural/Coq/preamble.ma b/helm/software/matita/contribs/procedural/Coq/preamble.ma index 04d88dc07..6e26169d5 100644 --- a/helm/software/matita/contribs/procedural/Coq/preamble.ma +++ b/helm/software/matita/contribs/procedural/Coq/preamble.ma @@ -41,3 +41,5 @@ theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A. apply cic:/Coq/Init/Logic/f_equal.con. assumption. qed. + +alias id "land" = "cic:/matita/procedural/Coq/Init/Logic/and.ind#xpointer(1/1)". -- 2.39.2