# HG changeset patch # User berghofe # Date 1038414138 -3600 # Node ID e2d17090052bbb15d12b1a27866b95f5c9171866 # Parent 09aeb7346d3f7a5acbf76e980fc316ec5af0759f Parameters in definitions are now renamed to avoid clashes with reserved ML keywords. diff -r 09aeb7346d3f -r e2d17090052b src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Nov 27 17:20:49 2002 +0100 +++ b/src/Pure/codegen.ML Wed Nov 27 17:22:18 2002 +0100 @@ -206,33 +206,6 @@ fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s); -(**** retrieve definition of constant ****) - -fun is_instance thy T1 T2 = - Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2); - -fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) => - s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); - -fun get_defn thy s T = - let - val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) - (thy :: Theory.ancestors_of thy)); - val defs = mapfilter (fn (_, t) => - (let - val (lhs, rhs) = Logic.dest_equals t; - val (c, args) = strip_comb lhs; - val (s', T') = dest_Const c - in if s=s' then Some (T', (args, rhs)) else None end) handle TERM _ => - None) axms; - val i = find_index (is_instance thy T o fst) defs - in - if i>=0 then Some (snd (nth_elem (i, defs)), - if length defs = 1 then None else Some i) - else None - end; - - (**** make valid ML identifiers ****) fun gen_mk_id kind rename sg s = @@ -254,9 +227,10 @@ val mk_type_id = gen_mk_id Sign.typeK (fn s => if s mem ThmDatabase.ml_reserved then s ^ "_type" else s); -fun rename_term t = +fun rename_terms ts = let - val names = add_term_names (t, map (fst o fst o dest_Var) (term_vars t)); + val names = foldr add_term_names + (ts, map (fst o fst) (Drule.vars_of_terms ts)); val clash = names inter ThmDatabase.ml_reserved; val ps = clash ~~ variantlist (clash, names); @@ -266,7 +240,36 @@ | rename (t $ u) = rename t $ rename u | rename t = t; in - rename t + map rename ts + end; + +val rename_term = hd o rename_terms o single; + + +(**** retrieve definition of constant ****) + +fun is_instance thy T1 T2 = + Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2); + +fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) => + s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); + +fun get_defn thy s T = + let + val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) + (thy :: Theory.ancestors_of thy)); + val defs = mapfilter (fn (_, t) => + (let + val (lhs, rhs) = Logic.dest_equals t; + val (c, args) = strip_comb lhs; + val (s', T') = dest_Const c + in if s=s' then Some (T', split_last (rename_terms (args @ [rhs]))) + else None end) handle TERM _ => None) axms; + val i = find_index (is_instance thy T o fst) defs + in + if i>=0 then Some (snd (nth_elem (i, defs)), + if length defs = 1 then None else Some i) + else None end; @@ -441,6 +444,8 @@ (**** Interface ****) +val str = setmp print_mode [] Pretty.str; + fun parse_mixfix rd s = (case Scan.finite Symbol.stopper (Scan.repeat ( $$ "_" >> K Arg @@ -453,7 +458,7 @@ || Scan.repeat1 ( $$ "'" |-- Scan.one Symbol.not_eof || Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*") - (Scan.one Symbol.not_eof)) >> (Pretty o Pretty.str o implode))) + (Scan.one Symbol.not_eof)) >> (Pretty o str o implode))) (Symbol.explode s) of (p, []) => p | _ => error ("Malformed annotation: " ^ quote s));