coq driver

Makefile.in

@@ -175,11 +175,17 @@ test: bin/why.byte  $(TOOLS)
 		--call --goal Test.G src/test.why --timeout 3
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
 		--output-file tmp.v --goal Test.G src/test.why 
-	bin/why.byte --call --driver drivers/alt_ergo.drv -I theories/ \
-		--goal ExpLog.Log_e theories/real.why 
+	echo bin/why.byte --call --timeout 1 --driver drivers/alt_ergo.drv -I theories/ \
+		--all-goals theories/real.why 
 	mkdir -p theories/coq
 	bin/why.byte --driver drivers/coq.drv -I theories/ \
-		--output-dir theories/coq --all-goals theories/real.why 
+		--output-dir theories/coq --goals-of real.Abs 
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of real.FromInt
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of real.ExpLog
+	bin/why.byte --driver drivers/coq.drv -I theories/ \
+		--output-dir theories/coq --goals-of real.Trigonometric
 	for i in theories/coq/*.v; do echo coq $$i; (coqc $$i || true) done
 
 testl: bin/whyl.byte

drivers/coq.drv

@@ -13,7 +13,7 @@ theory BuiltIn
 
   syntax type   int     "Z"
   syntax type   real    "R"
-  syntax logic  (_=_)   "(%1 = %2)"
+  syntax logic  (_=_)   "(%1 = %2)" 
   syntax logic  (_<>_)  "(%1 <> %2)"
 end
 
@@ -44,3 +44,47 @@ theory int.Int
 
 end
 
+theory int.Abs
+
+  syntax logic abs "(Zabs %1)"
+
+end
+
+theory real.Real
+
+  syntax logic zero "0%R"
+  syntax logic one "1%R"
+
+  syntax logic (_+_) "(%1 + %2)%R"
+  syntax logic (_-_) "(%1 - %2)%R"
+  syntax logic (-_)  "(-%1)%R"
+  syntax logic (_*_) "(%1 * %2)%R"
+  syntax logic (_/_) "(Rdiv %1 %2)%R"
+  syntax logic inv  "(Rinv %1)"
+
+  syntax logic (_<=_) "(%1 <= %2)%R"
+  syntax logic (_<_) "(%1 <  %2)%R"
+  syntax logic (_>=_) "(%1 >= %2)%R"
+  syntax logic (_>_) "(%1 >  %2)%R"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Inverse
+
+end
+
+
+theory real.Abs
+
+  prelude "Require Import Rbasic_fun."
+
+  syntax logic abs "(Rabs %1)"
+
+end
+

src/core/env.mli

@@ -27,6 +27,7 @@ type retrieve_theory = env -> string list -> theory Mnm.t
 
 val create_env : retrieve_theory -> env
 
+(** ??? *)
 val find_theory : env -> string list -> string -> theory
 
 val env_tag : env -> int

src/main.ml

@@ -173,7 +173,7 @@ let extract_goals ?filter =
   fun env drv acc th ->
     let l = split_theory th filter in
     let l = List.rev_map (fun (task,cl,used) -> 
-      let drv = Driver.cook_driver env cl used drv in
+      let drv = Driver.cook_driver env cl (Ident.Mid.add th.th_name th used) drv in
       (th,task,drv)) l in
     List.rev_append l acc
 
@@ -183,10 +183,112 @@ let file_sanitizer = None (* We should remove which character? *)
 let print_theory_namespace fmt th =
   Pretty.print_namespace fmt th.th_name.Ident.id_short th.th_export
 
+
+
+
+let do_goals env drv src_filename_printer dest_filename_printer file goals = 
+  (* Apply transformations *)
+  let goals = List.fold_left 
+    (fun acc (th,task,drv) -> 
+       List.rev_append 
+         (List.map (fun e -> (th,e,drv)) 
+            (Driver.apply_transforms drv task)
+         ) acc) [] goals 
+  in
+  (* Pretty-print the goals or call the prover *)
+  begin
+    match !output_dir with
+      | None -> ()
+      | Some dir (* we are in the output dir mode *) -> 
+          let file = 
+            let file = Filename.basename file in
+            let file = 
+              try
+                Filename.chop_extension file 
+              with Invalid_argument _ -> file in
+            Ident.string_unique src_filename_printer file in
+          List.iter 
+            (fun (th,task,drv) ->
+               let dest = 
+                 Driver.filename_of_goal drv 
+                   file th.th_name.Ident.id_short task in
+               (* Uniquify the filename before the extension if it exists*)
+               let i = 
+                 try String.rindex dest '.' 
+                 with Not_found -> String.length dest in
+               let name,ext = String.sub dest 0 i, 
+                 String.sub dest i (String.length dest- i) in
+               let name = Ident.string_unique dest_filename_printer name in
+               let filename = name^ext in
+               let filename = Filename.concat dir filename in
+               let cout = open_out filename in
+               let fmt = formatter_of_out_channel cout in
+               fprintf fmt "%a@?" (Driver.print_task drv) task;
+               close_out cout) goals
+  end;
+  begin
+    match !output_file with
+      | None -> ()
+      | Some file (* we are in the output file mode *) -> 
+          let fmt = if file = "-" then std_formatter
+          else formatter_of_out_channel (open_out file) 
+          in
+          let print_task fmt (th,task,drv) =
+            fprintf fmt "@[%a@]" (Driver.print_task drv) task
+          in
+          let print_zero fmt () = fprintf fmt "\000@?" in
+          fprintf fmt "%a@?" (Pp.print_list print_zero print_task) goals
+  end;
+  if !call then
+    (* we are in the call mode *)
+    let call (th,task,drv) = 
+      let res = 
+        Driver.call_prover ~debug:!debug ?timeout drv task in
+      printf "%s %s %s : %a@." 
+        file th.th_name.Ident.id_short 
+        ((task_goal task).Decl.pr_name).Ident.id_long
+        Call_provers.print_prover_result res in
+    List.iter call goals
+
+
+
+let do_no_file env drv src_filename_printer dest_filename_printer =
+  let drv =  
+    match drv with
+      | None -> eprintf "a driver is needed@."; exit 1
+      | Some drv -> drv in
+  (* Extract the goal(s) *)
+  Hashtbl.iter
+    (fun tname goals ->
+       let dir,file,th = match List.rev (Str.split (Str.regexp "\\.") tname) with
+         | t::p -> List.rev p, List.hd p, t
+         | _ -> assert false
+       in
+       let th = try Env.find_theory env dir th with Not_found -> 
+         eprintf "--goal/--goals_of : Unknown theory %s@." 
+           tname; exit 1 
+       in                
+       let filter = match goals with
+         | None -> None
+         | Some s -> Some 
+             (Hashtbl.fold 
+                (fun s l acc ->
+                   let pr = try ns_find_pr th.th_export l 
+                   with Not_found ->
+                     eprintf "--goal : Unknown goal %s@." s ; exit 1 in
+                   Decl.Spr.add pr acc
+                ) s Decl.Spr.empty) in
+       let goals = extract_goals ?filter env drv [] th in
+       do_goals env drv src_filename_printer dest_filename_printer file goals) 
+    which_theories 
+  
+
 let do_file env drv src_filename_printer dest_filename_printer file =
-  let file,cin = if file = "-" 
-  then "stdin",stdin
-  else file, open_in file in
+  let file,cin = 
+    if file = "-" 
+    then "stdin",stdin
+    else file, open_in file 
+  in
   if !parse_only then begin
     let lb = Lexing.from_channel cin in
     Loc.set_file file lb;
@@ -233,69 +335,10 @@ let do_file env drv src_filename_printer dest_filename_printer file =
                         ) s Decl.Spr.empty) in
                extract_goals ?filter env drv acc th
             ) which_theories [] in
-      (* Apply transformations *)
-      let goals = List.fold_left 
-        (fun acc (th,task,drv) -> 
-           List.rev_append 
-             (List.map (fun e -> (th,e,drv)) 
-                (Driver.apply_transforms drv task)
-             ) acc) [] goals in
-      (* Pretty-print the goals or call the prover *)
-      begin
-        match !output_dir with
-          | None -> ()
-          | Some dir (* we are in the output dir mode *) -> 
-              let file = 
-                let file = Filename.basename file in
-                let file = 
-                  try
-                    Filename.chop_extension file 
-                  with Invalid_argument _ -> file in
-                Ident.string_unique src_filename_printer file in
-              List.iter 
-                (fun (th,task,drv) ->
-                   let dest = 
-                     Driver.filename_of_goal drv 
-                       file th.th_name.Ident.id_short task in
-                   (* Uniquify the filename before the extension if it exists*)
-                   let i = 
-                     try String.rindex dest '.' 
-                     with Not_found -> String.length dest in
-                   let name,ext = String.sub dest 0 i, 
-                     String.sub dest i (String.length dest- i) in
-                   let name = Ident.string_unique dest_filename_printer name in
-                   let filename = name^ext in
-                   let filename = Filename.concat dir filename in
-                   let cout = open_out filename in
-                   let fmt = formatter_of_out_channel cout in
-                   fprintf fmt "%a@?" (Driver.print_task drv) task;
-                   close_out cout) goals
-      end;
-      begin
-        match !output_file with
-          | None -> ()
-          | Some file (* we are in the output file mode *) -> 
-              let fmt = if file = "-" then std_formatter
-                else formatter_of_out_channel (open_out file) 
-              in
-              let print_task fmt (th,task,drv) =
-                fprintf fmt "@[%a@]" (Driver.print_task drv) task
-              in
-              let print_zero fmt () = fprintf fmt "\000@?" in
-              fprintf fmt "%a@?" (Pp.print_list print_zero print_task) goals
-      end;
-      if !call then
-        (* we are in the call mode *)
-        let call (th,task,drv) = 
-          let res = 
-            Driver.call_prover ~debug:!debug ?timeout drv task in
-          printf "%s %s %s : %a@." 
-            file th.th_name.Ident.id_short 
-            ((task_goal task).Decl.pr_name).Ident.id_long
-            Call_provers.print_prover_result res in
-        List.iter call goals
+      do_goals env drv src_filename_printer dest_filename_printer file goals
   end
 
+
 let () =
   try
     let env = Env.create_env (Typing.retrieve !loadpath) in
@@ -318,7 +361,10 @@ let () =
       ?sanitizer:file_sanitizer [] in
     let dest_filename_printer = Ident.create_ident_printer 
       ?sanitizer:file_sanitizer [] in
-    Queue.iter (do_file env drv src_filename_printer dest_filename_printer)
+    if Queue.is_empty files then
+      do_no_file env drv src_filename_printer dest_filename_printer
+    else
+      Queue.iter (do_file env drv src_filename_printer dest_filename_printer)
       files
   with e when not !debug ->
     eprintf "%a@." report e;
@@ -326,7 +372,7 @@ let () =
 
 (*
 Local Variables: 
-compile-command: "unset LANG; make -C .. test"
+compile-command: "unset LANG; make -C .. byte"
 End: 
 *)
 

src/printer/coq.ml

@@ -189,7 +189,8 @@ and print_tnode opl opr drv fmt t = match t.t_node with
       forget_var v
   | Tapp (fs, tl) ->
     begin match query_ident drv fs.ls_name with
-      | Syntax s -> syntax_arguments s (print_term drv) fmt tl
+      | Syntax s ->           
+          syntax_arguments s (print_term drv) fmt tl
       | _ -> if unambig_fs fs
           then fprintf fmt "(%a %a)" print_ls fs
             (print_space_list (print_term drv)) tl

theories/int.why

@@ -25,6 +25,8 @@ theory Abs
   axiom Pos: forall x:int. x >= 0 -> abs(x) = x
   axiom Neg: forall x:int. x <= 0 -> abs(x) = -x
 
+  lemma Abs_pos: forall x:int. abs(x) >= 0
+
 end
 
 theory MinMax

theories/real.why

 
 
 theory Real 
+
   logic (< )(real, real)
   logic (<=)(real, real)
   logic (> )(real, real)
@@ -26,6 +27,8 @@ theory Abs
 
   lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x and x <= y
 
+  lemma Abs_pos: forall x:real. abs(x) >= 0.0
+
 end
 
 theory MinMax
@@ -61,6 +64,8 @@ theory FromInt
   axiom Neg: 
     forall x,y:int. from_int(Int.(-_)(x)) = - from_int(x)
 
+  lemma Test: from_int(2) = 2.0
+
 end
 
 theory Truncate