src/Pure/sign.ML
changeset 8725 0e48ee5b52db
parent 8715 2cdabe1bb350
child 8730 d97ee7249698
equal deleted inserted replaced
8724:ef7efded8fdc 8725:0e48ee5b52db
   123     (string * string * (string -> string * real)) list -> sg -> sg
   123     (string * string * (string -> string * real)) list -> sg -> sg
   124   val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   124   val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   125   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   125   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   126   val add_path: string -> sg -> sg
   126   val add_path: string -> sg -> sg
   127   val add_space: string * string list -> sg -> sg
   127   val add_space: string * string list -> sg -> sg
       
   128   val hide_space: string * string list -> sg -> sg
       
   129   val hide_space_i: string * string list -> sg -> sg
   128   val add_name: string -> sg -> sg
   130   val add_name: string -> sg -> sg
   129   val data_kinds: data -> string list
   131   val data_kinds: data -> string list
   130   val merge_refs: sg_ref * sg_ref -> sg_ref
   132   val merge_refs: sg_ref * sg_ref -> sg_ref
   131   val merge: sg * sg -> sg
   133   val merge: sg * sg -> sg
   132   val prep_ext: sg -> sg
   134   val prep_ext: sg -> sg
   405 val classK = "class";
   407 val classK = "class";
   406 val typeK = "type";
   408 val typeK = "type";
   407 val constK = "const";
   409 val constK = "const";
   408 
   410 
   409 
   411 
   410 (* add and retrieve names *)
   412 (* declare and retrieve names *)
   411 
   413 
   412 fun space_of spaces kind =
   414 fun space_of spaces kind =
   413   if_none (assoc (spaces, kind)) NameSpace.empty;
   415   if_none (assoc (spaces, kind)) NameSpace.empty;
   414 
   416 
   415 (*input and output of qualified names*)
   417 (*input and output of qualified names*)
   416 fun intrn spaces kind = NameSpace.intern (space_of spaces kind);
   418 fun intrn spaces kind = NameSpace.intern (space_of spaces kind);
   417 fun extrn spaces kind = NameSpace.extern (space_of spaces kind);
   419 fun extrn spaces kind = NameSpace.extern (space_of spaces kind);
   418 fun cond_extrn spaces kind = NameSpace.cond_extern (space_of spaces kind);
   420 fun cond_extrn spaces kind = NameSpace.cond_extern (space_of spaces kind);
   419 fun cond_extrn_table spaces kind tab = NameSpace.cond_extern_table (space_of spaces kind) tab;
   421 fun cond_extrn_table spaces kind tab = NameSpace.cond_extern_table (space_of spaces kind) tab;
   420 
   422 
   421 (*add names*)
   423 (*add / hide names*)
   422 fun add_names spaces kind names =
   424 fun change_space f spaces kind x = overwrite (spaces, (kind, f (space_of spaces kind, x)));
   423   let val space' = NameSpace.extend (space_of spaces kind, names) in
   425 val add_names = change_space NameSpace.extend;
   424     overwrite (spaces, (kind, space'))
   426 val hide_names = change_space NameSpace.hide;
   425   end;
       
   426 
   427 
   427 (*make full names*)
   428 (*make full names*)
   428 fun full path name =
   429 fun full path name =
   429   if name = "" then error "Attempt to declare empty name \"\""
   430   if name = "" then error "Attempt to declare empty name \"\""
   430   else if NameSpace.qualified name then
   431   else if NameSpace.is_qualified name then
   431     error ("Attempt to declare qualified name " ^ quote name)
   432     error ("Attempt to declare qualified name " ^ quote name)
   432   else NameSpace.pack (path @ [name]);
   433   else NameSpace.pack (path @ [name]);
   433 
   434 
   434 (*base name*)
   435 (*base name*)
   435 val base_name = NameSpace.base;
   436 val base_name = NameSpace.base;
   614   in nodups (([], []), ([], [])) tm; tm end;
   615   in nodups (([], []), ([], [])) tm; tm end;
   615 
   616 
   616 (*compute and check type of the term*)
   617 (*compute and check type of the term*)
   617 fun type_check sg tm =
   618 fun type_check sg tm =
   618   let
   619   let
   619     val prt =
   620     val prt = setmp Syntax.show_brackets true (pretty_term sg);
   620       setmp Syntax.show_brackets true
   621     val prT = pretty_typ sg;
   621         (setmp NameSpace.long_names true (pretty_term sg));
       
   622     val prT = setmp NameSpace.long_names true (pretty_typ sg);
       
   623 
   622 
   624     fun err_appl why bs t T u U =
   623     fun err_appl why bs t T u U =
   625       let
   624       let
   626         val xs = map Free bs;		(*we do not rename here*)
   625         val xs = map Free bs;		(*we do not rename here*)
   627         val t' = subst_bounds (xs, t);
   626         val t' = subst_bounds (xs, t);
   688 *)
   687 *)
   689 
   688 
   690 fun infer_types_simult sg def_type def_sort used freeze args =
   689 fun infer_types_simult sg def_type def_sort used freeze args =
   691   let
   690   let
   692     val tsig = tsig_of sg;
   691     val tsig = tsig_of sg;
   693     val prt =
   692     val prt = setmp Syntax.show_brackets true (pretty_term sg);
   694       setmp Syntax.show_brackets true
   693     val prT = pretty_typ sg;
   695         (setmp NameSpace.long_names true (pretty_term sg));
       
   696     val prT = setmp NameSpace.long_names true (pretty_typ sg);
       
   697 
   694 
   698     val termss = foldr multiply (map fst args, [[]]);
   695     val termss = foldr multiply (map fst args, [[]]);
   699     val typs =
   696     val typs =
   700       map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   697       map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   701 
   698 
   921   in
   918   in
   922     (syn, tsig, ctab, (path', spaces), data)
   919     (syn, tsig, ctab, (path', spaces), data)
   923   end;      
   920   end;      
   924 
   921 
   925 
   922 
   926 (* add to name space *)
   923 (* change name space *)
   927 
   924 
   928 fun ext_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
   925 fun ext_add_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
   929   (syn, tsig, ctab, (path, add_names spaces kind names), data);
   926   (syn, tsig, ctab, (path, add_names spaces kind names), data);
       
   927 
       
   928 fun ext_hide_space (syn, tsig, ctab, (path, spaces), data) (kind, xnames) =
       
   929   (syn, tsig, ctab, (path, hide_names spaces kind (map (intrn spaces kind) xnames)), data);
       
   930 
       
   931 fun ext_hide_space_i (syn, tsig, ctab, (path, spaces), data) (kind, names) =
       
   932   (syn, tsig, ctab, (path, hide_names spaces kind names), data);
   930 
   933 
   931 
   934 
   932 (* signature data *)
   935 (* signature data *)
   933 
   936 
   934 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
   937 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
   974 val add_trfunsT       = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
   977 val add_trfunsT       = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
   975 val add_tokentrfuns   = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
   978 val add_tokentrfuns   = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
   976 val add_trrules       = extend_sign true ext_trrules "#";
   979 val add_trrules       = extend_sign true ext_trrules "#";
   977 val add_trrules_i     = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   980 val add_trrules_i     = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   978 val add_path          = extend_sign true ext_path "#";
   981 val add_path          = extend_sign true ext_path "#";
   979 val add_space         = extend_sign true ext_space "#";
   982 val add_space         = extend_sign true ext_add_space "#";
       
   983 val hide_space        = extend_sign true ext_hide_space "#";
       
   984 val hide_space_i      = extend_sign true ext_hide_space_i "#";
   980 fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
   985 fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
   981 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
   986 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
   982 fun add_name name sg  = extend_sign true K name () sg;
   987 fun add_name name sg  = extend_sign true K name () sg;
   983 fun prep_ext sg       = extend_sign false K "#" () sg;
   988 fun prep_ext sg       = extend_sign false K "#" () sg;
   984 
   989