fixes for coq output

drivers/coq.drv

@@ -9,6 +9,17 @@ fail "Syntax error: \\(.*\\)$" "\\1"
 prelude "(* This file is generated by Why3's Coq driver *)"
 prelude "(* Beware! Only edit allowed sections below    *)" 
 
+(* À discuter *)
+transformation "simplify_recursive_definition"
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_recursion"
+
+transformation "simplify_formula"
+transformation "simplify_trivial_quantification_in_goal"
+
+
 theory BuiltIn
 
   prelude "Require Import ZArith."

src/driver/driver.mli

@@ -31,8 +31,11 @@ val load_driver : Env.env -> string -> driver
 
 (** {2 use a driver} *)
 
-(** file_of_task input_file theory_name task *)
 val file_of_task : driver -> string -> string -> Task.task -> string
+(** [file_of_task d f th t] produces a filename
+    for the prover of driver [d], for a task [t] generated from
+    a goal in theory [th] of filename [f]
+*)
 
 val call_on_buffer :
   command    : string ->

src/ide/gconfig.ml

@@ -44,7 +44,7 @@ let save_prover fmt p =
   fprintf fmt "version = \"%s\"@\n" p.prover_version;
   fprintf fmt "command = \"%s\"@\n" p.command;
   fprintf fmt "driver = \"%s\"@\n" p.driver_name;  
-  fprintf fmt "editor = \"%s\"@\n" p.editor;  
+  if p.editor <> "" then fprintf fmt "editor = \"%s\"@\n" p.editor;  
   fprintf fmt "@."
 
 let save_config config =

src/ide/gmain.ml

@@ -824,12 +824,10 @@ let edit_selected_row p =
     | Model.Row_theory _th ->
         ()
     | Model.Row_proof_attempt a ->
-        eprintf "schudeling editing@.";
         let g = a.Model.proof_goal in
         let t = g.Model.task in
-        let id = (Task.task_goal t).Decl.pr_name in
-        let name = id.Ident.id_string in
-        let file = name ^ ".v" in
+        let driver = a.Model.prover.driver in
+        let file = Driver.file_of_task driver "f" "th" t in
         a.Model.edited_as <- file;
         let old_status = a.Model.status in
         Helpers.set_proof_status a Scheduler.Running;
@@ -843,7 +841,7 @@ let edit_selected_row p =
         in
         Scheduler.edit_proof ~debug:false ~editor
           ~file
-          ~driver:a.Model.prover.driver
+          ~driver
           ~callback
           t
     | Model.Row_transformation _tr ->

src/printer/coq.ml

@@ -47,11 +47,35 @@ let forget_all () =
 let tv_set = ref Sid.empty
 
 (* type variables *)
+
 let print_tv fmt tv =
-  tv_set := Sid.add tv.tv_name !tv_set;
   let n = id_unique iprinter tv.tv_name in
   fprintf fmt "%s" n
 
+let print_tv_binder fmt tv =
+  tv_set := Sid.add tv.tv_name !tv_set;
+  let n = id_unique iprinter tv.tv_name in
+  fprintf fmt "(%s:Type)" n
+
+let print_ne_params fmt stv =
+  Stv.iter
+    (fun tv -> fprintf fmt "@ %a" print_tv_binder tv)
+    stv
+
+let print_ne_params_list fmt ltv =
+  List.iter
+    (fun tv -> fprintf fmt "@ %a" print_tv_binder tv)
+    ltv
+
+let print_params fmt stv =
+  if Stv.is_empty stv then () else
+    fprintf fmt "forall%a,@ " print_ne_params stv
+
+let print_params_list fmt ltv =
+  match ltv with
+    | [] -> () 
+    | _ -> fprintf fmt "forall%a,@ " print_ne_params_list ltv
+
 let forget_tvs () =
   Sid.iter (forget_id iprinter) !tv_set;
   tv_set := Sid.empty
@@ -83,14 +107,25 @@ type info = {
 
 let rec print_ty info fmt ty = match ty.ty_node with
   | Tyvar v -> print_tv fmt v
-  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
-      | Some s -> syntax_arguments s (print_ty info) fmt tl
-      | None -> begin match tl with
-          | []  -> print_ts fmt ts
-          | l   -> fprintf fmt "(%a@ %a)" print_ts ts
-                     (print_list space (print_ty info)) l
-        end
-    end
+  | Tyapp (ts, tl) when is_ts_tuple ts ->
+      begin 
+        match tl with
+          | []  -> fprintf fmt "unit"
+          | [ty] -> print_ty info fmt ty
+          | _   -> fprintf fmt "(%a@ %a)" print_ts ts
+              (print_list star (print_ty info)) tl
+      end      
+  | Tyapp (ts, tl) -> 
+      begin match query_syntax info.info_syn ts.ts_name with
+        | Some s -> syntax_arguments s (print_ty info) fmt tl
+        | None -> 
+            begin 
+              match tl with
+                | []  -> print_ts fmt ts
+                | l   -> fprintf fmt "(%a@ %a)" print_ts ts
+                    (print_list space (print_ty info)) l
+            end
+      end
 
 (* can the type of a value be derived from the type of the arguments? *)
 let unambig_fs fs =
@@ -271,20 +306,22 @@ let print_constr info fmt cs =
   fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
     (print_paren_l (print_ty info)) cs.ls_args
 
-let print_type_decl info fmt (ts,def) = match def with
-  | Tabstract -> begin match ts.ts_def with
-      | None ->
-          fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
-            print_ts ts (print_arrow_list print_tv) ts.ts_args
-      | Some ty ->
-          fprintf fmt "@[<hov 2>Definition %a %a :=@ %a@]@\n@\n"
-            print_ts ts (print_arrow_list print_tv) ts.ts_args
-	    (print_ty info) ty
+let print_type_decl info fmt (ts,def) = 
+  if is_ts_tuple ts then () else
+  match def with
+    | Tabstract -> begin match ts.ts_def with
+        | None ->
+            fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
+              print_ts ts print_params_list ts.ts_args
+        | Some ty ->
+            fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
+              print_ts ts (print_arrow_list print_tv) ts.ts_args
+	      (print_ty info) ty
       end
-  | Talgebraic csl ->
-      fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n@\n"
-        print_ts ts (print_arrow_list print_tv) ts.ts_args
-        (print_list newline (print_constr info)) csl
+    | Talgebraic csl ->
+        fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n@\n"
+          print_ts ts (print_arrow_list print_tv) ts.ts_args
+          (print_list newline (print_constr info)) csl
 
 let print_type_decl info fmt d =
   if not (Sid.mem (fst d).ts_name info.info_rem) then
@@ -296,18 +333,32 @@ let print_ls_type ?(arrow=false) info fmt ls =
   | None -> fprintf fmt "Prop"
   | Some ty -> print_ty info fmt ty
 
-let print_logic_decl info fmt (ls,ld) = match ld with
-  | Some ld ->
-      let vl,e = open_ls_defn ld in
-      fprintf fmt "@[<hov 2>Definition %a%a: %a :=@ %a.@]@\n@\n"
-        print_ls ls (print_space_list (print_vsty info)) vl
-        (print_ls_type info) ls.ls_value
-        (print_expr info) e;
-      List.iter forget_var vl
-  | None ->
-      fprintf fmt "@[<hov 2>Parameter %a: %a@ %a.@]@\n@\n"
-        print_ls ls (print_arrow_list (print_ty info)) ls.ls_args
-        (print_ls_type ~arrow:(List.length ls.ls_args > 0) info) ls.ls_value
+let print_logic_decl info fmt (ls,ld) = 
+  let params = ls_ty_freevars ls in
+  begin
+    match ld with
+      | Some ld ->
+          let vl,e = open_ls_defn ld in
+          fprintf fmt "@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
+            print_ls ls 
+            print_params params
+            (print_space_list (print_vsty info)) vl
+            (print_ls_type info) ls.ls_value
+            (print_expr info) e;
+          List.iter forget_var vl
+      | None ->
+          fprintf fmt "@[<hov 2>Parameter %a: %a%a@ %a.@]@\n"
+            print_ls ls 
+            print_params params
+            (print_arrow_list (print_ty info)) ls.ls_args
+            (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
+  end;
+  if Stv.is_empty params then 
+    fprintf fmt "@\n"
+  else
+    fprintf fmt "Implicit Arguments %a.@\n@\n"
+      print_ls ls 
+    
 
 let print_logic_decl info fmt d =
   if not (Sid.mem (fst d).ls_name info.info_rem) then 
@@ -375,8 +426,12 @@ let print_decl ?old info fmt d = match d.d_node with
      fprintf fmt "@\n@\n(* YOU MAY EDIT BELOW *)@\n@\n@\n";
       fprintf fmt "(* DO NOT EDIT BELOW *)@\n@\@\n";
  *)
-      fprintf fmt "@[<hov 2>%a %a : %a.@]@\n%a@\n" print_pkind k
-        print_pr pr (print_fmla info) f (print_proof ?old) k;
+      let params = f_ty_freevars Stv.empty f in
+      fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a@\n" 
+        print_pkind k
+        print_pr pr 
+        print_params params
+        (print_fmla info) f (print_proof ?old) k;
       forget_tvs ()
 
 let print_decls ?old info fmt dl =
@@ -393,3 +448,11 @@ let print_task pr thpr ?old fmt task =
 
 let () = register_printer "coq" print_task
 
+
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. "
+End: 
+*)

src/util/pp.ml

@@ -70,6 +70,7 @@ let print_pair_delim start sep stop pr1 pr2 fmt (a,b) =
 
 let dot fmt () = fprintf fmt ".@ "
 let comma fmt () = fprintf fmt ",@ "
+let star fmt () = fprintf fmt "*@ "
 let simple_comma fmt () = fprintf fmt ", "
 let underscore fmt () = fprintf fmt "_"
 let semi fmt () = fprintf fmt ";@ "

src/util/pp.mli

@@ -69,6 +69,7 @@ val newline : formatter -> unit -> unit
 val newline2 : formatter -> unit -> unit
 val dot : formatter -> unit -> unit
 val comma : formatter -> unit -> unit
+val star : formatter -> unit -> unit
 val simple_comma : formatter -> unit -> unit
 val semi : formatter -> unit -> unit
 val underscore : formatter -> unit -> unit

tests/test-claude.why

@@ -7,6 +7,6 @@ theory Test
 
    goal Test2: forall x:int. x*x >= 0
 
-   goal Test3: 1=0 -> false
+   goal Test3: 1<>0 
 end