more consistent parsing and reading of classes and type constructors
authorhaftmann
Sat Jun 15 17:19:23 2013 +0200 (2013-06-15)
changeset 52377afa72aaed518
parent 52376 90fd1922f45f
child 52378 08dbf9ff2140
more consistent parsing and reading of classes and type constructors
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Fri Jun 14 22:16:48 2013 -0700
     1.2 +++ b/src/Tools/Code/code_target.ML	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -88,6 +88,69 @@
     1.4  type const_syntax = Code_Printer.const_syntax;
     1.5  
     1.6  
     1.7 +(** checking and parsing of symbols **)
     1.8 +
     1.9 +fun cert_const thy const =
    1.10 +  let
    1.11 +    val _ = if Sign.declared_const thy const then ()
    1.12 +      else error ("No such constant: " ^ quote const);
    1.13 +  in const end;
    1.14 +
    1.15 +fun cert_tyco thy tyco =
    1.16 +  let
    1.17 +    val _ = if Sign.declared_tyname thy tyco then ()
    1.18 +      else error ("No such type constructor: " ^ quote tyco);
    1.19 +  in tyco end;
    1.20 +
    1.21 +fun read_tyco thy = #1 o dest_Type
    1.22 +  o Proof_Context.read_type_name_proper (Proof_Context.init_global thy) true;
    1.23 +
    1.24 +fun cert_class thy class =
    1.25 +  let
    1.26 +    val _ = Axclass.get_info thy class;
    1.27 +  in class end;
    1.28 +
    1.29 +fun read_class thy = Proof_Context.read_class (Proof_Context.init_global thy);
    1.30 +
    1.31 +val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
    1.32 +
    1.33 +fun cert_inst thy (class, tyco) =
    1.34 +  (cert_class thy class, cert_tyco thy tyco);
    1.35 +
    1.36 +fun read_inst thy (raw_tyco, raw_class) =
    1.37 +  (read_class thy raw_class, read_tyco thy raw_tyco);
    1.38 +
    1.39 +val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
    1.40 +
    1.41 +fun cert_syms thy =
    1.42 +  Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
    1.43 +    (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
    1.44 +
    1.45 +fun read_syms thy =
    1.46 +  Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
    1.47 +    (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
    1.48 +
    1.49 +fun check_name is_module s =
    1.50 +  let
    1.51 +    val _ = if s = "" then error "Bad empty code name" else ();
    1.52 +    val xs = Long_Name.explode s;
    1.53 +    val xs' = if is_module
    1.54 +        then map (Name.desymbolize true) xs
    1.55 +      else if length xs < 2
    1.56 +        then error ("Bad code name without module component: " ^ quote s)
    1.57 +      else
    1.58 +        let
    1.59 +          val (ys, y) = split_last xs;
    1.60 +          val ys' = map (Name.desymbolize true) ys;
    1.61 +          val y' = Name.desymbolize false y;
    1.62 +        in ys' @ [y'] end;
    1.63 +  in if xs' = xs
    1.64 +    then s
    1.65 +    else error ("Invalid code name: " ^ quote s ^ "\n"
    1.66 +      ^ "better try " ^ quote (Long_Name.implode xs'))
    1.67 +  end;
    1.68 +
    1.69 +
    1.70  (** serializations and serializer **)
    1.71  
    1.72  (* serialization: abstract nonsense to cover different destinies for generated code *)
    1.73 @@ -494,7 +557,7 @@
    1.74    >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
    1.75  
    1.76  val parse_consts = parse_names "consts" Args.term
    1.77 -  Code.check_const Code_Thingol.lookup_const ;
    1.78 +  Code.check_const Code_Thingol.lookup_const;
    1.79  
    1.80  val parse_types = parse_names "types" (Scan.lift Args.name)
    1.81    Sign.intern_type Code_Thingol.lookup_tyco;
    1.82 @@ -539,66 +602,7 @@
    1.83    end;
    1.84  
    1.85  
    1.86 -(* checking and parsing *)
    1.87 -
    1.88 -fun cert_const thy const =
    1.89 -  let
    1.90 -    val _ = if Sign.declared_const thy const then ()
    1.91 -      else error ("No such constant: " ^ quote const);
    1.92 -  in const end;
    1.93 -
    1.94 -fun cert_tyco thy tyco =
    1.95 -  let
    1.96 -    val _ = if Sign.declared_tyname thy tyco then ()
    1.97 -      else error ("No such type constructor: " ^ quote tyco);
    1.98 -  in tyco end;
    1.99 -
   1.100 -fun read_tyco thy = cert_tyco thy o Sign.intern_type thy;
   1.101 -
   1.102 -fun cert_class thy class =
   1.103 -  let
   1.104 -    val _ = Axclass.get_info thy class;
   1.105 -  in class end;
   1.106 -
   1.107 -fun read_class thy = cert_class thy o Sign.intern_class thy;
   1.108 -
   1.109 -val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
   1.110 -
   1.111 -fun cert_inst thy (class, tyco) =
   1.112 -  (cert_class thy class, cert_tyco thy tyco);
   1.113 -
   1.114 -fun read_inst thy (raw_tyco, raw_class) =
   1.115 -  (read_class thy raw_class, read_tyco thy raw_tyco);
   1.116 -
   1.117 -val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
   1.118 -
   1.119 -fun cert_syms thy =
   1.120 -  Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy))
   1.121 -    (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I;
   1.122 -
   1.123 -fun read_syms thy =
   1.124 -  Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy))
   1.125 -    (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I;
   1.126 -
   1.127 -fun check_name is_module s =
   1.128 -  let
   1.129 -    val _ = if s = "" then error "Bad empty code name" else ();
   1.130 -    val xs = Long_Name.explode s;
   1.131 -    val xs' = if is_module
   1.132 -        then map (Name.desymbolize true) xs
   1.133 -      else if length xs < 2
   1.134 -        then error ("Bad code name without module component: " ^ quote s)
   1.135 -      else
   1.136 -        let
   1.137 -          val (ys, y) = split_last xs;
   1.138 -          val ys' = map (Name.desymbolize true) ys;
   1.139 -          val y' = Name.desymbolize false y;
   1.140 -        in ys' @ [y'] end;
   1.141 -  in if xs' = xs
   1.142 -    then s
   1.143 -    else error ("Invalid code name: " ^ quote s ^ "\n"
   1.144 -      ^ "better try " ^ quote (Long_Name.implode xs'))
   1.145 -  end;
   1.146 +(* checking of syntax *)
   1.147  
   1.148  fun check_const_syntax thy c syn =
   1.149    if Code_Printer.requires_args syn > Code.args_number thy c
   1.150 @@ -744,9 +748,9 @@
   1.151  fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   1.152    parse_single_symbol_pragma @{keyword "constant"} Parse.term_group parse_const
   1.153      >> Code_Symbol.Constant
   1.154 -  || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.xname parse_tyco
   1.155 +  || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
   1.156      >> Code_Symbol.Type_Constructor
   1.157 -  || parse_single_symbol_pragma @{keyword "type_class"} Parse.xname parse_class
   1.158 +  || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
   1.159      >> Code_Symbol.Type_Class
   1.160    || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
   1.161      >> Code_Symbol.Class_Relation
   1.162 @@ -801,17 +805,17 @@
   1.163  
   1.164  val _ =
   1.165    Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
   1.166 -    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
   1.167 +    (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax
   1.168        add_tyco_syntax_cmd);
   1.169  
   1.170  val _ =
   1.171    Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
   1.172 -    (process_multi_syntax Parse.xname Parse.string
   1.173 +    (process_multi_syntax Parse.class Parse.string
   1.174        add_class_syntax_cmd);
   1.175  
   1.176  val _ =
   1.177    Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
   1.178 -    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) (Parse.minus >> K ())
   1.179 +    (process_multi_syntax parse_inst_ident (Parse.minus >> K ())
   1.180        add_instance_syntax_cmd);
   1.181  
   1.182  val _ =