diff -r e534e39f3531 -r bc0270e9d27f src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Sep 29 00:58:59 2005 +0200 +++ b/src/Pure/defs.ML Thu Sep 29 00:59:00 2005 +0200 @@ -1,720 +1,108 @@ -(* Title: Pure/General/defs.ML +(* Title: Pure/defs.ML ID: $Id$ - Author: Steven Obua, TU Muenchen + Author: Makarius -Checks if definitions preserve consistency of logic by enforcing that -there are no cyclic definitions. The algorithm is described in "An -Algorithm for Determining Definitional Cycles in Higher-Order Logic -with Overloading", Steven Obua, technical report, to be written :-) - -ATTENTION: -Currently this implementation of the cycle test contains a bug of which the author is fully aware. -This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. +Global well-formedness checks for constant definitions. Dependencies +are only tracked for non-overloaded definitions! *) signature DEFS = sig - (*true: record the full chain of definitions that lead to a circularity*) - val chain_history: bool ref - type graph - val empty: graph - val declare: theory -> string * typ -> graph -> graph - val define: theory -> string * typ -> string -> (string * typ) list -> graph -> graph - val finalize: theory -> string * typ -> graph -> graph - val merge: Pretty.pp -> graph -> graph -> graph - val finals: graph -> typ list Symtab.table - datatype overloadingstate = Open | Closed | Final - val overloading_info: graph -> string -> (typ * (string*typ) list * overloadingstate) option - val monomorphic: graph -> string -> bool + type T + val monomorphic: T -> string -> bool + val define: string -> string * typ -> (string * typ) list -> T -> T + val empty: T + val merge: Pretty.pp -> T * T -> T end -structure Defs :> DEFS = struct - -type tyenv = Type.tyenv -type edgelabel = (int * typ * typ * (typ * string * string) list) - -datatype overloadingstate = Open | Closed | Final - -datatype node = Node of - typ (* most general type of constant *) - * defnode Symtab.table - (* a table of defnodes, each corresponding to 1 definition of the - constant for a particular type, indexed by axiom name *) - * (unit Symtab.table) Symtab.table - (* a table of all back referencing defnodes to this node, - indexed by node name of the defnodes *) - * typ list (* a list of all finalized types *) - * overloadingstate - - and defnode = Defnode of - typ (* type of the constant in this particular definition *) - * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) - -fun getnode graph = the o Symtab.lookup graph -fun get_nodedefs (Node (_, defs, _, _, _)) = defs -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname -fun get_defnode' graph noderef = - Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef))) - -fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0; - -datatype graphaction = - Declare of string * typ - | Define of string * typ * string * string * (string * typ) list - | Finalize of string * typ - -type graph = int * string Symtab.table * graphaction list * node Symtab.table - -val chain_history = ref true - -val empty = (0, Symtab.empty, [], Symtab.empty) - -exception DEFS of string; -exception CIRCULAR of (typ * string * string) list; -exception INFINITE_CHAIN of (typ * string * string) list; -exception CLASH of string * string * string; -exception FINAL of string * typ; - -fun def_err s = raise (DEFS s) - -fun no_forwards defs = - Symtab.foldl - (fn (closed, (_, Defnode (_, edges))) => - if not closed then false else Symtab.is_empty edges) - (true, defs) - -fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts) - | checkT' (TFree (a, _)) = TVar ((a, 0), []) - | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), []) - | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []); - -fun checkT thy = Compress.typ thy o checkT'; - -fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2; +structure Defs (* FIXME : DEFS *) = +struct -fun subst_incr_tvar inc t = - if inc > 0 then - let - val tv = typ_tvars t - val t' = Logic.incr_tvar inc t - fun update_subst ((n, i), _) = - Vartab.update ((n, i), ([], TVar ((n, i + inc), []))); - in - (t', fold update_subst tv Vartab.empty) - end - else - (t, Vartab.empty) - -fun subst s ty = Envir.norm_type s ty - -fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history - -fun is_instance instance_ty general_ty = - Type.raw_instance (instance_ty, general_ty) - -fun is_instance_r instance_ty general_ty = - is_instance instance_ty (rename instance_ty general_ty) - -fun unify ty1 ty2 = - SOME (Type.raw_unify (ty1, ty2) Vartab.empty) - handle Type.TUNIFY => NONE - -(* - Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and - so that they are different. All indices in ty1 and ty2 are supposed to be less than or - equal to max. - Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than - all indices in s1, s2, ty1, ty2. -*) -fun unify_r max ty1 ty2 = - let - val max = Int.max(max, 0) - val max1 = max (* >= maxidx_of_typ ty1 *) - val max2 = max (* >= maxidx_of_typ ty2 *) - val max = Int.max(max, Int.max (max1, max2)) - val (ty1, s1) = subst_incr_tvar (max + 1) ty1 - val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 - val max = max + max1 + max2 + 2 - fun merge a b = Vartab.merge (fn _ => false) (a, b) - in - case unify ty1 ty2 of - NONE => NONE - | SOME s => SOME (max, merge s1 s, merge s2 s) - end - -fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2)) -fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2) - -fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) = - if maxidx <= 1000000 then edge else - let - - fun idxlist idx extract_ty inject_ty (tab, max) ts = - foldr - (fn (e, ((tab, max), ts)) => - let - val ((tab, max), ty) = idx (tab, max) (extract_ty e) - val e = inject_ty (ty, e) - in - ((tab, max), e::ts) - end) - ((tab,max), []) ts - - fun idx (tab,max) (TVar ((a,i),_)) = - (case Inttab.lookup tab i of - SOME j => ((tab, max), TVar ((a,j),[])) - | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[]))) - | idx (tab,max) (Type (t, ts)) = - let - val ((tab, max), ts) = idxlist idx I fst (tab, max) ts - in - ((tab,max), Type (t, ts)) - end - | idx (tab, max) ty = ((tab, max), ty) +(** datatype T **) - val ((tab,max), u1) = idx (Inttab.empty, 0) u1 - val ((tab,max), v1) = idx (tab, max) v1 - val ((tab,max), history) = - idxlist idx - (fn (ty,_,_) => ty) - (fn (ty, (_, s1, s2)) => (ty, s1, s2)) - (tab, max) history - in - (max, u1, v1, history) - end - -fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) = - let - val t1 = u1 --> v1 - val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2) - in - if (is_instance t1 t2) then - (if is_instance t2 t1 then - SOME (int_ord (length history2, length history1)) - else - SOME LESS) - else if (is_instance t2 t1) then - SOME GREATER - else - NONE - end - -fun merge_edges_1 (x, []) = [x] - | merge_edges_1 (x, (y::ys)) = - (case compare_edges x y of - SOME LESS => (y::ys) - | SOME EQUAL => (y::ys) - | SOME GREATER => merge_edges_1 (x, ys) - | NONE => y::(merge_edges_1 (x, ys))) - -fun merge_edges xs ys = foldl merge_edges_1 xs ys - -fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = - (cost, axmap, (Declare cty)::actions, - Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) - handle Symtab.DUP _ => - let - val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name) - in - if is_instance_r ty gty andalso is_instance_r gty ty then - g - else - def_err "constant is already declared with different type" - end - -fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty) - -val axcounter = ref (IntInf.fromInt 0) -fun newaxname axmap axname = - let - val c = !axcounter - val _ = axcounter := c+1 - val axname' = axname^"_"^(IntInf.toString c) - in - (Symtab.update (axname', axname) axmap, axname') - end +datatype T = Defs of + {consts: typ Graph.T, (*constant declarations and dependencies*) + specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*) + monomorphic: unit Symtab.table}; (*constants having monomorphic specs*) -fun translate_ex axmap x = - let - fun translate (ty, nodename, axname) = - (ty, nodename, the (Symtab.lookup axmap axname)) - in - case x of - INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) - | CIRCULAR cycle => raise (CIRCULAR (map translate cycle)) - | _ => raise x - end - -fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body = - let - val mainnode = (case Symtab.lookup graph mainref of - NONE => def_err ("constant "^mainref^" is not declared") - | SOME n => n) - val (Node (gty, defs, backs, finals, _)) = mainnode - val _ = (if is_instance_r ty gty then () - else def_err "type of constant does not match declared type") - fun check_def (s, Defnode (ty', _)) = - (if can_be_unified_r ty ty' then - raise (CLASH (mainref, axname, s)) - else if s = axname then - def_err "name of axiom is already used for another definition of this constant" - else false) - val _ = Symtab.exists check_def defs - fun check_final finalty = - (if can_be_unified_r finalty ty then - raise (FINAL (mainref, finalty)) - else - true) - val _ = forall check_final finals - - (* now we know that the only thing that can prevent acceptance of the definition - is a cyclic dependency *) +fun rep_defs (Defs args) = args; - fun insert_edges edges (nodename, links) = - (if links = [] then - edges - else - let - val links = map normalize_edge_idx links - in - Symtab.update (nodename, - case Symtab.lookup edges nodename of - NONE => links - | SOME links' => merge_edges links' links) edges - end) - - fun make_edges ((bodyn, bodyty), edges) = - let - val bnode = - (case Symtab.lookup graph bodyn of - NONE => def_err "body of constant definition references undeclared constant" - | SOME x => x) - val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode - in - if closed = Final then edges else - case unify_r 0 bodyty general_btyp of - NONE => edges - | SOME (maxidx, sigma1, sigma2) => - if exists (is_instance_r bodyty) bfinals then - edges - else - let - fun insert_trans_edges ((step1, edges), (nodename, links)) = - let - val (maxidx1, alpha1, beta1, defname) = step1 - fun connect (maxidx2, alpha2, beta2, history) = - case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of - NONE => NONE - | SOME (max, sleft, sright) => - SOME (max, subst sleft alpha1, subst sright beta2, - if !chain_history then - ((subst sleft beta1, bodyn, defname):: - (subst_history sright history)) - else []) - val links' = List.mapPartial connect links - in - (step1, insert_edges edges (nodename, links')) - end +fun make_defs (consts, specified, monomorphic) = + Defs {consts = consts, specified = specified, monomorphic = monomorphic}; - fun make_edges' ((swallowed, edges), - (def_name, Defnode (def_ty, def_edges))) = - if swallowed then - (swallowed, edges) - else - (case unify_r 0 bodyty def_ty of - NONE => (swallowed, edges) - | SOME (maxidx, sigma1, sigma2) => - (is_instance_r bodyty def_ty, - snd (Symtab.foldl insert_trans_edges - (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name), - edges), def_edges)))) - val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) - in - if swallowed then - edges - else - insert_edges edges - (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) - end - end - - val edges = foldl make_edges Symtab.empty body - - (* We also have to add the backreferences that this new defnode induces. *) - fun install_backrefs (graph, (noderef, links)) = - if links <> [] then - let - val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef - val _ = if closed = Final then - sys_error ("install_backrefs: closed node cannot be updated") - else () - val defnames = - (case Symtab.lookup backs mainref of - NONE => Symtab.empty - | SOME s => s) - val defnames' = Symtab.update_new (axname, ()) defnames - val backs' = Symtab.update (mainref, defnames') backs - in - Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph - end - else - graph - - val graph = Symtab.foldl install_backrefs (graph, edges) - - val (Node (_, _, backs, _, closed)) = getnode graph mainref - val closed = - if closed = Final then sys_error "define: closed node" - else if closed = Open andalso is_instance_r gty ty then Closed else closed - - val thisDefnode = Defnode (ty, edges) - val graph = Symtab.update (mainref, Node (gty, Symtab.update_new - (axname, thisDefnode) defs, backs, finals, closed)) graph - - (* Now we have to check all backreferences to this node and inform them about - the new defnode. In this section we also check for circularity. *) - fun update_backrefs ((backs, graph), (noderef, defnames)) = - let - fun update_defs ((defnames, graph),(defname, _)) = - let - val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = - getnode graph noderef - val _ = if closed = Final then sys_error "update_defs: closed node" else () - val (Defnode (def_ty, defnode_edges)) = - the (Symtab.lookup nodedefs defname) - val edges = the (Symtab.lookup defnode_edges mainref) - val refclosed = ref false +fun map_defs f (Defs {consts, specified, monomorphic}) = + make_defs (f (consts, specified, monomorphic)); - (* the type of thisDefnode is ty *) - fun update (e as (max, alpha, beta, history), (changed, edges)) = - case unify_r max beta ty of - NONE => (changed, e::edges) - | SOME (max', s_beta, s_ty) => - let - val alpha' = subst s_beta alpha - val ty' = subst s_ty ty - val _ = - if noderef = mainref andalso defname = axname then - (case unify alpha' ty' of - NONE => - if (is_instance_r ty' alpha') then - raise (INFINITE_CHAIN ( - (alpha', mainref, axname):: - (subst_history s_beta history)@ - [(ty', mainref, axname)])) - else () - | SOME s => - raise (CIRCULAR ( - (subst s alpha', mainref, axname):: - (subst_history s (subst_history s_beta history))@ - [(subst s ty', mainref, axname)]))) - else () - in - if is_instance_r beta ty then - (true, edges) - else - (changed, e::edges) - end - val (changed, edges') = foldl update (false, []) edges - val defnames' = if edges' = [] then - defnames - else - Symtab.update (defname, ()) defnames - in - if changed then - let - val defnode_edges' = - if edges' = [] then - Symtab.delete mainref defnode_edges - else - Symtab.update (mainref, edges') defnode_edges - val defnode' = Defnode (def_ty, defnode_edges') - val nodedefs' = Symtab.update (defname, defnode') nodedefs - val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' - andalso no_forwards nodedefs' - then Final else closed - val graph' = - Symtab.update - (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph - in - (defnames', graph') - end - else - (defnames', graph) - end - - val (defnames', graph') = Symtab.foldl update_defs - ((Symtab.empty, graph), defnames) - in - if Symtab.is_empty defnames' then - (backs, graph') - else - let - val backs' = Symtab.update_new (noderef, defnames') backs - in - (backs', graph') - end - end - - val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs) +(* specified consts *) - (* If a Circular exception is thrown then we never reach this point. *) - val (Node (gty, defs, _, finals, closed)) = getnode graph mainref - val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph - val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions - in - (cost+3, axmap, actions', graph) - end handle ex => translate_ex axmap ex - -fun define'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = - let - val ty = checkT thy ty - fun checkbody (n, t) = - let - val (Node (_, _, _,_, closed)) = getnode graph n - in - case closed of - Final => NONE - | _ => SOME (n, checkT thy t) - end - val body = distinct (List.mapPartial checkbody body) - val (axmap, axname) = newaxname axmap orig_axname - in - define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body - end - -fun finalize' (cost, axmap, history, graph) (noderef, ty) = - case Symtab.lookup graph noderef of - NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") - | SOME (Node (nodety, defs, backs, finals, closed)) => - let - val _ = - if (not (is_instance_r ty nodety)) then - def_err ("only type instances of the declared constant "^ - noderef^" can be finalized") - else () - val _ = Symtab.exists - (fn (def_name, Defnode (def_ty, _)) => - if can_be_unified_r ty def_ty then - def_err ("cannot finalize constant "^noderef^ - "; clash with definition "^def_name) - else - false) - defs - - fun update_finals [] = SOME [ty] - | update_finals (final_ty::finals) = - (if is_instance_r ty final_ty then NONE - else - case update_finals finals of - NONE => NONE - | (r as SOME finals) => - if (is_instance_r final_ty ty) then - r - else - SOME (final_ty :: finals)) - in - case update_finals finals of - NONE => (cost, axmap, history, graph) - | SOME finals => - let - val closed = if closed = Open andalso is_instance_r nodety ty then - Closed else - closed - val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph - - fun update_backref ((graph, backs), (backrefname, backdefnames)) = - let - fun update_backdef ((graph, defnames), (backdefname, _)) = - let - val (backnode as Node (backty, backdefs, backbacks, - backfinals, backclosed)) = - getnode graph backrefname - val (Defnode (def_ty, all_edges)) = - the (get_defnode backnode backdefname) +fun disjoint_types T U = + (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false) + handle Type.TUNIFY => true; - val (defnames', all_edges') = - case Symtab.lookup all_edges noderef of - NONE => sys_error "finalize: corrupt backref" - | SOME edges => - let - val edges' = List.filter (fn (_, _, beta, _) => - not (is_instance_r beta ty)) edges - in - if edges' = [] then - (defnames, Symtab.delete noderef all_edges) - else - (Symtab.update (backdefname, ()) defnames, - Symtab.update (noderef, edges') all_edges) - end - val defnode' = Defnode (def_ty, all_edges') - val backdefs' = Symtab.update (backdefname, defnode') backdefs - val backclosed' = if backclosed = Closed andalso - Symtab.is_empty all_edges' - andalso no_forwards backdefs' - then Final else backclosed - val backnode' = - Node (backty, backdefs', backbacks, backfinals, backclosed') - in - (Symtab.update (backrefname, backnode') graph, defnames') - end - - val (graph', defnames') = - Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) - in - (graph', if Symtab.is_empty defnames' then backs - else Symtab.update (backrefname, defnames') backs) - end - val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) - val Node ( _, defs, _, _, closed) = getnode graph' noderef - val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph' = Symtab.update (noderef, Node (nodety, defs, backs', - finals, closed)) graph' - val history' = (Finalize (noderef, ty)) :: history - in - (cost+1, axmap, history', graph') - end - end - -fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) - -fun update_axname ax orig_ax (cost, axmap, history, graph) = - (cost, Symtab.update (ax, orig_ax) axmap, history, graph) - -fun merge' (Declare cty, g) = declare' g cty - | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = - (case Symtab.lookup graph name of - NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body - | SOME (Node (_, defs, _, _, _)) => - (case Symtab.lookup defs axname of - NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body - | SOME _ => g)) - | merge' (Finalize finals, g) = finalize' g finals - -fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = - if cost1 < cost2 then - foldr merge' g2 actions1 - else - foldr merge' g1 actions2 - -fun finals (_, _, history, graph) = - Symtab.foldl - (fn (finals, (name, Node(_, _, _, ftys, _))) => - Symtab.update_new (name, ftys) finals) - (Symtab.empty, graph) - -fun overloading_info (_, axmap, _, graph) c = - let - fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty) - in - case Symtab.lookup graph c of - NONE => NONE - | SOME (Node (ty, defnodes, _, _, state)) => - SOME (ty, map translate (Symtab.dest defnodes), state) - end +fun check_specified c specified = + specified |> Inttab.forall (fn (i, (a, T)) => + specified |> Inttab.forall (fn (j, (b, U)) => + i = j orelse disjoint_types T U orelse + error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ + " for constant " ^ quote c))); -(* monomorphic consts -- neither parametric nor ad-hoc polymorphism *) - -fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts - | monomorphicT _ = false +(* monomorphic constants *) -fun monomorphic (_, _, _, graph) c = - (case Symtab.lookup graph c of - NONE => true - | SOME (Node (ty, defnodes, _, _, _)) => - Symtab.min_key defnodes = Symtab.max_key defnodes andalso - monomorphicT ty); - - - -(** diagnostics **) +val monomorphic = Symtab.defined o #monomorphic o rep_defs; -fun pretty_const pp (c, T) = - [Pretty.str c, Pretty.str " ::", Pretty.brk 1, - Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))]; - -fun pretty_path pp path = fold_rev (fn (T, c, def) => - fn [] => [Pretty.block (pretty_const pp (c, T))] - | prts => Pretty.block (pretty_const pp (c, T) @ - [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; - -fun defs_circular pp path = - Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path - |> Pretty.chunks |> Pretty.string_of; - -fun defs_infinite_chain pp path = - Pretty.str "Infinite chain of definitions: " :: pretty_path pp path - |> Pretty.chunks |> Pretty.string_of; - -fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; - -fun defs_final pp const = - (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) - |> Pretty.block |> Pretty.string_of; +fun update_monomorphic specified c = + let + val specs = the_default Inttab.empty (Symtab.lookup specified c); + fun is_monoT (Type (_, Ts)) = forall is_monoT Ts + | is_monoT _ = false; + val is_mono = + Inttab.is_empty specs orelse + Inttab.min_key specs = Inttab.max_key specs andalso + is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs))))); + in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end; -(* external interfaces *) +(* define consts *) + +fun err_cyclic cycles = + error ("Cyclic dependency of constants:\n" ^ + cat_lines (map (space_implode " -> " o map quote o rev) cycles)); -fun declare thy const defs = - if_none (try (declare'' thy defs) const) defs; +fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) => + let + fun declare (a, _) = Graph.default_node (a, const_type a); + fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G + handle Graph.CYCLES cycles => err_cyclic cycles; + + val (c, T) = lhs; + val no_overloading = Type.raw_instance (const_type c, T); -fun define thy const name rhs defs = - define'' thy defs const name rhs - handle DEFS msg => sys_error msg - | CIRCULAR path => error (defs_circular (Sign.pp thy) path) - | INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path) - | CLASH (_, def1, def2) => error (defs_clash def1 def2) - | FINAL const => error (defs_final (Sign.pp thy) const); + val consts' = + consts |> declare lhs |> fold declare rhs + |> K no_overloading ? add_deps (c, map #1 rhs); + val specified' = + specified |> Symtab.default (c, Inttab.empty) + |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c)); + val monomorphic' = monomorphic |> update_monomorphic specified' c; + in (consts', specified', monomorphic') end); + + +(* empty and merge *) -fun finalize thy const defs = - finalize'' thy defs const handle DEFS msg => sys_error msg; +val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty); -fun merge pp defs1 defs2 = - merge'' defs1 defs2 - handle CIRCULAR namess => error (defs_circular pp namess) - | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess); +fun merge pp + (Defs {consts = consts1, specified = specified1, monomorphic}, + Defs {consts = consts2, specified = specified2, ...}) = + let + val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true) + handle Graph.CYCLES cycles => err_cyclic cycles; + val specified' = (specified1, specified2) + |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME); + val monomorphic' = monomorphic + |> Symtab.fold (update_monomorphic specified' o #1) specified'; + in make_defs (consts', specified', monomorphic') end; end; - -(* - -fun tvar name = TVar ((name, 0), []) - -val bool = Type ("bool", []) -val int = Type ("int", []) -val lam = Type("lam", []) -val alpha = tvar "'a" -val beta = tvar "'b" -val gamma = tvar "'c" -fun pair a b = Type ("pair", [a,b]) -fun prm a = Type ("prm", [a]) -val name = Type ("name", []) - -val _ = print "make empty" -val g = Defs.empty - -val _ = print "declare perm" -val g = Defs.declare g ("perm", prm alpha --> beta --> beta) - -val _ = print "declare permF" -val g = Defs.declare g ("permF", prm alpha --> lam --> lam) - -val _ = print "define perm (1)" -val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" - [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)] - -val _ = print "define permF (1)" -val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app" - ([("perm", prm alpha --> lam --> lam), - ("perm", prm alpha --> lam --> lam), - ("perm", prm alpha --> lam --> lam), - ("perm", prm alpha --> name --> name)]) - -val _ = print "define perm (2)" -val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam" - [("permF", (prm alpha --> lam --> lam))] - -*)