X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=a41ccc99158a73562218887d2d786e57d903121e;hb=66929b8edb58d468a134b648466f3e9c45ba5c0e;hp=b9c46917c236c32006f0759a1b4fbc7b8c7c7dfa;hpb=36809208fa25a494e50004b321fa9a90108ae262;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index b9c46917c..a41ccc991 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 _ @@ -135,8 +135,7 @@ let rec justification term2pres p = Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres 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 rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = let indent = let is_decl e = (match e with @@ -151,7 +150,13 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion + 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 let presacontext = acontext2pres @@ -161,7 +166,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in context2pres - (if skip_initial_lambdas_internal then [] else p.Con.proof_context) + (match skip_initial_lambdas_internal with + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) + | _ -> p.Con.proof_context) presacontext in match p.Con.proof_name with @@ -174,7 +181,9 @@ and proof2pres ?skip_initial_lambdas 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 @@ -260,7 +269,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation])) ac continuation - and conclude2pres ?skip_initial_lambdas_internal is_top_down conclude indent omit_conclusion omit_dot = + and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot = let tconclude_body = match conclude.Con.conclude_conclusion with Some t (*when not omit_conclusion or @@ -273,11 +282,37 @@ and proof2pres ?skip_initial_lambdas 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 []) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) falseind conclude else + let prequel = + if + (match skip_initial_lambdas_internal with + None + | Some (`Later _) -> true + | Some (`Now _) -> false) + && 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 conclude in let ann_concl = @@ -286,11 +321,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = || conclude.Con.conclude_method = "TD_Conversion" then B.Text([],"") - else if omit_conclusion then B.Text([],"done.") + 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 [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 []) + ((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.b_kw "done"]) @ if not omit_dot then [B.Text([],".")] else []) in - B.V ([], [conclude_body; ann_concl]) + B.V ([], prequel @ [conclude_body; ann_concl]) | _ -> conclude_aux ?skip_initial_lambdas_internal conclude in if indent then @@ -324,7 +362,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = 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 ??? *) @@ -333,12 +371,16 @@ and proof2pres ?skip_initial_lambdas 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 ?skip_initial_lambdas_internal 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 = @@ -372,11 +414,11 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> assert false) in let term1 = (match List.nth conclude.Con.conclude_args 2 with - Con.Term t -> term2pres t + Con.Term (_,t) -> term2pres t | _ -> assert false) in let term2 = (match List.nth conclude.Con.conclude_args 5 with - Con.Term t -> term2pres t + Con.Term (_,t) -> term2pres t | _ -> assert false) in (* B.V ([], @@ -390,16 +432,18 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = *) 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 -> + | (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) @@ -407,10 +451,10 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = in let hd = match List.hd conclude.Con.conclude_args with - | Con.Term t -> t + | Con.Term (_,t) -> t | _ -> assert false in - B.HOV([],[B.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *) + B.HOV([],[B.b_kw "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 = @@ -431,7 +475,7 @@ and proof2pres ?skip_initial_lambdas 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" @@ -454,7 +498,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = None -> B.b_kw "the previous result" | 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???") @@ -485,7 +529,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = None -> B.b_kw "the previous result" | 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 @@ -559,7 +603,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (* 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 @@ -640,7 +684,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = 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 @@ -680,7 +724,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = 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 @@ -692,7 +736,12 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> assert false in - proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas 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