Thomas Tuerk avatar Thomas Tuerk committed 70c995c

implement target_mappings for types

Comments (0)

Files changed (14)

       (NameSet.diff (setcomp_bindings not_shadowed e) (pats_vars not_shadowed ps),
        NameSet.singleton (xl_to_name xl))
 
-
-let target_to_int = function
-  | Ast.Target_hol _ -> 6
-  | Ast.Target_ocaml _ -> 5
-  | Ast.Target_isa _ -> 4
-  | Ast.Target_coq _ -> 3
-  | Ast.Target_tex _ -> 2
-  | Ast.Target_html _ -> 1
-
-let ast_target_compare x y = Pervasives.compare (target_to_int x) (target_to_int y)
     variables that are currently bound in the enclosing environment (such
     variables cannot become comprehension variables) *)
 val setcomp_bindings : (Name.t -> bool) -> Ast.exp -> Set.Make(Name).t
-
-(** a comparison function for targets *)
-val ast_target_compare : Ast.target -> Ast.target -> int
   val lex_skip : Ast.lex_skip -> Ulib.Text.t
   val need_space : Output.t' -> Output.t' -> bool
 
-  val target : Ast.target option
+  val target : Target.target option
 
   val path_sep : t
   val list_sep : t
 
 module Html : Target = struct
   include Identity 
-  let target = Some (Ast.Target_html None)
+  let target = Some Target_html
 
   let forall = kwd "∀"
   let exists = kwd "∃"
 
   let need_space x y = false
 
-  let target = Some (Ast.Target_tex None)
+  let target = Some Target_tex
 
   let tkwd s = kwd (String.concat "" ["\\lemkw{"; s;  "}"])
   let tkwdl s = kwd (String.concat "" ["\\lemkw{"; s;  "}"]) ^ texspace
 module Ocaml : Target = struct
   include Identity 
 
-  let target = Some (Ast.Target_ocaml None)
+  let target = Some Target_ocaml
 
   let path_sep = kwd "."
 
     | Ast.Ws(r) -> r
     | Ast.Nl -> r"\n"
 
-  let target = Some (Ast.Target_isa None)
+  let target = Some Target_isa
 
   (* TODO : write need_space *)
 
     let (d2,s2) = f y in
       not d1 && not d2 && s1 = s2
 
-  let target = Some (Ast.Target_hol None)
+  let target = Some Target_hol
 
   let path_sep = meta "$"
   let list_sep = kwd ";"
 
 let is_identity_target = match T.target with
     None -> true
-  | Some (Ast.Target_isa _)   -> false
-  | Some (Ast.Target_hol _)   -> false
-  | Some (Ast.Target_coq _)   -> false
-  | Some (Ast.Target_ocaml _) -> false
-  | Some (Ast.Target_html _)  -> true
-  | Some (Ast.Target_tex _)   -> true
+  | Some Target_isa   -> false
+  | Some Target_hol   -> false
+  | Some Target_coq   -> false
+  | Some Target_ocaml -> false
+  | Some Target_html  -> true
+  | Some Target_tex   -> true
 
 
 (*
   | L_vector(s,p,b) -> ws s ^ kwd (String.concat "" [p;b])
 
 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)
+  Ident.to_output T.infix_op_format Type_ctor T.path_sep (typ_id_to_ident T.target A.env p)
 
 let nexp n =
   let rec nexp_int n = match n.nterm with
       ws s2 ^
       kwd ")"
 
-let ast_target_opt_to_target_opt t_opt = Util.option_map ast_target_to_target t_opt;;
-
 let const_ident_to_output a cd =
-  Ident.to_output T.infix_op_format a T.path_sep (const_id_to_ident (ast_target_opt_to_target_opt T.target) A.env cd)
+  Ident.to_output T.infix_op_format a T.path_sep (const_id_to_ident T.target A.env cd)
 ;;
 
 let tyvar tv =
   | P_var(n) ->
       Name.to_output T.infix_op_format Term_var n
   | P_const(cd,ps) ->
-      let oL = pattern_application_to_output (ast_target_opt_to_target_opt T.target) (Ident.to_output T.infix_op_format Term_const T.path_sep) pat A.env cd ps in
+      let oL = pattern_application_to_output T.target (Ident.to_output T.infix_op_format Term_const T.path_sep) pat A.env cd ps in
       concat texspace oL
   | P_record(s1,fields,s2) ->
       ws s1 ^
         ws s3 ^
         T.recup_end
   | Field(e,s,fd) ->
-      if (T.target = Some (Ast.Target_isa None)) then
+      if (T.target = Some Target_isa) then
         kwd "(" ^ T.field_access_start ^ 
         const_ident_to_output Term_field fd ^
         T.field_access_end ^ 
       T.set_start ^
       exp e1 ^
       ws s2 ^
-      (if T.target = Some (Ast.Target_isa(None)) then 
+      (if T.target = Some Target_isa then 
          (if (is_var_tup_exp e1 && NameSet.equal vars (nfmap_domain (C.exp_to_free e1))) then kwd "." else 
           T.setcomp_sep ^
           flat (List.map (fun x -> id Term_var (Name.to_rope x)) (NameSet.elements vars)) ^
 
   (* TODO: Add an Isabelle transformation to nested Quants *)
   | Quant(q,qbs,s2,e) ->
-      if (T.target = Some (Ast.Target_isa None)) then 
+      if (T.target = Some Target_isa) then 
         block is_user_exp 0 (
         kwd "(" ^ 
         flat (List.map (isa_quant q) qbs) ^
       ws s2 ^
       kwd "}"
 
-let in_target targs = Typed_ast.in_targets_opt T.target targs
+let in_target targs = Typed_ast.in_targets_opt (Util.option_map target_to_ast_target T.target) targs
 
 
 (****** Isabelle ******)
       end
   | Type_def(s, defs) ->
       let defs = 
-        if T.target = Some (Ast.Target_hol None) then 
+        if T.target = Some Target_hol then 
           Seplist.map (hol_strip_args (collect_type_names defs)) defs 
         else 
           defs 
       let n' = Name.strip_lskip n in 
       [(Name.to_rope n', Name.to_rope_tex Term_var n', p.locn)]
   | P_const(cd,ps) ->
-      let n = Ident.get_name (const_id_to_ident (ast_target_opt_to_target_opt T.target) A.env cd) in
+      let n = Ident.get_name (const_id_to_ident T.target A.env cd) in
       let n' = Name.strip_lskip n in 
       [(Name.to_rope n', Name.to_rope_tex Term_ctor n', p.locn)]
   | P_record(s1,fields,s2) ->
     (fun ((d,s),l) y -> 
        begin
          match T.target with 
-         | Some (Ast.Target_isa _) -> isa_def d (is_trans_loc l)
-         | Some (Ast.Target_tex _) -> raise (Failure "should be unreachable")
-         | Some (Ast.Target_html _) -> html_link_def d ^ def d (is_trans_loc l)
+         | Some Target_isa  -> isa_def d (is_trans_loc l)
+         | Some Target_tex  -> raise (Failure "should be unreachable")
+         | Some Target_html -> html_link_def d ^ def d (is_trans_loc l)
          | _ -> def d (is_trans_loc l)
        end ^
 
       (fun ((d,s),l) y -> 
          begin
            match T.target with 
-           | Some (Ast.Target_isa _) -> isa_def_extra gf d l 
-           | Some (Ast.Target_hol _) -> hol_def_extra gf d l 
-           | Some (Ast.Target_ocaml _) -> ocaml_def_extra gf d l 
+           | Some Target_isa   -> isa_def_extra gf d l 
+           | Some Target_hol   -> hol_def_extra gf d l 
+           | Some Target_ocaml -> ocaml_def_extra gf d l 
            | _ -> emp
          end ^
 
 
 let defs_to_rope ((ds:def list),end_lex_skips) =
   match T.target with
-  | Some (Ast.Target_tex _) -> 
+  | Some Target_tex -> 
       Ulib.Text.concat (r"") (List.map (function ((d,s),l) -> to_rope_tex_def d) ds) ^^^^
       (match to_rope_option_tex T.lex_skip T.need_space true (ws end_lex_skips) with None -> r"" | Some rr -> 
         r"\\lemdef{\n" ^^^^
 (* for -inc.tex file *)
 let defs_inc ((ds:def list),end_lex_skips) =
   match T.target with
-  | Some (Ast.Target_tex _) -> 
+  | Some Target_tex -> 
       batrope_pair_concat (List.map (function ((d,s),l) -> batrope_pair_concat (def_tex_inc d)) ds)
   | _ ->
       raise (Failure "defs_inc called on non-tex target")
        (fun ((d,s),l) y ->
           begin match T.target with
 
-              Some (Ast.Target_isa _) -> 
+              Some Target_isa -> 
                 begin 
                   match d with 
                       Open(s,m) -> 

src/finite_map.ml

   val set_default : 'a t -> 'a option -> 'a t
   val insert : 'a t -> (k * 'a) -> 'a t
   val apply : 'a t -> k -> 'a option
+  val apply_opt : 'a t -> k option -> 'a option
 
   val remove : 'a t -> k -> 'a t
   val in_dom : k -> 'a t -> bool
       Some(M.find k m)
     with
       | Not_found -> if S.mem k s then None else d_opt;;
+
+  let apply_opt (m, s, d_opt) = function None -> d_opt | Some k -> apply (m, s, d_opt) k
      
   let in_dom k (m, s, d_opt) = M.mem k m || (S.mem k s && d_opt <> None)
     
             (ms' @ [n]);
           (Name.get_lskip m', Name.replace_lskip m' None::ms', n)
 
+let mk_ident_names l i =
+  mk_ident (List.map (fun r -> (Name.add_lskip r, None)) l)
+    (Name.add_lskip i)
+    (Ast.Trans ("mk_ident_names", None))
+
+let mk_ident_strings l i =
+  mk_ident_names (List.map (fun n -> Name.from_string n) l) (Name.from_string i) 
+
 let from_id (Ast.Id(m,xl,l)) : t =
   mk_ident 
     (List.map (fun (xl,l) -> (Name.from_x xl, l)) m)
 (** Return the last name in the ident, e.g., M.Y.x gives x *)
 val get_name : t -> Name.lskips_t
 
+(** [mk_ident nsl ns l] generates a new identifiers giving full control. Whitespace is prohibited though and
+    only parenthesis might be used in the [Name.lskips_t]. Otherwise, this operation my fails and uses
+    the location [l] for the error message. *)
 val mk_ident : (Name.lskips_t * Ast.lex_skips) list -> Name.lskips_t -> Ast.l -> t
+
+(** Since [mk_ident] does not allow whitespace and parenthesis are often not needed, 
+    [mk_ident_names] provides a simpler interface that uses names. Since it cannot fail, the location is
+    not needed. *)
+val mk_ident_names : Name.t list -> Name.t -> t
+
+(** [mk_ident_strings] is a version of [mk_ident_names] that uses strings as input. *)
+val mk_ident_strings : string list -> string -> t
+
+
 val to_output : (Output.id_annot -> Ulib.Text.t -> Output.t) -> Output.id_annot -> Output.t -> t -> Output.t
 val get_first_lskip: t -> Ast.lex_skips
 val drop_parens : (Precedence.op -> Precedence.t) -> t -> t

src/initial_env.ml

 let (^^) = Filename.concat
 let r = Ulib.Text.of_latin1
 
+
+(** Build type_defs for build-in types *)
 let tds = 
   [(Path.listpath, mk_tc_type [Ty(Tyvar.from_rope (r"a"))] None);
    (Path.setpath, mk_tc_type [Ty(Tyvar.from_rope (r"a"))] None);
 let initial_d : Types.type_defs = 
   List.fold_right (fun x y -> Types.Pfmap.insert y x) tds Types.Pfmap.empty
 
+let initial_d = Types.type_defs_new_ident_type Ast.Unknown initial_d Path.numpath Target.Target_isa (Ident.mk_ident_strings [] "nat")
+
 let initial_local_env : Typed_ast.local_env =
   { empty_local_env with
     p_env = Nfmap.from_list 
                (Name.from_rope (r"unit"), (Path.unitpath, Ast.Unknown));
                (Name.from_rope (r"num"), (Path.numpath, Ast.Unknown))] }
 
+
 let initial_env : Typed_ast.env =
   { empty_env with local_env = initial_local_env; t_env = initial_d; i_env = Pfmap.empty }
 
 
 let target_compare = Pervasives.compare
 
+let ast_target_to_int = function
+  | Ast.Target_hol _ -> 6
+  | Ast.Target_ocaml _ -> 5
+  | Ast.Target_isa _ -> 4
+  | Ast.Target_coq _ -> 3
+  | Ast.Target_tex _ -> 2
+  | Ast.Target_html _ -> 1
+
+let ast_target_compare x y = Pervasives.compare (ast_target_to_int x) (ast_target_to_int y)
+
 module Targetmap = Finite_map.Dmap_map(
 struct 
   type t = target
   | Target_tex -> Name.from_rope (r"Tex")
   | Target_html -> Name.from_rope (r"Html")
 
-
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+(** Datatype and Function for Targets *)
+
+(** A datatype for Targets. In contrast to the one in
+    [ast.ml] this one does not carry white-space information. *)
 type target = 
   | Target_hol
   | Target_ocaml
   | Target_tex
   | Target_html
 
+(** [ast_target_to_target t] converts an ast-target to a
+    target. This essentially means dropping the white-space information. *)
 val ast_target_to_target : Ast.target -> target
+
+(** [target_to_ast_target t] converts a target [t] to an
+    ast_target. This essentially means adding empty white-space information. *)
 val target_to_ast_target : target -> Ast.target
+
+(** [ast_target_compare] is a comparison function for ast-targets. *)
+val ast_target_compare : Ast.target -> Ast.target -> int
+
+(** [target_compare] is a comparison function for targets. *)
 val target_compare : target -> target -> int
 
-(** target keyed finite maps *)
+(** target keyed finite maps with a default value*)
 module Targetmap : Finite_map.Dmap with type k = target
+
+(** target sets *)
 module Targetset : Set.S with type elt = target
 
-(** The set of all the possible targets *)
+(** The set of all the targets. *)
 val all_targets : Targetset.t
 
+(** [target_to_string t] returns a string description of a target [t]. *)
 val target_to_string : target -> string
+
+(** [target_opt_to_string t_opt] returns a string description of a target.
+    If some target is given, it does the same as [target_to_string]. Otherwise,
+    it returns a string description of the identity backend. *)
 val target_opt_to_string : target option -> string
-val target_to_output : Output.id_annot -> Ast.target -> Output.t
+
+(** [target_to_mname t] returns a name for a target. It is similar to
+    [target_to_string t]. However, it returns capitalised versions. *)
 val target_to_mname : target -> Name.t
+
+(** [target_to_output a t] returns output for a target [t] and id-annotation [a]. *)
+val target_to_output : Output.id_annot -> Ast.target -> Output.t
 let add_record_to_ctxt build_descr (ctxt : defn_ctxt) 
       (recs : (name_l * lskips * t) lskips_seplist) 
       : (const_descr_ref list * defn_ctxt)  =
-    (Seplist.fold_right
+    (Seplist.fold_left
       (fun ((fn,l'),sk1,t) (field_list, ctxt) ->
          let fn' = Name.strip_lskip fn in
          let field_descr = build_descr fn' l' t in
   | Some t -> (match targets_opt with 
                  None -> true
                | Some (neg, _, targets, _) -> 
-                 let is_in = Seplist.exists (fun t' -> Ast_util.ast_target_compare t t' = 0) targets in
+                 let is_in = Seplist.exists (fun t' -> ast_target_compare t t' = 0) targets in
                  if neg then not is_in else is_in)
 
 type val_def = 
   in
   id
 
-
 let ident_get_first_lskip id =
   match id.id_path with
     | Id_none sk -> sk

src/typed_ast_syntax.ml

     | Some(fl) -> fl
     | _ -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal(l, "not a field type")))
 
-let names_mk_ident l i loc =
-  Ident.mk_ident (List.map (fun r -> (Name.add_lskip r, None)) l)
-    (Name.add_lskip i)
-    loc
-
-let mk_ident l i loc =
-  names_mk_ident (List.map (fun n -> Name.from_rope (r n)) l) (Name.from_rope (r i)) loc
+let names_mk_ident l i loc = Ident.mk_ident_names l i
+let mk_ident l i loc = Ident.mk_ident_strings l i
 
 let get_const_id (env : env) l mp n inst =
 let (c_ref, c_d) = get_const env mp n in
 }
 
 type type_target_rep =
-  | TR_dummy
+  | TR_rename of Name.t
+  | TR_new_ident of Ident.t
 
 type type_descr = { 
   type_tparams : tnvar list;
   type_varname_regexp : string option;
   type_fields : (const_descr_ref list) option;
   type_constr : constr_family_descr list;
-(*  target_rep : type_target_rep Target.Targetmap.t  *)
+  type_target_rep : type_target_rep Target.Targetmap.t
 }
 
 
   type_abbrev = Some abbrev;
   type_varname_regexp = None;
   type_fields = None;
-  type_constr = []
+  type_constr = [];
+  type_target_rep = Target.Targetmap.empty
 }
 
 let mk_tc_type vars reg = Tc_type { 
   type_abbrev = None;
   type_varname_regexp = reg;
   type_fields = None;
-  type_constr = []
+  type_constr = [];
+  type_target_rep = Target.Targetmap.empty
 }
 
 type type_defs = tc_def Pfmap.t
   let l = Ast.Trans ("type_defs_add_constr_family", Some l) in
   type_defs_update_tc_type l d p (fun tc -> {tc with type_constr = cf :: tc.type_constr})
 
-let type_defs_lookup l (d : type_defs) (t : t) =
+let type_defs_rename_type l (d : type_defs) (p : Path.t) (t: Target.target) (n : Name.t) : type_defs =
+  let l = Ast.Trans ("type_defs_rename_type", Some l) in
+  let up td = begin
+    let tm = td.type_target_rep in
+    let tm' = Target.Targetmap.insert tm (t, TR_rename n) in
+    {td with type_target_rep = tm'}
+  end in
+  type_defs_update_tc_type l d p up
+
+let type_defs_new_ident_type l (d : type_defs) (p : Path.t) (t: Target.target) (i : Ident.t) : type_defs =
+  let l = Ast.Trans ("type_defs_target_type", Some l) in
+  let up td = begin
+    let tm = td.type_target_rep in
+    let tm' = Target.Targetmap.insert tm (t, TR_new_ident i) in
+    {td with type_target_rep = tm'}
+  end in
+  type_defs_update_tc_type l d p up
+
+let type_defs_lookup l (d : type_defs) (p : Path.t) =
     let l = Ast.Trans ("type_defs_lookup", Some l) in
+    match (Pfmap.apply d p) with
+      | Some (Tc_type td) -> td
+      | _ -> raise (env_no_type_exp l p)
+
+let type_defs_lookup_typ l (d : type_defs) (t : t) =
     match t with 
-      | { t = Tapp(_, p) } -> begin
-          match (Pfmap.apply d p) with
-            | Some (Tc_type td) -> Some td
-            | _ -> raise (env_no_type_exp l p)
-        end  
+      | { t = Tapp(_, p) } -> Some (type_defs_lookup l d p)
       | _ -> None
 
 let type_defs_get_constr_families l (d : type_defs) (t : t) (c : const_descr_ref) : constr_family_descr list =
-  match type_defs_lookup l d t with 
+  match type_defs_lookup_typ l d t with 
     | None -> []
     | Some td -> List.filter (fun fs -> List.mem c fs.constr_list) td.type_constr
 
    (** the case split function for this constructor list, [None] means that pattern matching is used. *)
 }
 
+(** the target representation of a type *)
+type type_target_rep =
+  | TR_rename of Name.t (** Rename the type to the given name. This means keeping the module structure unchanged and just modifying the name *)
+  | TR_new_ident of Ident.t (** Replace the type identifier with the given one. Module prefixes are thrown away and replaced *)
+
 (** a type description  **)
 type type_descr = { 
   type_tparams : tnvar list;
   type_fields : (const_descr_ref list) option;
   (** if it is a record type, the list of fields *)
 
-  type_constr : constr_family_descr list
+  type_constr : constr_family_descr list;
   (** the constructors of this type *)
+  
+  type_target_rep : type_target_rep Target.Targetmap.t
+  (** target representation of the type *)
 }
 
 type tc_def = 
 
 val type_defs_add_constr_family : Ast.l -> type_defs -> Path.t -> constr_family_descr -> type_defs
 
-(** [type_defs_get_constr_families d t c] gets all constructor family descriptions for type [t] in
+(** [type_defs_get_constr_families l d t c] gets all constructor family descriptions for type [t] in
     type environment [d], which contain the constant [c]. *)
 val type_defs_get_constr_families : Ast.l -> type_defs -> t -> const_descr_ref -> constr_family_descr list
 
-val type_defs_lookup : Ast.l -> type_defs -> t -> type_descr option
+(** [type_def_rename_type l d p t n] renames the type with path [p] in the defs [d] to the name [n] for
+target [t]. Renaming means that the module structure is kept. Only the name is changed. *)
+val type_defs_rename_type: Ast.l -> type_defs -> Path.t -> Target.target -> Name.t -> type_defs
+
+(** [type_def_new_ident_type l d p t i] changes the representation of the type with path [p] in the defs [d] to the identifier [i] for
+target [t]. This means that the whole module structure is lost and replace by the identifier. *)
+val type_defs_new_ident_type: Ast.l -> type_defs -> Path.t -> Target.target -> Ident.t -> type_defs
 
+(** [type_defs_lookup_typ l d t] looks up the description of type [t] in defs [d]. *)
+val type_defs_lookup_typ : Ast.l -> type_defs -> t -> type_descr option
 
+(** [type_defs_lookup l d p] looks up the description of type with path [p] in defs [d]. *)
+val type_defs_lookup : Ast.l -> type_defs -> Path.t -> type_descr
 
 (** Generates a type abbreviation *)
 val mk_tc_type_abbrev : tnvar list -> t -> tc_def
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.