Commit e9bd8564 authored by MARCHE Claude's avatar MARCHE Claude

doc: fixed generation of ocaml doc'

parent 740951f5
......@@ -845,12 +845,12 @@ FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
apidoc: $(FILESTODOC)
mkdir -p apidoc
$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
$(LIBINCLUDES) $(FILESTODOC)
$(LIBINCLUDES) -I src $(FILESTODOC)
# $(LIBML)
doc/apidoc.tex: $(FILESTODOC)
$(OCAMLDOC) -o doc/apidoc.tex -latex -noheader -notrailer $(INCLUDES) \
$(LIBINCLUDES) $(FILESTODOC)
$(LIBINCLUDES) -I src $(FILESTODOC)
# $(LIBML)
clean::
......
......@@ -230,8 +230,9 @@ is that they statically guarantee that only well-typed terms can be
constructed.
Here is the way we build the formula $2+2=4$. The main difficult is to
access the internal identifier for addition: it must retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why}.
access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
Section~\ref{theory:Int}).
\begin{verbatim}
let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4")
......@@ -246,7 +247,7 @@ let fmla3 : Term.fmla = Term.f_equ two_plus_two four
An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed
the constructor \texttt{t\_app\_infer} infers the type of the resulting
term. One could also provide the expected term as follows.
term. One could also provide the expected type as follows.
\begin{verbatim}
let two_plus_two : Term.term =
Term.t_app plus_symbol [two;two] Ty.ty_int
......
......@@ -2,6 +2,7 @@
\label{chap:library}
\section{Integers}
\label{theory:Int}
\section{Integer divisions}
......
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open Why
(** Proof database *)
(** {2 data types} *)
......@@ -105,11 +107,11 @@ val parent_goal : transf -> goal
(*
val transf_id : transf -> transf_id
*)
val subgoals : transf -> goal Why.Util.Mstr.t
val subgoals : transf -> goal Util.Mstr.t
(** theory accessors *)
val theory_name : theory -> string
val goals : theory -> goal Why.Util.Mstr.t
val goals : theory -> goal Util.Mstr.t
(*
val verified : theory -> bool
*)
......@@ -118,7 +120,7 @@ val verified : theory -> bool
(*
val file_name : file -> string
*)
val theories : file -> theory Why.Util.Mstr.t
val theories : file -> theory Util.Mstr.t
(** {2 The persistent database} *)
......
......@@ -132,6 +132,52 @@ let t ?(use_meta=true) ~notdeft ~notdeff ~notls =
trans notls)
else trans notls
(*
let fold_on_logic f task env =
match task.Task.task_decl with
| { Theory.td_node = Theory.Decl d } ->
begin
match d.d_node with
| Dlogic dl ->
List.fold_left
(fun acc (ls,ld) -> f ls ld acc)
env dl
| _ -> env
end
| _ -> env
*)
let get_goal task =
match task.Task.task_decl with
| { Theory.td_node = Theory.Decl d } ->
begin
match d.d_node with
| Dprop(Pgoal,_pr,f) ->
begin
match f.f_node with
| Fapp(ps,_tl) ->
try
match
(Mid.find ps.ls_name task.Task.task_known).d_node
with
| Dlogic dl ->
let def = List.assoc ps dl in
begin
match def with
| Some _def -> assert false (* TODO *)
| None ->
Printer.unsupportedFmla f "has no definition"
end
| Dind _ ->
Printer.unsupportedFmla f
"inductive def cannot be inlined"
| Dprop _ | Dtype _ -> assert false
with Not_found -> assert false
end
| _ -> assert false
end
| _ -> assert false
let all = t ~use_meta:true ~notdeft:ffalse ~notdeff:ffalse ~notls:ffalse
(** TODO : restrict to linear substitution,
......
......@@ -74,7 +74,7 @@ val list_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val map_join_left : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'a list -> 'b
val list_apply : ('a -> 'b list) -> 'a list -> 'b list
(** [list_apply f [a1;..;an] returns (f a1)@...@(f an) *)
(** [list_apply f [a1;..;an]] returns (f a1)@...@(f an) *)
val list_fold_product :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment