diff --git a/src/Pure/Syntax/parser.ML b/src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML +++ b/src/Pure/Syntax/parser.ML @@ -1,708 +1,707 @@ (* Title: Pure/Syntax/parser.ML Author: Carsten Clasohm, Sonia Mahjoub Author: Makarius General context-free parser for the inner syntax of terms and types. *) signature PARSER = sig type gram val empty_gram: gram - val extend_gram: Syntax_Ext.xprod list -> gram -> gram - val make_gram: Syntax_Ext.xprod list -> gram + val make_gram: Syntax_Ext.xprod list -> Syntax_Ext.xprod list -> gram option -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = Node of string * parsetree list | Tip of Lexicon.token exception PARSETREE of parsetree val pretty_parsetree: parsetree -> Pretty.T val parse: gram -> string -> Lexicon.token list -> parsetree list val branching_level: int Config.T end; structure Parser: PARSER = struct (** datatype gram **) (* nonterminals *) (*production for the NTs are stored in a vector, indexed by the NT tag*) type nt = int; type tags = nt Symtab.table; val tags_empty: tags = Symtab.empty; fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags); fun tags_lookup (tags: tags) = Symtab.lookup tags; fun tags_insert tag (tags: tags) = Symtab.update_new tag tags; fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.build (Symtab.fold (Inttab.update_new o swap) tags)); type nts = Intset.T; val nts_empty: nts = Intset.empty; val nts_merge: nts * nts -> nts = Intset.merge; fun nts_insert nt : nts -> nts = Intset.insert nt; fun nts_member (nts: nts) = Intset.member nts; fun nts_fold f (nts: nts) = Intset.fold f nts; fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1; fun nts_is_empty (nts: nts) = Intset.is_empty nts; fun nts_is_unique (nts: nts) = Intset.size nts <= 1; (* tokens *) structure Tokens = Set(type key = Lexicon.token val ord = Lexicon.tokens_match_ord); fun tokens_find P tokens = Tokens.get_first (fn tok => if P tok then SOME tok else NONE) tokens; fun tokens_add (nt: nt, tokens) = if Tokens.is_empty tokens then I else cons (nt, tokens); (* productions *) datatype symb = Terminal of Lexicon.token | Nonterminal of nt * int; (*(tag, prio)*) structure Prods = Table(Tokens.Key); type prods = (symb list * string * int) list Prods.table; (*start_token ~> [(rhs, name, prio)]*) val prods_empty: prods = Prods.empty; fun prods_lookup (prods: prods) = Prods.lookup_list prods; fun prods_update entry : prods -> prods = Prods.update entry; fun prods_content (prods: prods) = distinct (op =) (maps #2 (Prods.dest prods)); type nt_gram = (nts * Tokens.T) * prods; (*dependent_nts, start_tokens, prods*) (*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*) val nt_gram_empty: nt_gram = ((nts_empty, Tokens.empty), prods_empty); type chains = unit Int_Graph.T; fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains; fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains; fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains; val chains_empty: chains = Int_Graph.empty; fun chains_member (chains: chains) = Int_Graph.is_edge chains; fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ()); fun chains_insert (from, to) = chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to); datatype gram = Gram of {nt_count: int, prod_count: int, tags: tags, chains: chains, lambdas: nts, prods: nt_gram Vector.vector}; (*"tags" is used to map NT names (i.e. strings) to tags; chain productions are not stored as normal productions but instead as an entry in "chains": from -> to; lambda productions are stored as normal productions and also as an entry in "lambdas"*) (*productions for which no starting token is known yet are associated with this token*) val unknown_start = Lexicon.eof; fun get_start tks = (case Tokens.min tks of SOME tk => tk | NONE => unknown_start); fun add_production array_prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) = let (*store chain if it does not already exist*) val (chain, new_chain, chains') = (case (pri, rhs) of (~1, [Nonterminal (from, ~1)]) => if chains_member chains (from, lhs) then (SOME from, false, chains) else (SOME from, true, chains_insert (from, lhs) chains) | _ => let val chains' = chains |> chains_declare lhs |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs; in (NONE, false, chains') end); (*propagate new chain in lookahead and lambdas; added_starts is used later to associate existing productions with new starting tokens*) val (added_starts, lambdas') = if not new_chain then ([], lambdas) else let (*lookahead of chain's source*) val ((_, from_tks), _) = Array.nth array_prods (the chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead to = let val ((to_nts, to_tks), ps) = Array.nth array_prods to; val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*) val to_tks' = Tokens.merge (to_tks, new_tks); val _ = Array.upd array_prods to ((to_nts, to_tks'), ps); in tokens_add (to, new_tks) end; val tos = chains_all_succs chains' [lhs]; in (fold copy_lookahead tos [], lambdas |> nts_member lambdas lhs ? fold nts_insert tos) end; (*test if new production can produce lambda (rhs must either be empty or only consist of lambda NTs)*) val new_lambdas = if forall (fn Nonterminal (id, _) => nts_member lambdas' id | Terminal _ => false) rhs then SOME (filter_out (nts_member lambdas') (chains_all_succs chains' [lhs])) else NONE; val lambdas'' = fold nts_insert (these new_lambdas) lambdas'; (*list optional terminal and all nonterminals on which the lookahead of a production depends*) fun lookahead_dependency _ [] nts = (NONE, nts) | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts) | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts = if nts_member lambdas nt then lookahead_dependency lambdas symbs (nts_insert nt nts) else (NONE, nts_insert nt nts); (*get all known starting tokens for a nonterminal*) fun starts_for_nt nt = snd (fst (Array.nth array_prods nt)); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = let (*propagate added lambda NT*) fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas) | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) val ((dependent, l_starts), _) = Array.nth array_prods l; (*check productions whose lookahead may depend on lambda NT*) fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods = (add_lambda, nt_dependencies, added_tks, nt_prods) | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda nt_dependencies added_tks nt_prods = let val (tk, nts) = lookahead_dependency lambdas rhs nts_empty in if nts_member nts l then (*update production's lookahead*) let val new_lambda = is_none tk andalso nts_subset (nts, lambdas); val new_tks = Tokens.empty |> fold Tokens.insert (the_list tk) |> nts_fold (curry Tokens.merge o starts_for_nt) nts |> Tokens.subtract l_starts; val added_tks' = Tokens.merge (added_tks, new_tks); val nt_dependencies' = nts_merge (nt_dependencies, nts); (*associate production with new starting tokens*) fun copy tk nt_prods = prods_update (tk, p :: prods_lookup nt_prods tk) nt_prods; val nt_prods' = nt_prods |> Tokens.fold copy new_tks |> new_lambda ? copy Lexicon.dummy; in examine_prods ps (add_lambda orelse new_lambda) nt_dependencies' added_tks' nt_prods' end else (*skip production*) examine_prods ps add_lambda nt_dependencies added_tks nt_prods end; (*check each NT whose lookahead depends on new lambda NT*) fun process_nts nt (added_lambdas, added_starts) = let val ((old_nts, old_tks), nt_prods) = Array.nth array_prods nt; (*existing productions whose lookahead may depend on l*) val tk_prods = prods_lookup nt_prods (get_start l_starts); (*add_lambda is true if an existing production of the nt produces lambda due to the new lambda NT l*) val (add_lambda, nt_dependencies, added_tks, nt_prods') = examine_prods tk_prods false nts_empty Tokens.empty nt_prods; val new_nts = nts_merge (old_nts, nt_dependencies); val new_tks = Tokens.merge (old_tks, added_tks); val added_lambdas' = added_lambdas |> add_lambda ? cons nt; val _ = Array.upd array_prods nt ((new_nts, new_tks), nt_prods'); (*N.B. that because the tks component is used to access existing productions we have to add new tokens at the _end_ of the list*) val added_starts' = tokens_add (nt, added_tks) added_starts; in (added_lambdas', added_starts') end; val (added_lambdas, added_starts') = nts_fold process_nts dependent ([], added_starts); val added_lambdas' = filter_out (nts_member lambdas) added_lambdas; in propagate_lambda (ls @ added_lambdas') added_starts' (fold nts_insert added_lambdas' lambdas) end; in propagate_lambda (nts_fold (fn l => not (nts_member lambdas l) ? cons l) lambdas'' []) added_starts lambdas'' end; (*insert production into grammar*) val added_starts' = if is_some chain then added_starts' (*don't store chain production*) else let (*lookahead tokens of new production and on which NTs lookahead depends*) val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty; val start_tks = Tokens.empty |> fold Tokens.insert (the_list start_tk) |> nts_fold (curry Tokens.merge o starts_for_nt) start_nts; val start_tks' = start_tks |> (if is_some new_lambdas then Tokens.insert Lexicon.dummy else if Tokens.is_empty start_tks then Tokens.insert unknown_start else I); (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts nt initial = (if initial then let val ((old_nts, old_tks), ps) = Array.nth array_prods nt in if nts_member old_nts lhs then () else Array.upd array_prods nt ((nts_insert lhs old_nts, old_tks), ps) end else (); false); (*add new start tokens to chained NTs' lookahead list; also store new production for lhs NT*) fun add_tks [] added = added | add_tks (nt :: nts) added = let val ((old_nts, old_tks), nt_prods) = Array.nth array_prods nt; val new_tks = Tokens.subtract old_tks start_tks; (*store new production*) fun store tk (prods, _) = let val tk_prods = prods_lookup prods tk; val tk_prods' = new_prod :: tk_prods; val prods' = prods_update (tk, tk_prods') prods; in (prods', true) end; val (nt_prods', changed) = (nt_prods, false) |> nt = lhs ? Tokens.fold store start_tks'; val _ = if not changed andalso Tokens.is_empty new_tks then () else Array.upd array_prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'); in add_tks nts (tokens_add (nt, new_tks) added) end; val _ = nts_fold add_nts start_nts true; in add_tks (chains_all_succs chains' [lhs]) [] end; (*associate productions with new lookaheads*) val _ = let (*propagate added start tokens*) fun add_starts [] = () | add_starts ((changed_nt, new_tks) :: starts) = let (*token under which old productions which depend on changed_nt could be stored*) val key = tokens_find (not o Tokens.member new_tks) (starts_for_nt changed_nt) |> the_default unknown_start; (*copy productions whose lookahead depends on changed_nt; if key = SOME unknown_start then tk_prods is used to hold the productions not copied*) fun update_prods [] result = result | update_prods ((p as (rhs, _: string, _: nt)) :: ps) (tk_prods, nt_prods) = let (*lookahead dependency for production*) val (tk, depends) = lookahead_dependency lambdas' rhs nts_empty; (*test if this production has to be copied*) val update = nts_member depends changed_nt; (*test if production could already be associated with a member of new_tks*) val lambda = not (nts_is_unique depends) orelse not (nts_is_empty depends) andalso is_some tk andalso Tokens.member new_tks (the tk); (*associate production with new starting tokens*) fun copy tk nt_prods = let val tk_prods = prods_lookup nt_prods tk; val tk_prods' = if not lambda then p :: tk_prods else insert (op =) p tk_prods; (*if production depends on lambda NT we have to look for duplicates*) in prods_update (tk, tk_prods') nt_prods end; val result = if update then (tk_prods, Tokens.fold copy new_tks nt_prods) else if key = unknown_start then (p :: tk_prods, nt_prods) else (tk_prods, nt_prods); in update_prods ps result end; (*copy existing productions for new starting tokens*) fun process_nts nt = let val ((nts, tks), nt_prods) = Array.nth array_prods nt; val tk_prods = prods_lookup nt_prods key; (*associate productions with new lookahead tokens*) val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); val nt_prods'' = if key = unknown_start then prods_update (key, tk_prods') nt_prods' else nt_prods'; val added_tks = Tokens.subtract tks new_tks; val tks' = Tokens.merge (tks, added_tks); val _ = Array.upd array_prods nt ((nts, tks'), nt_prods''); in tokens_add (nt, added_tks) end; val ((dependent, _), _) = Array.nth array_prods changed_nt; in add_starts (starts @ nts_fold process_nts dependent []) end; in add_starts added_starts' end; in (chains', lambdas') end; (* pretty_gram *) fun pretty_gram (Gram {tags, prods, chains, ...}) = let val print_nt = tags_name tags; fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")"); fun pretty_symb (Terminal tok) = if Lexicon.is_literal tok then Pretty.quote (Pretty.keyword1 (Lexicon.str_of_token tok)) else Pretty.str (Lexicon.str_of_token tok) | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p); fun pretty_const "" = [] | pretty_const c = [Pretty.str ("\<^bold>\ " ^ quote c)]; fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); fun pretty_prod (name, tag) = (prods_content (#2 (Vector.nth prods tag)) @ map prod_of_chain (chains_preds chains tag)) |> map (fn (symbs, const, p) => Pretty.block (Pretty.breaks (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const))); in maps pretty_prod (tags_content tags) end; (** operations on grammars **) val empty_gram = Gram {nt_count = 0, prod_count = 0, tags = tags_empty, chains = chains_empty, lambdas = nts_empty, prods = Vector.fromList [nt_gram_empty]}; - -(*Add productions to a grammar*) -fun extend_gram [] gram = gram - | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = - let - (*Get tag for existing nonterminal or create a new one*) - fun get_tag nt_count tags nt = - (case tags_lookup tags nt of - SOME tag => (nt_count, tags, tag) - | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); - - (*Convert symbols to the form used by the parser; - delimiters and predefined terms are stored as terminals, - nonterminals are converted to integer tags*) - fun symb_of [] nt_count tags result = (nt_count, tags, rev result) - | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = - symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) - | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = - let - val (nt_count', tags', new_symb) = - (case Lexicon.get_terminal s of - NONE => - let val (nt_count', tags', s_tag) = get_tag nt_count tags s; - in (nt_count', tags', Nonterminal (s_tag, p)) end - | SOME tk => (nt_count, tags, Terminal tk)); - in symb_of ss nt_count' tags' (new_symb :: result) end - | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; +fun extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = + let + (*Get tag for existing nonterminal or create a new one*) + fun get_tag nt_count tags nt = + (case tags_lookup tags nt of + SOME tag => (nt_count, tags, tag) + | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); - (*Convert list of productions by invoking symb_of for each of them*) - fun prod_of [] nt_count prod_count tags result = - (nt_count, prod_count, tags, result) - | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps) - nt_count prod_count tags result = - let - val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; - val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; - in - prod_of ps nt_count'' (prod_count + 1) tags'' - ((lhs_tag, (prods, const, pri)) :: result) - end; - - val (nt_count', prod_count', tags', xprods') = - prod_of xprods nt_count prod_count tags []; + (*Convert symbols to the form used by the parser; + delimiters and predefined terms are stored as terminals, + nonterminals are converted to integer tags*) + fun symb_of [] nt_count tags result = (nt_count, tags, rev result) + | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = + symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) + | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = + let + val (nt_count', tags', new_symb) = + (case Lexicon.get_terminal s of + NONE => + let val (nt_count', tags', s_tag) = get_tag nt_count tags s; + in (nt_count', tags', Nonterminal (s_tag, p)) end + | SOME tk => (nt_count, tags, Terminal tk)); + in symb_of ss nt_count' tags' (new_symb :: result) end + | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; - val array_prods' = - Array.tabulate (nt_count', fn i => - if i < nt_count then Vector.nth prods i - else nt_gram_empty); + (*Convert list of productions by invoking symb_of for each of them*) + fun prod_of [] nt_count prod_count tags result = + (nt_count, prod_count, tags, result) + | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps) + nt_count prod_count tags result = + let + val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; + val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; + in + prod_of ps nt_count'' (prod_count + 1) tags'' + ((lhs_tag, (prods, const, pri)) :: result) + end; - val (chains', lambdas') = - (chains, lambdas) |> fold (add_production array_prods') xprods'; - in - Gram - {nt_count = nt_count', - prod_count = prod_count', - tags = tags', - chains = chains', - lambdas = lambdas', - prods = Array.vector array_prods'} - end; + val (nt_count', prod_count', tags', xprods') = + prod_of xprods nt_count prod_count tags []; -fun make_gram xprods = extend_gram xprods empty_gram; + val array_prods' = + Array.tabulate (nt_count', fn i => + if i < nt_count then Vector.nth prods i + else nt_gram_empty); + + val (chains', lambdas') = + (chains, lambdas) |> fold (add_production array_prods') xprods'; + in + Gram + {nt_count = nt_count', + prod_count = prod_count', + tags = tags', + chains = chains', + lambdas = lambdas', + prods = Array.vector array_prods'} + end; + +fun make_gram [] _ (SOME gram) = gram + | make_gram new_xprods _ (SOME gram) = extend_gram new_xprods gram + | make_gram [] [] NONE = empty_gram + | make_gram new_xprods old_xprods NONE = extend_gram (new_xprods @ old_xprods) empty_gram; (** parser **) (* parsetree *) datatype parsetree = Node of string * parsetree list | Tip of Lexicon.token; exception PARSETREE of parsetree; fun pretty_parsetree parsetree = let fun pretty (Node (c, pts)) = [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))] | pretty (Tip tok) = if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else []; in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end; (* parser state *) type state = nt * int * (*identification and production precedence*) parsetree list * (*already parsed nonterminals on rhs*) symb list * (*rest of rhs*) string * (*name of production*) int; (*index for previous state list*) (*Get all rhss with precedence >= min_prec*) fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec); (*Get all rhss with precedence >= min_prec and < max_prec*) fun get_RHS' min_prec max_prec = filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) fun mk_states i lhs_ID rhss = let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i); in map mk_state rhss end; (*Add parse tree to list and eliminate duplicates saving the maximum precedence*) fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) | conc (t, prec) ((t', prec') :: ts) = if t = t' then (SOME prec', if prec' >= prec then (t', prec') :: ts else (t, prec) :: ts) else let val (n, ts') = conc (t, prec) ts in (n, (t', prec') :: ts') end; (*Update entry in used*) fun update_trees (A, t) used = let val (i, ts) = the (Inttab.lookup used A); val (n, ts') = conc t ts; in (n, Inttab.update (A, (i, ts')) used) end; (*Replace entry in used*) fun update_prec (A, prec) = Inttab.map_entry A (fn (_, ts) => (prec, ts)); fun getS A max_prec NONE Si = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) Si | getS A max_prec (SOME min_prec) Si = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec > min_prec andalso prec <= max_prec | _ => false) Si; fun get_states Estate j A max_prec = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) (Array.nth Estate j); fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = if Lexicon.valued_token c orelse id <> "" then (A, j, Tip c :: ts, sa, id, i) else (A, j, ts, sa, id, i); fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) = (A, j, tt @ ts, sa, id, i); fun movedot_lambda [] _ = [] | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) = if k <= ki then (B, j, t @ tss, sa, id, i) :: movedot_lambda ts state else movedot_lambda ts state; (*trigger value for warnings*) val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600); (*get all productions of a NT and NTs chained to it which can be started by specified token*) fun prods_for (Gram {prods, chains, ...}) tk nt = let fun token_prods prods = fold cons (prods_lookup prods tk) #> fold cons (prods_lookup prods Lexicon.dummy); fun nt_prods nt = #2 (Vector.nth prods nt); in fold (token_prods o nt_prods) (chains_all_preds chains [nt]) [] end; fun PROCESSS gram Estate i c states = let fun processS _ [] (Si, Sii) = (Si, Sii) | processS used (S :: States) (Si, Sii) = (case S of (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => let (*predictor operation*) val (used', new_states) = (case Inttab.lookup used nt of SOME (used_prec, l) => (*nonterminal has been processed*) if used_prec <= min_prec then (*wanted precedence has been processed*) (used, movedot_lambda l S) else (*wanted precedence hasn't been parsed yet*) let val tk_prods = prods_for gram c nt; val States' = mk_states i nt (get_RHS' min_prec used_prec tk_prods); in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = prods_for gram c nt; val States' = mk_states i nt (get_RHS min_prec tk_prods); in (Inttab.update (nt, (min_prec, [])) used, States') end); in processS used' (new_states @ States) (S :: Si, Sii) end | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*) processS used States (S :: Si, if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii) | (A, prec, ts, [], id, j) => (*completer operation*) let val tt = if id = "" then ts else [Node (id, rev ts)] in if j = i then (*lambda production?*) let val (prec', used') = update_trees (A, (tt, prec)) used; val Slist = getS A prec prec' Si; val States' = map (movedot_nonterm tt) Slist; in processS used' (States' @ States) (S :: Si, Sii) end else let val Slist = get_states Estate j A prec in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end end) in processS Inttab.empty states ([], []) end; fun produce gram stateset i indata prev_token = (case Array.nth stateset i of [] => let val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata; val pos = Position.here (Lexicon.pos_of_token prev_token); in if null toks then error ("Inner syntax error: unexpected end of input" ^ pos) else error ("Inner syntax error" ^ pos ^ Markup.markup Markup.no_report ("\n" ^ Pretty.string_of (Pretty.block [ Pretty.str "at", Pretty.brk 1, Pretty.block (Pretty.str "\"" :: Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @ [Pretty.str "\""])]))) end | s => (case indata of [] => s | c :: cs => let val (si, sii) = PROCESSS gram stateset i c s; val _ = Array.upd stateset i si; val _ = Array.upd stateset (i + 1) sii; in produce gram stateset (i + 1) cs c end)); fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; fun earley (gram as Gram {tags, ...}) startsymbol indata = let val start_tag = (case tags_lookup tags startsymbol of SOME tag => tag | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol)); val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)]; val s = length indata + 1; val Estate = Array.array (s, []); val _ = Array.upd Estate 0 S0; in get_trees (produce gram Estate 0 indata Lexicon.eof) end; fun parse gram start toks = let val end_pos = (case try List.last toks of NONE => Position.none | SOME tok => Lexicon.end_pos_of_token tok); val r = (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of [] => raise Fail "Inner syntax: no parse trees" | pts => pts); in r end; end; diff --git a/src/Pure/Syntax/syntax.ML b/src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML +++ b/src/Pure/Syntax/syntax.ML @@ -1,688 +1,692 @@ (* Title: Pure/Syntax/syntax.ML Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Standard Isabelle syntax, based on arbitrary context-free grammars (specified by mixfix declarations). *) signature SYNTAX = sig type operations val install_operations: operations -> theory -> theory val root: string Config.T val ambiguity_warning: bool Config.T val ambiguity_limit: int Config.T val encode_input: Input.source -> XML.tree val implode_input: Input.source -> string val read_input_pos: string -> Position.T val read_input: string -> Input.source val parse_input: Proof.context -> (XML.tree list -> 'a) -> (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ val parse_term: Proof.context -> string -> term val parse_prop: Proof.context -> string -> term val unparse_sort: Proof.context -> sort -> Pretty.T val unparse_classrel: Proof.context -> class list -> Pretty.T val unparse_arity: Proof.context -> arity -> Pretty.T val unparse_typ: Proof.context -> typ -> Pretty.T val unparse_term: Proof.context -> term -> Pretty.T val check_sort: Proof.context -> sort -> sort val check_typ: Proof.context -> typ -> typ val check_term: Proof.context -> term -> term val check_prop: Proof.context -> term -> term val check_typs: Proof.context -> typ list -> typ list val check_terms: Proof.context -> term list -> term list val check_props: Proof.context -> term list -> term list val uncheck_sort: Proof.context -> sort -> sort val uncheck_arity: Proof.context -> arity -> arity val uncheck_classrel: Proof.context -> class list -> class list val uncheck_typs: Proof.context -> typ list -> typ list val uncheck_terms: Proof.context -> term list -> term list val read_sort: Proof.context -> string -> sort val read_typ: Proof.context -> string -> typ val read_term: Proof.context -> string -> term val read_prop: Proof.context -> string -> term val read_typs: Proof.context -> string list -> typ list val read_terms: Proof.context -> string list -> term list val read_props: Proof.context -> string list -> term list val read_sort_global: theory -> string -> sort val read_typ_global: theory -> string -> typ val read_term_global: theory -> string -> term val read_prop_global: theory -> string -> term val pretty_term: Proof.context -> term -> Pretty.T val pretty_typ: Proof.context -> typ -> Pretty.T val pretty_sort: Proof.context -> sort -> Pretty.T val pretty_classrel: Proof.context -> class list -> Pretty.T val pretty_arity: Proof.context -> arity -> Pretty.T val string_of_term: Proof.context -> term -> string val string_of_typ: Proof.context -> typ -> string val string_of_sort: Proof.context -> sort -> string val string_of_classrel: Proof.context -> class list -> string val string_of_arity: Proof.context -> arity -> string val is_pretty_global: Proof.context -> bool val set_pretty_global: bool -> Proof.context -> Proof.context val init_pretty_global: theory -> Proof.context val init_pretty: Context.generic -> Proof.context val pretty_term_global: theory -> term -> Pretty.T val pretty_typ_global: theory -> typ -> Pretty.T val pretty_sort_global: theory -> sort -> Pretty.T val string_of_term_global: theory -> term -> string val string_of_typ_global: theory -> typ -> string val string_of_sort_global: theory -> sort -> string val pretty_flexpair: Proof.context -> term * term -> Pretty.T list type syntax val eq_syntax: syntax * syntax -> bool - val force_syntax: syntax -> unit datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int} val get_approx: syntax -> string -> approx option val lookup_const: syntax -> string -> string option val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option val print_translation: syntax -> string -> Proof.context -> typ -> term list -> term (*exception Match*) val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list val print_ast_translation: syntax -> string -> Proof.context -> Ast.ast list -> Ast.ast (*exception Match*) val prtabs: syntax -> Printer.prtabs type mode val mode_default: mode val mode_input: mode val empty_syntax: syntax val merge_syntax: syntax * syntax -> syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule val update_trfuns: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_const_gram: bool -> string list -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_trrules: Ast.ast trrule list -> syntax -> syntax val remove_trrules: Ast.ast trrule list -> syntax -> syntax val const: string -> term val free: string -> term val var: indexname -> term end; structure Syntax: SYNTAX = struct (** inner syntax operations **) (* operations *) type operations = {parse_sort: Proof.context -> string -> sort, parse_typ: Proof.context -> string -> typ, parse_term: Proof.context -> string -> term, parse_prop: Proof.context -> string -> term, unparse_sort: Proof.context -> sort -> Pretty.T, unparse_typ: Proof.context -> typ -> Pretty.T, unparse_term: Proof.context -> term -> Pretty.T, check_typs: Proof.context -> typ list -> typ list, check_terms: Proof.context -> term list -> term list, check_props: Proof.context -> term list -> term list, uncheck_typs: Proof.context -> typ list -> typ list, uncheck_terms: Proof.context -> term list -> term list}; structure Operations = Theory_Data ( type T = operations option; val empty = NONE; val merge = merge_options; ); fun install_operations ops = Operations.map (fn NONE => SOME ops | SOME _ => raise Fail "Inner syntax operations already installed"); fun operation which ctxt x = (case Operations.get (Proof_Context.theory_of ctxt) of NONE => raise Fail "Inner syntax operations not installed" | SOME ops => which ops ctxt x); (* configuration options *) val root = Config.declare_string ("syntax_root", \<^here>) (K "any"); val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true); val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10); (* formal input *) fun encode_input source = let val delimited = Input.is_delimited source; val pos = Input.pos_of source; val text = Input.text_of source; in XML.Elem (Markup.input delimited (Position.properties_of pos), [XML.Text text]) end; val implode_input = encode_input #> YXML.string_of; local fun input_range (XML.Elem ((name, props), _)) = if name = Markup.inputN then (Markup.is_delimited props, Position.range_of_properties props) else (false, Position.no_range) | input_range (XML.Text _) = (false, Position.no_range); fun input_source tree = let val text = XML.content_of [tree]; val (delimited, range) = input_range tree; in Input.source delimited text range end; in fun read_input_pos str = #1 (#2 (input_range (YXML.parse str handle Fail msg => error msg))); fun read_input str = input_source (YXML.parse str handle Fail msg => error msg); fun parse_input ctxt decode markup parse str = let fun parse_tree tree = let val source = input_source tree; val syms = Input.source_explode source; val pos = Input.pos_of source; val _ = Context_Position.reports ctxt [(pos, Markup.cartouche), (pos, markup (Input.is_delimited source))]; val _ = if Options.default_bool "update_inner_syntax_cartouches" then Context_Position.report_text ctxt pos Markup.update (cartouche (Symbol_Pos.content syms)) else (); in parse (syms, pos) end; in (case YXML.parse_body str handle Fail msg => error msg of body as [tree as XML.Elem ((name, _), _)] => if name = Markup.inputN then parse_tree tree else decode body | [tree as XML.Text _] => parse_tree tree | body => decode body) end; end; (* (un)parsing *) val parse_sort = operation #parse_sort; val parse_typ = operation #parse_typ; val parse_term = operation #parse_term; val parse_prop = operation #parse_prop; val unparse_sort = operation #unparse_sort; val unparse_typ = operation #unparse_typ; val unparse_term = operation #unparse_term; (* (un)checking *) val check_typs = operation #check_typs; val check_terms = operation #check_terms; val check_props = operation #check_props; val check_typ = singleton o check_typs; val check_term = singleton o check_terms; val check_prop = singleton o check_props; val uncheck_typs = operation #uncheck_typs; val uncheck_terms = operation #uncheck_terms; (* derived operations for algebra of sorts *) local fun map_sort f S = (case f (TFree ("", S)) of TFree ("", S') => S' | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); in val check_sort = map_sort o check_typ; val uncheck_sort = map_sort o singleton o uncheck_typs; end; val uncheck_classrel = map o singleton o uncheck_sort; fun unparse_classrel ctxt cs = Pretty.block (flat (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs))); fun uncheck_arity ctxt (a, Ss, S) = let val T = Type (a, replicate (length Ss) dummyT); val a' = (case singleton (uncheck_typs ctxt) T of Type (a', _) => a' | T => raise TYPE ("uncheck_arity", [T], [])); val Ss' = map (uncheck_sort ctxt) Ss; val S' = uncheck_sort ctxt S; in (a', Ss', S') end; fun unparse_arity ctxt (a, Ss, S) = let val prtT = unparse_typ ctxt (Type (a, [])); val dom = if null Ss then [] else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1]; in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end; (* read = parse + check *) fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; fun read_typs ctxt = grouped 10 Par_List.map_independent (parse_typ ctxt) #> check_typs ctxt; fun read_terms ctxt = grouped 10 Par_List.map_independent (parse_term ctxt) #> check_terms ctxt; fun read_props ctxt = grouped 10 Par_List.map_independent (parse_prop ctxt) #> check_props ctxt; val read_typ = singleton o read_typs; val read_term = singleton o read_terms; val read_prop = singleton o read_props; val read_sort_global = read_sort o Proof_Context.init_global; val read_typ_global = read_typ o Proof_Context.init_global; val read_term_global = read_term o Proof_Context.init_global; val read_prop_global = read_prop o Proof_Context.init_global; (* pretty = uncheck + unparse *) fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt; fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt; fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt; fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt; val string_of_term = Pretty.string_of oo pretty_term; val string_of_typ = Pretty.string_of oo pretty_typ; val string_of_sort = Pretty.string_of oo pretty_sort; val string_of_classrel = Pretty.string_of oo pretty_classrel; val string_of_arity = Pretty.string_of oo pretty_arity; (* global pretty printing *) val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false); val is_pretty_global = Config.apply pretty_global; val set_pretty_global = Config.put pretty_global; val init_pretty_global = set_pretty_global true o Proof_Context.init_global; val init_pretty = Context.cases init_pretty_global I; val pretty_term_global = pretty_term o init_pretty_global; val pretty_typ_global = pretty_typ o init_pretty_global; val pretty_sort_global = pretty_sort o init_pretty_global; val string_of_term_global = string_of_term o init_pretty_global; val string_of_typ_global = string_of_typ o init_pretty_global; val string_of_sort_global = string_of_sort o init_pretty_global; (* derived operations *) fun pretty_flexpair ctxt (t, u) = [pretty_term ctxt t, Pretty.str " \\<^sup>?", Pretty.brk 1, pretty_term ctxt u]; (** tables of translation functions **) (* parse (ast) translations *) fun err_dup_trfun name c = error ("More than one " ^ name ^ " for " ^ quote c); fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); fun remove_trtab trfuns = fold (Symtab.remove Syntax_Ext.eq_trfun) trfuns; fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab) handle Symtab.DUP c => err_dup_trfun name c; fun merge_trtabs name tab1 tab2 = Symtab.merge Syntax_Ext.eq_trfun (tab1, tab2) handle Symtab.DUP c => err_dup_trfun name c; (* print (ast) translations *) fun apply_tr' tab c ctxt T args = let val fns = map fst (Symtab.lookup_list tab c); fun app_first [] = raise Match | app_first (f :: fs) = f ctxt T args handle Match => app_first fs; in app_first fns end; fun apply_ast_tr' tab c ctxt args = let val fns = map fst (Symtab.lookup_list tab c); fun app_first [] = raise Match | app_first (f :: fs) = f ctxt args handle Match => app_first fs; in app_first fns end; fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syntax_Ext.eq_trfun) trfuns; fun remove_tr'tab trfuns = fold (Symtab.remove_list Syntax_Ext.eq_trfun) trfuns; fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syntax_Ext.eq_trfun (tab1, tab2); (** tables of translation rules **) type ruletab = (Ast.ast * Ast.ast) list Symtab.table; fun dest_ruletab tab = maps snd (Symtab.dest tab); val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r)); val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); (** datatype syntax **) datatype syntax = Syntax of { input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, - gram: Parser.gram lazy, + gram: Parser.gram Synchronized.cache, consts: string Symtab.table, prmodes: string list, parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, parse_ruletab: ruletab, parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table, print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table, print_ruletab: ruletab, print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, prtabs: Printer.prtabs} * stamp; fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; -fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram); - datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}; fun get_approx (Syntax ({prtabs, ...}, _)) c = (case Printer.get_infix prtabs c of SOME infx => SOME (Infix infx) | NONE => (case Printer.get_prefix prtabs c of SOME prfx => SOME prfx | NONE => Printer.get_binder prtabs c) |> Option.map Prefix); fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; -fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Lazy.force gram); +fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Synchronized.cache_eval gram); fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; fun parse_rules (Syntax ({parse_ruletab, ...}, _)) = Symtab.lookup_list parse_ruletab; fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab; fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab; fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab; fun prtabs (Syntax ({prtabs, ...}, _)) = prtabs; type mode = string * bool; val mode_default = ("", true); val mode_input = (Print_Mode.input, true); +fun extend_gram new_xprods old_xprods gram = + Synchronized.cache (fn () => + Parser.make_gram new_xprods old_xprods (Synchronized.cache_peek gram)); + +fun new_gram new_xprods = + Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE); + (* empty_syntax *) val empty_syntax = Syntax ({input = [], lexicon = Scan.empty_lexicon, - gram = Lazy.value Parser.empty_gram, + gram = Synchronized.cache (fn () => Parser.empty_gram), consts = Symtab.empty, prmodes = [], parse_ast_trtab = Symtab.empty, parse_ruletab = Symtab.empty, parse_trtab = Symtab.empty, print_trtab = Symtab.empty, print_ruletab = Symtab.empty, print_ast_trtab = Symtab.empty, prtabs = Printer.empty_prtabs}, stamp ()); (* update_syntax *) fun update_const (c, b) tab = if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c)) then tab else Symtab.update (c, b) tab; fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val Syntax_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val new_xprods = if inout then distinct (op =) (filter_out (member (op =) input) xprods) else []; fun if_inout xs = if inout then xs else []; in Syntax ({input = new_xprods @ input, lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, - gram = if null new_xprods then gram else Lazy.map (Parser.extend_gram new_xprods) gram, + gram = if null new_xprods then gram else extend_gram new_xprods input gram, consts = fold update_const consts2 consts1, prmodes = insert (op =) mode prmodes, parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab, parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab, print_trtab = update_tr'tab print_translation print_trtab, print_ruletab = update_ruletab print_rules print_ruletab, print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab, prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ()) end; (* remove_syntax *) fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let val Syntax_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val input' = if inout then subtract (op =) xprods input else input; val changed = length input <> length input'; fun if_inout xs = if inout then xs else []; in Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon, - gram = if changed then Lazy.value (Parser.make_gram input') else gram, + gram = if changed then new_gram input' else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab, parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab, parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab, print_trtab = remove_tr'tab print_translation print_trtab, print_ruletab = remove_ruletab print_rules print_ruletab, print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab, prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ()) end; (* merge_syntax *) fun merge_syntax (Syntax (tabs1, _), Syntax (tabs2, _)) = let val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1, prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1, prtabs = prtabs1} = tabs1; val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2, prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2; val (input', gram') = if pointer_eq (input1, input2) then (input1, gram1) else (case subtract (op =) input1 input2 of [] => (input1, gram1) | new_xprods2 => if subset (op =) (input1, input2) then (input2, gram2) else let val input' = new_xprods2 @ input1; - val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input'); + val gram' = new_gram input'; in (input', gram') end); in Syntax ({input = input', lexicon = Scan.merge_lexicons (lexicon1, lexicon2), gram = gram', consts = Symtab.merge (K true) (consts1, consts2), prmodes = Library.merge (op =) (prmodes1, prmodes2), parse_ast_trtab = merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2, parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2, parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2, print_trtab = merge_tr'tabs print_trtab1 print_trtab2, print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2, print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2, prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ()) end; (** print syntax **) local fun pretty_strs_qs name strs = Pretty.strs (name :: map quote (sort_strings strs)); fun pretty_gram (Syntax (tabs, _)) = let val {lexicon, prmodes, gram, ...} = tabs; val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes); in [Pretty.block (Pretty.breaks (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))), - Pretty.big_list "productions:" (Parser.pretty_gram (Lazy.force gram)), + Pretty.big_list "productions:" (Parser.pretty_gram (Synchronized.cache_eval gram)), pretty_strs_qs "print modes:" prmodes'] end; fun pretty_trans (Syntax (tabs, _)) = let fun pretty_tab name tab = pretty_strs_qs name (sort_strings (Symtab.keys tab)); fun pretty_ruletab name tab = Pretty.big_list name (map (Pretty.item o single o Ast.pretty_rule) (dest_ruletab tab)); val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, ...} = tabs; in [pretty_tab "consts:" consts, pretty_tab "parse_ast_translation:" parse_ast_trtab, pretty_ruletab "parse_rules:" parse_ruletab, pretty_tab "parse_translation:" parse_trtab, pretty_tab "print_translation:" print_trtab, pretty_ruletab "print_rules:" print_ruletab, pretty_tab "print_ast_translation:" print_ast_trtab] end; in fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn); fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn); fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn); end; (** prepare translation rules **) (* rules *) datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a; fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y) | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y) | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y); fun parse_rule (Parse_Rule pats) = SOME pats | parse_rule (Print_Rule _) = NONE | parse_rule (Parse_Print_Rule pats) = SOME pats; fun print_rule (Parse_Rule _) = NONE | print_rule (Print_Rule pats) = SOME (swap pats) | print_rule (Parse_Print_Rule pats) = SOME (swap pats); (* check_rules *) local fun check_rule rule = (case Ast.rule_error rule of SOME msg => error ("Error in syntax translation rule: " ^ msg ^ "\n" ^ Pretty.string_of (Ast.pretty_rule rule)) | NONE => rule); in fun check_rules rules = (map check_rule (map_filter parse_rule rules), map check_rule (map_filter print_rule rules)); end; (** modify syntax **) val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns; fun update_type_gram add prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls); fun update_const_gram add logical_types prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls); val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; open Lexicon.Syntax; end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,350 +1,349 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val local_setup: (Proof.context -> Proof.context) -> unit val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_const: string -> theory -> theory val add_deps_type: string -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun local_setup f = Context.>> (Context.map_proof f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; fun rep_thy (Thy args) = args; fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], [])); fun merge args = let val thy0 = #1 (hd args); val {pos, id, ...} = rep_thy (#2 (hd args)); val merge_defs = Defs.merge (Defs.global_context thy0); val merge_wrappers = Library.merge (eq_snd op =); val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args); val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args); val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args); val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args); in make_thy (pos, id, axioms', defs', (bgs', ens')) end; ); val rep_theory = rep_thy o Thy.get; fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Position.make_entity_markup def id Markup.theoryN (name, pos); fun init_markup (name, pos) thy = let val id = serial (); val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)]; in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup {def = false} (Context.theory_long_name thy) id pos end; fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = Context.get_theory long thy name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => map (Context.theory_name long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.init_naming |> Sign.local_path |> apply_wrappers wrappers - |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs)); val rhs_extras = TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd)) |> TFrees.keys; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun add_deps_const c thy = let val T = Logic.unvarifyT_global (Sign.the_const_type thy c); in thy |> add_deps_global "" (const_dep thy (c, T)) [] end; fun add_deps_type c thy = let val n = Sign.arity_number thy c; val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); in thy |> add_deps_global "" (type_dep (c, args)) [] end fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; end;