src/Pure/codegen.ML
changeset 16458 4c6fd0c01d28
parent 16364 dc9f7066d80a
child 16649 d88271eb5b26
     1.1 --- a/src/Pure/codegen.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -38,8 +38,8 @@
     1.4    val invoke_tycodegen: theory -> string -> bool ->
     1.5      (exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T
     1.6    val mk_id: string -> string
     1.7 -  val mk_const_id: Sign.sg -> string -> string
     1.8 -  val mk_type_id: Sign.sg -> string -> string
     1.9 +  val mk_const_id: theory -> string -> string
    1.10 +  val mk_type_id: theory -> string -> string
    1.11    val rename_term: term -> term
    1.12    val new_names: term -> string list -> string list
    1.13    val new_name: term -> string -> string
    1.14 @@ -50,8 +50,8 @@
    1.15    val eta_expand: term -> term list -> int -> term
    1.16    val strip_tname: string -> string
    1.17    val mk_type: bool -> typ -> Pretty.T
    1.18 -  val mk_term_of: Sign.sg -> bool -> typ -> Pretty.T
    1.19 -  val mk_gen: Sign.sg -> bool -> string list -> string -> typ -> Pretty.T
    1.20 +  val mk_term_of: theory -> bool -> typ -> Pretty.T
    1.21 +  val mk_gen: theory -> bool -> string list -> string -> typ -> Pretty.T
    1.22    val test_fn: (int -> (string * term) list option) ref
    1.23    val test_term: theory -> int -> int -> term -> (string * term) list option
    1.24    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    1.25 @@ -121,14 +121,14 @@
    1.26  fun set_iterations iterations ({size, default_type, ...} : test_params) =
    1.27    {size = size, iterations = iterations, default_type = default_type};
    1.28  
    1.29 -fun set_default_type s sg ({size, iterations, ...} : test_params) =
    1.30 +fun set_default_type s thy ({size, iterations, ...} : test_params) =
    1.31    {size = size, iterations = iterations,
    1.32 -   default_type = SOME (typ_of (read_ctyp sg s))};
    1.33 +   default_type = SOME (typ_of (read_ctyp thy s))};
    1.34  
    1.35  (* data kind 'Pure/codegen' *)
    1.36 - 
    1.37 -structure CodegenArgs =
    1.38 -struct
    1.39 +
    1.40 +structure CodegenData = TheoryDataFun
    1.41 +(struct
    1.42    val name = "Pure/codegen";
    1.43    type T =
    1.44      {codegens : (string * term codegen) list,
    1.45 @@ -143,9 +143,9 @@
    1.46      {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
    1.47       preprocs = [], test_params = default_test_params};
    1.48    val copy = I;
    1.49 -  val prep_ext = I;
    1.50 +  val extend = I;
    1.51  
    1.52 -  fun merge
    1.53 +  fun merge _
    1.54      ({codegens = codegens1, tycodegens = tycodegens1,
    1.55        consts = consts1, types = types1, attrs = attrs1,
    1.56        preprocs = preprocs1, test_params = test_params1},
    1.57 @@ -160,13 +160,12 @@
    1.58       preprocs = merge_alists' preprocs1 preprocs2,
    1.59       test_params = merge_test_params test_params1 test_params2};
    1.60  
    1.61 -  fun print sg ({codegens, tycodegens, ...} : T) =
    1.62 +  fun print _ ({codegens, tycodegens, ...} : T) =
    1.63      Pretty.writeln (Pretty.chunks
    1.64        [Pretty.strs ("term code generators:" :: map fst codegens),
    1.65         Pretty.strs ("type code generators:" :: map fst tycodegens)]);
    1.66 -end;
    1.67 +end);
    1.68  
    1.69 -structure CodegenData = TheoryDataFun(CodegenArgs);
    1.70  val _ = Context.add_setup [CodegenData.init];
    1.71  val print_codegens = CodegenData.print;
    1.72  
    1.73 @@ -265,18 +264,17 @@
    1.74  
    1.75  fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
    1.76    let
    1.77 -    val sg = sign_of thy;
    1.78      val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
    1.79        CodegenData.get thy;
    1.80 -    val cname = Sign.intern_const sg s;
    1.81 +    val cname = Sign.intern_const thy s;
    1.82    in
    1.83 -    (case Sign.const_type sg cname of
    1.84 +    (case Sign.const_type thy cname of
    1.85         SOME T =>
    1.86           let val T' = (case tyopt of
    1.87                  NONE => T
    1.88                | SOME ty =>
    1.89 -                  let val U = prep_type sg ty
    1.90 -                  in if Sign.typ_instance sg (U, T) then U
    1.91 +                  let val U = prep_type thy ty
    1.92 +                  in if Sign.typ_instance thy (U, T) then U
    1.93                      else error ("Illegal type constraint for constant " ^ cname)
    1.94                    end)
    1.95           in (case assoc (consts, (cname, T')) of
    1.96 @@ -291,7 +289,7 @@
    1.97    end) (thy, xs);
    1.98  
    1.99  val assoc_consts_i = gen_assoc_consts (K I);
   1.100 -val assoc_consts = gen_assoc_consts (fn sg => typ_of o read_ctyp sg);
   1.101 +val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp);
   1.102  
   1.103  
   1.104  (**** associate types with target language types ****)
   1.105 @@ -322,7 +320,7 @@
   1.106      ("<" :: "^" :: xs, ">") => (true, implode xs)
   1.107    | ("<" :: xs, ">") => (false, implode xs)
   1.108    | _ => sys_error "dest_sym");
   1.109 -  
   1.110 +
   1.111  fun mk_id s = if s = "" then "" else
   1.112    let
   1.113      fun check_str [] = []
   1.114 @@ -341,12 +339,12 @@
   1.115      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   1.116    end;
   1.117  
   1.118 -fun mk_const_id sg s =
   1.119 -  let val s' = mk_id (Sign.extern_const sg s)
   1.120 +fun mk_const_id thy s =
   1.121 +  let val s' = mk_id (Sign.extern_const thy s)
   1.122    in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
   1.123  
   1.124 -fun mk_type_id sg s =
   1.125 -  let val s' = mk_id (Sign.extern_type sg s)
   1.126 +fun mk_type_id thy s =
   1.127 +  let val s' = mk_id (Sign.extern_type thy s)
   1.128    in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
   1.129  
   1.130  fun rename_terms ts =
   1.131 @@ -570,11 +568,10 @@
   1.132  fun gen_generate_code prep_term thy =
   1.133    setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   1.134    let
   1.135 -    val sg = sign_of thy;
   1.136      val gr = Graph.new_node ("<Top>", (NONE, "")) Graph.empty;
   1.137      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   1.138        (invoke_codegen thy "<Top>" false (gr, t)))
   1.139 -        (gr, map (apsnd (prep_term sg)) xs)
   1.140 +        (gr, map (apsnd (prep_term thy)) xs)
   1.141      val code =
   1.142        "structure Generated =\nstruct\n\n" ^
   1.143        output_code gr' ["<Top>"] ^
   1.144 @@ -585,7 +582,7 @@
   1.145  
   1.146  val generate_code_i = gen_generate_code (K I);
   1.147  val generate_code = gen_generate_code
   1.148 -  (fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT);
   1.149 +  (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT);
   1.150  
   1.151  
   1.152  (**** Reflection ****)
   1.153 @@ -603,22 +600,22 @@
   1.154        [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
   1.155         Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
   1.156  
   1.157 -fun mk_term_of sg p (TVar ((s, i), _)) = Pretty.str
   1.158 +fun mk_term_of _ p (TVar ((s, i), _)) = Pretty.str
   1.159        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
   1.160 -  | mk_term_of sg p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   1.161 -  | mk_term_of sg p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.162 -      (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id sg s) ::
   1.163 -        List.concat (map (fn T => [mk_term_of sg true T, mk_type true T]) Ts))));
   1.164 +  | mk_term_of _ p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   1.165 +  | mk_term_of thy p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.166 +      (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id thy s) ::
   1.167 +        List.concat (map (fn T => [mk_term_of thy true T, mk_type true T]) Ts))));
   1.168  
   1.169  
   1.170  (**** Test data generators ****)
   1.171  
   1.172 -fun mk_gen sg p xs a (TVar ((s, i), _)) = Pretty.str
   1.173 +fun mk_gen _ p xs a (TVar ((s, i), _)) = Pretty.str
   1.174        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   1.175 -  | mk_gen sg p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   1.176 -  | mk_gen sg p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.177 -      (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id sg s ^
   1.178 -        (if s mem xs then "'" else "")) :: map (mk_gen sg true xs a) Ts @
   1.179 +  | mk_gen _ p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   1.180 +  | mk_gen thy p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.181 +      (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id thy s ^
   1.182 +        (if s mem xs then "'" else "")) :: map (mk_gen thy true xs a) Ts @
   1.183          (if s mem xs then [Pretty.str a] else []))));
   1.184  
   1.185  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
   1.186 @@ -629,7 +626,6 @@
   1.187        "Term to be tested contains type variables";
   1.188      val _ = assert (null (term_vars t))
   1.189        "Term to be tested contains schematic variables";
   1.190 -    val sg = sign_of thy;
   1.191      val frees = map dest_Free (term_frees t);
   1.192      val szname = variant (map fst frees) "i";
   1.193      val s = "structure TestTerm =\nstruct\n\n" ^
   1.194 @@ -641,7 +637,7 @@
   1.195            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
   1.196              Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
   1.197                Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
   1.198 -              mk_gen sg false [] "" T, Pretty.brk 1,
   1.199 +              mk_gen thy false [] "" T, Pretty.brk 1,
   1.200                Pretty.str (szname ^ ";")]) frees)),
   1.201              Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
   1.202              Pretty.block [Pretty.str "if ",
   1.203 @@ -652,7 +648,7 @@
   1.204                  List.concat (separate [Pretty.str ",", Pretty.brk 1]
   1.205                    (map (fn (s, T) => [Pretty.block
   1.206                      [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   1.207 -                     mk_app false (mk_term_of sg false T)
   1.208 +                     mk_app false (mk_term_of thy false T)
   1.209                         [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
   1.210                    [Pretty.str "]"])]],
   1.211              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
   1.212 @@ -670,12 +666,12 @@
   1.213  
   1.214  fun test_goal ({size, iterations, default_type}, tvinsts) i st =
   1.215    let
   1.216 -    val sg = Toplevel.sign_of st;
   1.217 +    val thy = Toplevel.theory_of st;
   1.218      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
   1.219        | strip t = t;
   1.220      val (gi, frees) = Logic.goal_params
   1.221        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
   1.222 -    val gi' = ObjectLogic.atomize_term sg (map_term_types
   1.223 +    val gi' = ObjectLogic.atomize_term thy (map_term_types
   1.224        (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
   1.225          getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
   1.226    in case test_term (Toplevel.theory_of st) size iterations gi' of
   1.227 @@ -683,7 +679,7 @@
   1.228      | SOME cex => writeln ("Counterexample found:\n" ^
   1.229          Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
   1.230            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
   1.231 -            Sign.pretty_term sg t]) cex)))
   1.232 +            Sign.pretty_term thy t]) cex)))
   1.233    end;
   1.234  
   1.235  
   1.236 @@ -753,8 +749,8 @@
   1.237    P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
   1.238  
   1.239  fun parse_tyinst xs =
   1.240 -  (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn sg =>
   1.241 -    fn (x, ys) => (x, (v, typ_of (read_ctyp sg s)) :: ys))) xs;
   1.242 +  (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
   1.243 +    fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;
   1.244  
   1.245  fun app [] x = x
   1.246    | app (f :: fs) x = app fs (f x);
   1.247 @@ -768,7 +764,7 @@
   1.248  val testP =
   1.249    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   1.250    (Scan.option (P.$$$ "[" |-- P.list1
   1.251 -    (   parse_test_params >> (fn f => fn sg => apfst (f sg))
   1.252 +    (   parse_test_params >> (fn f => fn thy => apfst (f thy))
   1.253       || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
   1.254      (fn (ps, g) => Toplevel.keep (fn st =>
   1.255        test_goal (app (getOpt (Option.map