added fillin_mixfix' needed by serializer
authorhaftmann
Mon Nov 07 09:34:51 2005 +0100 (2005-11-07)
changeset 18098227ecb2cfa3d
parent 18097 d196d84c306f
child 18099 e956b04fea22
added fillin_mixfix' needed by serializer
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Sun Nov 06 01:21:37 2005 +0100
     1.2 +++ b/src/Pure/codegen.ML	Mon Nov 07 09:34:51 2005 +0100
     1.3 @@ -78,6 +78,7 @@
     1.4    val eval_result: term ref
     1.5    val eval_term: theory -> term -> term
     1.6    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
     1.7 +  val fillin_mixfix': 'a mixfix list -> Pretty.T list -> string list * Pretty.T
     1.8    val mk_deftab: theory -> deftab
     1.9  
    1.10    val get_node: codegr -> string -> node
    1.11 @@ -552,7 +553,7 @@
    1.12  fun is_instance thy T1 T2 =
    1.13    Sign.typ_instance thy (T1, Type.varifyT T2);
    1.14  
    1.15 -fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
    1.16 +fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
    1.17    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
    1.18  
    1.19  fun get_aux_code xs = List.mapPartial (fn (m, code) =>
    1.20 @@ -634,6 +635,25 @@
    1.21    | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
    1.22        q :: pretty_mixfix module module' ms ps qs;
    1.23  
    1.24 +fun fillin_mixfix' ms args =
    1.25 +  let
    1.26 +    fun fillin [] [] vars = (vars, [])
    1.27 +      | fillin (Arg :: ms) [] vars =
    1.28 +          let
    1.29 +            val v = "a_" ^ (string_of_int o length) vars;
    1.30 +          in fillin ms args (v::vars) ||> (cons o Pretty.str) v end
    1.31 +      | fillin (Arg :: ms) (a :: args) vars =
    1.32 +          fillin ms args vars ||> cons a
    1.33 +      | fillin (Ignore :: ms) args vars =
    1.34 +          fillin ms args vars
    1.35 +      | fillin (Module :: ms) args vars =
    1.36 +          fillin ms args vars
    1.37 +      | fillin (Pretty p :: ms) args vars =
    1.38 +          fillin ms args vars ||> cons p
    1.39 +      | fillin (Quote _ :: ms) args vars =
    1.40 +          error ("no quotes currently supported in codegen patterns");
    1.41 +  in fillin ms args [] ||> Pretty.block end;
    1.42 +
    1.43  
    1.44  (**** default code generators ****)
    1.45  
    1.46 @@ -811,7 +831,7 @@
    1.47      fun string_of_cycle (a :: b :: cs) =
    1.48            let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
    1.49              if a = a' then Option.map (pair x)
    1.50 -              (find_first (equal b o #2 o Graph.get_node gr)
    1.51 +              (Library.find_first (equal b o #2 o Graph.get_node gr)
    1.52                  (Graph.imm_succs gr x))
    1.53              else NONE) code
    1.54            in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end