SSL Setup.thy

theory Setup
imports Main
begin

ML_file ‹../antiquote_setup.ML›
ML_file ‹../more_antiquote.ML›

declare [[default_code_width = 74]]

syntax
  "_alpha" :: "type"  (‹α›)
  "_alpha_ofsort" :: "sort ==> type"  (‹α' ::_› [0] 1000)
  "_beta" :: "type"  (‹β›)
  "_beta_ofsort" :: "sort ==> type"  (‹β' ::_› [0] 1000)

parse_ast_translation ‹
  let
  fun alpha_ast_tr [] = Ast.Variable "'a"
  | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
  fun alpha_ofsort_ast_tr [ast] =
  Ast.Appl [Ast.Constant 🍋‹_ofsort›, Ast.Variable "'a", ast]
  | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
  fun beta_ast_tr [] = Ast.Variable "'b"
  | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
  fun beta_ofsort_ast_tr [ast] =
  Ast.Appl [Ast.Constant 🍋‹_ofsort›, Ast.Variable "'b", ast]
  | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
  in
  [(🍋‹_alpha›, K alpha_ast_tr),
  (🍋‹_alpha_ofsort›, K alpha_ofsort_ast_tr),
  (🍋‹_beta›, K beta_ast_tr),
  (🍋‹_beta_ofsort›, K beta_ofsort_ast_tr)]
  end
 ›

end