# HG changeset patch # User wenzelm # Date 1191859988 -7200 # Node ID afae05eb1f1c981e54791df199ecd334a5451df9 # Parent c74ad8782eeb5355a48cbb1ca3f702317d9955af maintain typargs for abbrevs as well; diff -r c74ad8782eeb -r afae05eb1f1c src/Pure/consts.ML --- a/src/Pure/consts.ML Mon Oct 08 18:13:07 2007 +0200 +++ b/src/Pure/consts.ML Mon Oct 08 18:13:08 2007 +0200 @@ -46,14 +46,13 @@ (* datatype T *) -datatype kind = - LogicalConst of int list list | (*typargs positions*) - Abbreviation of term * term * bool (*rhs, normal rhs, force_expand*); +type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool}; -type decl = {T: typ, kind: kind, tags: Markup.property list, authentic: bool}; +type abbrev = {rhs: term, normal_rhs: term, force_expand: bool}; +fun dest_abbrev ({rhs, normal_rhs, ...}: abbrev) = (rhs, normal_rhs); datatype T = Consts of - {decls: (decl * serial) NameSpace.table, + {decls: ((decl * abbrev option) * serial) NameSpace.table, constraints: typ Symtab.table, rev_abbrevs: (term * term) list Symtab.table} * stamp; @@ -71,13 +70,10 @@ (* dest consts *) -fun dest_kind (LogicalConst _) = NONE - | dest_kind (Abbreviation (t, t', _)) = SOME (t, t'); - fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) = {constants = (space, - Symtab.fold (fn (c, ({T, kind, ...}, _)) => - Symtab.update (c, (T, dest_kind kind))) decls Symtab.empty), + Symtab.fold (fn (c, (({T, ...}, abbr), _)) => + Symtab.update (c, (T, Option.map dest_abbrev abbr))) decls Symtab.empty), constraints = (space, constraints)}; @@ -88,26 +84,25 @@ SOME (decl, _) => decl | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], [])); -fun logical_const consts c = +fun the_declaration consts c = (case the_const consts c of - {T, kind = LogicalConst ps, ...} => (T, ps) + ({T, ...}, NONE) => T | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], [])); fun the_abbreviation consts c = (case the_const consts c of - {T, kind = Abbreviation (t, t', _), ...} => (T, (t, t')) + ({T, ...}, SOME abbr) => (T, dest_abbrev abbr) | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], [])); -val the_declaration = #1 oo logical_const; -val type_arguments = #2 oo logical_const; +val type_arguments = (#typargs o #1) oo the_const; val is_monomorphic = null oo type_arguments; fun the_constraint (consts as Consts ({constraints, ...}, _)) c = (case Symtab.lookup constraints c of SOME T => T - | NONE => #T (the_const consts c)); + | NONE => #T (#1 (the_const consts c))); -val the_tags = #tags oo the_const; +val the_tags = (#tags o #1) oo the_const; (* name space and syntax *) @@ -119,12 +114,12 @@ fun extern_early consts c = (case try (the_const consts) c of - SOME {authentic = true, ...} => Syntax.constN ^ c + SOME ({authentic = true, ...}, _) => Syntax.constN ^ c | _ => extern consts c); fun syntax consts (c, mx) = let - val {T, authentic, ...} = the_const consts c handle TYPE (msg, _, _) => error msg; + val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg; val c' = if authentic then Syntax.constN ^ c else NameSpace.base c; in (c', T, mx) end; @@ -136,7 +131,7 @@ fun read_const consts raw_c = let val c = intern consts raw_c; - val {T, ...} = the_const consts c handle TYPE (msg, _, _) => error msg; + val ({T, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg; in Const (c, T) end; @@ -158,13 +153,13 @@ | Const (c, T) => let val T' = certT T; - val {T = U, kind, ...} = the_const consts c; + val ({T = U, ...}, abbr) = the_const consts c; in if not (Type.raw_instance (T', U)) then err "Illegal type for constant" (c, T) else - (case kind of - Abbreviation (_, u, force_expand) => + (case abbr of + SOME {normal_rhs = u, force_expand, ...} => if do_expand orelse force_expand then Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ => err "Illegal type for abbreviation" (c, T), args') @@ -178,12 +173,26 @@ (* typargs -- view actual const type as instance of declaration *) +local + +fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos + | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos) + | args_of (TFree _) _ = I +and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is + | args_of_list [] _ _ = I; + fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is | subscript T [] = T | subscript T _ = raise Subscript; +in + +fun typargs_of T = map #2 (rev (args_of T [] [])); + fun typargs consts (c, T) = map (subscript T) (type_arguments consts c); +end; + fun instance consts (c, Ts) = let val declT = the_declaration consts c; @@ -216,15 +225,8 @@ fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) => let - fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos - | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos) - | args_of (TFree _) _ = I - and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is - | args_of_list [] _ _ = I; - val decl = - {T = declT, kind = LogicalConst (map #2 (rev (args_of declT [] []))), - tags = tags, authentic = authentic}; - val decls' = decls |> extend_decls naming (c, (decl, serial ())); + val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic}; + val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ())); in (decls', constraints, rev_abbrevs) end); @@ -279,10 +281,10 @@ in consts |> map_consts (fn (decls, constraints, rev_abbrevs) => let - val decl = - {T = T, kind = Abbreviation (rhs, rhs', force_expand), tags = tags, authentic = true}; + val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true}; + val abbr = {rhs = rhs, normal_rhs = rhs', force_expand = force_expand}; val decls' = decls - |> extend_decls naming (c, (decl, serial ())); + |> extend_decls naming (c, ((decl, SOME abbr), serial ())); val rev_abbrevs' = rev_abbrevs |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs); in (decls', constraints, rev_abbrevs') end)