- made modes_of more robust
authorberghofe
Thu Mar 07 12:03:43 2002 +0100 (2002-03-07)
changeset 13038e968745986f1
parent 13037 f7f29f8380ce
child 13039 cfcc1f6f21df
- made modes_of more robust
- assoc_code now has higher priority than inductive_codegen
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Mar 06 23:59:28 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Mar 07 12:03:43 2002 +0100
     1.3 @@ -127,6 +127,10 @@
     1.4  val term_vs = map (fst o fst o dest_Var) o term_vars;
     1.5  val terms_vs = distinct o flat o (map term_vs);
     1.6  
     1.7 +fun assoc' s tab key = (case assoc (tab, key) of
     1.8 +      None => error ("Unable to determine " ^ s ^ " of " ^ quote key)
     1.9 +    | Some x => x);
    1.10 +
    1.11  (** collect all Vars in a term (with duplicates!) **)
    1.12  fun term_vTs t = map (apfst fst o dest_Var)
    1.13    (filter is_Var (foldl_aterms (op :: o Library.swap) ([], t)));
    1.14 @@ -163,11 +167,12 @@
    1.15          (fn (None, _) => [None]
    1.16            | (Some js, arg) => map Some
    1.17                (filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
    1.18 -                (iss ~~ args)))) (the (assoc (modes, name))))
    1.19 +                (iss ~~ args)))) (assoc' "modes" modes name))
    1.20  
    1.21    in (case strip_comb t of
    1.22        (Const (name, _), args) => mk_modes name args
    1.23 -    | (Var ((name, _), _), args) => mk_modes name args)
    1.24 +    | (Var ((name, _), _), args) => mk_modes name args
    1.25 +    | (Free (name, _), args) => mk_modes name args)
    1.26    end;
    1.27  
    1.28  datatype indprem = Prem of term list * term | Sidecond of term;
    1.29 @@ -478,9 +483,9 @@
    1.30    end;
    1.31  
    1.32  fun mk_ind_call thy gr dep t u is_query = (case head_of u of
    1.33 -  Const (s, _) => (case get_clauses thy s of
    1.34 -       None => None
    1.35 -     | Some (names, intrs) =>
    1.36 +  Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
    1.37 +       (None, _) => None
    1.38 +     | (Some (names, intrs), None) =>
    1.39           let
    1.40            fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
    1.41                  ((ts, mode), i+1)
    1.42 @@ -504,7 +509,8 @@
    1.43           in
    1.44             Some (gr3, Pretty.block
    1.45               (ps @ [Pretty.brk 1, mk_tuple in_ps]))
    1.46 -         end)
    1.47 +         end
    1.48 +     | _ => None)
    1.49    | _ => None);
    1.50  
    1.51  fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =