# HG changeset patch # User wenzelm # Date 1302019605 -7200 # Node ID dd8029f71e1c6c073d53575b45bcf5adfb4e5b64 # Parent 5a4d30cd47a7d1682d7c1ac0f42dbeb998eb581b separate module for standard implementation of inner syntax operations; diff -r 5a4d30cd47a7 -r dd8029f71e1c src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Apr 05 15:46:35 2011 +0200 +++ b/src/Pure/IsaMakefile Tue Apr 05 18:06:45 2011 +0200 @@ -184,6 +184,7 @@ Syntax/parser.ML \ Syntax/printer.ML \ Syntax/simple_syntax.ML \ + Syntax/standard_syntax.ML \ Syntax/syn_ext.ML \ Syntax/syn_trans.ML \ Syntax/syntax.ML \ diff -r 5a4d30cd47a7 -r dd8029f71e1c src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 05 15:46:35 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 18:06:45 2011 +0200 @@ -26,6 +26,7 @@ val naming_of: Proof.context -> Name_Space.naming val restore_naming: Proof.context -> Proof.context -> Proof.context val full_name: Proof.context -> binding -> string + val syntax_of: Proof.context -> Local_Syntax.T val syn_of: Proof.context -> Syntax.syntax val tsig_of: Proof.context -> Type.tsig val set_defsort: sort -> Proof.context -> Proof.context @@ -65,6 +66,7 @@ val allow_dummies: Proof.context -> Proof.context val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort + val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort val type_context: Proof.context -> Syntax.type_context val term_context: Proof.context -> Syntax.term_context val decode_term: Proof.context -> @@ -746,93 +748,6 @@ -(** inner syntax operations **) - -local - -fun parse_failed ctxt pos msg kind = - cat_error msg ("Failed to parse " ^ kind ^ - Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); - -fun parse_sort ctxt text = - let - val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; - val S = - Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos) - handle ERROR msg => parse_failed ctxt pos msg "sort"; - in Type.minimize_sort (tsig_of ctxt) S end; - -fun parse_typ ctxt text = - let - val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; - val T = - Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos) - handle ERROR msg => parse_failed ctxt pos msg "type"; - in T end; - -fun parse_term T ctxt text = - let - val (T', _) = Type_Infer.paramify_dummies T 0; - val (markup, kind) = - if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); - val (syms, pos) = Syntax.parse_token ctxt markup text; - - val default_root = Config.get ctxt Syntax.default_root; - val root = - (case T' of - Type (c, _) => - if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c - then default_root else c - | _ => default_root); - - fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) - handle exn as ERROR _ => Exn.Exn exn; - val t = - Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt) - root (syms, pos) - handle ERROR msg => parse_failed ctxt pos msg kind; - in t end; - - -fun unparse_sort ctxt = - Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)} - ctxt (syn_of ctxt); - -fun unparse_typ ctxt = - let - val tsig = tsig_of ctxt; - val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; - in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end; - -fun unparse_term ctxt = - let - val tsig = tsig_of ctxt; - val syntax = syntax_of ctxt; - val consts = consts_of ctxt; - val extern = - {extern_class = Type.extern_class tsig, - extern_type = Type.extern_type tsig, - extern_const = Consts.extern consts}; - in - Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt - (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt))) - end; - -in - -val _ = Syntax.install_operations - {parse_sort = parse_sort, - parse_typ = parse_typ, - parse_term = parse_term dummyT, - parse_prop = parse_term propT, - unparse_sort = unparse_sort, - unparse_typ = unparse_typ, - unparse_term = unparse_term}; - -end; - - - (** export results **) fun common_export is_goal inner outer = diff -r 5a4d30cd47a7 -r dd8029f71e1c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Apr 05 15:46:35 2011 +0200 +++ b/src/Pure/ROOT.ML Tue Apr 05 18:06:45 2011 +0200 @@ -170,9 +170,10 @@ use "Isar/object_logic.ML"; use "Isar/rule_cases.ML"; use "Isar/auto_bind.ML"; +use "type_infer.ML"; use "Syntax/local_syntax.ML"; -use "type_infer.ML"; use "Isar/proof_context.ML"; +use "Syntax/standard_syntax.ML"; use "Isar/local_defs.ML"; (*proof term operations*) diff -r 5a4d30cd47a7 -r dd8029f71e1c src/Pure/Syntax/standard_syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/standard_syntax.ML Tue Apr 05 18:06:45 2011 +0200 @@ -0,0 +1,91 @@ +(* Title: Pure/Syntax/standard_syntax.ML + Author: Makarius + +Standard implementation of inner syntax operations. +*) + +structure Standard_Syntax: sig end = +struct + +fun parse_failed ctxt pos msg kind = + cat_error msg ("Failed to parse " ^ kind ^ + Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad "")); + +fun parse_sort ctxt text = + let + val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; + val S = + Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt) + (ProofContext.syn_of ctxt) (syms, pos) + handle ERROR msg => parse_failed ctxt pos msg "sort"; + in Type.minimize_sort (ProofContext.tsig_of ctxt) S end; + +fun parse_typ ctxt text = + let + val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; + val T = + Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt) + (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos) + handle ERROR msg => parse_failed ctxt pos msg "type"; + in T end; + +fun parse_term T ctxt text = + let + val (T', _) = Type_Infer.paramify_dummies T 0; + val (markup, kind) = + if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term"); + val (syms, pos) = Syntax.parse_token ctxt markup text; + + val default_root = Config.get ctxt Syntax.default_root; + val root = + (case T' of + Type (c, _) => + if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c + then default_root else c + | _ => default_root); + + fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) + handle exn as ERROR _ => Exn.Exn exn; + val t = + Syntax.standard_parse_term check ctxt + (ProofContext.type_context ctxt) (ProofContext.term_context ctxt) + (ProofContext.syn_of ctxt) root (syms, pos) + handle ERROR msg => parse_failed ctxt pos msg kind; + in t end; + + +fun unparse_sort ctxt = + Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)} + ctxt (ProofContext.syn_of ctxt); + +fun unparse_typ ctxt = + let + val tsig = ProofContext.tsig_of ctxt; + val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig}; + in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end; + +fun unparse_term ctxt = + let + val tsig = ProofContext.tsig_of ctxt; + val syntax = ProofContext.syntax_of ctxt; + val consts = ProofContext.consts_of ctxt; + val extern = + {extern_class = Type.extern_class tsig, + extern_type = Type.extern_type tsig, + extern_const = Consts.extern consts}; + in + Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt + (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt))) + end; + + +val _ = Syntax.install_operations + {parse_sort = parse_sort, + parse_typ = parse_typ, + parse_term = parse_term dummyT, + parse_prop = parse_term propT, + unparse_sort = unparse_sort, + unparse_typ = unparse_typ, + unparse_term = unparse_term}; + +end;