gappa printer and intro transformation

Makefile.in

@@ -129,7 +129,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		encoding_enumeration encoding encoding_decorate_mono \
 		libencoding encoding_decorate encoding_bridge \
 		encoding_explicit encoding_simple2 \
-		encoding_instantiate simplify_array filter_trigger
+		encoding_instantiate simplify_array filter_trigger \
+		intro
 
 LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
 

doc/manpages.tex

@@ -47,17 +47,26 @@ It is also installable from sources, available from the site \url{http://wwwfun.
 \begin{description}
 \item[eliminate\_algebraic] Replaces algebraic data types by first-order
 definitions~\cite{paskevich09rr}
-\item[eliminate\_builtin]
+\item[eliminate\_builtin] Suppress definitions of symbols which are
+  declared as builtin in the driver, i.e. with a ``syntax'' rule.
+  
 \item[eliminate\_definition]
 \item[eliminate\_definition\_func]
 \item[eliminate\_definition\_pred]
+\item[eliminate\_if\_fmla] replaces formulas of the form if f1 then f2
+  else f3 by an equivalent formula using implications and other
+  connectives. (TODO: detail)
+\item[eliminate\_if\_term] replaces terms of the form if formula then
+  t2 else t3 by lift it at the level of the formula (TODO: detail)
 \item[eliminate\_if]
-\item[eliminate\_if\_fmla]
-\item[eliminate\_if\_term]
-\item[eliminate\_inductive]
-\item[eliminate\_let]
+  apply both two above transformations
+\item[eliminate\_inductive] replaces inductive predicates by
+  (incomplete) axiomatic definitions, i.e construction axioms and an
+  inversion axiom (TODO: detail)
 \item[eliminate\_let\_fmla]
 \item[eliminate\_let\_term]
+\item[eliminate\_let]
+  apply both two above transformations
 \item[eliminate\_mutual\_recursion]
 \item[eliminate\_recursion]
 \item[encoding\_decorate\_mono]
@@ -72,11 +81,49 @@ Should we cite \cite{conchon08smt} here?
 \item[hypothesis\_selection]
 \item[inline\_all]
 \item[inline\_trivial]
+  removes definitions of the form
+\begin{verbatim}
+logic f x_1 .. x_n = (g e_1 .. e_k)
+\end{verbatim}
+when each e_i is either a constant or one of the x_j, and
+each x_1 .. x_n occur at most once in the e_i 
+
 \item[remove\_triggers]
 \item[simplify\_array]
-\item[simplify\_formula]
+\item[simplify\_formula] reduces trivial equalities $t=t$ to True and
+  then simplifies propositional structure: removes True, False, ``f
+  and f'' to ``f'', etc.
 \item[simplify\_recursive\_definition]
+  reduces mutually recursive definitions if they are not really mutually recursive, e.g.:
+\begin{verbatim}
+logic f : ... = .... g ...
+
+with g : .. = e
+\end{verbatim}
+becomes
+\begin{verbatim}
+logic g : .. = e
+logic f : ... = .... g ...
+\end{verbatim}
+if f does not occur in e
+
 \item[simplify\_trivial\_quantification]
+  simplifies quantifications of the form
+\begin{verbatim}
+  forall x, x=t -> P(x)
+\end{verbatim}
+or
+\begin{verbatim}
+  forall x, t=x -> P(x)
+\end{verbatim}
+  when x does not occur in t
+  into 
+\begin{verbatim}
+P(t)
+\end{verbatim}
+  More generally, it applies this simplification whenever x=t appear
+  in a negative position.
+  
 \item[simplify\_trivial\_quantification\_in\_goal]
 \item[split\_premise]
 \end{description}

drivers/gappa.drv

@@ -19,6 +19,7 @@ transformation "eliminate_if"
 transformation "eliminate_let"
 transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
+transformation "intros"
 
 theory BuiltIn
   syntax type int   "int"
@@ -38,11 +39,6 @@ theory int.Int
   syntax logic (*)  "(%1 * %2)"
   syntax logic (-_) "(-%1)"
 
-  syntax logic (<=) "(%1 <= %2)"
-  syntax logic (<)  "(%1 <  %2)"
-  syntax logic (>=) "(%1 >= %2)"
-  syntax logic (>)  "(%1 >  %2)"
-
   remove prop CommutativeGroup.Comm.Comm
   remove prop CommutativeGroup.Assoc.Assoc
   remove prop CommutativeGroup.Unit_def
@@ -72,11 +68,6 @@ theory real.Real
   syntax logic (-_) "(-%1)"
   syntax logic inv  "(1.0 / %1)"
 
-  syntax logic (<=) "(%1 <= %2)"
-  syntax logic (<)  "(%1 <  %2)"
-  syntax logic (>=) "(%1 >= %2)"
-  syntax logic (>)  "(%1 >  %2)"
-
   remove prop CommutativeGroup.Comm.Comm
   remove prop CommutativeGroup.Assoc.Assoc
   remove prop CommutativeGroup.Unit_def
@@ -93,6 +84,12 @@ theory real.Real
 
 end
 
+theory real.Abs
+
+  syntax logic abs  "| %1 |"
+
+end
+
 (*
 Local Variables: 
 mode: why

src/ide/gmain.ml

@@ -488,6 +488,7 @@ let prover_on_unproved_goals p () =
 (*****************************************************)
 
 let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
+let intro_transformation = Trans.lookup_transform "intros" gconfig.env
 
 let split_unproved_goals () =
   List.iter
@@ -846,6 +847,7 @@ let select_row p =
   match filter_model#get ~row ~column:Model.index_column with
     | Model.Row_goal g ->
         let t = g.Model.task in
+        let t = Trans.apply intro_transformation t in 
         let task_text = Pp.string_of Pretty.print_task t in
         task_view#source_buffer#set_text task_text;
         task_view#scroll_to_mark `INSERT;

src/printer/gappa.ml

@@ -69,7 +69,8 @@ let rec print_term info fmt t =
       assert false
   | Tconst c ->
       Pretty.print_const fmt c
-  | Tvar { vs_name = id } ->
+  | Tvar { vs_name = id } 
+  | Tapp ( { ls_name = id } ,[] ) ->
       print_ident fmt id
   | Tapp (ls, tl) -> 
       begin match query_syntax info.info_syn ls.ls_name with
@@ -96,7 +97,7 @@ let rec print_fmla info fmt f =
   match f.f_node with
   | Fapp ({ ls_name = id }, []) ->
       print_ident fmt id
-  | Fapp (ls, [t1;t2]) when ls == ps_equ -> 
+  | Fapp (ls, [t1;t2]) when ls_equal ls ps_equ -> 
       begin try
         let c1 = constant_value t1 in
         fprintf fmt "%a in [%s,%s]" term t2 c1 c1          

src/transform/split_conjunction.mli

@@ -29,7 +29,7 @@ val split_pos_neg_all   : Task.task Trans.tlist
 
 (**  naming convention :
      - pos : move the conjuctions in positive sub-formula to top level
-     - pos : move the conjuctions in negative sub-formula to top level
+     - neg : move the conjuctions in negative sub-formula to top level
      - goal : apply the transformation only to goal
      - axiom : apply the transformation only to axioms
      - all : apply the transformation to goal and axioms *)

tests/test-claude.why

@@ -12,5 +12,15 @@ theory Test
    goal Test2: forall x:int. x*x >= 0
 
    goal Test3: 1<>0 
+
+   goal Test4: 1=2 -> 3=4 
+
+   goal Test5: forall x:int. x <> 0 -> x*x > 0
+
+   use import real.Real
+   use import real.Abs
+
+   goal Test6: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
+
 end