a bit of cleaning before implementing Coq realizations

src/core/printer.ml

@@ -204,12 +204,14 @@ let get_syntax_map task =
   let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
   sm
 
+(*
 let get_syntax_map_of_theory theory =
   let sm = Mid.empty in
   let sm = Theory.on_meta meta_syntax_type sm_add_ts sm theory in
   let sm = Theory.on_meta meta_syntax_logic sm_add_ls sm theory in
   let sm = Theory.on_meta meta_remove_prop sm_add_pr sm theory in
   sm
+*)
 
 let query_syntax sm id = Mid.find_option id sm
 

src/core/printer.mli

@@ -57,7 +57,9 @@ type syntax_map = string Mid.t
 (* [syntax_map] maps the idents of removed props to "" *)
 
 val get_syntax_map : task -> syntax_map
+(*
 val get_syntax_map_of_theory : theory -> syntax_map
+*)
 
 val query_syntax : syntax_map -> ident -> string option
 

src/core/theory.ml

@@ -720,6 +720,7 @@ let on_meta meta fn acc theory =
   Stdecl.fold add tds.tds_set acc
 *)
 
+(*
 let on_meta _meta fn acc theory =
   let tdecls = theory.th_decls in
   List.fold_left
@@ -728,6 +729,7 @@ let on_meta _meta fn acc theory =
          | Meta (_,ma) -> fn acc ma
          | _ -> acc)
     acc tdecls
+*)
 
 
 (** Base theories *)

src/core/theory.mli

@@ -180,7 +180,9 @@ val clone_meta : tdecl -> symbol_map -> tdecl
 (* [clone_meta td_meta sm] produces from [td_meta]
  * a new Meta tdecl instantiated with respect to [sm]]. *)
 
+(*
 val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
+*)
 
 (** Base theories *)
 

src/main.ml

@@ -145,7 +145,7 @@ let option_list = Arg.align [
   "--prover", Arg.String (fun s -> opt_prover := Some s),
       " same as -P";
   "--coq-realize", Arg.String (fun s -> opt_coq_realization := Some s),
-      " produce, in given file, a Coq realization of the theory given \
+      " <file> produce, in given file, a Coq realization of the theory given \
         using -T";
   "-F", Arg.String (fun s -> opt_parser := Some s),
       "<format> Select input format (default: \"why\")";
@@ -482,7 +482,24 @@ let do_local_theory env drv fname m (tname,_,t,glist) =
   in
   do_theory env drv fname tname th glist
 
-let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_glist) =
+let do_coq_realize_theory_raw env _drv oldf th =
+  let old =
+    if Sys.file_exists oldf
+    then
+      begin
+        let backup = oldf ^ ".bak" in
+        Sys.rename oldf backup;
+        Some(open_in backup)
+      end
+    else None
+  in
+  let ch = open_out oldf in
+  let fmt = formatter_of_out_channel ch in
+  Queue.iter
+    (Coq.print_theory ?old env [] Ident.Mid.empty fmt) th
+
+let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_ths) =
+  eprintf "[Coq realization] theory '%s' of file '%s'.@." tname fname;
   let th = try Mstr.find t m with Not_found ->
     eprintf "Theory '%s' not found in file '%s'.@." tname fname;
     exit 1
@@ -505,7 +522,15 @@ let do_input env drv = function
   | None, _ when !opt_parse_only || !opt_type_only ->
       ()
   | None, tlist ->
-      Queue.iter (do_global_theory env drv) tlist
+      begin
+        match !opt_coq_realization with
+          | Some f ->
+              eprintf "[Coq realization] output file: %s@." f;
+(*
+              Queue.iter (do_coq_realize_theory_raw env drv f) tlist
+*)
+          | None -> Queue.iter (do_global_theory env drv) tlist
+      end
   | Some f, tlist ->
       let fname, cin = match f with
         | "-" -> "stdin", stdin
@@ -518,6 +543,7 @@ let do_input env drv = function
       else
         match !opt_coq_realization with
           | Some f ->
+              eprintf "[Coq realization] output file: %s@." f;
               Queue.iter (do_coq_realize_theory env drv f fname m) tlist
           | None ->
               if Queue.is_empty tlist then

src/printer/coq.ml

@@ -683,28 +683,25 @@ let () = register_printer "coq" print_task
 open Theory
 
 let print_tdecl ~old info fmt d = match d.td_node with
-  | Decl d -> print_decl ~old info fmt d
-  | Use _t -> ()
-(*
-      fprintf fmt "Require Import %s.@\n@\n" (id_unique iprinter t.th_name)
-*)
+  | Decl d ->
+      print_decl ~old info fmt d
+  | Use t ->
+      fprintf fmt "Require %s.@\n@\n"
+        (id_unique iprinter t.th_name)
   | Meta _ -> assert false (* TODO ? *)
   | Clone _ -> assert false (* TODO *)
 
 let print_tdecls ~old info fmt dl =
-  fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_tdecl ~old info)) dl
+  fprintf fmt "@[<hov>%a@\n@]"
+    (print_list nothing (print_tdecl ~old info)) dl
 
 let print_theory _env pr thpr ?old fmt th =
   forget_all ();
   print_prelude fmt pr;
   print_prelude_for_theory th fmt thpr;
-(* TODO
-  let info = {
-    info_syn = get_syntax_map th;
-    info_syn = get_remove_set th} in
-*)
   let info = {
-    info_syn = Mid.empty (* get_syntax_map_of_theory th *);
+    info_syn = (Mid.empty : string Ident.Mid.t)
+      (* get_syntax_map_of_theory th*);
     realization = true;
   }
   in

tests/test-claude.why

@@ -130,7 +130,6 @@ theory TestRealize
 
   axiom P_arefl: forall x:t. not (p x x)
 
-(*
   axiom P_total: forall x y:t. p x y \/ p y x \/ x=y
 
   function f t : t
@@ -139,14 +138,10 @@ theory TestRealize
 
   lemma B : forall x:t. not (p x (f x))
 
-*)
-
 end
 
 theory TestRealizeUse
 
-(*  use import int.Int *)
-
   use import TestRealize
 
   function q t : t
@@ -155,6 +150,16 @@ theory TestRealizeUse
 
 end
 
+theory TestRealizeUseInt
+
+  use import int.Int
+
+  function q int : int
+
+  axiom C : forall x:int. q x + x >= 0
+
+end
+
 theory TestInline
 
   use import int.Int