# HG changeset patch # User wenzelm # Date 1322235149 -3600 # Node ID b23c42b9f78a5bf8aa7222decab5518cfd60bda0 # Parent 6bdf8b926f502fb02d977b2eb98d511a8e4f1599 prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future; diff -r 6bdf8b926f50 -r b23c42b9f78a src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Fri Nov 25 14:23:36 2011 +0100 +++ b/src/Pure/Syntax/parser.ML Fri Nov 25 16:32:29 2011 +0100 @@ -9,7 +9,7 @@ type gram val empty_gram: gram val extend_gram: Syntax_Ext.xprod list -> gram -> gram - val merge_gram: gram * gram -> gram + val make_gram: Syntax_Ext.xprod list -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = Node of string * parsetree list | @@ -526,105 +526,7 @@ prods = Array.vector prods'} end; - -(*Merge two grammars*) -fun merge_gram (gram_a, gram_b) = - let - (*find out which grammar is bigger*) - val - (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1, - chains = chains1, lambdas = lambdas1, prods = prods1}, - Gram {nt_count = nt_count2, prod_count = prod_count2, tags = tags2, - chains = chains2, lambdas = lambdas2, prods = prods2}) = - let - val Gram {prod_count = count_a, ...} = gram_a; - val Gram {prod_count = count_b, ...} = gram_b; - in - if count_a > count_b - then (gram_a, gram_b) - else (gram_b, gram_a) - end; - - (*get existing tag from grammar1 or create a new one*) - fun get_tag nt_count tags nt = - (case Symtab.lookup tags nt of - SOME tag => (nt_count, tags, tag) - | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count)); - - val ((nt_count1', tags1'), tag_table) = - let - val table = Array.array (nt_count2, ~1); - - fun the_nt tag = - the (Symtab.get_first (fn (n, t) => if t = tag then SOME n else NONE) tags2); - fun store_tag nt_count tags ~1 = (nt_count, tags) - | store_tag nt_count tags tag = - let - val (nt_count', tags', tag') = get_tag nt_count tags (the_nt tag); - val _ = Array.update (table, tag, tag'); - in store_tag nt_count' tags' (tag - 1) end; - in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end; - - (*convert grammar2 tag to grammar1 tag*) - fun convert_tag tag = Array.sub (tag_table, tag); - - (*convert chain list to raw productions*) - fun mk_chain_prods [] result = result - | mk_chain_prods ((to, froms) :: cs) result = - let - val to_tag = convert_tag to; - - fun make [] result = result - | make (from :: froms) result = make froms - ((to_tag, ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result); - in mk_chain_prods cs (make froms [] @ result) end; - - val chain_prods = mk_chain_prods chains2 []; - - (*convert prods2 array to productions*) - fun process_nt ~1 result = result - | process_nt nt result = - let - val nt_prods = fold (union (op =) o snd) (snd (Vector.sub (prods2, nt))) []; - val lhs_tag = convert_tag nt; - - (*convert tags in rhs*) - fun process_rhs [] result = result - | process_rhs (Terminal tk :: rhs) result = - process_rhs rhs (result @ [Terminal tk]) - | process_rhs (Nonterminal (nt, prec) :: rhs) result = - process_rhs rhs (result @ [Nonterminal (convert_tag nt, prec)]); - - (*convert tags in productions*) - fun process_prods [] result = result - | process_prods ((rhs, id, prec) :: ps) result = - process_prods ps ((lhs_tag, (process_rhs rhs [], id, prec)) :: result); - in process_nt (nt - 1) (process_prods nt_prods [] @ result) end; - - val raw_prods = chain_prods @ process_nt (nt_count2 - 1) []; - - val prods1' = - let - fun get_prod i = - if i < nt_count1 then Vector.sub (prods1, i) - else (([], []), []); - in Array.tabulate (nt_count1', get_prod) end; - - val fromto_chains = inverse_chains chains1 []; - - val (fromto_chains', lambdas', SOME prod_count1') = - add_prods prods1' fromto_chains lambdas1 (SOME prod_count1) raw_prods; - - val chains' = inverse_chains fromto_chains' []; - in - Gram - {nt_count = nt_count1', - prod_count = prod_count1', - tags = tags1', - chains = chains', - lambdas = lambdas', - prods = Array.vector prods1'} - end; +fun make_gram xprods = extend_gram xprods empty_gram; diff -r 6bdf8b926f50 -r b23c42b9f78a src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Nov 25 14:23:36 2011 +0100 +++ b/src/Pure/Syntax/syntax.ML Fri Nov 25 16:32:29 2011 +0100 @@ -74,7 +74,7 @@ val string_of_sort_global: theory -> sort -> string type syntax val eq_syntax: syntax * syntax -> bool - val join_syntax: syntax -> unit + val force_syntax: syntax -> unit val lookup_const: syntax -> string -> string option val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list @@ -92,7 +92,7 @@ val mode_default: mode val mode_input: mode val empty_syntax: syntax - val merge_syntaxes: syntax -> syntax -> syntax + val merge_syntax: syntax * syntax -> syntax val token_markers: string list val basic_nonterms: string list val print_gram: syntax -> unit @@ -379,16 +379,11 @@ (** datatype syntax **) -fun future_gram deps e = - singleton - (Future.cond_forks {name = "Syntax.gram", group = NONE, - deps = map Future.task_of deps, pri = 0, interrupts = true}) e; - datatype syntax = Syntax of { input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, - gram: Parser.gram future, + gram: Parser.gram lazy, consts: string Symtab.table, prmodes: string list, parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, @@ -401,12 +396,12 @@ fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; -fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram); +fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram); 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 ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Future.join gram); +fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Lazy.force gram); fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; @@ -427,7 +422,7 @@ val empty_syntax = Syntax ({input = [], lexicon = Scan.empty_lexicon, - gram = Future.value Parser.empty_gram, + gram = Lazy.value Parser.empty_gram, consts = Symtab.empty, prmodes = [], parse_ast_trtab = Symtab.empty, @@ -460,7 +455,7 @@ Syntax ({input = new_xprods @ input, lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, - gram = Future.value (Parser.extend_gram new_xprods (Future.join gram)), + gram = Lazy.value (Parser.extend_gram new_xprods (Lazy.force gram)), consts = fold update_const consts2 consts1, prmodes = insert (op =) mode prmodes, parse_ast_trtab = @@ -489,7 +484,7 @@ Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon, - gram = if changed then Future.value (Parser.extend_gram input' Parser.empty_gram) else gram, + gram = if changed then Lazy.value (Parser.make_gram input') else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab, @@ -502,9 +497,9 @@ end; -(* merge_syntaxes *) +(* merge_syntax *) -fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) = +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, @@ -515,12 +510,22 @@ 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') = + (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 (fn () => Parser.make_gram input'); + in (input', gram') end); in Syntax - ({input = Library.merge (op =) (input1, input2), + ({input = input', lexicon = Scan.merge_lexicons (lexicon1, lexicon2), - gram = future_gram [gram1, gram2] (fn () => - Parser.merge_gram (Future.join gram1, Future.join gram2)), + gram = gram', consts = Symtab.merge (K true) (consts1, consts2), prmodes = Library.merge (op =) (prmodes1, prmodes2), parse_ast_trtab = @@ -560,7 +565,7 @@ val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes); in [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon), - Pretty.big_list "prods:" (Parser.pretty_gram (Future.join gram)), + Pretty.big_list "prods:" (Parser.pretty_gram (Lazy.force gram)), pretty_strs_qs "print modes:" prmodes'] end; @@ -596,7 +601,7 @@ (* reconstructing infixes -- educated guessing *) fun guess_infix (Syntax ({gram, ...}, _)) c = - (case Parser.guess_infix_lr (Future.join gram) c of + (case Parser.guess_infix_lr (Lazy.force gram) c of SOME (s, l, r, j) => SOME (if l then Mixfix.Infixl (s, j) else if r then Mixfix.Infixr (s, j) diff -r 6bdf8b926f50 -r b23c42b9f78a src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Nov 25 14:23:36 2011 +0100 +++ b/src/Pure/sign.ML Fri Nov 25 16:32:29 2011 +0100 @@ -149,7 +149,7 @@ val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2; val naming = Name_Space.default_naming; - val syn = Syntax.merge_syntaxes syn1 syn2; + val syn = Syntax.merge_syntax (syn1, syn2); val tsig = Type.merge_tsig ctxt (tsig1, tsig2); val consts = Consts.merge (consts1, consts2); in make_sign (naming, syn, tsig, consts) end; diff -r 6bdf8b926f50 -r b23c42b9f78a src/Pure/theory.ML --- a/src/Pure/theory.ML Fri Nov 25 14:23:36 2011 +0100 +++ b/src/Pure/theory.ML Fri Nov 25 16:32:29 2011 +0100 @@ -147,7 +147,7 @@ |> Sign.local_path |> Sign.map_naming (Name_Space.set_theory_name name) |> apply_wrappers wrappers - |> tap (Syntax.join_syntax o Sign.syn_of) + |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy =