X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=8fe5657b32feeb2cba52a68d8d704199f54d202e;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=ee11e9b6d76c36690c31a20474620bce5a842208;hpb=79d584e8f049226ec9cf68e9e06880ed0d95af51;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index ee11e9b6d..8fe5657b3 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -113,31 +113,43 @@ let make_args_for_apply term2pres args = (List.fold_right (make_arg_for_apply false) tl []) | _ -> assert false -let get_name = function +let get_name ?(default="_") = function | Some s -> s - | None -> "_" + | None -> default let add_xref id = function | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) -let rec justification term2pres p = - if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or - ((p.Con.proof_context = []) & - (p.Con.proof_apply_context = []) & - (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then +let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = + if p.Con.proof_conclude.Con.conclude_method = "Exact" && + ignore_atoms + then + [], None + else if + (p.Con.proof_conclude.Con.conclude_method = "Exact" && not ignore_atoms) || + (p.Con.proof_context = [] && + p.Con.proof_apply_context = [] && + p.Con.proof_conclude.Con.conclude_method = "Apply") + then let pres_args = - 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 + make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args + in + [B.H([], + (if for_rewriting_step then (B.b_kw "exact") else (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 true term2pres p])*) - proof2pres true term2pres p, None + [B.H([], + if for_rewriting_step then + [B.b_kw "proof"] + else + [B.b_kw "by"; B.b_space; B.b_kw "proof"] + )], + Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = - let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = + let rec proof2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion = let indent = let is_decl e = (match e with @@ -153,18 +165,20 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = let body = let presconclude = conclude2pres - ?skip_initial_lambdas_internal: - (match skip_initial_lambdas_internal with - Some (`Later s) -> Some (`Now s) - | _ -> None) - is_top_down - p.Con.proof_name p.Con.proof_conclude indent omit_conclusion - omit_dot in + ?skip_initial_lambdas_internal: + (match skip_initial_lambdas_internal with + Some (`Later s) -> Some (`Now s) + | _ -> None) + is_top_down p.Con.proof_name p.Con.proof_conclude indent + omit_conclusion in_bu_conversion in let presacontext = acontext2pres - (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") - p.Con.proof_apply_context - presconclude indent + (if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then + is_top_down + else + false) + p.Con.proof_apply_context + presconclude indent (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in context2pres @@ -173,6 +187,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> p.Con.proof_context) presacontext in +(* +let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in +*) match p.Con.proof_name with None -> body | Some name -> @@ -278,18 +295,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = [] -> in_bu_conversion | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" 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], + let hd = proof2pres is_top_down p in_bu_conversion in + let hd = if indent then B.indent hd else hd in + B.V([Some "helm","xref",p.Con.proof_id], [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation]) in aux ac - and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot = + and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion = let tconclude_body = match conclude.Con.conclude_conclusion with Some t (*when not omit_conclusion or @@ -336,19 +349,21 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = if conclude.Con.conclude_method = "Intros+LetTac" || conclude.Con.conclude_method = "ByInduction" || conclude.Con.conclude_method = "TD_Conversion" + || conclude.Con.conclude_method = "Eq_chain" then B.Text([],"") else if omit_conclusion then B.H([], [B.b_kw "done" ; B.Text([],".") ]) else B.b_hv [] - ((if not is_top_down || omit_dot then + ((if not is_top_down || in_bu_conversion then (make_concl "we proved" concl) :: if not is_top_down then - [B.b_space; B.Text([],"(previous)")] + let name = get_name ~default:"previous" name in + [B.b_space; B.Text([],"(" ^ name ^ ")")] else [] else [B.b_kw "done"] - ) @ if not omit_dot then [B.Text([],".")] else []) + ) @ if not in_bu_conversion then [B.Text([],".")] else []) in B.V ([], prequel @ [conclude_body; ann_concl]) | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude @@ -432,16 +447,37 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with - Con.ArgProof p -> justification term2pres p + Con.ArgProof p -> + justification ~for_rewriting_step:true ~ignore_atoms:true + term2pres p | _ -> assert false) in + let justif = + match justif2 with + None -> justif1 + | Some j -> [j] + in + let index_term1, index_term2 = + if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2 + in let term1 = - (match List.nth conclude.Con.conclude_args 2 with + (match List.nth conclude.Con.conclude_args index_term1 with Con.Term (_,t) -> term2pres t | _ -> assert false) in let term2 = - (match List.nth conclude.Con.conclude_args 5 with + (match List.nth conclude.Con.conclude_args index_term2 with Con.Term (_,t) -> term2pres t | _ -> assert false) in + let justif = + match justif with + [] -> [] + | _ -> + justif @ + [B.V([], + [B.b_kw "we proved (" ; + term1 ; + B.b_kw "=" ; + term2; B.b_kw ") (equality)."])] + in (* B.V ([], B.H ([],[ @@ -452,30 +488,23 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.b_space; justif1]):: match justif2 with None -> [] | Some j -> [B.indent j]) *) - if (conclude.Con.conclude_method = "RewriteLR" && is_top_down) - || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then - B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"]) - else - B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"]) -(*CSC: bad idea - B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1; B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *) + B.V([], justif @ [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 -> []) + let j1,j2 = + justification ~for_rewriting_step:true ~ignore_atoms:false term2pres p + in + j1, 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) + let justif1,justif2 = justification p in + B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw + "=";B.b_space;term2pres t;B.b_space]@justif1@ + (if tl <> [] then [B.Text ([],".")] else [B.b_space; B.b_kw "done" ; B.Text([],".")])@ + justif2))::(aux tl) | _ -> assert false in let hd = @@ -483,8 +512,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Con.Term (_,t) -> t | _ -> assert false in - B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *) - B.V ([],aux (List.tl conclude.Con.conclude_args))]) + if is_top_down then + B.HOV([], + [B.b_kw "conclude";B.b_space;term2pres hd; + B.V ([],aux (List.tl conclude.Con.conclude_args))]) + else + B.HOV([], + [B.b_kw "obtain";B.b_space;B.b_kw "FIXMEXX"; B.b_space;term2pres hd; + 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 @@ -524,7 +559,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.b_kw "the previous result" + None -> B.b_kw "previous" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> @@ -555,7 +590,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.b_kw "the previous result" + None -> B.b_kw "previous" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> @@ -780,7 +815,9 @@ let conjecture2pres term2pres (id, n, context, ty) = (B.b_hv [Some "helm", "xref", id] ((B.b_toggle [ B.b_h [] [B.b_text [] "{...}"; B.b_space]; - B.b_hv [] (List.map + B.b_hv [] (HExtlib.list_concat ~sep:[B.b_text [] ";"; B.b_space] + (List.map (fun x -> [x]) + (List.map (function | None -> B.b_h [] @@ -821,7 +858,7 @@ let conjecture2pres term2pres (id, n, context, ty) = | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); proof2pres true term2pres p]) - (List.rev context)) ] :: + (List.rev context)))) ] :: [ B.b_h [] [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); B.b_object (p_mi [] (string_of_int n)) ; @@ -860,8 +897,10 @@ let recursion_kind2pres params kind = match kind with | `Recursive _ -> "Recursive definition" | `CoRecursive -> "CoRecursive definition" - | `Inductive _ -> "Inductive definition" - | `CoInductive _ -> "CoInductive definition" + | `Inductive i -> + "Inductive definition with "^string_of_int i^" fixed parameter(s)" + | `CoInductive i -> + "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)" in B.b_h [] (B.b_kw kind :: params2pres params) @@ -935,7 +974,7 @@ let content2pres 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 + TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres (CicNotationPres.render ids_to_uris ~prec