X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2Fcontent2pres.ml;h=b9c46917c236c32006f0759a1b4fbc7b8c7c7dfa;hb=614e3c3fb219e404e60810bfc04072351803b8e8;hp=543ea0ac8436c8bc39bed6f31b74aeadcf587341;hpb=971a1e0f0c80f1165ff2c5ba956702f41819cac4;p=helm.git diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml index 543ea0ac8..b9c46917c 100644 --- a/components/content_pres/content2pres.ml +++ b/components/content_pres/content2pres.ml @@ -100,10 +100,10 @@ let make_args_for_apply term2pres args = | Con.Term t -> if is_first then (term2pres t)::row - else (B.b_object (P.Mi([],"_")))::row + else (B.b_object (P.Mi([],"?")))::row | Con.ArgProof _ | Con.ArgMethod _ -> - (B.b_object (P.Mi([],"_")))::row + (B.b_object (P.Mi([],"?")))::row in if is_first then res else B.skip::res in @@ -130,13 +130,13 @@ let rec justification term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in B.H([], (B.b_kw "by")::B.b_space:: - B.Text([],"(")::pres_args@[B.Text([],")")]), None - else - (B.b_kw "by"), - Some (B.b_toggle [B.b_kw "proof";proof2pres term2pres p]) + B.Text([],"(")::pres_args@[B.Text([],")")]), None + else (B.b_kw "by"), + Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) -and proof2pres term2pres p = - let rec proof2pres p = +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 @@ -151,10 +151,19 @@ and proof2pres term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres p.Con.proof_conclude indent omit_conclusion in + conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion + omit_dot in let presacontext = - acontext2pres p.Con.proof_apply_context presconclude indent in - context2pres p.Con.proof_context presacontext in + acontext2pres + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + p.Con.proof_apply_context + presconclude indent + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + 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 -> @@ -167,9 +176,7 @@ and proof2pres term2pres p = "proof of" ac in B.b_toggle [ concl; body ] in - B.V ([], - [B.Text ([],"(" ^ name ^ ")"); - B.indent action]) + B.indent action and context2pres c continuation = (* we generate a subtable for each context element, for selection @@ -203,96 +210,96 @@ and proof2pres term2pres p = and ce2pres_in_proof_context_element = function | `Joint ho -> B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs)) - | (`Declaration _) as x -> ce2pres x - | (`Hypothesis _) as x -> ce2pres x + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x | (`Proof _) as x -> ce2pres x - | (`Definition _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x - and ce2pres = + and ce2pres = function `Declaration d -> - (match d.Con.dec_name with - Some s -> - let ty = term2pres d.Con.dec_type in - B.H ([], - [(B.b_kw "Assume"); - B.b_space; - B.Object ([], P.Mi([],s)); - B.Text([],":"); - ty]) - | None -> - prerr_endline "NO NAME!!"; assert false) + let ty = term2pres d.Con.dec_type in + B.H ([], + [(B.b_kw "assume"); + B.b_space; + B.Object ([], P.Mi([],get_name d.Con.dec_name)); + B.Text([],":"); + ty; + B.Text([],".")]) | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> - let ty = term2pres h.Con.dec_type in - B.H ([], - [(B.b_kw "Suppose"); - B.b_space; - B.Text([],"("); - B.Object ([], P.Mi ([],s)); - B.Text([],")"); - B.b_space; - ty]) - | None -> - prerr_endline "NO NAME!!"; assert false) + let ty = term2pres h.Con.dec_type in + B.H ([], + [(B.b_kw "suppose"); + B.b_space; + ty; + B.b_space; + B.Text([],"("); + B.Object ([], P.Mi ([],get_name h.Con.dec_name)); + B.Text([],")"); + B.Text([],".")]) | `Proof p -> - proof2pres p + proof2pres false p false | `Definition d -> - (match d.Con.def_name with - Some s -> - let term = term2pres d.Con.def_term in - B.H ([], - [ B.b_kw "Let"; B.b_space; - B.Object ([], P.Mi([],s)); - B.Text([]," = "); - term]) - | None -> - prerr_endline "NO NAME!!"; assert false) - - and acontext2pres ac continuation indent = + let term = term2pres d.Con.def_term in + B.H ([], + [ B.b_kw "let"; B.b_space; + B.Object ([], P.Mi([],get_name d.Con.def_name)); + B.Text([],Utf8Macro.unicode_of_tex "\\def"); + term]) + + and acontext2pres is_top_down ac continuation indent in_bu_conversion = List.fold_right (fun p continuation -> - let hd = - if indent then - B.indent (proof2pres p) - else - proof2pres p in + let hd = + if indent then + B.indent (proof2pres is_top_down p in_bu_conversion) + else + proof2pres is_top_down p in_bu_conversion + in B.V([Some "helm","xref",p.Con.proof_id], [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation])) ac continuation - and conclude2pres conclude indent omit_conclusion = + 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 + Some t (*when not omit_conclusion or (* CSC: I ignore the omit_conclusion flag in this case. *) (* CSC: Is this the correct behaviour? In the stylesheets *) (* CSC: we simply generated nothing (i.e. the output type *) (* CSC: of the function should become an option. *) - conclude.Con.conclude_method = "BU_Conversion" -> - let concl = (term2pres t) in + conclude.Con.conclude_method = "BU_Conversion" *) -> + let concl = term2pres t in if conclude.Con.conclude_method = "BU_Conversion" then - make_concl "that is equivalent to" concl + B.b_hv [] + (make_concl "that is equivalent to" concl :: + if is_top_down then [B.b_space ; B.Text([],"done.")] else []) else if conclude.Con.conclude_method = "FalseInd" then (* 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 = "TD_Conversion" then - make_concl "that is equivalent to" concl - else make_concl "we conclude" concl in - B.V ([], [conclude_body; ann_concl]) - | _ -> conclude_aux conclude in - if indent then - B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], - [tconclude_body])) - else - B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) + if conclude.Con.conclude_method = "Intros+LetTac" + || conclude.Con.conclude_method = "ByInduction" + || conclude.Con.conclude_method = "TD_Conversion" + then + B.Text([],"") + else if omit_conclusion then B.Text([],"done.") + else B.b_hv [] + ((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 ?skip_initial_lambdas_internal conclude + in + if indent then + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], + [tconclude_body])) + 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 @@ -308,9 +315,10 @@ and proof2pres term2pres p = | Some c -> (term2pres c)) in B.V ([], - [make_concl "we must prove" expected; + [make_concl "we need to prove" expected; make_concl "or equivalently" synth; - proof2pres subproof]) + B.Text([],"."); + proof2pres true subproof false]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then @@ -324,15 +332,13 @@ and proof2pres term2pres p = | err -> assert false) in (match conclude.Con.conclude_conclusion with None -> - B.b_h [] [B.b_kw "Consider"; B.b_space; arg] + B.b_h [] [B.b_kw "by"; B.b_space; arg] | Some c -> let conclusion = term2pres c in - make_row - [arg; B.b_space; B.b_kw "proves"] - conclusion + B.b_h [] [B.b_kw "by"; B.b_space; arg] ) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2pres p + [Con.ArgProof p] -> proof2pres ?skip_initial_lambdas_internal true p false | _ -> assert false) (* OLD CODE let conclusion = @@ -344,7 +350,7 @@ and proof2pres term2pres p = B.V ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [B.H([],[B.Object([],proof2pres p)]); + [B.H([],[B.Object([],proof2pres p false)]); B.H([],[B.Object([], (make_concl "we proved 1" conclusion))])]); | _ -> assert false) @@ -360,7 +366,7 @@ and proof2pres term2pres p = else if (conclude.Con.conclude_method = "FalseInd") then falseind conclude else if (conclude.Con.conclude_method = "Rewrite") then - let justif1, justif2 = + let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with Con.ArgProof p -> justification term2pres p | _ -> assert false) in @@ -372,14 +378,40 @@ and proof2pres term2pres p = (match List.nth conclude.Con.conclude_args 5 with Con.Term t -> term2pres t | _ -> assert false) in +(* B.V ([], B.H ([],[ (B.b_kw "rewrite"); B.b_space; term1; B.b_space; (B.b_kw "with"); - B.b_space; term2; - B.b_space; justif1]) :: - match justif2 with None -> [] | Some j -> [B.indent j]) + B.b_space; term2; + B.b_space; justif1]):: + match justif2 with None -> [] | Some j -> [B.indent j]) +*) 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 = + 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@ + (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl) + | _ -> assert false + in + let hd = + match List.hd conclude.Con.conclude_args with + | Con.Term t -> t + | _ -> assert false + in + 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 = make_args_for_apply term2pres conclude.Con.conclude_args in @@ -400,7 +432,7 @@ and proof2pres term2pres p = | Con.Premise prem -> B.b_kw "premise" | Con.Lemma lemma -> B.b_kw "lemma" | Con.Term t -> term2pres t - | Con.ArgProof p -> proof2pres p + | Con.ArgProof p -> proof2pres true p false | Con.ArgMethod s -> B.b_kw "method" and case conclude = @@ -460,7 +492,7 @@ and proof2pres term2pres p = (make_concl "we proceed by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V ([], induction_on::to_prove:: (make_cases args_for_cases)) + B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases)) and make_cases l = List.map make_case l @@ -483,21 +515,20 @@ and proof2pres term2pres p = (match e with `Declaration h | `Hypothesis h -> - let name = - (match h.Con.dec_name with - None -> "NO NAME???" - | Some n ->n) in + let name = get_name h.Con.dec_name in [B.b_space; + B.Text([],"("); B.Object ([], P.Mi ([],name)); B.Text([],":"); - (term2pres h.Con.dec_type)] - | _ -> [B.Text ([],"???")]) in + (term2pres h.Con.dec_type); + B.Text([],")")] + | _ -> assert false (*[B.Text ([],"???")]*)) in dec@p) args [] in let pattern = B.H ([], - (B.b_kw "Case"::B.b_space::name::pattern_aux)@ + (B.b_kw "case"::B.b_space::name::pattern_aux)@ [B.b_space; - B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in + B.Text([], ".")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with None -> B.b_kw "No conclusion!!!" @@ -513,20 +544,22 @@ and proof2pres term2pres p = `Hypothesis h -> let name = (match h.Con.dec_name with - None -> "no name" + None -> "useless" | Some s -> s) in B.indent (B.H ([], - [B.Text([],"("); + [term2pres h.Con.dec_type; + B.b_space; + B.Text([],"("); B.Object ([], P.Mi ([],name)); B.Text([],")"); - B.b_space; - term2pres h.Con.dec_type])) + B.Text([],".")])) | _ -> assert false in let hyps = List.map make_hyp indhyps in text::hyps) in (* let acontext = acontext2pres_old p.Con.proof_apply_context true in *) - let body = conclude2pres p.Con.proof_conclude true false in + let body = + conclude2pres true p.Con.proof_conclude true true false in let presacontext = let acontext_id = match p.Con.proof_apply_context with @@ -535,8 +568,12 @@ and proof2pres term2pres p = in B.Action([None,"type","toggle"], [ B.indent (add_xref acontext_id (B.b_kw "Proof")); - acontext2pres p.Con.proof_apply_context body true]) in - B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) + acontext2pres + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + p.Con.proof_apply_context body true + (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") + ]) in + B.V ([], pattern::induction_hypothesis@[asubconcl;B.Text([],".");presacontext]) | _ -> assert false and falseind conclude = @@ -564,7 +601,7 @@ and proof2pres term2pres p = [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.b_kw "is contradictory, hence" ] | _ -> assert false) in - (* let body = proof2pres {proof with Con.proof_context = tl} in *) + (* let body = proof2pres {proof with Con.proof_context = tl} false in *) make_row arg proof_conclusion and andind conclude = @@ -588,28 +625,25 @@ and proof2pres term2pres p = | _ -> assert false) in match proof.Con.proof_context with `Hypothesis hyp1::`Hypothesis hyp2::tl -> - let get_name hyp = - (match hyp.Con.dec_name with - None -> "_" - | Some s -> s) in let preshyp1 = B.H ([], [B.Text([],"("); - B.Object ([], P.Mi([],get_name hyp1)); + B.Object ([], P.Mi([],get_name hyp1.Con.dec_name)); B.Text([],")"); B.skip; term2pres hyp1.Con.dec_type]) in let preshyp2 = B.H ([], [B.Text([],"("); - B.Object ([], P.Mi([],get_name hyp2)); + B.Object ([], P.Mi([],get_name hyp2.Con.dec_name)); B.Text([],")"); B.skip; term2pres hyp2.Con.dec_type]) in - (* let body = proof2pres {proof with Con.proof_context = tl} in *) - let body = conclude2pres proof.Con.proof_conclude false true in + (* let body = proof2pres {proof with Con.proof_context = tl} false in *) + let body= conclude2pres false proof.Con.proof_conclude false true false in let presacontext = - acontext2pres proof.Con.proof_apply_context body false in + acontext2pres false proof.Con.proof_apply_context body false false + in B.V ([], [B.H ([],arg@[B.skip; B.b_kw "we have"]); @@ -630,29 +664,26 @@ and proof2pres term2pres p = match proof.Con.proof_context with `Declaration decl::`Hypothesis hyp::tl | `Hypothesis decl::`Hypothesis hyp::tl -> - let get_name decl = - (match decl.Con.dec_name with - None -> "_" - | Some s -> s) in let presdecl = B.H ([], [(B.b_kw "let"); B.skip; - B.Object ([], P.Mi([],get_name decl)); + B.Object ([], P.Mi([],get_name decl.Con.dec_name)); B.Text([],":"); term2pres decl.Con.dec_type]) in let suchthat = B.H ([], [(B.b_kw "such that"); B.skip; B.Text([],"("); - B.Object ([], P.Mi([],get_name hyp)); + B.Object ([], P.Mi([],get_name hyp.Con.dec_name)); B.Text([],")"); B.skip; term2pres hyp.Con.dec_type]) in - (* let body = proof2pres {proof with Con.proof_context = tl} in *) - let body = conclude2pres proof.Con.proof_conclude false true in + (* let body = proof2pres {proof with Con.proof_context = tl} false in *) + let body= conclude2pres false proof.Con.proof_conclude false true false in let presacontext = - acontext2pres proof.Con.proof_apply_context body false in + acontext2pres false proof.Con.proof_apply_context body false false + in B.V ([], [presdecl; @@ -661,7 +692,7 @@ and proof2pres term2pres p = | _ -> assert false in - proof2pres p + proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas is_top_down p false exception ToDo @@ -712,7 +743,7 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); - proof2pres term2pres p]) + proof2pres true term2pres p]) (List.rev context)) ] :: [ B.b_h [] [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); @@ -777,26 +808,35 @@ 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 ("Proof " ^ name) :: params2pres params); - B.b_kw "Thesis:"; - B.indent (term2pres thesis) ] @ + ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: + params2pres params @ [B.b_kw ":"]); + B.indent (term2pres thesis) ; B.b_kw "." ] @ metasenv2pres term2pres metasenv @ - [proof2pres term2pres p]) + [proof ; B.b_kw "qed."]) | `Def (_, ty, `Definition body) -> let name = get_name body.Content.def_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); - B.b_kw "Type:"; + ([B.b_h [] + (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]); B.indent (term2pres ty)] @ metasenv2pres term2pres metasenv @ - [B.b_kw "Body:"; term2pres body.Content.def_term]) + [B.b_kw ":="; + B.indent (term2pres body.Content.def_term); + B.b_kw "."]) | `Decl (_, `Declaration decl) | `Decl (_, `Hypothesis decl) -> let name = get_name decl.Content.dec_name in @@ -812,13 +852,14 @@ 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 - (fun annterm -> +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 in - CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris ~prec (TermContentPres.pp_ast ast))) -