diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:18 2007 +0200 +++ b/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:20 2007 +0200 @@ -10,17 +10,14 @@ sig type T val timing: bool ref - val funcs: T -> CodeUnit.const -> thm list - val typ: T -> CodeUnit.const -> typ - val all: T -> CodeUnit.const list + val funcs: T -> string -> thm list + val typ: T -> string -> typ + val all: T -> string list val pretty: theory -> T -> Pretty.T - val make: theory -> CodeUnit.const list -> T - val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T + val make: theory -> string list -> T + val make_consts: theory -> string list -> string list * T val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a - val intervene: theory -> T -> T - (*FIXME drop intervene as soon as possible*) - structure Constgraph : GRAPH end structure CodeFuncgr : CODE_FUNCGR = @@ -28,23 +25,18 @@ (** the graph type **) -structure Constgraph = GraphFun ( - type key = CodeUnit.const; - val ord = CodeUnit.const_ord; -); - -type T = (typ * thm list) Constgraph.T; +type T = (typ * thm list) Graph.T; fun funcs funcgr = - these o Option.map snd o try (Constgraph.get_node funcgr); + these o Option.map snd o try (Graph.get_node funcgr); fun typ funcgr = - fst o Constgraph.get_node funcgr; + fst o Graph.get_node funcgr; -fun all funcgr = Constgraph.keys funcgr; +fun all funcgr = Graph.keys funcgr; fun pretty thy funcgr = - AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr) + AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr) |> (map o apfst) (CodeUnit.string_of_const thy) |> sort (string_ord o pairself fst) |> map (fn (s, thms) => @@ -63,13 +55,9 @@ |> (fold o fold_aterms) (fn Const c => f c | _ => I); fun consts_of (const, []) = [] - | consts_of (const, thms as thm :: _) = + | consts_of (const, thms as _ :: _) = let - val thy = Thm.theory_of_thm thm; - val is_refl = curry CodeUnit.eq_const const; - fun the_const c = case try (CodeUnit.const_of_cexpr thy) c - of SOME const => if is_refl const then I else insert CodeUnit.eq_const const - | NONE => I + fun the_const (c, _) = if c = const then I else insert (op =) c in fold_consts the_const thms [] end; fun insts_of thy algebra c ty_decl ty = @@ -114,7 +102,7 @@ local -exception INVALID of CodeUnit.const list * string; +exception INVALID of string list * string; fun resort_thms algebra tap_typ [] = [] | resort_thms algebra tap_typ (thms as thm :: _) = @@ -123,11 +111,11 @@ val cs = fold_consts (insert (op =)) thms []; fun match_const c (ty, ty_decl) = let - val tys = CodeUnit.typargs thy (c, ty); - val sorts = map (snd o dest_TVar) (CodeUnit.typargs thy (c, ty_decl)); + val tys = Sign.const_typargs thy (c, ty); + val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl)); in fold2 (curry (CodeUnit.typ_sort_inst algebra)) tys sorts end; - fun match (c_ty as (c, ty)) = - case tap_typ c_ty + fun match (c, ty) = + case tap_typ c of SOME ty_decl => match_const c (ty, ty_decl) | NONE => I; val tvars = fold match cs Vartab.empty; @@ -135,7 +123,7 @@ fun resort_funcss thy algebra funcgr = let - val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy); + val typ_funcgr = try (fst o Graph.get_node funcgr); fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms) handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e ^ ",\nfor constant " ^ CodeUnit.string_of_const thy const @@ -150,12 +138,11 @@ in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end; fun resort_recs funcss = let - fun tap_typ c_ty = case try (CodeUnit.const_of_cexpr thy) c_ty - of SOME const => AList.lookup (CodeUnit.eq_const) funcss const - |> these - |> try hd - |> Option.map (snd o CodeUnit.head_func) - | NONE => NONE; + fun tap_typ c = + AList.lookup (op =) funcss c + |> these + |> try hd + |> Option.map (snd o CodeUnit.head_func); val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss); val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; in (unchanged, funcss') end; @@ -172,7 +159,7 @@ try (AxClass.params_of_class thy) class |> Option.map snd |> these - |> map (fn (c, _) => (c, SOME tyco)) + |> map (fn (c, _) => Class.inst_const thy (c, tyco)) in Symtab.empty |> fold (fn (tyco, class) => @@ -184,8 +171,7 @@ fun instances_of_consts thy algebra funcgr consts = let fun inst (cexpr as (c, ty)) = insts_of thy algebra c - ((fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy) cexpr) - ty handle CLASS_ERROR => []; + ((fst o Graph.get_node funcgr) c) ty handle CLASS_ERROR => []; in [] |> fold (fold (insert (op =)) o inst) consts @@ -193,13 +179,13 @@ end; fun ensure_const' thy algebra funcgr const auxgr = - if can (Constgraph.get_node funcgr) const + if can (Graph.get_node funcgr) const then (NONE, auxgr) - else if can (Constgraph.get_node auxgr) const + else if can (Graph.get_node auxgr) const then (SOME const, auxgr) else if is_some (Code.get_datatype_of_constr thy const) then auxgr - |> Constgraph.new_node (const, []) + |> Graph.new_node (const, []) |> pair (SOME const) else let val thms = Code.these_funcs thy const @@ -208,9 +194,9 @@ val rhs = consts_of (const, thms); in auxgr - |> Constgraph.new_node (const, thms) + |> Graph.new_node (const, thms) |> fold_map (ensure_const thy algebra funcgr) rhs - |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const') + |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const') | NONE => I) rhs') |> pair (SOME const) end @@ -225,24 +211,25 @@ let val funcss = raw_funcss |> resort_funcss thy algebra funcgr - |> filter_out (can (Constgraph.get_node funcgr) o fst); - fun typ_func const [] = Code.default_typ thy const - | typ_func (_, NONE) (thm :: _) = (snd o CodeUnit.head_func) thm - | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) = - let - val (_, ty) = CodeUnit.head_func thm; - val SOME class = AxClass.class_of_param thy c; - val sorts_decl = Sorts.mg_domain algebra tyco [class]; - val tys = CodeUnit.typargs thy (c, ty); - val sorts = map (snd o dest_TVar) tys; - in if sorts = sorts_decl then ty - else raise INVALID ([const], "Illegal instantation for class operation " - ^ CodeUnit.string_of_const thy const - ^ "\nin defining equations\n" - ^ (cat_lines o map string_of_thm) thms) - end; + |> filter_out (can (Graph.get_node funcgr) o fst); + fun typ_func c [] = Code.default_typ thy c + | typ_func c (thms as thm :: _) = case Class.param_const thy c + of SOME (c', tyco) => + let + val (_, ty) = CodeUnit.head_func thm; + val SOME class = AxClass.class_of_param thy c'; + val sorts_decl = Sorts.mg_domain algebra tyco [class]; + val tys = Sign.const_typargs thy (c, ty); + val sorts = map (snd o dest_TVar) tys; + in if sorts = sorts_decl then ty + else raise INVALID ([c], "Illegal instantation for class operation " + ^ CodeUnit.string_of_const thy c + ^ "\nin defining equations\n" + ^ (cat_lines o map string_of_thm) thms) + end + | NONE => (snd o CodeUnit.head_func) thm; fun add_funcs (const, thms) = - Constgraph.new_node (const, (typ_func const thms, thms)); + Graph.new_node (const, (typ_func const thms, thms)); fun add_deps (funcs as (const, thms)) funcgr = let val deps = consts_of funcs; @@ -251,8 +238,8 @@ in funcgr |> ensure_consts' thy algebra insts - |> fold (curry Constgraph.add_edge const) deps - |> fold (curry Constgraph.add_edge const) insts + |> fold (curry Graph.add_edge const) deps + |> fold (curry Graph.add_edge const) insts end; in funcgr @@ -261,29 +248,24 @@ end and ensure_consts' thy algebra cs funcgr = let - val auxgr = Constgraph.empty + val auxgr = Graph.empty |> fold (snd oo ensure_const thy algebra funcgr) cs; in funcgr |> fold (merge_funcss thy algebra) - (map (AList.make (Constgraph.get_node auxgr)) - (rev (Constgraph.strong_conn auxgr))) + (map (AList.make (Graph.get_node auxgr)) + (rev (Graph.strong_conn auxgr))) end handle INVALID (cs', msg) - => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg); - -fun ensure_consts thy consts funcgr = - let - val algebra = Code.coregular_algebra thy - in ensure_consts' thy algebra consts funcgr - handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " - ^ commas (map (CodeUnit.string_of_const thy) cs')) - end; + => raise INVALID (fold (insert (op =)) cs' cs, msg); in (** retrieval interfaces **) -val ensure_consts = ensure_consts; +fun ensure_consts thy algebra consts funcgr = + ensure_consts' thy algebra consts funcgr + handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " + ^ commas (map (CodeUnit.string_of_const thy) cs')); fun check_consts thy consts funcgr = let @@ -294,25 +276,20 @@ val (consts', funcgr') = fold_map try_const consts funcgr; in (map_filter I consts', funcgr') end; -fun ensure_consts_term_proto thy f ct funcgr = +fun raw_eval thy f ct funcgr = let - fun consts_of thy t = - fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t [] - fun rhs_conv conv thm = - let - val thm' = (conv o Thm.rhs_of) thm; - in Thm.transitive thm thm' end + val algebra = Code.coregular_algebra thy; + fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I) + (Thm.term_of ct) []; val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); val thm1 = Code.preprocess_conv ct; val ct' = Thm.rhs_of thm1; - val consts = consts_of thy (Thm.term_of ct'); - val funcgr' = ensure_consts thy consts funcgr; - val algebra = Code.coregular_algebra thy; + val cs = map fst (consts_of ct'); + val funcgr' = ensure_consts thy algebra cs funcgr; val (_, thm2) = Thm.varifyT' [] thm1; val thm3 = Thm.reflexive (Thm.rhs_of thm2); - val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodeUnit.const_of_cexpr thy); - val [thm4] = resort_thms algebra typ_funcgr [thm3]; + val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3]; val tfrees = Term.add_tfrees (Thm.prop_of thm1) []; fun inst thm = let @@ -323,56 +300,54 @@ val thm5 = inst thm2; val thm6 = inst thm4; val ct'' = Thm.rhs_of thm6; - val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; + val c_exprs = consts_of ct''; val drop = drop_classes thy tfrees; - val instdefs = instances_of_consts thy algebra funcgr' cs; - val funcgr'' = ensure_consts thy instdefs funcgr'; - in (f funcgr'' drop ct'' thm5, funcgr'') end; + val instdefs = instances_of_consts thy algebra funcgr' c_exprs; + val funcgr'' = ensure_consts thy algebra instdefs funcgr'; + in (f drop thm5 funcgr'' ct'' , funcgr'') end; -fun ensure_consts_eval thy conv = +fun raw_eval_conv thy conv = let - fun conv' funcgr drop_classes ct thm1 = + fun conv' drop_classes thm1 funcgr ct = let val thm2 = conv funcgr ct; val thm3 = Code.postprocess_conv (Thm.rhs_of thm2); val thm23 = drop_classes (Thm.transitive thm2 thm3); in Thm.transitive thm1 thm23 handle THM _ => - error ("eval_conv - could not construct proof:\n" + error ("could not construct proof:\n" ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3]) end; - in ensure_consts_term_proto thy conv' end; + in raw_eval thy conv' end; -fun ensure_consts_term thy f = +fun raw_eval_term thy f = let - fun f' funcgr drop_classes ct thm1 = f funcgr ct; - in ensure_consts_term_proto thy f' end; + fun f' _ _ funcgr ct = f funcgr ct; + in raw_eval thy f' end; end; (*local*) structure Funcgr = CodeDataFun (struct type T = T; - val empty = Constgraph.empty; - fun merge _ _ = Constgraph.empty; - fun purge _ NONE _ = Constgraph.empty + val empty = Graph.empty; + fun merge _ _ = Graph.empty; + fun purge _ NONE _ = Graph.empty | purge _ (SOME cs) funcgr = - Constgraph.del_nodes ((Constgraph.all_preds funcgr - o filter (can (Constgraph.get_node funcgr))) cs) funcgr; + Graph.del_nodes ((Graph.all_preds funcgr + o filter (can (Graph.get_node funcgr))) cs) funcgr; end); fun make thy = - Funcgr.change thy o ensure_consts thy; + Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy); fun make_consts thy = Funcgr.change_yield thy o check_consts thy; fun eval_conv thy f = - fst o Funcgr.change_yield thy o ensure_consts_eval thy f; + fst o Funcgr.change_yield thy o raw_eval_conv thy f; fun eval_term thy f = - fst o Funcgr.change_yield thy o ensure_consts_term thy f; - -fun intervene thy funcgr = Funcgr.change thy (K funcgr); + fst o Funcgr.change_yield thy o raw_eval_term thy f; end; (*struct*)