"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 -> assert false | 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) -> [v], var, t
+ | _ -> assert false
+ else
+ match t with
+ | 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_hv []
+ ([ B.b_space; B.b_text [] name ] @ params @
+ [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
+ B.b_text [] ":"; B.b_space; 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
+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
(id,params,metasenv,obj)
=
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
(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
+ (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