provide structure Syntax early (before structure Type), back-patch check/uncheck later;
authorwenzelm
Sun Apr 17 23:47:05 2011 +0200 (2011-04-17)
changeset 42382dcd983ee2c29
parent 42381 309ec68442c6
child 42383 0ae4ad40d7b5
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
src/Pure/ROOT.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/src/Pure/ROOT.ML	Sun Apr 17 21:42:47 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sun Apr 17 23:47:05 2011 +0200
     1.3 @@ -103,24 +103,16 @@
     1.4  
     1.5  use "name.ML";
     1.6  use "term.ML";
     1.7 -use "term_ord.ML";
     1.8 -use "term_subst.ML";
     1.9 -use "old_term.ML";
    1.10  use "General/pretty.ML";
    1.11  use "context.ML";
    1.12  use "config.ML";
    1.13  use "context_position.ML";
    1.14 -use "General/name_space.ML";
    1.15 -use "sorts.ML";
    1.16 -use "type.ML";
    1.17 -use "logic.ML";
    1.18  
    1.19  
    1.20  (* inner syntax *)
    1.21  
    1.22  use "Syntax/term_position.ML";
    1.23  use "Syntax/lexicon.ML";
    1.24 -use "Syntax/simple_syntax.ML";
    1.25  use "Syntax/ast.ML";
    1.26  use "Syntax/syntax_ext.ML";
    1.27  use "Syntax/parser.ML";
    1.28 @@ -132,6 +124,14 @@
    1.29  
    1.30  (* core of tactical proof system *)
    1.31  
    1.32 +use "term_ord.ML";
    1.33 +use "term_subst.ML";
    1.34 +use "old_term.ML";
    1.35 +use "General/name_space.ML";
    1.36 +use "sorts.ML";
    1.37 +use "type.ML";
    1.38 +use "logic.ML";
    1.39 +use "Syntax/simple_syntax.ML";
    1.40  use "net.ML";
    1.41  use "item_net.ML";
    1.42  use "envir.ML";
     2.1 --- a/src/Pure/Syntax/printer.ML	Sun Apr 17 21:42:47 2011 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Sun Apr 17 23:47:05 2011 +0200
     2.3 @@ -36,12 +36,12 @@
     2.4    val pretty_term_ast: bool -> Proof.context -> prtabs ->
     2.5      (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     2.6      (string -> string -> Pretty.T option) ->
     2.7 -    (string -> Markup.T list * xstring) ->
     2.8 +    (string -> Markup.T list * string) ->
     2.9      Ast.ast -> Pretty.T list
    2.10    val pretty_typ_ast: Proof.context -> prtabs ->
    2.11      (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
    2.12      (string -> string -> Pretty.T option) ->
    2.13 -    (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
    2.14 +    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
    2.15  end;
    2.16  
    2.17  structure Printer: PRINTER =
     3.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 21:42:47 2011 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Apr 17 23:47:05 2011 +0200
     3.3 @@ -10,6 +10,8 @@
     3.4    val const: string -> term
     3.5    val free: string -> term
     3.6    val var: indexname -> term
     3.7 +  type operations
     3.8 +  val install_operations: operations -> unit
     3.9    val root: string Config.T
    3.10    val positions_raw: Config.raw
    3.11    val positions: bool Config.T
    3.12 @@ -28,14 +30,6 @@
    3.13    val unparse_arity: Proof.context -> arity -> Pretty.T
    3.14    val unparse_typ: Proof.context -> typ -> Pretty.T
    3.15    val unparse_term: Proof.context -> term -> Pretty.T
    3.16 -  val install_operations:
    3.17 -   {parse_sort: Proof.context -> string -> sort,
    3.18 -    parse_typ: Proof.context -> string -> typ,
    3.19 -    parse_term: Proof.context -> string -> term,
    3.20 -    parse_prop: Proof.context -> string -> term,
    3.21 -    unparse_sort: Proof.context -> sort -> Pretty.T,
    3.22 -    unparse_typ: Proof.context -> typ -> Pretty.T,
    3.23 -    unparse_term: Proof.context -> term -> Pretty.T} -> unit
    3.24    val print_checks: Proof.context -> unit
    3.25    val add_typ_check: int -> string ->
    3.26      (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    3.27 @@ -49,6 +43,10 @@
    3.28    val add_term_uncheck: int -> string ->
    3.29      (term list -> Proof.context -> (term list * Proof.context) option) ->
    3.30      Context.generic -> Context.generic
    3.31 +  val typ_check: Proof.context -> typ list -> typ list
    3.32 +  val term_check: Proof.context -> term list -> term list
    3.33 +  val typ_uncheck: Proof.context -> typ list -> typ list
    3.34 +  val term_uncheck: Proof.context -> term list -> term list
    3.35    val check_sort: Proof.context -> sort -> sort
    3.36    val check_typ: Proof.context -> typ -> typ
    3.37    val check_term: Proof.context -> term -> term
    3.38 @@ -151,6 +149,31 @@
    3.39  
    3.40  (** inner syntax operations **)
    3.41  
    3.42 +(* back-patched operations *)
    3.43 +
    3.44 +type operations =
    3.45 + {parse_sort: Proof.context -> string -> sort,
    3.46 +  parse_typ: Proof.context -> string -> typ,
    3.47 +  parse_term: Proof.context -> string -> term,
    3.48 +  parse_prop: Proof.context -> string -> term,
    3.49 +  unparse_sort: Proof.context -> sort -> Pretty.T,
    3.50 +  unparse_typ: Proof.context -> typ -> Pretty.T,
    3.51 +  unparse_term: Proof.context -> term -> Pretty.T,
    3.52 +  check_typs: Proof.context -> typ list -> typ list,
    3.53 +  check_terms: Proof.context -> term list -> term list,
    3.54 +  check_props: Proof.context -> term list -> term list,
    3.55 +  uncheck_typs: Proof.context -> typ list -> typ list,
    3.56 +  uncheck_terms: Proof.context -> term list -> term list};
    3.57 +
    3.58 +val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
    3.59 +fun install_operations ops = Single_Assignment.assign operations ops;
    3.60 +
    3.61 +fun operation which ctxt x =
    3.62 +  (case Single_Assignment.peek operations of
    3.63 +    NONE => raise Fail "Inner syntax operations not installed"
    3.64 +  | SOME ops => which ops ctxt x);
    3.65 +
    3.66 +
    3.67  (* configuration options *)
    3.68  
    3.69  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
    3.70 @@ -191,26 +214,6 @@
    3.71      val _ = Context_Position.report ctxt pos markup;
    3.72    in (syms, pos) end;
    3.73  
    3.74 -local
    3.75 -
    3.76 -type operations =
    3.77 - {parse_sort: Proof.context -> string -> sort,
    3.78 -  parse_typ: Proof.context -> string -> typ,
    3.79 -  parse_term: Proof.context -> string -> term,
    3.80 -  parse_prop: Proof.context -> string -> term,
    3.81 -  unparse_sort: Proof.context -> sort -> Pretty.T,
    3.82 -  unparse_typ: Proof.context -> typ -> Pretty.T,
    3.83 -  unparse_term: Proof.context -> term -> Pretty.T};
    3.84 -
    3.85 -val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
    3.86 -
    3.87 -fun operation which ctxt x =
    3.88 -  (case Single_Assignment.peek operations of
    3.89 -    NONE => raise Fail "Inner syntax operations not installed"
    3.90 -  | SOME ops => which ops ctxt x);
    3.91 -
    3.92 -in
    3.93 -
    3.94  val parse_sort = operation #parse_sort;
    3.95  val parse_typ = operation #parse_typ;
    3.96  val parse_term = operation #parse_term;
    3.97 @@ -219,10 +222,6 @@
    3.98  val unparse_typ = operation #unparse_typ;
    3.99  val unparse_term = operation #unparse_term;
   3.100  
   3.101 -fun install_operations ops = Single_Assignment.assign operations ops;
   3.102 -
   3.103 -end;
   3.104 -
   3.105  
   3.106  (* context-sensitive (un)checking *)
   3.107  
   3.108 @@ -290,17 +289,22 @@
   3.109  fun add_typ_uncheck stage = gen_add apfst (stage, true);
   3.110  fun add_term_uncheck stage = gen_add apsnd (stage, true);
   3.111  
   3.112 -val check_typs = gen_check fst false;
   3.113 -val check_terms = gen_check snd false;
   3.114 -fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   3.115 +val typ_check = gen_check fst false;
   3.116 +val term_check = gen_check snd false;
   3.117 +val typ_uncheck = gen_check fst true;
   3.118 +val term_uncheck = gen_check snd true;
   3.119 +
   3.120 +val check_typs = operation #check_typs;
   3.121 +val check_terms = operation #check_terms;
   3.122 +val check_props = operation #check_props;
   3.123  
   3.124  val check_typ = singleton o check_typs;
   3.125  val check_term = singleton o check_terms;
   3.126  val check_prop = singleton o check_props;
   3.127  val check_sort = map_sort o check_typ;
   3.128  
   3.129 -val uncheck_typs = gen_check fst true;
   3.130 -val uncheck_terms = gen_check snd true;
   3.131 +val uncheck_typs = operation #uncheck_typs;
   3.132 +val uncheck_terms = operation #uncheck_terms;
   3.133  val uncheck_sort = map_sort o singleton o uncheck_typs;
   3.134  
   3.135  end;
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 21:42:47 2011 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Apr 17 23:47:05 2011 +0200
     4.3 @@ -702,6 +702,17 @@
     4.4  
     4.5  
     4.6  
     4.7 +(** check/uncheck **)
     4.8 +
     4.9 +val check_typs = Syntax.typ_check;
    4.10 +val check_terms = Syntax.term_check;
    4.11 +fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
    4.12 +
    4.13 +val uncheck_typs = Syntax.typ_uncheck;
    4.14 +val uncheck_terms = Syntax.term_uncheck;
    4.15 +
    4.16 +
    4.17 +
    4.18  (** install operations **)
    4.19  
    4.20  val _ = Syntax.install_operations
    4.21 @@ -711,6 +722,11 @@
    4.22     parse_prop = parse_term true,
    4.23     unparse_sort = unparse_sort,
    4.24     unparse_typ = unparse_typ,
    4.25 -   unparse_term = unparse_term};
    4.26 +   unparse_term = unparse_term,
    4.27 +   check_typs = check_typs,
    4.28 +   check_terms = check_terms,
    4.29 +   check_props = check_props,
    4.30 +   uncheck_typs = uncheck_typs,
    4.31 +   uncheck_terms = uncheck_terms};
    4.32  
    4.33  end;