separate module for standard implementation of inner syntax operations;
authorwenzelm
Tue Apr 05 18:06:45 2011 +0200 (2011-04-05)
changeset 42241dd8029f71e1c
parent 42240 5a4d30cd47a7
child 42242 39261908e12f
separate module for standard implementation of inner syntax operations;
src/Pure/IsaMakefile
src/Pure/Isar/proof_context.ML
src/Pure/ROOT.ML
src/Pure/Syntax/standard_syntax.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Apr 05 15:46:35 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Apr 05 18:06:45 2011 +0200
     1.3 @@ -184,6 +184,7 @@
     1.4    Syntax/parser.ML					\
     1.5    Syntax/printer.ML					\
     1.6    Syntax/simple_syntax.ML				\
     1.7 +  Syntax/standard_syntax.ML				\
     1.8    Syntax/syn_ext.ML					\
     1.9    Syntax/syn_trans.ML					\
    1.10    Syntax/syntax.ML					\
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 05 15:46:35 2011 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 05 18:06:45 2011 +0200
     2.3 @@ -26,6 +26,7 @@
     2.4    val naming_of: Proof.context -> Name_Space.naming
     2.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
     2.6    val full_name: Proof.context -> binding -> string
     2.7 +  val syntax_of: Proof.context -> Local_Syntax.T
     2.8    val syn_of: Proof.context -> Syntax.syntax
     2.9    val tsig_of: Proof.context -> Type.tsig
    2.10    val set_defsort: sort -> Proof.context -> Proof.context
    2.11 @@ -65,6 +66,7 @@
    2.12    val allow_dummies: Proof.context -> Proof.context
    2.13    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
    2.14    val check_tfree: Proof.context -> string * sort -> string * sort
    2.15 +  val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
    2.16    val type_context: Proof.context -> Syntax.type_context
    2.17    val term_context: Proof.context -> Syntax.term_context
    2.18    val decode_term: Proof.context ->
    2.19 @@ -746,93 +748,6 @@
    2.20  
    2.21  
    2.22  
    2.23 -(** inner syntax operations **)
    2.24 -
    2.25 -local
    2.26 -
    2.27 -fun parse_failed ctxt pos msg kind =
    2.28 -  cat_error msg ("Failed to parse " ^ kind ^
    2.29 -    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
    2.30 -
    2.31 -fun parse_sort ctxt text =
    2.32 -  let
    2.33 -    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    2.34 -    val S =
    2.35 -      Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
    2.36 -      handle ERROR msg => parse_failed ctxt pos msg "sort";
    2.37 -  in Type.minimize_sort (tsig_of ctxt) S end;
    2.38 -
    2.39 -fun parse_typ ctxt text =
    2.40 -  let
    2.41 -    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    2.42 -    val T =
    2.43 -      Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
    2.44 -      handle ERROR msg => parse_failed ctxt pos msg "type";
    2.45 -  in T end;
    2.46 -
    2.47 -fun parse_term T ctxt text =
    2.48 -  let
    2.49 -    val (T', _) = Type_Infer.paramify_dummies T 0;
    2.50 -    val (markup, kind) =
    2.51 -      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    2.52 -    val (syms, pos) = Syntax.parse_token ctxt markup text;
    2.53 -
    2.54 -    val default_root = Config.get ctxt Syntax.default_root;
    2.55 -    val root =
    2.56 -      (case T' of
    2.57 -        Type (c, _) =>
    2.58 -          if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c
    2.59 -          then default_root else c
    2.60 -      | _ => default_root);
    2.61 -
    2.62 -    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
    2.63 -      handle exn as ERROR _ => Exn.Exn exn;
    2.64 -    val t =
    2.65 -      Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
    2.66 -        root (syms, pos)
    2.67 -      handle ERROR msg => parse_failed ctxt pos msg kind;
    2.68 -  in t end;
    2.69 -
    2.70 -
    2.71 -fun unparse_sort ctxt =
    2.72 -  Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
    2.73 -    ctxt (syn_of ctxt);
    2.74 -
    2.75 -fun unparse_typ ctxt =
    2.76 -  let
    2.77 -    val tsig = tsig_of ctxt;
    2.78 -    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
    2.79 -  in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
    2.80 -
    2.81 -fun unparse_term ctxt =
    2.82 -  let
    2.83 -    val tsig = tsig_of ctxt;
    2.84 -    val syntax = syntax_of ctxt;
    2.85 -    val consts = consts_of ctxt;
    2.86 -    val extern =
    2.87 -     {extern_class = Type.extern_class tsig,
    2.88 -      extern_type = Type.extern_type tsig,
    2.89 -      extern_const = Consts.extern consts};
    2.90 -  in
    2.91 -    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
    2.92 -      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt)))
    2.93 -  end;
    2.94 -
    2.95 -in
    2.96 -
    2.97 -val _ = Syntax.install_operations
    2.98 -  {parse_sort = parse_sort,
    2.99 -   parse_typ = parse_typ,
   2.100 -   parse_term = parse_term dummyT,
   2.101 -   parse_prop = parse_term propT,
   2.102 -   unparse_sort = unparse_sort,
   2.103 -   unparse_typ = unparse_typ,
   2.104 -   unparse_term = unparse_term};
   2.105 -
   2.106 -end;
   2.107 -
   2.108 -
   2.109 -
   2.110  (** export results **)
   2.111  
   2.112  fun common_export is_goal inner outer =
     3.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 15:46:35 2011 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 18:06:45 2011 +0200
     3.3 @@ -170,9 +170,10 @@
     3.4  use "Isar/object_logic.ML";
     3.5  use "Isar/rule_cases.ML";
     3.6  use "Isar/auto_bind.ML";
     3.7 +use "type_infer.ML";
     3.8  use "Syntax/local_syntax.ML";
     3.9 -use "type_infer.ML";
    3.10  use "Isar/proof_context.ML";
    3.11 +use "Syntax/standard_syntax.ML";
    3.12  use "Isar/local_defs.ML";
    3.13  
    3.14  (*proof term operations*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Syntax/standard_syntax.ML	Tue Apr 05 18:06:45 2011 +0200
     4.3 @@ -0,0 +1,91 @@
     4.4 +(*  Title:      Pure/Syntax/standard_syntax.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Standard implementation of inner syntax operations.
     4.8 +*)
     4.9 +
    4.10 +structure Standard_Syntax: sig end =
    4.11 +struct
    4.12 +
    4.13 +fun parse_failed ctxt pos msg kind =
    4.14 +  cat_error msg ("Failed to parse " ^ kind ^
    4.15 +    Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
    4.16 +
    4.17 +fun parse_sort ctxt text =
    4.18 +  let
    4.19 +    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    4.20 +    val S =
    4.21 +      Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt)
    4.22 +          (ProofContext.syn_of ctxt) (syms, pos)
    4.23 +        handle ERROR msg => parse_failed ctxt pos msg "sort";
    4.24 +  in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
    4.25 +
    4.26 +fun parse_typ ctxt text =
    4.27 +  let
    4.28 +    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    4.29 +    val T =
    4.30 +      Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt)
    4.31 +          (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos)
    4.32 +        handle ERROR msg => parse_failed ctxt pos msg "type";
    4.33 +  in T end;
    4.34 +
    4.35 +fun parse_term T ctxt text =
    4.36 +  let
    4.37 +    val (T', _) = Type_Infer.paramify_dummies T 0;
    4.38 +    val (markup, kind) =
    4.39 +      if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    4.40 +    val (syms, pos) = Syntax.parse_token ctxt markup text;
    4.41 +
    4.42 +    val default_root = Config.get ctxt Syntax.default_root;
    4.43 +    val root =
    4.44 +      (case T' of
    4.45 +        Type (c, _) =>
    4.46 +          if c <> "prop" andalso Type.is_logtype (ProofContext.tsig_of ctxt) c
    4.47 +          then default_root else c
    4.48 +      | _ => default_root);
    4.49 +
    4.50 +    fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
    4.51 +      handle exn as ERROR _ => Exn.Exn exn;
    4.52 +    val t =
    4.53 +      Syntax.standard_parse_term check ctxt
    4.54 +        (ProofContext.type_context ctxt) (ProofContext.term_context ctxt)
    4.55 +        (ProofContext.syn_of ctxt) root (syms, pos)
    4.56 +      handle ERROR msg => parse_failed ctxt pos msg kind;
    4.57 +  in t end;
    4.58 +
    4.59 +
    4.60 +fun unparse_sort ctxt =
    4.61 +  Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
    4.62 +    ctxt (ProofContext.syn_of ctxt);
    4.63 +
    4.64 +fun unparse_typ ctxt =
    4.65 +  let
    4.66 +    val tsig = ProofContext.tsig_of ctxt;
    4.67 +    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
    4.68 +  in Syntax.standard_unparse_typ extern ctxt (ProofContext.syn_of ctxt) end;
    4.69 +
    4.70 +fun unparse_term ctxt =
    4.71 +  let
    4.72 +    val tsig = ProofContext.tsig_of ctxt;
    4.73 +    val syntax = ProofContext.syntax_of ctxt;
    4.74 +    val consts = ProofContext.consts_of ctxt;
    4.75 +    val extern =
    4.76 +     {extern_class = Type.extern_class tsig,
    4.77 +      extern_type = Type.extern_type tsig,
    4.78 +      extern_const = Consts.extern consts};
    4.79 +  in
    4.80 +    Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
    4.81 +      (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (ProofContext.theory_of ctxt)))
    4.82 +  end;
    4.83 +
    4.84 +
    4.85 +val _ = Syntax.install_operations
    4.86 +  {parse_sort = parse_sort,
    4.87 +   parse_typ = parse_typ,
    4.88 +   parse_term = parse_term dummyT,
    4.89 +   parse_prop = parse_term propT,
    4.90 +   unparse_sort = unparse_sort,
    4.91 +   unparse_typ = unparse_typ,
    4.92 +   unparse_term = unparse_term};
    4.93 +
    4.94 +end;