From 55ec3926f6fbb5dba13705659fe94d0db38b2666 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Jun 2007 07:35:59 +0000 Subject: [PATCH] hacks for paramodulation declarative proofs --- .../components/acic_content/acic2content.ml | 6 +- .../acic_procedural/acic2Procedural.ml | 18 +----- .../acic_procedural/acic2Procedural.mli | 2 +- .../components/content_pres/content2pres.ml | 60 ++++++++++++------- .../components/content_pres/content2pres.mli | 1 + helm/software/matita/applyTransformation.ml | 33 +++++----- helm/software/matita/applyTransformation.mli | 3 +- helm/software/matita/matitaScript.ml | 23 ++++++- 8 files changed, 89 insertions(+), 57 deletions(-) diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 1b8c287fa..eddee38b1 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -479,7 +479,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = } in generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types - else raise Not_a_proof + else + raise Not_a_proof | C.ALetIn (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then @@ -500,7 +501,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = } in generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types - else raise Not_a_proof + else + raise Not_a_proof | C.AAppl (id,li) -> (try coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 23b934d51..f39aa18bd 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -56,7 +56,6 @@ type status = { clears_note: string; case: int list; skip_thm_and_qed : bool; - skip_initial_lambdas : bool; } (* helpers ******************************************************************) @@ -376,12 +375,7 @@ and proc_proof st t = (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) | None -> None, "\nNo types" in - let context, clears = - if st.skip_initial_lambdas then - st.context, [] - else - Cn.get_clears st.context (H.cic t) xtypes - 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; } in @@ -429,13 +423,6 @@ 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 - let ast = - if st.skip_initial_lambdas then - match ast with - | T.Intros _::tl -> tl - | ast -> ast - else ast - in if st.skip_thm_and_qed then ast else T.Theorem (Some s, t, "") :: ast @ [T.Qed text] | _ -> @@ -444,7 +431,7 @@ let proc_obj st = function (* interface functions ******************************************************) let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth -?(skip_thm_and_qed=false) ?(skip_initial_lambdas=false) prefix aobj = +?(skip_thm_and_qed=false) prefix aobj = let st = { sorts = ids_to_inner_sorts; types = ids_to_inner_types; @@ -457,7 +444,6 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth clears_note = ""; case = []; skip_thm_and_qed = skip_thm_and_qed; - skip_initial_lambdas = skip_initial_lambdas; } in HLog.debug "Procedural: level 2 transformation"; let steps = proc_obj st aobj in diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index 35092fb16..08e49a343 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -26,7 +26,7 @@ val acic2procedural: 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 -> ?skip_initial_lambdas:bool -> + ?depth:int -> ?skip_thm_and_qed:bool -> string -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index e377706b7..b9c46917c 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -134,8 +134,9 @@ let rec justification term2pres p = else (B.b_kw "by"), Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) -and proof2pres is_top_down term2pres p = - let rec proof2pres is_top_down p omit_dot = +and proof2pres ?skip_initial_lambdas is_top_down term2pres p = + let rec proof2pres ?(skip_initial_lambdas_internal=false) is_top_down p omit_dot = + prerr_endline p.Con.proof_conclude.Con.conclude_method; let indent = let is_decl e = (match e with @@ -150,16 +151,19 @@ and proof2pres is_top_down term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres is_top_down p.Con.proof_conclude indent omit_conclusion + conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion omit_dot in let presacontext = acontext2pres (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") - p.Con.proof_apply_context presconclude indent + p.Con.proof_apply_context + presconclude indent (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in - context2pres p.Con.proof_context presacontext - in + context2pres + (if skip_initial_lambdas_internal then [] else p.Con.proof_context) + presacontext + in match p.Con.proof_name with None -> body | Some name -> @@ -256,7 +260,7 @@ and proof2pres is_top_down term2pres p = [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation])) ac continuation - and conclude2pres is_top_down conclude indent omit_conclusion omit_dot = + and conclude2pres ?skip_initial_lambdas_internal is_top_down conclude indent omit_conclusion omit_dot = let tconclude_body = match conclude.Con.conclude_conclusion with Some t (*when not omit_conclusion or @@ -274,7 +278,8 @@ and proof2pres is_top_down term2pres p = (* false ind is in charge to add the conclusion *) falseind conclude else - let conclude_body = conclude_aux conclude in + let conclude_body = + conclude_aux ?skip_initial_lambdas_internal conclude in let ann_concl = if conclude.Con.conclude_method = "Intros+LetTac" || conclude.Con.conclude_method = "ByInduction" @@ -286,7 +291,7 @@ and proof2pres is_top_down term2pres p = ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else []) in B.V ([], [conclude_body; ann_concl]) - | _ -> conclude_aux conclude + | _ -> conclude_aux ?skip_initial_lambdas_internal conclude in if indent then B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], @@ -294,7 +299,7 @@ and proof2pres is_top_down term2pres p = else B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - and conclude_aux conclude = + and conclude_aux ?skip_initial_lambdas_internal conclude = if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with @@ -333,7 +338,7 @@ and proof2pres is_top_down term2pres p = ) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2pres true p false + [Con.ArgProof p] -> proof2pres ?skip_initial_lambdas_internal true p false | _ -> assert false) (* OLD CODE let conclusion = @@ -385,14 +390,19 @@ and proof2pres is_top_down term2pres p = *) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = - let j1,j2 = justification term2pres p in + if skip_initial_lambdas <> None (* cheating *) then + [B.b_kw "by _"] + else + let j1,j2 = justification term2pres p in j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> []) in let rec aux args = match args with | [] -> [] | (Con.ArgProof p)::(Con.Term t)::tl -> - B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl) + B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw + "=";B.b_space;term2pres t;B.b_space]@justification p@ + (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl) | _ -> assert false in let hd = @@ -400,7 +410,7 @@ and proof2pres is_top_down term2pres p = | Con.Term t -> t | _ -> assert false in - B.HOV([],[term2pres hd; (* B.b_space; *) + B.HOV([],[B.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *) B.V ([],aux (List.tl conclude.Con.conclude_args))]) else if conclude.Con.conclude_method = "Apply" then let pres_args = @@ -682,7 +692,7 @@ and proof2pres is_top_down term2pres p = | _ -> assert false in - proof2pres is_top_down p false + proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas is_top_down p false exception ToDo @@ -798,16 +808,24 @@ let joint_def2pres term2pres def = | `Inductive ind -> inductive2pres term2pres ind | _ -> assert false (* ZACK or raise ToDo? *) -let content2pres term2pres (id,params,metasenv,obj) = +let content2pres + ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres + (id,params,metasenv,obj) += match obj with | `Def (Content.Const, thesis, `Proof p) -> let name = get_name p.Content.proof_name in + let proof = proof2pres true term2pres ?skip_initial_lambdas p in + if skip_thm_and_qed then + proof + else B.b_v [Some "helm","xref","id"] - ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]); + ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: + params2pres params @ [B.b_kw ":"]); B.indent (term2pres thesis) ; B.b_kw "." ] @ metasenv2pres term2pres metasenv @ - [proof2pres true term2pres p ; B.b_kw "qed."]) + [proof ; B.b_kw "qed."]) | `Def (_, ty, `Definition body) -> let name = get_name body.Content.def_name in B.b_v @@ -834,8 +852,10 @@ let content2pres term2pres (id,params,metasenv,obj) = :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) | _ -> raise ToDo -let content2pres ~ids_to_inner_sorts = - content2pres +let content2pres + ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts += + content2pres ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts annterm diff --git a/helm/software/components/content_pres/content2pres.mli b/helm/software/components/content_pres/content2pres.mli index 793c31a4f..6dd0fd8aa 100644 --- a/helm/software/components/content_pres/content2pres.mli +++ b/helm/software/components/content_pres/content2pres.mli @@ -33,6 +33,7 @@ (**************************************************************************) val content2pres: + ?skip_initial_lambdas:bool -> ?skip_thm_and_qed:bool -> ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.cobj -> CicNotationPres.boxml_markup diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 0b8bbd1bc..3cfaff526 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -150,7 +150,7 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = let bobj = CicNotationPres.box_of_mpres ( CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast) + (TermContentPres.pp_ast ast) ) in let render = function _::x::_ -> x | _ -> assert false in @@ -166,34 +166,39 @@ let txt_of_cic_object let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in - aobj, ids_to_inner_sorts, ids_to_inner_types + aobj, ids_to_inner_sorts, ids_to_inner_types with e -> let msg = "txt_of_cic_object: " ^ Printexc.to_string e in - failwith msg + failwith msg in match style with | G.Declarative -> let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in - let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in - let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in + let cobj = + Acic2content.annobj2content + ids_to_inner_sorts ids_to_inner_types aobj + in + let bobj = + Content2pres.content2pres + ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj + in remove_closed_substs ("\n\n" ^ - BoxPp.render_to_string ?map_unicode_to_tex + BoxPp.render_to_string ?map_unicode_to_tex (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) - ) + ) | G.Procedural depth -> let obj = ProceduralOptimizer.optimize_obj obj in - let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in + let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in let term_pp = term2pres (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 ~term_pp ~lazy_term_pp ~obj_pp in - let script = + let script = Acic2Procedural.acic2procedural - ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed - ?skip_initial_lambdas prefix aobj + ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj in - String.concat "" (List.map aux script) ^ "\n\n" + String.concat "" (List.map aux script) ^ "\n\n" let txt_of_inline_macro style suri prefix = let print_exc = function @@ -208,7 +213,7 @@ let txt_of_inline_macro style suri prefix = (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) with | e -> - Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" - (UriManager.string_of_uri uri) (print_exc e) + Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" + (UriManager.string_of_uri uri) (print_exc e) in String.concat "" (List.map map sorted_uris) diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 63c3beedf..170980cb0 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -68,7 +68,8 @@ val txt_of_cic_sequent_conclusion: (* columns, rendering style, name prefix, object *) val txt_of_cic_object: ?map_unicode_to_tex:bool -> - ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool -> + ?skip_thm_and_qed:bool -> + ?skip_initial_lambdas:bool -> int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index c6f21c3f6..e446b67f5 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -548,9 +548,26 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Auto.revision time size depth in let proof_script = - if List.exists (fun (s,_) -> s = "paramodulation") params then - (* use declarative output *) - "Not supported yet" + if true (* List.exists (fun (s,_) -> s = "paramodulation") params *) then + let proof_term = + 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 + prerr_endline (CicPp.ppterm proof_term); + (* use declarative output *) + let obj = + (* il proof_term vive in cc, devo metterci i lambda no? *) + (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[])) + in + ApplyTransformation.txt_of_cic_object + ~map_unicode_to_tex:false + ~skip_thm_and_qed:true + ~skip_initial_lambdas:true + 80 GrafiteAst.Declarative "" obj else if true then (* use cic2grafite *) -- 2.39.2