| 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 ~ignore_atoms term2pres p =
+let rec justification ~for_rewriting_step ~ignore_atoms term2pres p =
if p.Con.proof_conclude.Con.conclude_method = "Exact" &&
ignore_atoms
then
make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
in
[B.H([],
- (B.b_kw "by")::B.b_space::
+ (*(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([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])],
+ [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 ?skip_initial_lambdas is_top_down term2pres p =
| _ -> 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 ->
|| conclude.Con.conclude_method = "RewriteRL" then
let justif1,justif2 =
(match (List.nth conclude.Con.conclude_args 6) with
- Con.ArgProof p -> justification ~ignore_atoms:true term2pres p
+ Con.ArgProof p ->
+ justification ~for_rewriting_step:true ~ignore_atoms:true
+ term2pres p
| _ -> assert false) in
let justif =
match justif2 with
| Some j -> [j]
in
let index_term1, index_term2 =
- if (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
- || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
- then 2,5 else 5,2
+ if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
in
let term1 =
(match List.nth conclude.Con.conclude_args index_term1 with
B.V([], justif @ [B.b_kw "by _"])
else if conclude.Con.conclude_method = "Eq_chain" then
let justification p =
- let j1,j2 = justification ~ignore_atoms:false term2pres p in
+ 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 =
(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 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)))
projects / helm.git / blobdiff