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
(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 []
(match dec_name with
None -> "_"
| Some n -> n));
- B.b_text [] ":";
+ B.b_text [] ":"; B.b_space;
term2pres ty ]
| Some (`Definition d) ->
let
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
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
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 =
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
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)
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)))
projects / helm.git / blobdiff