| _ -> assert false
;;
+let get_name = function
+ | Some s -> s
+ | None -> "_"
+
let rec justification term2pres p =
let module Con = Content in
let module P = Mpresentation in
(fun ce continuation ->
let xref = get_xref ce in
B.V([Some "helm", "xref", xref ],
- [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]);
+ [B.H([Some "helm", "xref", "ce_"^xref],
+ [ce2pres_in_proof_context_element ce]);
continuation])) tl continuation in
let hd_xref= get_xref hd in
B.V([],
[B.H([Some "helm", "xref", "ce_"^hd_xref],
- [ce2pres hd]);
+ [ce2pres_in_proof_context_element hd]);
continuation'])
-
- and ce2pres =
+
+ and ce2pres_in_joint_context_element = function
+ | `Inductive _ -> assert false (* TODO *)
+ | (`Declaration _) as x -> ce2pres x
+ | (`Hypothesis _) as x -> ce2pres x
+ | (`Proof _) as x -> ce2pres x
+ | (`Definition _) as x -> ce2pres x
+
+ and ce2pres_in_proof_context_element = function
+ | `Joint ho ->
+ B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs))
+ | (`Declaration _) as x -> ce2pres x
+ | (`Hypothesis _) as x -> ce2pres x
+ | (`Proof _) as x -> ce2pres x
+ | (`Definition _) as x -> ce2pres x
+
+ and ce2pres =
let module Con = Content in
- function
+ function
`Declaration d ->
(match d.Con.dec_name with
Some s ->
term])
| None ->
prerr_endline "NO NAME!!"; assert false)
- | `Joint ho ->
- B.Text ([],"jointdef")
and acontext2pres ac continuation indent =
let module Con = Content in
let arg =
(match conclude.Con.conclude_args with
[Con.Term t] -> term2pres t
- | _ -> assert false) in
+ | [Con.Premise p] ->
+ (match p.Con.premise_binder with
+ | None -> assert false; (* unnamed hypothesis ??? *)
+ | Some s -> B.Text([],s))
+ | err -> assert false) in
(match conclude.Con.conclude_conclusion with
None ->
B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
B.Text ([],"a proof???")
| Con.ArgMethod s ->
B.Text ([],"a method???")) in
- (make_concl "we proceede by cases on" case_arg) in
+ (make_concl "we proceed by cases on" case_arg) in
let to_prove =
(make_concl "to prove" proof_conclusion) in
B.V
B.Text ([],"a proof???")
| Con.ArgMethod s ->
B.Text ([],"a method???")) in
- (make_concl "we proceede by induction on" arg) in
+ (make_concl "we proceed by induction on" arg) in
let to_prove =
(make_concl "to prove" proof_conclusion) in
B.V
(let _ = incr counter; in (string_of_int !counter)))) ::
(List.map (conjecture2pres term2pres) metasenv'))]
-let get_name = function
- | Some s -> s
- | None -> "_"
+let params2pres params =
+ let param2pres uri =
+ B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
+ (UriManager.name_of_uri uri)
+ in
+ let rec spatiate = function
+ | [] -> []
+ | hd :: [] -> [hd]
+ | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
+ in
+ match params with
+ | [] -> []
+ | p ->
+ let params = spatiate (List.map param2pres p) in
+ [B.b_space;
+ B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
+
+let recursion_kind2pres params kind =
+ let kind =
+ match kind with
+ | `Recursive _ -> "Recursive definition"
+ | `CoRecursive -> "CoRecursive definition"
+ | `Inductive _ -> "Inductive definition"
+ | `CoInductive _ -> "CoInductive definition"
+ in
+ B.b_h [] (B.b_text [] kind :: params2pres params)
+
+let inductive2pres term2pres ind =
+ let constructor2pres decl =
+ B.b_h [] [
+ B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
+ B.b_space;
+ term2pres decl.Content.dec_type
+ ]
+ in
+ B.b_v []
+ (B.b_h [] [
+ B.b_text [] (ind.Content.inductive_name ^ " of arity ");
+ term2pres ind.Content.inductive_type ]
+ :: List.map constructor2pres ind.Content.inductive_constructors)
-let pp_params = function
- | [] -> ""
- | params ->
- " (" ^
- String.concat " ; " (List.map UriManager.string_of_uri params) ^
- ")"
+let joint_def2pres term2pres def =
+ match def with
+ | `Inductive ind -> inductive2pres term2pres ind
+ | _ -> assert false (* ZACK or raise ToDo? *)
let content2pres term2pres (id,params,metasenv,obj) =
match obj with
| `Def (Content.Const, thesis, `Proof p) ->
let name = get_name p.Content.proof_name in
B.b_v
- [None,"helm:xref","id"]
- ([ B.b_text [] ("Proof " ^ name ^ pp_params params);
+ [Some "helm","xref","id"]
+ ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params);
B.b_text [] "Thesis:";
B.indent (term2pres thesis) ] @
metasenv2pres term2pres metasenv @
| `Def (_, ty, `Definition body) ->
let name = get_name body.Content.def_name in
B.b_v
- [None,"helm:xref","id"]
- ([B.b_text [] ("Definition " ^ name ^ pp_params params);
+ [Some "helm","xref","id"]
+ ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params);
B.b_text [] "Type:";
B.indent (term2pres ty)] @
metasenv2pres term2pres metasenv @
| `Decl (_, `Hypothesis decl) ->
let name = get_name decl.Content.dec_name in
B.b_v
- [None,"helm:xref","id"]
- ([B.b_text [] ("Axiom " ^ name ^ pp_params params);
+ [Some "helm","xref","id"]
+ ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params);
B.b_text [] "Type:";
B.indent (term2pres decl.Content.dec_type)] @
metasenv2pres term2pres metasenv)
+ | `Joint joint ->
+ B.b_v []
+ (recursion_kind2pres params joint.Content.joint_kind
+ :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
| _ -> raise ToDo
;;