src/Pure/sign.ML
changeset 4844 4fb63c77f2df
parent 4627 ae95666c71cc
child 4892 0f80e924009d
equal deleted inserted replaced
4843:df709de137af 4844:4fb63c77f2df
    37   val eq_sg: sg * sg -> bool
    37   val eq_sg: sg * sg -> bool
    38   val same_sg: sg * sg -> bool
    38   val same_sg: sg * sg -> bool
    39   val is_draft: sg -> bool
    39   val is_draft: sg -> bool
    40   val const_type: sg -> string -> typ option
    40   val const_type: sg -> string -> typ option
    41   val classes: sg -> class list
    41   val classes: sg -> class list
       
    42   val defaultS: sg -> sort
    42   val subsort: sg -> sort * sort -> bool
    43   val subsort: sg -> sort * sort -> bool
    43   val nodup_Vars: term -> unit
    44   val nodup_Vars: term -> unit
    44   val norm_sort: sg -> sort -> sort
    45   val norm_sort: sg -> sort -> sort
    45   val nonempty_sort: sg -> sort list -> sort -> bool
    46   val nonempty_sort: sg -> sort list -> sort -> bool
    46   val of_sort: sg -> typ * sort -> bool
    47   val of_sort: sg -> typ * sort -> bool
    47   val long_names: bool ref
    48   val long_names: bool ref
    48   val classK: string
    49   val classK: string
    49   val typeK: string
    50   val typeK: string
    50   val constK: string
    51   val constK: string
    51   val full_name: sg -> bstring -> string
    52   val full_name: sg -> bstring -> string
       
    53   val full_name_path: sg -> string -> bstring -> string
    52   val base_name: string -> bstring
    54   val base_name: string -> bstring
    53   val intern: sg -> string -> xstring -> string
    55   val intern: sg -> string -> xstring -> string
    54   val extern: sg -> string -> string -> xstring
    56   val extern: sg -> string -> string -> xstring
    55   val cond_extern: sg -> string -> string -> xstring
    57   val cond_extern: sg -> string -> string -> xstring
    56   val intern_class: sg -> xclass -> class
    58   val intern_class: sg -> xclass -> class
    91   val add_classrel: (xclass * xclass) list -> sg -> sg
    93   val add_classrel: (xclass * xclass) list -> sg -> sg
    92   val add_classrel_i: (class * class) list -> sg -> sg
    94   val add_classrel_i: (class * class) list -> sg -> sg
    93   val add_defsort: xsort -> sg -> sg
    95   val add_defsort: xsort -> sg -> sg
    94   val add_defsort_i: sort -> sg -> sg
    96   val add_defsort_i: sort -> sg -> sg
    95   val add_types: (bstring * int * mixfix) list -> sg -> sg
    97   val add_types: (bstring * int * mixfix) list -> sg -> sg
       
    98   val add_nonterminals: bstring list -> sg -> sg
    96   val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
    99   val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
    97   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
   100   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
    98   val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
   101   val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
    99   val add_arities_i: (string * sort list * sort) list -> sg -> sg
   102   val add_arities_i: (string * sort list * sort) list -> sg -> sg
   100   val add_consts: (bstring * string * mixfix) list -> sg -> sg
   103   val add_consts: (bstring * string * mixfix) list -> sg -> sg
   194 
   197 
   195 fun deref (SgRef (Some (ref sg))) = sg
   198 fun deref (SgRef (Some (ref sg))) = sg
   196   | deref (SgRef None) = sys_error "Sign.deref";
   199   | deref (SgRef None) = sys_error "Sign.deref";
   197 
   200 
   198 fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   201 fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   199   if name = "" orelse name = "#" then
   202   if name = "" orelse ord name = ord "#" then
   200     raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   203     raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   201   else name;
   204   else name;
   202 
   205 
   203 
   206 
   204 (* inclusion and equality *)
   207 (* inclusion and equality *)
   235   same version of it*)
   238   same version of it*)
   236 fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   239 fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   237   eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   240   eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   238 
   241 
   239 (*test for drafts*)
   242 (*test for drafts*)
   240 fun is_draft (Sg ({stamps = ref "#" :: _, ...}, _)) = true
   243 fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) = name = "" orelse ord name = ord "#";
   241   | is_draft _ = false;
       
   242 
   244 
   243 
   245 
   244 (* classes and sorts *)
   246 (* classes and sorts *)
   245 
   247 
   246 val classes = #classes o Type.rep_tsig o tsig_of;
   248 val classes = #classes o Type.rep_tsig o tsig_of;
   247 
   249 
       
   250 val defaultS = Type.defaultS o tsig_of;
   248 val subsort = Type.subsort o tsig_of;
   251 val subsort = Type.subsort o tsig_of;
   249 val norm_sort = Type.norm_sort o tsig_of;
   252 val norm_sort = Type.norm_sort o tsig_of;
   250 val nonempty_sort = Type.nonempty_sort o tsig_of;
   253 val nonempty_sort = Type.nonempty_sort o tsig_of;
   251 
   254 
   252 fun of_sort (Sg (_, {tsig, ...})) =
   255 fun of_sort (Sg (_, {tsig, ...})) =
   450   fun intern_const sg = intrn (spaces_of sg) constK;
   453   fun intern_const sg = intrn (spaces_of sg) constK;
   451 
   454 
   452   val intern_tycons = intrn_tycons o spaces_of;
   455   val intern_tycons = intrn_tycons o spaces_of;
   453 
   456 
   454   val full_name = full o #path o rep_sg;
   457   val full_name = full o #path o rep_sg;
       
   458   fun full_name_path sg elems name =		(* FIXME "..", "/" semantics (!?) *)
       
   459     full (#path (rep_sg sg) @ NameSpace.unpack elems) name;
   455 end;
   460 end;
   456 
   461 
   457 
   462 
   458 
   463 
   459 (** pretty printing of terms, types etc. **)
   464 (** pretty printing of terms, types etc. **)
   679     (Syntax.extend_type_gram syn types,
   684     (Syntax.extend_type_gram syn types,
   680       Type.ext_tsig_types tsig decls, ctab,
   685       Type.ext_tsig_types tsig decls, ctab,
   681       (path, add_names spaces typeK (map fst decls)), data)
   686       (path, add_names spaces typeK (map fst decls)), data)
   682   end;
   687   end;
   683 
   688 
       
   689 fun ext_nonterminals sg nonterms =
       
   690   ext_types sg (map (fn n => (n, 0, Syntax.NoSyn)) nonterms);
       
   691 
   684 
   692 
   685 (* add type abbreviations *)
   693 (* add type abbreviations *)
   686 
   694 
   687 fun read_abbr syn tsig spaces (t, vs, rhs_src) =
   695 fun read_abbr syn tsig spaces (t, vs, rhs_src) =
   688   (t, vs, rd_raw_typ syn tsig spaces (K None) rhs_src)
   696   (t, vs, rd_raw_typ syn tsig spaces (K None) rhs_src)
   816   (extfun syn args, tsig, ctab, names, data);
   824   (extfun syn args, tsig, ctab, names, data);
   817 
   825 
   818 
   826 
   819 (* add to path *)
   827 (* add to path *)
   820 
   828 
   821 fun ext_path (syn, tsig, ctab, (path, spaces), data) elem =
   829 fun ext_path (syn, tsig, ctab, (path, spaces), data) elems =
   822   let
   830   let
   823     val path' =
   831     val path' =
   824       if elem = ".." andalso not (null path) then fst (split_last path)
   832       if elems = ".." andalso not (null path) then fst (split_last path)
   825       else if elem = "/" then []
   833       else if elems = "/" then []
   826       else path @ NameSpace.unpack elem;
   834       else path @ NameSpace.unpack elems;
   827   in
   835   in
   828     (syn, tsig, ctab, (path', spaces), data)
   836     (syn, tsig, ctab, (path', spaces), data)
   829   end;      
   837   end;      
   830 
   838 
   831 
   839 
   851 val add_classrel     = extend_sign true (ext_classrel true) "#";
   859 val add_classrel     = extend_sign true (ext_classrel true) "#";
   852 val add_classrel_i   = extend_sign true (ext_classrel false) "#";
   860 val add_classrel_i   = extend_sign true (ext_classrel false) "#";
   853 val add_defsort      = extend_sign true (ext_defsort true) "#";
   861 val add_defsort      = extend_sign true (ext_defsort true) "#";
   854 val add_defsort_i    = extend_sign true (ext_defsort false) "#";
   862 val add_defsort_i    = extend_sign true (ext_defsort false) "#";
   855 val add_types        = extend_sign true ext_types "#";
   863 val add_types        = extend_sign true ext_types "#";
       
   864 val add_nonterminals = extend_sign true ext_nonterminals "#";
   856 val add_tyabbrs      = extend_sign true ext_tyabbrs "#";
   865 val add_tyabbrs      = extend_sign true ext_tyabbrs "#";
   857 val add_tyabbrs_i    = extend_sign true ext_tyabbrs_i "#";
   866 val add_tyabbrs_i    = extend_sign true ext_tyabbrs_i "#";
   858 val add_arities      = extend_sign true (ext_arities true) "#";
   867 val add_arities      = extend_sign true (ext_arities true) "#";
   859 val add_arities_i    = extend_sign true (ext_arities false) "#";
   868 val add_arities_i    = extend_sign true (ext_arities false) "#";
   860 val add_consts       = extend_sign true ext_consts "#";
   869 val add_consts       = extend_sign true ext_consts "#";