Commit 652e4920 authored by Andrei Paskevich's avatar Andrei Paskevich

minor changes

parent 9b17d241
......@@ -5,6 +5,14 @@
o fix BTS 13849
o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
introduce constants, as an alternative to "function"
o [TPTP] new parser for TPTP files with support for the newest
TFA1 format (TPTP with polymorphic types and arithmetic)
o [API] Dtype declaration kind is split into two: Dtype for
declarations of a single abstract type or type alias, and
Ddata for a list of (mutually recursive) algebraic types.
Similarly, Dlogic declaration kind is split into Dparam for
a single abstract function/predicate symbol and Dlogic for
a list of (mutually recursive) defined symbols.
version 0.71, October 13, 2011
==============================
......
......@@ -160,7 +160,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- DONE (CLAUDE) Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
- (ANDREI) better use of Alt-Ergo's builtin theories: records, enumeration types
- DONE (ANDREI) better use of Alt-Ergo's builtin theories: records, enumeration types
(Alt-Ergo >= 0.94) => at least two drivers for Alt-Ergo, depending on its
version number
......
......@@ -118,18 +118,17 @@ let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
\end{verbatim}
The task for our second formula is a bit more complex to build, because
the variables A and B must be added as logic declarations in the task.
the variables A and B must be added as abstract (i.e.~not defined)
propositional symbols in the task.
\begin{verbatim}
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 is:@\n%a@]@." Pretty.print_task task2
\end{verbatim}
The argument \texttt{None} is the declarations of logic symbols means
that they do not have any definition.
Execution of our OCaml program now outputs:
\begin{verbatim}
......
......@@ -81,29 +81,52 @@ _why3()
COMPREPLY=( $( compgen -W 'none top deep' -- "$cur" ) )
return 0
;;
-latex|--latex|-latex2|--latex2)
_filedir -d
return 0
;;
--debug)
flags=$($1 --list-debug-flags | grep -v '^Known ' | cut -d ' ' -f 3)
COMPREPLY=( $( compgen -W "$flags" -- "$cur" ) )
return 0
;;
# Why3session options
--filter-prover)
provers=$(${1/session/} --list-provers | grep -v '^Known ' | cut -d ' ' -f 3)
COMPREPLY=( $( compgen -W "$provers" -- "$cur" ) )
return 0
;;
--filter-obsolete|--filter-archived|--filter-verified-goal|--filter-verified)
COMPREPLY=( $( compgen -W 'yes no all' -- "$cur" ) )
return 0
;;
--style)
COMPREPLY=( $( compgen -W 'simple jstree' -- "$cur" ) )
return 0
;;
esac
help="--help"
case "$1" in
*why3session*)
if [ "$cword" -eq 1 ] ; then
cmds=$($1 --help 2>&1 | tail -n +4 | head -n -2 | cut -d ' ' -f 1)
COMPREPLY=( $( compgen -W "$cmds -v --version -h --help" -- "$cur" ) )
return 0
fi
help="${words[1]} --help"
;;
esac
_filedir
case "$cur" in
-*) COMPREPLY+=( $( compgen -W '$( _parse_help "$1" )' -- "$cur" ) )
-*) COMPREPLY+=( $( compgen -W '$( _parse_help "$1" "$help" )' -- "$cur" ) )
return 0
;;
esac
} && complete -F _why3 \
why3 why3ml why3ide why3config why3doc why3html why3replayer why3session \
why3 why3ml why3ide why3config why3doc why3replayer why3session \
why3.opt why3ml.opt why3ide.opt why3config.opt why3doc.opt \
why3html.opt why3replayer.opt why3session.opt \
why3replayer.opt why3session.opt \
why3.byte why3ml.byte why3ide.byte why3config.byte why3doc.byte \
why3html.byte why3replayer.byte why3session.byte
why3replayer.byte why3session.byte
......@@ -33,7 +33,7 @@ let spec =
("-style <n>",
Arg.Set_int opt_style,
" sets output style (1 or 2, default 1)") ::
("-dir <path>",
("-o <path>",
Arg.Set_string opt_output_dir,
" where to produce LaTeX files (default: session dir)") ::
("-longtable",
......
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