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=4d5ec86f5aff02446e9d0b6d44c6278b48991039;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 4d5ec86f5..72f51c5f8 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms 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")):: + (*(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 @@ -183,7 +184,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = in context2pres (match skip_initial_lambdas_internal with - Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context) + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) | _ -> p.Con.proof_context) presacontext in @@ -908,6 +909,7 @@ let recursion_kind2pres params kind = "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 = @@ -924,13 +926,95 @@ 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 - ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres +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 @@ -963,7 +1047,7 @@ let content2pres 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) @@ -976,11 +1060,70 @@ 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 +(* FG: prec not optional in my patch *) (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 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)))