X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=6606b088be10f49c8ae12fa60a3727cd88751a60;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=6d8031d85b4e67d3f71b1001d224f02db92ede61;hpb=a4a2345e2efaf4cc64aa4daf40e2bce05a400f12;p=helm.git diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index 6d8031d85..6606b088b 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -46,6 +46,7 @@ let p_mi a b = Mpresentation.Mi(a,b) let p_mo a b = Mpresentation.Mo(a,b) let p_mrow a b = Mpresentation.Mrow(a,b) let p_mphantom a b = Mpresentation.Mphantom(a,b) +let b_ink a = Box.Ink a let rec split n l = if n = 0 then [],l @@ -149,8 +150,7 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = )], 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 in_bu_conversion = +and proof2pres0 term2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion = let indent = let is_decl e = (match e with @@ -165,7 +165,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres + conclude2pres term2pres ?skip_initial_lambdas_internal: (match skip_initial_lambdas_internal with Some (`Later s) -> Some (`Now s) @@ -173,7 +173,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = is_top_down p.Con.proof_name p.Con.proof_conclude indent omit_conclusion in_bu_conversion in let presacontext = - acontext2pres + acontext2pres term2pres (if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then is_top_down else @@ -182,11 +182,11 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = presconclude indent (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in - context2pres + context2pres term2pres (match skip_initial_lambdas_internal with Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) | _ -> p.Con.proof_context) - presacontext + ~continuation: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 @@ -207,7 +207,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( in B.indent action - and context2pres c continuation = +and context2pres term2pres c ~continuation = (* we generate a subtable for each context element, for selection purposes The table generated by the head-element does not have an xref; @@ -221,30 +221,30 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( let xref = get_xref ce in B.V([Some "helm", "xref", xref ], [B.H([Some "helm", "xref", "ce_"^xref], - [ce2pres_in_proof_context_element ce]); + [ce2pres_in_proof_context_element term2pres ce]); continuation])) tl continuation in let hd_xref= get_xref hd in B.V([], [B.H([Some "helm", "xref", "ce_"^hd_xref], - [ce2pres_in_proof_context_element hd]); + [ce2pres_in_proof_context_element term2pres hd]); continuation']) - and ce2pres_in_joint_context_element = function +and ce2pres_in_joint_context_element term2pres = function | `Inductive _ -> assert false (* TODO *) - | (`Declaration _) as x -> ce2pres x - | (`Hypothesis _) as x -> ce2pres x - | (`Proof _) as x -> ce2pres x - | (`Definition _) as x -> ce2pres x + | (`Declaration _) + | (`Hypothesis _) + | (`Proof _) + | (`Definition _) as x -> ce2pres term2pres x - and ce2pres_in_proof_context_element = function +and ce2pres_in_proof_context_element term2pres = 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 - | (`Proof _) as x -> ce2pres x - | (`Definition _) as x -> ce2pres x + B.H ([],(List.map (ce2pres_in_joint_context_element term2pres) ho.Content.joint_defs)) + | (`Declaration _) + | (`Hypothesis _) + | (`Proof _) + | (`Definition _) as x -> ce2pres term2pres x - and ce2pres = +and ce2pres term2pres = function `Declaration d -> let ty = term2pres d.Con.dec_type in @@ -267,7 +267,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.Text([],")"); B.Text([],".")]) | `Proof p -> - proof2pres false p false + proof2pres0 term2pres false p false | `Definition d -> let term = term2pres d.Con.def_term in B.H ([], @@ -276,7 +276,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.Text([],Utf8Macro.unicode_of_tex "\\def"); term]) - and acontext2pres is_top_down ac continuation indent in_bu_conversion = +and acontext2pres term2pres is_top_down ac continuation indent in_bu_conversion = let rec aux = function [] -> continuation @@ -296,14 +296,14 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( [] -> 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 = proof2pres0 term2pres 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 in_bu_conversion = +and conclude2pres term2pres ?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 @@ -320,7 +320,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.Text([],".")] else [B.Text([],".")]) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) - falseind conclude + falseind term2pres conclude else let prequel = if @@ -345,7 +345,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( else [] in let conclude_body = - conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in + conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude in let ann_concl = if conclude.Con.conclude_method = "Intros+LetTac" || conclude.Con.conclude_method = "ByInduction" @@ -367,7 +367,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( ) @ 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 + | _ -> conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude in if indent then B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], @@ -375,7 +375,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( else B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - and conclude_aux ?skip_initial_lambdas_internal is_top_down conclude = +and conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude = if conclude.Con.conclude_method = "TD_Conversion" then let expected = (match conclude.Con.conclude_conclusion with @@ -393,7 +393,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( ([], [make_concl "we need to prove" expected; B.H ([],[make_concl "or equivalently" synth; B.Text([],".")]); - proof2pres true subproof false]) + proof2pres0 term2pres true subproof false]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false else if conclude.Con.conclude_method = "Exact" then @@ -416,7 +416,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( [Con.ArgProof p] -> (match conclude.Con.conclude_args with [Con.ArgProof p] -> - proof2pres ?skip_initial_lambdas_internal true p false + proof2pres0 term2pres ?skip_initial_lambdas_internal true p false | _ -> assert false) | _ -> assert false) (* OLD CODE @@ -429,21 +429,21 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.V ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [B.H([],[B.Object([],proof2pres p false)]); + [B.H([],[B.Object([],proof2pres p term2pres false)]); B.H([],[B.Object([], (make_concl "we proved 1" conclusion))])]); | _ -> assert false) *) else if (conclude.Con.conclude_method = "Case") then - case conclude + case term2pres conclude else if (conclude.Con.conclude_method = "ByInduction") then - byinduction conclude + byinduction term2pres conclude else if (conclude.Con.conclude_method = "Exists") then - exists conclude + exists term2pres conclude else if (conclude.Con.conclude_method = "AndInd") then - andind conclude + andind term2pres conclude else if (conclude.Con.conclude_method = "FalseInd") then - falseind conclude + falseind term2pres conclude else if conclude.Con.conclude_method = "RewriteLR" || conclude.Con.conclude_method = "RewriteRL" then let justif1,justif2 = @@ -531,20 +531,20 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( else B.V ([], [ B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to"); - (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))]) + (B.indent (B.V ([], args2pres term2pres conclude.Con.conclude_args)))]) - and args2pres l = List.map arg2pres l +and args2pres term2pres l = List.map (arg2pres term2pres) l - and arg2pres = +and arg2pres term2pres = function 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.ArgProof p -> proof2pres true p false + | Con.ArgProof p -> proof2pres0 term2pres true p false | Con.ArgMethod s -> B.b_kw "method" - and case conclude = +and case term2pres conclude = let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> B.b_kw "No conclusion???" @@ -571,9 +571,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( (make_concl "we proceed by cases on" case_arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V ([], case_on::to_prove::(make_cases args_for_cases)) + B.V ([], case_on::to_prove::(make_cases term2pres args_for_cases)) - and byinduction conclude = +and byinduction term2pres conclude = let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> B.b_kw "No conclusion???" @@ -601,11 +601,11 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( (make_concl "we proceed by induction on" arg) in let to_prove = B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in - B.V ([], induction_on::to_prove::(make_cases args_for_cases)) + B.V ([], induction_on::to_prove::(make_cases term2pres args_for_cases)) - and make_cases l = List.map make_case l +and make_cases term2pres l = List.map (make_case term2pres) l - and make_case = +and make_case term2pres = function Con.ArgProof p -> let name = @@ -666,7 +666,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( let hyps = List.map make_hyp indhyps in text::hyps) in let body = - conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in + conclude2pres term2pres 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 @@ -675,7 +675,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( in B.Action([None,"type","toggle"], [ B.indent (add_xref acontext_id (B.b_kw "Proof")); - acontext2pres + acontext2pres term2pres (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") @@ -683,7 +683,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext]) | _ -> assert false - and falseind conclude = +and falseind term2pres conclude = let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> B.b_kw "No conclusion???" @@ -710,7 +710,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( | _ -> assert false) in make_row arg proof_conclusion - and andind conclude = +and andind term2pres conclude = let proof,case_arg = (match conclude.Con.conclude_args with [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg @@ -746,10 +746,10 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.skip; term2pres hyp2.Con.dec_type]) in let body = - conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + conclude2pres term2pres 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 + acontext2pres term2pres false proof.Con.proof_apply_context body false false in B.V ([], @@ -760,7 +760,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( presacontext]); | _ -> assert false - and exists conclude = +and exists term2pres conclude = let proof = (match conclude.Con.conclude_args with [Con.Aux(n);_;Con.ArgProof proof;_] -> proof @@ -787,10 +787,10 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( B.skip; term2pres hyp.Con.dec_type]) in let body = - conclude2pres false proof.Con.proof_name proof.Con.proof_conclude + conclude2pres term2pres 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 + acontext2pres term2pres false proof.Con.proof_apply_context body false false in B.V ([], @@ -799,13 +799,13 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( presacontext]); | _ -> assert false - in - 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 +and proof2pres ?skip_initial_lambdas is_top_down term2pres p = + proof2pres0 term2pres + ?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 @@ -976,14 +976,14 @@ let njoint_def2pres term2pres joint_kind defs = (List.map (njoint_def2pres term2pres) defs))) ;; -let ncontent2pres0 +let nobj2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres (id,metasenv,obj : NotationPt.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 + let proof = proof2pres true ?skip_initial_lambdas term2pres p in if skip_thm_and_qed then proof else @@ -1020,15 +1020,75 @@ let ncontent2pres0 joint.Content.joint_kind joint.Content.joint_defs] | _ -> raise ToDo -let ncontent2pres status ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = +let nterm2pres status ~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 status ast))) + fun ?(prec=90) ast -> + CicNotationPres.box_of_mpres + (CicNotationPres.render status ~lookup_uri ~prec + (TermContentPres.pp_ast status ast)) + +let nobj2pres status ~ids_to_nrefs = + nobj2pres0 ?skip_initial_lambdas:None ?skip_thm_and_qed:None + (nterm2pres status ~ids_to_nrefs) + +let nconjlist2pres0 term2pres context = + let rec aux accum = + function + [] -> accum + | None::tl -> aux accum tl + | (Some (`Declaration d))::tl -> + let + { Con.dec_name = dec_name ; + Con.dec_id = dec_id ; + Con.dec_type = ty } = d in + let r = + Box.b_h [Some "helm", "xref", dec_id] + [ Box.b_object (p_mi [] + (match dec_name with + None -> "_" + | Some n -> n)) ; + Box.b_space; Box.b_text [] ":"; Box.b_space; + term2pres ty] in + aux (r::accum) tl + | (Some (`Definition d))::tl -> + let + { Con.def_name = def_name ; + Con.def_id = def_id ; + Con.def_term = bo } = d in + let r = + Box.b_h [Some "helm", "xref", def_id] + [ Box.b_object (p_mi [] + (match def_name with + None -> "_" + | Some n -> n)) ; Box.b_space ; + Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ; + Box.b_space; term2pres bo] in + aux (r::accum) tl + | _::_ -> assert false + in + if context <> [] then [Box.b_v [] (aux [] context)] else [] + +let sequent2pres0 term2pres (_,_,context,ty) = + let pres_context = nconjlist2pres0 term2pres context in + let pres_goal = term2pres ty in + (Box.b_h [] [ + Box.b_space; + (Box.b_v [] + (Box.b_space :: + pres_context @ [ + b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *) + Box.b_space; + pres_goal]))]) + +let ncontext2pres status ~ids_to_nrefs ctx = + let ctx = HExtlib.filter_map (fun x -> x) ctx in + context2pres (nterm2pres status ~ids_to_nrefs) ~continuation:Box.smallskip + (ctx:>NotationPt.term Con.in_proof_context_element list) + +let nsequent2pres status ~ids_to_nrefs = + sequent2pres0 (nterm2pres status ~ids_to_nrefs)