From 4ed8829233095bdf2ab1c15021ba815084d19b70 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 16 Jul 2008 18:16:19 +0000 Subject: [PATCH] Procedural: some comments added in the generated script tests/fguidi.ma: we removed the dependence from legacy/coq.ma ApplyTransformation: new function procedural_text_of_cic_term for use in matitaScript (still disabled) --- .../acic_procedural/acic2Procedural.ml | 70 ++++++++++++------- .../acic_procedural/acic2Procedural.mli | 12 +++- .../acic_procedural/proceduralHelpers.ml | 24 +++++-- .../acic_procedural/proceduralHelpers.mli | 2 + helm/software/matita/applyTransformation.ml | 29 ++++++-- helm/software/matita/applyTransformation.mli | 6 ++ helm/software/matita/matitaScript.ml | 24 ++----- helm/software/matita/tests/fguidi.ma | 20 +----- 8 files changed, 113 insertions(+), 74 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 298259cb5..c95e815da 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -47,17 +47,13 @@ module H = ProceduralHelpers type status = { sorts : (C.id, A.sort_kind) Hashtbl.t; types : (C.id, A.anntypes) Hashtbl.t; - prefix: string; max_depth: int option; depth: int; context: C.context; - clears: string list; - clears_note: string; - case: int list; - skip_thm_and_qed : bool; + case: int list } -let debug = true +let debug = false (* helpers ******************************************************************) @@ -173,6 +169,23 @@ try | (_, _, _, cs) -> List.map fst cs with Invalid_argument _ -> failwith "A2P.get_ind_names" +let string_of_atomic = function + | C.ARel (_, _, _, s) -> s + | C.AVar (_, uri, _) -> H.name_of_uri uri None None + | C.AConst (_, uri, _) -> H.name_of_uri uri None None + | C.AMutInd (_, uri, i, _) -> H.name_of_uri uri (Some i) None + | C.AMutConstruct (_, uri, i, j, _) -> H.name_of_uri uri (Some i) (Some j) + | _ -> "" + +let get_sub_names head l = + let s = string_of_atomic head in + if s = "" then [] else + let map (names, i) _ = + let name = Printf.sprintf "%s_%u" s i in name :: names, succ i + in + let names, _ = List.fold_left map ([], 1) l in + List.rev names + (* proof construction *******************************************************) let anonymous_premise = C.Name "PREMISE" @@ -238,10 +251,7 @@ let get_intro = function | C.Name s -> Some s let mk_preamble st what script = - let clears st script = - if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script - in - clears st (convert st what @ script) + convert st what @ script let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what @@ -384,7 +394,8 @@ and proc_appl st what hd tl = (* convert_elim st what what e @ *) script2 @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> - let qs = proc_bkd_proofs (next st) synth [] classes tl in + let names = get_sub_names hd tl in + let qs = proc_bkd_proofs (next st) synth names classes tl in let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else @@ -406,9 +417,8 @@ and proc_proof st t = (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) | None -> None, "\nNo types" in - let context, clears = Cn.get_clears st.context (H.cic t) xtypes in - let note = Pp.ppcontext st.context ^ note in - {st with context = context; clears = clears; clears_note = note; } + let context, _clears = Cn.get_clears st.context (H.cic t) xtypes in + {st with context = context} in match t with | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t @@ -436,7 +446,7 @@ try let aux (inv, _) v = if I.overlaps synth inv then None else if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else - Some (fun _ -> [T.Apply (v, dtext ^ "dependent")]) + Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")])) in let ps = T.list_map2_filter aux classes ts in let b = List.length ps > 1 in @@ -459,8 +469,7 @@ let proc_obj st = function let ast = proc_proof st v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in - if st.skip_thm_and_qed then ast - else T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text] + T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text] | C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars -> [T.Statement (`Definition, Some s, t, Some v, "")] | C.AConstant (_, _, s, None, t, [], pars) -> @@ -470,21 +479,32 @@ let proc_obj st = function (* interface functions ******************************************************) -let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth -?(skip_thm_and_qed=false) prefix aobj = +let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth + prefix anobj = let st = { sorts = ids_to_inner_sorts; types = ids_to_inner_types; - prefix = prefix; max_depth = depth; depth = 0; context = []; - clears = []; - clears_note = ""; - case = []; - skip_thm_and_qed = skip_thm_and_qed; + case = [] + } in + HLog.debug "Procedural: level 2 transformation"; + let steps = proc_obj st anobj in + HLog.debug "Procedural: grafite rendering"; + List.rev (T.render_steps [] steps) + +let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth + prefix context annterm = + let st = { + sorts = ids_to_inner_sorts; + types = ids_to_inner_types; + max_depth = depth; + depth = 0; + context = context; + case = [] } in HLog.debug "Procedural: level 2 transformation"; - let steps = proc_obj st aobj in + let steps = proc_proof st annterm in HLog.debug "Procedural: grafite rendering"; List.rev (T.render_steps [] steps) diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index 08e49a343..7d830447b 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -23,12 +23,18 @@ * http://cs.unibo.it/helm/. *) -val acic2procedural: +val procedural_of_acic_object: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> ?skip_thm_and_qed:bool -> - string -> Cic.annobj -> + ?depth:int -> string -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list +val procedural_of_acic_term: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> + ?depth:int -> string -> Cic.context -> Cic.annterm -> + (Cic.annterm, Cic.annterm, + Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) + GrafiteAst.statement list diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 54e8ebe05..d6f844d71 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -133,11 +133,11 @@ let get_ind_type uri tyno = let get_default_eliminator context uri tyno ty = let _, (name, _, _, _) = get_ind_type uri tyno in let ext = match get_tail context (get_type context ty) with - | C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort (C.CProp _) -> "_rect" - | C.Sort (C.Type _) -> "_rect" - | t -> + | C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort (C.CProp _) -> "_rect" + | C.Sort (C.Type _) -> "_rect" + | t -> Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t); assert false in @@ -171,6 +171,20 @@ let occurs c ~what ~where = let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in !result +let name_of_uri uri tyno cno = + let get_ind_type tys tyno = + let s, _, _, cs = List.nth tys tyno in s, cs + in + match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with + | C.Variable (s, _, _, _, _), _, _ -> s + | C.Constant (s, _, _, _, _), _, _ -> s + | C.InductiveDefinition (tys, _, _, _), Some i, None -> + let s, _ = get_ind_type tys i in s + | C.InductiveDefinition (tys, _, _, _), Some i, Some j -> + let _, cs = get_ind_type tys i in + let s, _ = List.nth cs (pred j) in s + | _ -> assert false + (* Ensuring Barendregt convenction ******************************************) let rec add_entries map c = function diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index e1b7f49f6..a02d8ab1d 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -57,6 +57,8 @@ val cic: Cic.annterm -> Cic.term val occurs: Cic.context -> what:Cic.term -> where:Cic.term -> bool +val name_of_uri: + UriManager.uri -> int option -> int option -> string val cic_bc: Cic.context -> Cic.term -> Cic.term val acic_bc: diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 150ec8de0..0597fcf99 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -198,9 +198,9 @@ let txt_of_cic_object let aux = GrafiteAstPp.pp_statement ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = - Acic2Procedural.acic2procedural + Acic2Procedural.procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types - ?depth ?skip_thm_and_qed prefix aobj + ?depth prefix aobj in "\n\n" ^ String.concat "" (List.map aux script) @@ -233,8 +233,27 @@ let txt_of_inline_macro ~map_unicode_to_tex style name prefix = let _, baseuri, _, _ = Librarian.baseuri_of_script ~include_paths name in - baseuri + baseuri ^ "/" in txt_of_inline_uri ~map_unicode_to_tex style suri prefix - - + +(****************************************************************************) +(* procedural_txt_of_cic_term *) + +let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = + let annterm, ids_to_inner_sorts, ids_to_inner_types = + try Cic2acic.acic_term_of_cic_term context term + with e -> + let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in + failwith msg + in + let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in + let lazy_term_pp = term_pp in + let obj_pp = CicNotationPp.pp_obj term_pp in + let aux = GrafiteAstPp.pp_statement + ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in + let script = + Acic2Procedural.procedural_of_acic_term + ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm + in + String.concat "" (List.map aux script) diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 788ef6810..4b0251743 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -77,3 +77,9 @@ val txt_of_cic_object: val txt_of_inline_macro: map_unicode_to_tex:bool -> GrafiteAst.presentation_style -> string -> string -> string + +(* columns, rendering depth, context, term *) +val procedural_txt_of_cic_term: + map_unicode_to_tex:bool -> int -> ?depth:int -> + Cic.context -> Cic.term -> + string diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 34ca16d25..4fa7d9e5f 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -561,25 +561,11 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status cic2grafite cc menv proof_term else (* alternative using FG stuff *) - let proof_term, how_many_lambdas = - Auto.lambda_close ~prefix_name:"orrible_hack_" - proof_term menv cc - in - let ty,_ = - CicTypeChecker.type_of_aux' - menv [] proof_term CicUniv.empty_ugraph - in - let obj = - Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) - in - Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" - (strip_comments - (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~skip_thm_and_qed:true - ~skip_initial_lambdas:how_many_lambdas - 80 (GrafiteAst.Procedural None) "" obj)) + let map_unicode_to_tex = + Helm_registry.get_bool "matita.paste_unicode_as_tex" + in + ApplyTransformation.procedural_txt_of_cic_term + ~map_unicode_to_tex 78 cc proof_term in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length diff --git a/helm/software/matita/tests/fguidi.ma b/helm/software/matita/tests/fguidi.ma index b6bc3d907..966ff7cc2 100644 --- a/helm/software/matita/tests/fguidi.ma +++ b/helm/software/matita/tests/fguidi.ma @@ -12,22 +12,8 @@ (* *) (**************************************************************************) - -include "coq.ma". - -alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". -alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". -alias id "le" = "cic:/matita/tests/fguidi/le.ind#xpointer(1/1)". -alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con". -alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". -alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". -alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". - -alias symbol "and" (instance 0) = "Coq's logical and". -alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". -alias symbol "exists" (instance 0) = "Coq's exists". +include "logic/connectives.ma". +include "nat/nat.ma". definition is_S: nat \to Prop \def \lambda n. match n with @@ -95,7 +81,7 @@ qed. theorem le_gen_S_x_cc: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to (le (S m) x). -intros. elim H. elim H1. cut ((S x1) = x). elim Hcut. autobatch. +intros. elim H. elim H1. cut ((S a) = x). elim Hcut. autobatch. elim H2. autobatch. qed. -- 2.39.2