Commits

Thomas Tuerk committed bd5c60f

move type target and related functions from Typed_ast to new file Target

this allows Targetmap to be used by Types

  • Participants
  • Parent commits f831f51

Comments (0)

Files changed (22)

File src/backend.ml

 open Typed_ast
 open Typed_ast_syntax
 open Output
-
+open Target
 
 let gen_extra_level = ref 3
 
   | L_one(s) -> ws s ^ T.const_bone
   | L_vector(s,p,b) -> ws s ^ kwd (String.concat "" [p;b])
 
-let typ_ident_to_output p =     
+let typ_ident_to_output (p : Path.t id) =     
   Ident.to_output T.infix_op_format Type_ctor T.path_sep (resolve_ident_path p p.descr)
 
 let nexp n =

File src/coq_backend.ml

 open Output
 open Typed_ast
 open Typed_ast_syntax
+open Target
 
 let print_and_fail l s =
   raise (Reporting_basic.err_general true l s)
           emp
         else
           combine [from_string "{"; flat tyvars; from_string " : Type}"]
-    and coq_function_application_to_output id args = function_application_to_output (Some Typed_ast.Target_coq)
+    and coq_function_application_to_output id args = function_application_to_output (Some Target.Target_coq)
            (Ident.to_output coq_infix_op Term_const path_sep) exp A.env id args
     and exp e =
       let is_user_exp = Typed_ast_syntax.is_trans_exp e in

File src/def_trans.ml

 
 open Typed_ast
 open Typed_ast_syntax
+open Target
 type def_macro = Name.t list -> env -> def -> (env * def list) option
 
 let r = Ulib.Text.of_latin1

File src/initial_env.ml

 
 open Typed_ast
 open Types
+open Target
 open Process_file
 
 let (^^) = Filename.concat
   in f()
 
 type t = 
-    Typed_ast.env * (Typed_ast.target option * Ulib.Text.t list) list
+    Typed_ast.env * (Target.target option * Ulib.Text.t list) list
 
 let filename_to_mod file =
   Ulib.Text.of_latin1 (String.capitalize (Filename.basename (Filename.chop_extension file))) 

File src/initial_env.mli

 
 open Types
 type t = 
-    Typed_ast.env * (Typed_ast.target option * Ulib.Text.t list) list
-val add_to_init : Typed_ast.target -> string -> t -> t
+    Typed_ast.env * (Target.target option * Ulib.Text.t list) list
+val add_to_init : Target.target -> string -> t -> t
 
 module Initial_libs(P : sig val path : string end) : sig
   val init : t
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
   ( "-tex", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then
-                backends := Some(Typed_ast.Target_tex)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_tex)) !backends) then
+                backends := Some(Target.Target_tex)::!backends),
     " generate LaTeX");
   ( "-html", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
-                backends := Some(Typed_ast.Target_html)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_html)) !backends) then
+                backends := Some(Target.Target_html)::!backends),
     " generate Html");
   ( "-hol", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then
-                backends := Some(Typed_ast.Target_hol)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_hol)) !backends) then
+                backends := Some(Target.Target_hol)::!backends),
     " generate HOL");
   ( "-ocaml", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then
-                backends := Some(Typed_ast.Target_ocaml)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_ocaml)) !backends) then
+                backends := Some(Target.Target_ocaml)::!backends),
     " generate OCaml");
   ( "-isa",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then
-                backends := Some(Typed_ast.Target_isa)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_isa)) !backends) then
+                backends := Some(Target.Target_isa)::!backends),
     " generate Isabelle");
   ( "-coq",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then
-                backends := Some(Typed_ast.Target_coq)::!backends),
+    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_coq)) !backends) then
+                backends := Some(Target.Target_coq)::!backends),
     " generate Coq");
   ( "-ident",
     Arg.Unit (fun b -> if not (List.mem None !backends) then
             I.init
   in
   (* TODO: These should go into the sets of top-level constant names *)
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_hol) !hol_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_ocaml) !ocaml_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in
+  let init = List.fold_right (Initial_env.add_to_init Target.Target_hol) !hol_lib init in
+  let init = List.fold_right (Initial_env.add_to_init Target.Target_ocaml) !ocaml_lib init in
+  let init = List.fold_right (Initial_env.add_to_init Target.Target_isa) !isa_lib init in
+  let init = List.fold_right (Initial_env.add_to_init Target.Target_coq) !coq_lib init in
 
   let consts = 
     List.map
              (fun x s ->
                 match x with
                   | None -> s
-                  | Some(Typed_ast.Target_tex) -> s
-                  | Some(Typed_ast.Target_html) -> s
-                  | Some(t) -> Typed_ast.Targetset.add t s)
+                  | Some(Target.Target_tex) -> s
+                  | Some(Target.Target_html) -> s
+                  | Some(t) -> Target.Targetset.add t s)
              !backends
-             Typed_ast.Targetset.empty 
+             Target.Targetset.empty 
          in
          let (new_env,tast) = check_ast backend_set [mod_name_name] env ast in
 
   let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in
   let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in
     ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends);
-    (if List.mem (Some(Typed_ast.Target_tex)) !backends then 
+    (if List.mem (Some(Target.Target_tex)) !backends then 
        output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
 
 let _ = 

File src/patterns.ml

 
 open Typed_ast
 open Typed_ast_syntax
+open Target
 open Pattern_syntax
 
 let r = Ulib.Text.of_latin1
 (*    (fun _   -> record_matrix_compile_fun) *)]
 
 (* Target specific ones, use [basic_compile_funs] as a fallback. *)
-let get_target_compile_funs (topt:Typed_ast.target option) : (bool -> env -> var_name_generator -> Types.t -> Ast.l -> matrix_compile_fun) list = 
+let get_target_compile_funs (topt:target option) : (bool -> env -> var_name_generator -> Types.t -> Ast.l -> matrix_compile_fun) list = 
   let rec target_compile_funs topt =
     match topt with
     | Some Target_ocaml -> [

File src/patterns.mli

 (**************************************************************************)
 
 open Typed_ast
+open Target
 
 (** pattern compilation *)
 

File src/process_file.ml

 
 type instances = Types.instance list Types.Pfmap.t
 
-let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list) 
+let check_ast (ts : Target.Targetset.t) (mod_path : Name.t list) 
       (env : Typed_ast.env)
       (ast, end_lex_skips)
       : Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
     | Ident.No_type(l,m) ->
         raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
 
-let check_ast_as_module (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
+let check_ast_as_module (ts : Target.Targetset.t) (mod_path : Name.t list)
       (e : Typed_ast.env) 
       (mod_name : Ulib.Text.t) (ast, end_lex_skips)
       : Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
       | None ->
           let r = B.ident_defs m.typed_ast in
             Printf.printf "%s" (Ulib.Text.to_string r)
-      | Some(Typed_ast.Target_html) -> 
+      | Some(Target.Target_html) -> 
           begin
             let r = B.html_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".html") in
               Printf.fprintf o "%s" html_postamble;
               close_output_with_check ext_o
           end
-      | Some(Typed_ast.Target_hol) ->
+      | Some(Target.Target_hol) ->
           begin
             let (r_main, r_extra_opt) = B.hol_defs m.typed_ast in
             let hol_header o = begin
                 close_output_with_check ext_o
               end in ()
           end
-      | Some(Typed_ast.Target_tex) -> 
+      | Some(Target.Target_tex) -> 
           begin
             let rr = B.tex_defs m.typed_ast in
             (* complete tex document, wrapped in tex_preamble and tex_postamble *)
                     Printf.fprintf o "%s" (Ulib.Text.to_string r_usage);
                     close_output_with_check ext_o
           end
-      | Some(Typed_ast.Target_ocaml) -> 
+      | Some(Target.Target_ocaml) -> 
           begin
             let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in
             let _ = begin
                 close_output_with_check ext_o
              end in ()
           end
-      | Some(Typed_ast.Target_isa) -> 
+      | Some(Target.Target_isa) -> 
           begin
           try begin
             let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in
                     raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans_header (l, msg)))
           end
 
-      | Some(Typed_ast.Target_coq) -> 
+      | Some(Target.Target_coq) -> 
           begin
             let r = B.coq_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".v") in

File src/process_file.mli

 (**************************************************************************)
 
 open Typed_ast
+open Target
 
 val parse_file : string -> Ast.defs * Ast.lex_skips
 

File src/reporting.ml

   
 type warning = 
   | Warn_general of bool * Ast.l * string
-  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Typed_ast.target option
+  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target option
   | Warn_pattern_compilation_failed of Ast.l * Typed_ast.pat list * warn_source
   | Warn_pattern_not_exhaustive of Ast.l * Typed_ast.pat list list
   | Warn_def_not_exhaustive of Ast.l * string * Typed_ast.pat list list
   | Warn_pattern_redundant of Ast.l * (int * Typed_ast.pat) list * Typed_ast.exp
   | Warn_def_redundant of Ast.l * string * (int * Typed_ast.pat) list * Typed_ast.def
-  | Warn_pattern_needs_compilation of Ast.l * Typed_ast.target option * Typed_ast.exp * Typed_ast.exp
+  | Warn_pattern_needs_compilation of Ast.l * Target.target option * Typed_ast.exp * Typed_ast.exp
   | Warn_unused_vars of Ast.l * string list * warn_source
-  | Warn_fun_clauses_resorted of Ast.l * Typed_ast.target option * string list * Typed_ast.def
+  | Warn_fun_clauses_resorted of Ast.l * Target.target option * string list * Typed_ast.def
   | Warn_record_resorted of Ast.l * Typed_ast.exp
   | Warn_no_decidable_equality of Ast.l * string
 
   | Warn_general (b, l, m) -> Some (b, l, m)
 
   | Warn_rename (l, n_org, n_via_opt, n_new, targ) ->
-     let target_s = (Typed_ast.target_opt_to_string targ) in
+     let target_s = (Target.target_opt_to_string targ) in
      let via_s = (Util.option_default "" (Util.option_map (fun (n, l') -> "\n  via '"^n^"' at " ^
                   loc_to_string true l') n_via_opt)) in
      let m = Format.sprintf "renaming '%s' to '%s' for target %s%s" n_org n_new target_s via_s in
       Some (true, l, m)
 
   | Warn_pattern_needs_compilation (l, targ, e_old, e_new) -> 
-      let target_s = Typed_ast.target_opt_to_string targ in
+      let target_s = Target.target_opt_to_string targ in
       let m_basic = "pattern compilation used for target " ^ target_s in
       let m_verb = if not verbose then "" else begin
         let e_old_s = Ulib.Text.to_string (B.ident_exp e_old) in
       let fun_label = if List.length nl > 1 then "functions " else "function " in
       let fsL = List.map (fun s -> ("'" ^ s ^ "'")) nl in
       let fs = String.concat ", " fsL in
-      let target_s = Typed_ast.target_opt_to_string targ in
+      let target_s = Target.target_opt_to_string targ in
       let m : string = Format.sprintf "function definition clauses of %s %s reordered for target %s" fun_label fs target_s in
       Some (false, l, m)
 

File src/reporting.mli

   | Warn_general of bool * Ast.l * string
     (** [Warn_general vl ls m] is a general warning with message [m], locations [ls] and a flag [vl] whether to print these locations verbosely. *)
 
-  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Typed_ast.target option 
+  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target option 
     (** Warning about renaming an identifier. The arguments are the old name, an optional intermediate one, the new name and the target *)
 
   | Warn_pattern_compilation_failed of Ast.l * Typed_ast.pat list * warn_source 
   | Warn_def_redundant of Ast.l * string * (int * Typed_ast.pat) list * Typed_ast.def 
     (** redundant patterns in function definition *)
 
-  | Warn_pattern_needs_compilation of Ast.l * Typed_ast.target option * Typed_ast.exp * Typed_ast.exp 
+  | Warn_pattern_needs_compilation of Ast.l * Target.target option * Typed_ast.exp * Typed_ast.exp 
     (** [Warn_pattern_needs_compilation l topt old_e new_e] warns about the compilation of [old_e] to [new_e] for target [topt] *)
 
   | Warn_unused_vars of Ast.l * string list * warn_source 
     (** unused variables detected *)
 
-  | Warn_fun_clauses_resorted of Ast.l * Typed_ast.target option * string list * Typed_ast.def 
+  | Warn_fun_clauses_resorted of Ast.l * Target.target option * string list * Typed_ast.def 
     (** clauses of mutually recursive function definitions resorted *)
 
   | Warn_record_resorted of Ast.l * Typed_ast.exp

File src/target.ml

+(**************************************************************************)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(**************************************************************************)
+
+let r = Ulib.Text.of_latin1
+
+type target = 
+  | Target_hol
+  | Target_ocaml
+  | Target_isa
+  | Target_coq
+  | Target_tex
+  | Target_html
+
+let ast_target_to_target t = match t with
+  | Ast.Target_hol   _ -> Target_hol 
+  | Ast.Target_ocaml _ -> Target_ocaml 
+  | Ast.Target_isa   _ -> Target_isa
+  | Ast.Target_coq   _ -> Target_coq
+  | Ast.Target_tex   _ -> Target_tex
+  | Ast.Target_html  _ -> Target_html
+
+let target_to_ast_target t = match t with
+  | Target_hol   -> Ast.Target_hol None
+  | Target_ocaml -> Ast.Target_ocaml None
+  | Target_isa   -> Ast.Target_isa None
+  | Target_coq   -> Ast.Target_coq None
+  | Target_tex   -> Ast.Target_tex None
+  | Target_html  -> Ast.Target_html None
+
+let target_compare = Pervasives.compare
+
+module Targetmap = Finite_map.Dmap_map(
+struct 
+  type t = target
+  let compare = target_compare
+end)
+
+module Targetset = Set.Make(
+struct 
+  type t = target
+  let compare = target_compare
+end)
+
+let all_targets = 
+  List.fold_right Targetset.add 
+    [Target_hol; Target_ocaml; Target_isa; Target_coq; Target_tex; Target_html] 
+    Targetset.empty
+
+let target_to_string = function
+  | Target_hol -> "hol"
+  | Target_ocaml -> "ocaml"
+  | Target_isa -> "isabelle"
+  | Target_coq -> "coq"
+  | Target_tex -> "tex"
+  | Target_html -> "html"
+
+let target_opt_to_string = function
+  | None -> "ident"
+  | Some t -> target_to_string t
+
+let target_to_output a t = 
+  let open Output in
+    match t with
+      | Ast.Target_hol(s) -> ws s ^ id a (r"hol")
+      | Ast.Target_ocaml(s) -> ws s ^ id a (r"ocaml")
+      | Ast.Target_isa(s) -> ws s ^ id a (r"isabelle")
+      | Ast.Target_coq(s) -> ws s ^ id a (r"coq")
+      | Ast.Target_tex(s) -> ws s ^ id a (r"tex")
+      | Ast.Target_html(s) -> ws s ^ id a (r"html")
+
+let target_to_mname = function
+  | Target_hol -> Name.from_rope (r"Hol")
+  | Target_ocaml -> Name.from_rope (r"Ocaml")
+  | Target_isa -> Name.from_rope (r"Isabelle")
+  | Target_coq -> Name.from_rope (r"Coq")
+  | Target_tex -> Name.from_rope (r"Tex")
+  | Target_html -> Name.from_rope (r"Html")
+
+

File src/target.mli

+(**************************************************************************)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(**************************************************************************)
+
+type target = 
+  | Target_hol
+  | Target_ocaml
+  | Target_isa
+  | Target_coq
+  | Target_tex
+  | Target_html
+
+val ast_target_to_target : Ast.target -> target
+val target_to_ast_target : target -> Ast.target
+val target_compare : target -> target -> int
+
+(** target keyed finite maps *)
+module Targetmap : Finite_map.Dmap with type k = target
+module Targetset : Set.S with type elt = target
+
+(** The set of all the possible targets *)
+val all_targets : Targetset.t
+
+val target_to_string : target -> string
+val target_opt_to_string : target option -> string
+val target_to_output : Output.id_annot -> Ast.target -> Output.t
+val target_to_mname : target -> Name.t

File src/target_trans.ml

 struct
 
   open Typed_ast
+  open Target
 
   module T = Trans.Macros(struct let d = C.d let i = C.i end)
   module M = Def_trans.Macros

File src/target_trans.mli

   (* For each target, returns the (pre-backend) transformation function, and the
   * local variable renaming function (for Typed_ast.Exp_context.avoid) *)
   val get_transformation : 
-    Typed_ast.target option -> Typed_ast.NameSet.t -> 
+    Target.target option -> Typed_ast.NameSet.t -> 
     ((Typed_ast.env -> Typed_ast.checked_module -> (Typed_ast.env * Typed_ast.checked_module)) *
      (Typed_ast.NameSet.t -> Typed_ast.var_avoid_f))
   
   (* Rename the arguments to definitions, if they clash with constants in a given set of constants.
      This was previously part of the transformation returned by get_transformation. It got moved
      out in order to see all the renamings of definitions before changing their arguments. *)
-  val rename_def_params : Typed_ast.target option -> Typed_ast.NameSet.t ->  Typed_ast.checked_module list ->  Typed_ast.checked_module list
+  val rename_def_params : Target.target option -> Typed_ast.NameSet.t ->  Typed_ast.checked_module list ->  Typed_ast.checked_module list
 
   (* extend the set of constants that should be avoided, depending on the definitions in
      the modules passed as arguments *)
   val extend_consts:
-    Typed_ast.target option -> Typed_ast.NameSet.t -> Typed_ast.checked_module list -> Typed_ast.NameSet.t
+    Target.target option -> Typed_ast.NameSet.t -> Typed_ast.checked_module list -> Typed_ast.NameSet.t
 end
 
 (** This flag enables pattern compilation for the identity backend. Used for debugging. *)

File src/trans.ml

 open Typed_ast
 open Typed_ast_syntax
 open Pattern_syntax
+open Target
 open Util
 exception Trans_error of Ast.l * string
 

File src/typecheck.ml

 open Types
 open Typed_ast
 open Typed_ast_syntax
+open Target
 
 let raise_error = Ident.raise_error
 let raise_error_string = Ident.raise_error_string

File src/typecheck.mli

 open Types
 
 val check_defs : 
-  Typed_ast.Targetset.t ->
+  Target.Targetset.t ->
   Name.t list ->
   Typed_ast.env ->
   Ast.defs ->

File src/typed_ast.ml

 (**************************************************************************)
 
 open Types
+open Target
 module P = Precedence
 module NameSet = Set.Make(Name)
 module Nfmap = Finite_map.Fmap_map(Name)
 
 type 'a lskips_seplist = ('a, lskips) Seplist.t
 
-type target = 
-  | Target_hol
-  | Target_ocaml
-  | Target_isa
-  | Target_coq
-  | Target_tex
-  | Target_html
-
-let ast_target_to_target t = match t with
-  | Ast.Target_hol   _ -> Target_hol 
-  | Ast.Target_ocaml _ -> Target_ocaml 
-  | Ast.Target_isa   _ -> Target_isa
-  | Ast.Target_coq   _ -> Target_coq
-  | Ast.Target_tex   _ -> Target_tex
-  | Ast.Target_html  _ -> Target_html
-
-let target_to_ast_target t = match t with
-  | Target_hol   -> Ast.Target_hol None
-  | Target_ocaml -> Ast.Target_ocaml None
-  | Target_isa   -> Ast.Target_isa None
-  | Target_coq   -> Ast.Target_coq None
-  | Target_tex   -> Ast.Target_tex None
-  | Target_html  -> Ast.Target_html None
-
-let target_compare = Pervasives.compare
-
-module Targetmap = Finite_map.Dmap_map(
-struct 
-  type t = target
-  let compare = target_compare
-end)
-
-module Targetset = Set.Make(
-struct 
-  type t = target
-  let compare = target_compare
-end)
-
-let all_targets = 
-  List.fold_right Targetset.add 
-    [Target_hol; Target_ocaml; Target_isa; Target_coq; Target_tex; Target_html] 
-    Targetset.empty
-
-let target_to_string = function
-  | Target_hol -> "hol"
-  | Target_ocaml -> "ocaml"
-  | Target_isa -> "isabelle"
-  | Target_coq -> "coq"
-  | Target_tex -> "tex"
-  | Target_html -> "html"
-
-let target_opt_to_string = function
-  | None -> "ident"
-  | Some t -> target_to_string t
-
-let target_to_output a t = 
-  let open Output in
-    match t with
-      | Ast.Target_hol(s) -> ws s ^ id a (r"hol")
-      | Ast.Target_ocaml(s) -> ws s ^ id a (r"ocaml")
-      | Ast.Target_isa(s) -> ws s ^ id a (r"isabelle")
-      | Ast.Target_coq(s) -> ws s ^ id a (r"coq")
-      | Ast.Target_tex(s) -> ws s ^ id a (r"tex")
-      | Ast.Target_html(s) -> ws s ^ id a (r"html")
-
-let target_to_mname = function
-  | Target_hol -> Name.from_rope (r"Hol")
-  | Target_ocaml -> Name.from_rope (r"Ocaml")
-  | Target_isa -> Name.from_rope (r"Isabelle")
-  | Target_coq -> Name.from_rope (r"Coq")
-  | Target_tex -> Name.from_rope (r"Tex")
-  | Target_html -> Name.from_rope (r"Html")
-
-
 type env_tag = 
   | K_method
   | K_instance

File src/typed_ast.mli

 (** Get only the comments (and a trailing space) *)
 val lskips_only_comments : lskips list -> lskips
 
-type target = 
-  | Target_hol
-  | Target_ocaml
-  | Target_isa
-  | Target_coq
-  | Target_tex
-  | Target_html
-
-val ast_target_to_target : Ast.target -> target
-val target_to_ast_target : target -> Ast.target
-val target_compare : target -> target -> int
-
-(** target keyed finite maps *)
-module Targetmap : Finite_map.Dmap with type k = target
-module Targetset : Set.S with type elt = target
-
-(** The set of all the possible targets *)
-val all_targets : Targetset.t
-
-val target_to_string : target -> string
-val target_opt_to_string : target option -> string
-val target_to_output : Output.id_annot -> Ast.target -> Output.t
-val target_to_mname : target -> Name.t
-
 (** What kind of top-level definition a particular constant is *)
 type env_tag = 
   | K_method   (** A class method *)
   | K_constr (** A type constructor *)
   | K_val  (** A val specification that has no definitions *)
   | K_let   (** A let definition with no target specific definitions or val spec *)
-  | K_target of bool * Targetset.t
+  | K_target of bool * Target.Targetset.t
       (** A definition that also has a val specification. There is a target-specific
           definition for each target in the set, and the bool is true if there is a
           target non-specific definition *)
     (** The location for the first occurrence of a definition/specification of
         this constant *)
 
-    target_rep : const_target_rep Targetmap.t; 
+    target_rep : const_target_rep Target.Targetmap.t; 
     (** Target-specific representation of for this constant *)
   }
 
 
 val local_env_union : local_env -> local_env -> local_env
 val delimit_pat : Precedence.pat_context -> pat -> pat
-val get_new_constants_types : target option -> checked_module list -> Ast.l Nfmap.t * Ast.l Nfmap.t
+val get_new_constants_types : Target.target option -> checked_module list -> Ast.l Nfmap.t * Ast.l Nfmap.t
 
 exception Renaming_error of Ast.l * string
-val get_renames_of_defs : target option -> (Path.t * ( Ast.l * Path.t)) list -> def list -> (Path.t * ( Ast.l * Path.t)) list
+val get_renames_of_defs : Target.target option -> (Path.t * ( Ast.l * Path.t)) list -> def list -> (Path.t * ( Ast.l * Path.t)) list
 
 type name_kind =
   | Nk_typeconstr

File src/types.ml

    (** the case split function for this constructor list, [None] means that pattern matching is used. *)
 }
 
+type type_target_rep =
+  | TR_dummy
+
 type type_descr = { 
   type_tparams : tnvar list;
   type_abbrev : t option;
   type_varname_regexp : string option;
   type_fields : (const_descr_ref list) option;
-  type_constr : constr_family_descr list
+  type_constr : constr_family_descr list;
+(*  target_rep : type_target_rep Target.Targetmap.t  *)
 }
 
+
 type tc_def = 
   | Tc_type of type_descr
   | Tc_class of tnvar * (Name.t * t) list