X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=e377706b7ddb69b49650306eb5a71180b0d9d6e6;hpb=621e13b0fb2be2367e80f71555732907da06ee31;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index e377706b7..72f51c5f8 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -97,8 +97,8 @@ let make_args_for_apply term2pres args = Some "xlink", "href", lemma.Con.lemma_uri ] in (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row - | Con.Term t -> - if is_first then + | Con.Term (b,t) -> + if is_first || (not b) then (term2pres t)::row else (B.b_object (P.Mi([],"?")))::row | Con.ArgProof _ @@ -113,29 +113,44 @@ 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 - else (B.b_kw "by"), - Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) + 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_kw "by"):: + B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")])], None + else + [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 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 is_top_down p in_bu_conversion = let indent = let is_decl e = (match e with @@ -150,16 +165,32 @@ 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 - omit_dot in + 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 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 p.Con.proof_context presacontext - in + context2pres + (match skip_initial_lambdas_internal with + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) + | _ -> 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 -> @@ -170,7 +201,9 @@ and proof2pres is_top_down term2pres p = let concl = make_concl ~attrs:[ Some "helm", "xref", p.Con.proof_id ] "proof of" ac in - B.b_toggle [ concl; body ] + B.b_toggle [ B.H ([], [concl; B.skip ; B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")") ]) ; body ] in B.indent action @@ -244,19 +277,33 @@ and proof2pres is_top_down term2pres p = 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 is_top_down p in_bu_conversion) - else - proof2pres is_top_down p in_bu_conversion + let rec aux = + function + [] -> continuation + | p::tl -> + let continuation = aux tl in + (* Applicative context get flattened and the "body" of a BU_Conversion + is put in the applicative context. Thus two different situations + are possible: + {method = "BU_Conversion"; applicative_context=[p1; ...; pn]} + {method = xxx; applicative_context = + [ p1; ...; pn; {method="BU_Conversion"} ; p_{n+1}; ... ; pm ]} + In both situations only pn must be processed in in_bu_conversion + mode + *) + let in_bu_conversion = + match tl with + [] -> in_bu_conversion + | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" in + 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])) ac continuation + [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); + continuation]) + in aux ac - and conclude2pres is_top_down 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 @@ -269,24 +316,58 @@ and proof2pres is_top_down term2pres p = if conclude.Con.conclude_method = "BU_Conversion" then B.b_hv [] (make_concl "that is equivalent to" concl :: - if is_top_down then [B.b_space ; B.Text([],"done.")] else []) + if is_top_down then [B.b_space ; B.b_kw "done"; + B.Text([],".")] else [B.Text([],".")]) 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 prequel = + if + (not is_top_down) && + conclude.Con.conclude_method = "Intros+LetTac" + then + let name = get_name name in + [B.V ([], + [ B.H([], + let expected = + (match conclude.Con.conclude_conclusion with + None -> B.Text([],"NO EXPECTED!!!") + | Some c -> term2pres c) + in + [make_concl "we need to prove" expected; + B.skip; + B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")"); + B.Text ([],".") + ])])] + else + [] in + let conclude_body = + conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in let ann_concl = 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.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 []) + else if omit_conclusion then + B.H([], [B.b_kw "done" ; B.Text([],".") ]) + else + B.b_hv [] + ((if not is_top_down || in_bu_conversion then + (make_concl "we proved" concl) :: + if not is_top_down then + let name = get_name ~default:"previous" name in + [B.b_space; B.Text([],"(" ^ name ^ ")")] + else [] + else [B.b_kw "done"] + ) @ if not in_bu_conversion then [B.Text([],".")] else []) in - B.V ([], [conclude_body; ann_concl]) - | _ -> conclude_aux conclude + B.V ([], prequel @ [conclude_body; ann_concl]) + | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in if indent then B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], @@ -294,7 +375,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 is_top_down conclude = if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with @@ -311,15 +392,14 @@ and proof2pres is_top_down term2pres p = B.V ([], [make_concl "we need to prove" expected; - make_concl "or equivalently" synth; - B.Text([],"."); + B.H ([],[make_concl "or equivalently" synth; 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 let arg = (match conclude.Con.conclude_args with - [Con.Term t] -> term2pres t + [Con.Term (b,t)] -> assert (not b);term2pres t | [Con.Premise p] -> (match p.Con.premise_binder with | None -> assert false; (* unnamed hypothesis ??? *) @@ -328,12 +408,16 @@ and proof2pres is_top_down term2pres p = (match conclude.Con.conclude_conclusion with None -> B.b_h [] [B.b_kw "by"; B.b_space; arg] - | Some c -> let conclusion = term2pres c in + | Some c -> 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 true p false + [Con.ArgProof p] -> + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> + proof2pres ?skip_initial_lambdas_internal true p false + | _ -> assert false) | _ -> assert false) (* OLD CODE let conclusion = @@ -360,19 +444,41 @@ and proof2pres is_top_down term2pres p = andind conclude else if (conclude.Con.conclude_method = "FalseInd") then falseind conclude - else if (conclude.Con.conclude_method = "Rewrite") then + else if conclude.Con.conclude_method = "RewriteLR" + || 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 - Con.Term t -> term2pres t + (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 - Con.Term t -> term2pres t + (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 ([],[ @@ -382,26 +488,39 @@ and proof2pres is_top_down term2pres p = 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 _"]) +*) + B.V([], justif @ [B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = - 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))::(aux tl) + | (Con.ArgProof p)::(Con.Term (_,t))::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 = match List.hd conclude.Con.conclude_args with - | Con.Term t -> t + | Con.Term (_,t) -> t | _ -> assert false in - B.HOV([],[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 @@ -421,7 +540,7 @@ and proof2pres is_top_down term2pres p = Con.Aux n -> B.b_kw ("aux " ^ n) | Con.Premise prem -> B.b_kw "premise" | Con.Lemma lemma -> B.b_kw "lemma" - | Con.Term t -> term2pres t + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> proof2pres true p false | Con.ArgMethod s -> B.b_kw "method" @@ -441,10 +560,10 @@ and proof2pres 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 -> + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> B.b_kw "a proof???" | Con.ArgMethod s -> B.b_kw "a method???") @@ -472,17 +591,17 @@ and proof2pres 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 -> + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> B.b_kw "a proof???" | Con.ArgMethod s -> B.b_kw "a method???") in (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:: B.Text([],".")::(make_cases args_for_cases)) + B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in + B.V ([], induction_on::to_prove::(make_cases args_for_cases)) and make_cases l = List.map make_case l @@ -546,10 +665,8 @@ and proof2pres is_top_down term2pres p = | _ -> 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 true p.Con.proof_conclude true true false in + conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in let presacontext = let acontext_id = match p.Con.proof_apply_context with @@ -563,7 +680,7 @@ and proof2pres is_top_down term2pres p = 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]) + B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext]) | _ -> assert false and falseind conclude = @@ -591,7 +708,6 @@ and proof2pres is_top_down 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} false in *) make_row arg proof_conclusion and andind conclude = @@ -629,8 +745,9 @@ and proof2pres is_top_down term2pres p = B.Text([],")"); B.skip; term2pres hyp2.Con.dec_type]) 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 body = + conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -669,8 +786,9 @@ and proof2pres is_top_down term2pres p = B.Text([],")"); B.skip; term2pres hyp.Con.dec_type]) 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 body = + conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -682,7 +800,12 @@ and proof2pres is_top_down term2pres p = | _ -> assert false in - proof2pres is_top_down p false + proof2pres + ?skip_initial_lambdas_internal: + (match skip_initial_lambdas with + None -> Some (`Later 0) (* we already printed theorem: *) + | Some n -> Some (`Later n)) + is_top_down p false exception ToDo @@ -693,7 +816,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 [] @@ -711,7 +836,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 @@ -724,6 +849,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 @@ -733,12 +859,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 @@ -773,10 +903,13 @@ 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) +;; let inductive2pres term2pres ind = let constructor2pres decl = @@ -793,21 +926,111 @@ let inductive2pres term2pres ind = term2pres ind.Content.inductive_type ] :: List.map constructor2pres ind.Content.inductive_constructors) -let joint_def2pres term2pres def = +let definition2pres ?recno term2pres d = + let name = match d.Content.def_name with Some x -> x|_->assert false in + let rno = match recno with None -> -1 (* cofix *) | Some x -> x in + let ty = d.Content.def_type in + let module P = CicNotationPt in + let rec split_pi i t = + if i <= 1 then + match t with + | P.Binder ((`Pi|`Forall),(var,_ as v),t) + | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> + [v], var, t + | _ -> assert false + else + match t with + | P.Binder ((`Pi|`Forall), var ,ty) + | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) -> + let l, r, t = split_pi (i-1) ty in + var :: l, r, t + | _ -> assert false + in + let params, rec_param, ty = split_pi rno ty in + let body = d.Content.def_term in + let params = + List.map + (function + | (name,Some ty) -> + B.b_h [] [B.b_text [] "("; term2pres name; B.b_text [] " : "; + B.b_space; term2pres ty; B.b_text [] ")"; B.b_space] + | (name,None) -> B.b_h [] [term2pres name;B.b_space]) + params + in + B.b_hv [] + [B.b_hov (RenderingAttrs.indent_attributes `BoxML) + ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ + [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] + @ [B.b_h [] + ((if rno <> -1 then + [B.b_kw "on";B.b_space;term2pres rec_param] else []) + @ [ B.b_space; B.b_text [] ":";]) ] + @[ B.indent(term2pres ty)]); + B.b_text [] ":="; + B.b_h [] [B.b_space;term2pres body] ] +;; + +let joint_def2pres ?recno term2pres def = match def with | `Inductive ind -> inductive2pres term2pres ind - | _ -> assert false (* ZACK or raise ToDo? *) + | _ -> assert false +;; -let content2pres term2pres (id,params,metasenv,obj) = +let njoint_def2pres ?recno term2pres def = + match def with + | `Inductive ind -> inductive2pres term2pres ind + | `Definition def -> definition2pres ?recno term2pres def + | _ -> assert false +;; + +let njoint_def2pres term2pres joint_kind defs = + match joint_kind with + | `Recursive recnos -> + B.b_hv [] (B.b_kw "nlet rec " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map2 (fun a b -> njoint_def2pres ~recno:a term2pres b) + recnos defs))) + | `CoRecursive -> + B.b_hv [] (B.b_kw "nlet corec " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) + | `Inductive _ -> + B.b_hv [] (B.b_kw "ninductive " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) + | `CoInductive _ -> + B.b_hv [] (B.b_kw "ncoinductive " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) +;; + +let content2pres0 + ?skip_initial_lambdas ?(skip_thm_and_qed=false) + (term2pres : ?prec:int -> 'a) + (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.indent (term2pres thesis) ; B.b_kw "." ] @ + ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: + params2pres params @ [B.b_kw ":"]); + B.H ([],[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 @@ -824,7 +1047,7 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name decl.Content.dec_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + ([B.b_h [] (B.b_kw ("axiom " ^ name) :: params2pres params); B.b_kw "Type:"; B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) @@ -834,12 +1057,73 @@ 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 += + content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed +(* FG: prec not optional in my patch *) (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 + (CicNotationPres.render + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec (TermContentPres.pp_ast ast))) + +let ncontent2pres0 + ?skip_initial_lambdas ?(skip_thm_and_qed=false) + (term2pres : ?prec:int -> 'a) + (id,params,metasenv,obj : CicNotationPt.term Content.cobj) += + 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 ("ntheorem " ^ name) :: + params2pres params @ [B.b_kw ":"]); + B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @ + metasenv2pres term2pres metasenv @ + [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 ("ndefinition " ^ name) :: params2pres params @ [B.b_kw ":"]); + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [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 + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("naxiom " ^ name) :: params2pres params); + B.b_kw "Type:"; + B.indent (term2pres decl.Content.dec_type)] @ + metasenv2pres term2pres metasenv) + | `Joint joint -> + B.b_v [] + [njoint_def2pres term2pres + joint.Content.joint_kind joint.Content.joint_defs] + | _ -> raise ToDo + +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 + ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed + (fun ?(prec=90) ast -> + CicNotationPres.box_of_mpres + (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))