Use relative paths whenever possible in code.

examples/proofs/binary_search/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/binary_search.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/binary_search.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/btree/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/btree.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/btree.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/intptr/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/intptr.c]. *)
 Section code.
   Definition file_0 : string := "examples/intptr.c".
-  Definition file_1 : string := "???".
+  Definition file_1 : string := "include/refinedc.h".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/lock/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/lock.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/lock.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/malloc1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/malloc1.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/malloc1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mpool/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/mpool.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/mpool.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mpool_simpl/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/mpool_simpl.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/mpool_simpl.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mutable_map/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/mutable_map.c]. *)
 Section code.
   Definition file_0 : string := "examples/mutable_map.c".
-  Definition file_1 : string := "???".
+  Definition file_1 : string := "include/refinedc.h".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/ocaml_runtime/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/ocaml_runtime.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/ocaml_runtime.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/paper_example_2_1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_1.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/paper_example_2_1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/paper_example_2_2/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_2.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/paper_example_2_2.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/queue/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/queue.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/queue.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/reverse/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/reverse.c]. *)
 Section code.
   Definition file_0 : string := "examples/reverse.c".
-  Definition file_1 : string := "???".
+  Definition file_1 : string := "include/refinedc.h".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/simple_union/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/simple_union.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/simple_union.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/tagged_ptr/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/tagged_ptr.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/tagged_ptr.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo1.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/talk_demo1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo2/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo2.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/talk_demo2.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo3/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo3.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/talk_demo3.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/wrapping_add/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/wrapping_add.c]. *)
 Section code.
-  Definition file_0 : string := "???".
+  Definition file_0 : string := "include/refinedc.h".
   Definition file_1 : string := "examples/wrapping_add.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

frontend/coq_pp.ml

@@ -291,7 +291,8 @@ type import = string * string
 let pp_import ff (from, mod_name) =
   Format.fprintf ff "From %s Require Import %s.@;" from mod_name
 
-let pp_code : import list -> Coq_ast.t pp = fun imports ff ast ->
+let pp_code : string -> import list -> Coq_ast.t pp =
+    fun root_dir imports ff ast ->
   (* Formatting utilities. *)
   let pp fmt = Format.fprintf ff fmt in
 
@@ -325,8 +326,11 @@ let pp_code : import list -> Coq_ast.t pp = fun imports ff ast ->
         (locs, files)
       in
       let pp_file_def (file, key) =
-        (* FIXME! HACK!*)
-        fprintf ff "@;Definition file_%i : string := \"%s\"." key (if String.rcontains_from file 1 '/' then "???" else file)
+        let file =
+          try Filename.relative_path root_dir file
+          with Invalid_argument(_) -> file
+        in
+        fprintf ff "@;Definition file_%i : string := \"%s\"." key file
       in
       List.iter pp_file_def all_files;
       let pp_loc_def d =
@@ -1377,15 +1381,15 @@ let pp_proof : string -> func_def -> import list -> string list -> proof_kind
   pp "@]@;End proof_%s.@]" def.func_name
 
 type mode =
-  | Code of import list
+  | Code of string * import list
   | Spec of string * import list * inlined_code * typedef list * string list
   | Fprf of string * func_def * import list * string list * proof_kind
 
 let write : mode -> string -> Coq_ast.t -> unit = fun mode fname ast ->
   let pp =
     match mode with
-    | Code(imports)                          ->
-        pp_code imports
+    | Code(root_dir,imports)                 ->
+        pp_code root_dir imports
     | Spec(path,imports,inlined,tydefs,ctxt) ->
         pp_spec path imports inlined tydefs ctxt
     | Fprf(path,def,imports,ctxt,kind)       ->