X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=282cfe26ee1655329ab3600802211bc020f6dcf9;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=b9e89769472371c31b3a27e4ae8beedf1db53c49;hpb=b02253b371aadbbb37226a685b9bd8777a64d175;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index b9e897694..282cfe26e 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -121,7 +121,7 @@ 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 ~ignore_atoms term2pres p = +let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = if p.Con.proof_conclude.Con.conclude_method = "Exact" && ignore_atoms then @@ -136,10 +136,16 @@ let rec justification ~ignore_atoms term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in [B.H([], - (B.b_kw "by")::B.b_space:: + (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.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])], + [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 = @@ -441,7 +447,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = (match (List.nth conclude.Con.conclude_args 6) with - Con.ArgProof p -> justification ~ignore_atoms:true term2pres p + Con.ArgProof p -> + justification ~for_rewriting_step:true ~ignore_atoms:true + term2pres p | _ -> assert false) in let justif = match justif2 with @@ -483,7 +491,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.V([], justif @ [B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = - let j1,j2 = justification ~ignore_atoms:false term2pres p in + 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 = @@ -805,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 [] @@ -823,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) = (match dec_name with None -> "_" | Some n -> n)); - B.b_text [] ":"; + B.b_text [] ":"; B.b_space; term2pres ty ] | Some (`Definition d) -> let @@ -836,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + B.b_space; term2pres bo] | Some (`Proof p) -> let proof_name = p.Content.proof_name in @@ -845,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + B.b_space; proof2pres true term2pres p]) - (List.rev context)) ] :: + (List.rev context)))) ] :: [ B.b_h [] - [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + [ B.b_space; + B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + B.b_space; B.b_object (p_mi [] (string_of_int n)) ; B.b_text [] ":" ; + B.b_space; term2pres ty ]]))) let metasenv2pres term2pres = function @@ -885,8 +902,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) @@ -910,7 +929,7 @@ let joint_def2pres term2pres def = | `Inductive ind -> inductive2pres term2pres ind | _ -> assert false (* ZACK or raise ToDo? *) -let content2pres +let content2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres (id,params,metasenv,obj) = @@ -957,11 +976,24 @@ let content2pres let content2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts = - content2pres ?skip_initial_lambdas ?skip_thm_and_qed + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) annterm -> let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in CicNotationPres.box_of_mpres - (CicNotationPres.render ids_to_uris ~prec + (CicNotationPres.render + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec (TermContentPres.pp_ast ast))) + +let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = + let lookup_uri id = + try + let nref = Hashtbl.find ids_to_nrefs id in + Some (NReference.string_of_reference nref) + with Not_found -> None + in + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed + (fun ?(prec=90) ast -> + CicNotationPres.box_of_mpres + (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))