src/Pure/Syntax/syntax_trans.ML
changeset 52144 9065615d0360
parent 52143 36ffe23b25f8
child 52163 72e83c82c1d4
equal deleted inserted replaced
52143:36ffe23b25f8 52144:9065615d0360
    49     string * (Proof.context -> term list -> term)
    49     string * (Proof.context -> term list -> term)
    50   val update_name_tr': term -> term
    50   val update_name_tr': term -> term
    51   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    51   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    52   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
    52   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
    53   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    53   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    54   val struct_parse_translation: string list ->
    54   val struct_tr: string list -> string * (Proof.context -> term list -> term)
    55     (string * (Proof.context -> term list -> term)) list
    55   val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
    56   val struct_print_ast_translation: string list ->
       
    57     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
       
    58 end;
    56 end;
    59 
    57 
    60 structure Syntax_Trans: SYNTAX_TRANS =
    58 structure Syntax_Trans: SYNTAX_TRANS =
    61 struct
    59 struct
    62 
    60 
   243   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
   241   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
   244 
   242 
   245 fun index_tr [t] = t
   243 fun index_tr [t] = t
   246   | index_tr ts = raise TERM ("index_tr", ts);
   244   | index_tr ts = raise TERM ("index_tr", ts);
   247 
   245 
   248 fun the_struct [] = error "Illegal reference to implicit structure"
   246 fun struct_tr structs =
   249   | the_struct (x :: _) = x;
   247   ("_struct", fn _ =>
   250 
   248     (fn [Const ("_indexdefault", _)] =>
   251 fun struct_tr structs [Const ("_indexdefault", _)] =
   249         (case structs of
   252       Syntax.const (Lexicon.mark_fixed (the_struct structs))
   250           x :: _ => Syntax.const (Lexicon.mark_fixed x)
   253   | struct_tr _ ts = raise TERM ("struct_tr", ts);
   251         | _ => error "Illegal reference to implicit structure")
       
   252       | ts => raise TERM ("struct_tr", ts)));
   254 
   253 
   255 
   254 
   256 
   255 
   257 (** print (ast) translations **)
   256 (** print (ast) translations **)
   258 
   257 
   490 (* indexed syntax *)
   489 (* indexed syntax *)
   491 
   490 
   492 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   491 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   493   | index_ast_tr' _ = raise Match;
   492   | index_ast_tr' _ = raise Match;
   494 
   493 
   495 fun struct_ast_tr' structs [Ast.Constant "_indexdefault"] =
   494 fun struct_ast_tr' structs =
   496       Ast.Appl [Ast.Constant "_free",
   495   ("_struct", fn _ =>
   497         Ast.Variable (the_struct structs handle ERROR _ => raise Match)]
   496     (fn [Ast.Constant "_indexdefault"] =>
   498   | struct_ast_tr' _ _ = raise Match;
   497         (case structs of
       
   498           x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
       
   499         | _ => raise Match)
       
   500       | _ => raise Match));
   499 
   501 
   500 
   502 
   501 
   503 
   502 (** Pure translations **)
   504 (** Pure translations **)
   503 
   505 
   533   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   535   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   534   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   536   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   535   ("\\<^const>==>", fn _ => impl_ast_tr'),
   537   ("\\<^const>==>", fn _ => impl_ast_tr'),
   536   ("_index", fn _ => index_ast_tr')];
   538   ("_index", fn _ => index_ast_tr')];
   537 
   539 
   538 fun struct_parse_translation structs = [("_struct", fn _ => struct_tr structs)];
       
   539 fun struct_print_ast_translation structs = [("_struct", fn _ => struct_ast_tr' structs)];
       
   540 
       
   541 end;
   540 end;
   542 
   541 
   543 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
   542 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
   544 open Basic_Syntax_Trans;
   543 open Basic_Syntax_Trans;