18

1 
(* Title: Pure/Syntax/sextension.ML

0

2 
ID: $Id$


3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen


4 

18

5 
Syntax extensions (external interface): mixfix declarations, syntax rules,


6 
infixes, binders and the Pure syntax.

0

7 


8 
TODO:

18

9 
move ast_to_term (?)

0

10 
*)


11 


12 
infix > < <>;


13 


14 
signature SEXTENSION0 =


15 
sig


16 
structure Ast: AST


17 
local open Ast in


18 
datatype mixfix =


19 
Mixfix of string * string * string * int list * int 


20 
Delimfix of string * string * string 


21 
Infixl of string * string * int 


22 
Infixr of string * string * int 


23 
Binder of string * string * string * int * int 


24 
TInfixl of string * string * int 


25 
TInfixr of string * string * int


26 
datatype xrule =


27 
op > of (string * string) * (string * string) 


28 
op < of (string * string) * (string * string) 


29 
op <> of (string * string) * (string * string)


30 
datatype sext =


31 
Sext of {


32 
mixfix: mixfix list,


33 
parse_translation: (string * (term list > term)) list,


34 
print_translation: (string * (term list > term)) list} 


35 
NewSext of {


36 
mixfix: mixfix list,


37 
xrules: xrule list,


38 
parse_ast_translation: (string * (ast list > ast)) list,


39 
parse_translation: (string * (term list > term)) list,


40 
print_translation: (string * (term list > term)) list,


41 
print_ast_translation: (string * (ast list > ast)) list}


42 
val eta_contract: bool ref


43 
val mk_binder_tr: string * string > string * (term list > term)


44 
val mk_binder_tr': string * string > string * (term list > term)


45 
val dependent_tr': string * string > term list > term


46 
val max_pri: int


47 
end


48 
end;


49 


50 
signature SEXTENSION1 =


51 
sig


52 
include SEXTENSION0


53 
val empty_sext: sext


54 
val simple_sext: mixfix list > sext


55 
val constants: sext > (string list * string) list


56 
val pure_sext: sext


57 
val syntax_types: string list


58 
val constrainAbsC: string


59 
end;


60 


61 
signature SEXTENSION =


62 
sig


63 
include SEXTENSION1


64 
structure Extension: EXTENSION


65 
sharing Extension.XGram.Ast = Ast


66 
local open Extension Ast in


67 
val xrules_of: sext > xrule list


68 
val abs_tr': term > term


69 
val appl_ast_tr': ast * ast list > ast


70 
val ext_of_sext: string list > string list > (string > typ) > sext > ext


71 
val ast_to_term: (string > (term list > term) option) > ast > term


72 
val constrainIdtC: string


73 
val apropC: string


74 
end


75 
end;


76 

18

77 
functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON): SEXTENSION =

0

78 
struct


79 


80 
structure Extension = TypeExt.Extension;


81 
structure Ast = Extension.XGram.Ast;

18

82 
open Lexicon Extension Extension.XGram Ast;

0

83 


84 


85 
(** datatype sext **)


86 


87 
datatype mixfix =


88 
Mixfix of string * string * string * int list * int 


89 
Delimfix of string * string * string 


90 
Infixl of string * string * int 


91 
Infixr of string * string * int 


92 
Binder of string * string * string * int * int 


93 
TInfixl of string * string * int 


94 
TInfixr of string * string * int;


95 


96 
datatype xrule =


97 
op > of (string * string) * (string * string) 


98 
op < of (string * string) * (string * string) 


99 
op <> of (string * string) * (string * string);


100 


101 
datatype sext =


102 
Sext of {


103 
mixfix: mixfix list,


104 
parse_translation: (string * (term list > term)) list,


105 
print_translation: (string * (term list > term)) list} 


106 
NewSext of {


107 
mixfix: mixfix list,


108 
xrules: xrule list,


109 
parse_ast_translation: (string * (ast list > ast)) list,


110 
parse_translation: (string * (term list > term)) list,


111 
print_translation: (string * (term list > term)) list,


112 
print_ast_translation: (string * (ast list > ast)) list};


113 


114 


115 
(* simple_sext *)


116 


117 
fun simple_sext mixfix =


118 
Sext {mixfix = mixfix, parse_translation = [], print_translation = []};


119 


120 


121 
(* empty_sext *)


122 


123 
val empty_sext = simple_sext [];


124 


125 


126 
(* sext_components *)


127 


128 
fun sext_components (Sext {mixfix, parse_translation, print_translation}) =


129 
{mixfix = mixfix,


130 
xrules = [],


131 
parse_ast_translation = [],


132 
parse_translation = parse_translation,


133 
print_translation = print_translation,


134 
print_ast_translation = []}


135 
 sext_components (NewSext cmps) = cmps;


136 


137 


138 
(* mixfix_of *)


139 


140 
fun mixfix_of (Sext {mixfix, ...}) = mixfix


141 
 mixfix_of (NewSext {mixfix, ...}) = mixfix;


142 


143 


144 
(* xrules_of *)


145 


146 
fun xrules_of (Sext _) = []


147 
 xrules_of (NewSext {xrules, ...}) = xrules;


148 


149 


150 

18

151 
(** parse (ast) translations **)

0

152 


153 
(* application *)


154 


155 
fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)


156 
 appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;


157 


158 


159 
(* abstraction *)


160 


161 
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]


162 
 idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;


163 


164 
fun lambda_ast_tr (*"_lambda"*) [idts, body] =

18

165 
fold_ast_p "_abs" (unfold_ast "_idts" idts, body)

0

166 
 lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;


167 

18

168 
fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)


169 
 abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =

0

170 
if c = constrainC then


171 
Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT

18

172 
else raise_term "abs_tr" ts


173 
 abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;

0

174 


175 

18

176 
(* nondependent abstraction *)


177 


178 
fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)


179 
 k_tr (*"_K"*) ts = raise_term "k_tr" ts;


180 


181 


182 
(* binder *)

0

183 


184 
fun mk_binder_tr (sy, name) =


185 
let


186 
val const = Const (name, dummyT);


187 


188 
fun tr (Free (x, T), t) = const $ absfree (x, T, t)


189 
 tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))

18

190 
 tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =

0

191 
if c = constrainC then


192 
const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT)

18

193 
else raise_term "binder_tr" [t1, t]


194 
 tr (t1, t2) = raise_term "binder_tr" [t1, t2];

0

195 


196 
fun binder_tr (*sy*) [idts, body] = tr (idts, body)

18

197 
 binder_tr (*sy*) ts = raise_term "binder_tr" ts;

0

198 
in


199 
(sy, binder_tr)


200 
end;


201 


202 


203 
(* atomic props *)


204 

18

205 
fun aprop_tr (*"_aprop"*) [t] =


206 
Const (constrainC, dummyT) $ t $ Free ("prop", dummyT)


207 
 aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;

0

208 


209 


210 
(* meta implication *)


211 


212 
fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =


213 
fold_ast_p "==>" (unfold_ast "_asms" asms, concl)


214 
 bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;


215 


216 


217 

18

218 
(** print (ast) translations **)

0

219 


220 
(* application *)


221 


222 
fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]


223 
 appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];


224 


225 

18

226 
(* abstraction *)

0

227 


228 
fun strip_abss vars_of body_of tm =


229 
let

18

230 
fun free (x, _) = Free (x, dummyT);


231 

0

232 
val vars = vars_of tm;


233 
val body = body_of tm;


234 
val rev_new_vars = rename_wrt_term body vars;


235 
in

18

236 
(map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body))

0

237 
end;


238 


239 
(*do (partial) etacontraction before printing*)


240 


241 
val eta_contract = ref false;


242 


243 
fun eta_contr tm =


244 
let


245 
fun eta_abs (Abs (a, T, t)) =


246 
(case eta_abs t of

18

247 
t' as f $ u =>

0

248 
(case eta_abs u of


249 
Bound 0 =>


250 
if not (0 mem loose_bnos f) then incr_boundvars ~1 f


251 
else Abs (a, T, t')


252 
 _ => Abs (a, T, t'))


253 
 t' => Abs (a, T, t'))


254 
 eta_abs t = t;


255 
in


256 
if ! eta_contract then eta_abs tm else tm


257 
end;


258 


259 


260 
fun abs_tr' tm =

18

261 
foldr (fn (x, t) => Const ("_abs", dummyT) $ x $ t)

0

262 
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm));


263 


264 

18

265 
fun abs_ast_tr' (*"_abs"*) asts =


266 
(case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of


267 
([], _) => raise_ast "abs_ast_tr'" asts

0

268 
 (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);


269 


270 

18

271 
(* binder *)

0

272 


273 
fun mk_binder_tr' (name, sy) =


274 
let


275 
fun mk_idts [] = raise Match (*abort translation*)


276 
 mk_idts [idt] = idt


277 
 mk_idts (idt :: idts) = Const ("_idts", dummyT) $ idt $ mk_idts idts;


278 


279 
fun tr' t =


280 
let


281 
val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;


282 
in


283 
Const (sy, dummyT) $ mk_idts xs $ bd


284 
end;


285 


286 
fun binder_tr' (*name*) (t :: ts) =


287 
list_comb (tr' (Const (name, dummyT) $ t), ts)


288 
 binder_tr' (*name*) [] = raise Match;


289 
in


290 
(name, binder_tr')


291 
end;


292 


293 


294 
(* idts *)


295 


296 
fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =


297 
if c = constrainC then


298 
Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]


299 
else raise Match


300 
 idts_ast_tr' (*"_idts"*) _ = raise Match;


301 


302 


303 
(* meta implication *)


304 


305 
fun impl_ast_tr' (*"==>"*) asts =


306 
(case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of

18

307 
(asms as _ :: _ :: _, concl)

0

308 
=> Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]


309 
 _ => raise Match);


310 


311 

18

312 
(* dependent / nondependent quantifiers *)

0

313 

18

314 
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =

0

315 
if 0 mem (loose_bnos B) then


316 
let val (x', B') = variant_abs (x, dummyT, B);

18

317 
in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) end


318 
else list_comb (Const (r, dummyT) $ A $ B, ts)

0

319 
 dependent_tr' _ _ = raise Match;


320 


321 


322 

18

323 
(** ext_of_sext **)

0

324 

18

325 
fun strip_esc str =

0

326 
let

18

327 
fun strip ("'" :: c :: cs) = c :: strip cs


328 
 strip ["'"] = []


329 
 strip (c :: cs) = c :: strip cs


330 
 strip [] = [];

0

331 
in

18

332 
implode (strip (explode str))

0

333 
end;


334 

18

335 
fun infix_name sy = "op " ^ strip_esc sy;

0

336 


337 


338 
fun ext_of_sext roots xconsts read_typ sext =


339 
let

18

340 
val {mixfix, parse_ast_translation, parse_translation, print_translation,


341 
print_ast_translation, ...} = sext_components sext;

0

342 

18

343 
val tinfixT = [typeT, typeT] > typeT;

0

344 


345 
fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)


346 
 binder _ = None;


347 


348 
fun binder_typ ty =


349 
(case read_typ ty of


350 
Type ("fun", [Type ("fun", [_, T2]), T3]) =>


351 
[Type ("idts", []), T2] > T3

18

352 
 _ => error ("Illegal binder type " ^ quote ty));

0

353 

18

354 
fun mk_infix sy T c p1 p2 p3 =


355 
[Mfix ("op " ^ sy, T, c, [], max_pri),


356 
Mfix ("(_ " ^ sy ^ "/ _)", T, c, [p1, p2], p3)];


357 


358 
fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)]

0

359 
 mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]


360 
 mfix_of (Infixl (sy, ty, p)) =

18

361 
mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p

0

362 
 mfix_of (Infixr (sy, ty, p)) =

18

363 
mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p

0

364 
 mfix_of (Binder (sy, ty, _, p, q)) =


365 
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]


366 
 mfix_of (TInfixl (s, c, p)) =

18

367 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)]

0

368 
 mfix_of (TInfixr (s, c, p)) =

18

369 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)];

0

370 


371 
val mfix = flat (map mfix_of mixfix);

18

372 
val binders = mapfilter binder mixfix;


373 
val bparses = map mk_binder_tr binders;


374 
val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) binders;

0

375 
in


376 
Ext {


377 
roots = roots, mfix = mfix,

18

378 
extra_consts = distinct (filter is_xid xconsts),

0

379 
parse_ast_translation = parse_ast_translation,


380 
parse_translation = bparses @ parse_translation,


381 
print_translation = bprints @ print_translation,


382 
print_ast_translation = print_ast_translation}


383 
end;


384 


385 


386 

18

387 
(** constants **)


388 


389 
fun constants sext =


390 
let


391 
fun consts (Delimfix (_, ty, c)) = ([c], ty)


392 
 consts (Mixfix (_, ty, c, _, _)) = ([c], ty)


393 
 consts (Infixl (c, ty, _)) = ([infix_name c], ty)


394 
 consts (Infixr (c, ty, _)) = ([infix_name c], ty)


395 
 consts (Binder (_, ty, c, _, _)) = ([c], ty)


396 
 consts _ = ([""], ""); (*is filtered out below*)


397 
in


398 
distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))


399 
end;


400 


401 


402 

0

403 
(** ast_to_term **)


404 


405 
fun ast_to_term trf ast =


406 
let


407 
fun trans a args =


408 
(case trf a of


409 
None => list_comb (Const (a, dummyT), args)

18

410 
 Some f => f args handle exn


411 
=> (writeln ("Error in parse translation for " ^ quote a); raise exn));

0

412 

18

413 
fun term_of (Constant a) = trans a []


414 
 term_of (Variable x) = scan_var x


415 
 term_of (Appl (Constant a :: (asts as _ :: _))) =


416 
trans a (map term_of asts)


417 
 term_of (Appl (ast :: (asts as _ :: _))) =


418 
list_comb (term_of ast, map term_of asts)


419 
 term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];

0

420 
in

18

421 
term_of ast

0

422 
end;


423 


424 


425 


426 
(** the Pure syntax **)


427 


428 
val pure_sext =


429 
NewSext {


430 
mixfix = [


431 
Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0),


432 
Delimfix ("_", "'a => " ^ args, ""),


433 
Delimfix ("_,/ _", "['a, " ^ args ^ "] => " ^ args, "_args"),


434 
Delimfix ("_", "id => idt", ""),


435 
Mixfix ("_::_", "[id, type] => idt", "_idtyp", [0, 0], 0),


436 
Delimfix ("'(_')", "idt => idt", ""),


437 
Delimfix ("_", "idt => idts", ""),


438 
Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0),


439 
Delimfix ("_", "id => aprop", ""),


440 
Delimfix ("_", "var => aprop", ""),

113

441 
Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),

0

442 
Delimfix ("PROP _", "aprop => prop", "_aprop"),


443 
Delimfix ("_", "prop => asms", ""),


444 
Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"),


445 
Mixfix ("((3[ _ ]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),


446 
Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2),


447 
Mixfix ("(_ =?=/ _)", "['a::{}, 'a] => prop", "=?=", [3, 2], 2),


448 
Mixfix ("(_ ==>/ _)", "[prop, prop] => prop", "==>", [2, 1], 1),


449 
Binder ("!!", "('a::logic => prop) => prop", "all", 0, 0)],


450 
xrules = [],


451 
parse_ast_translation =


452 
[(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),

18

453 
("_bigimpl", bigimpl_ast_tr)],


454 
parse_translation = [("_abs", abs_tr), ("_K", k_tr), ("_aprop", aprop_tr)],

0

455 
print_translation = [],

18

456 
print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'),

0

457 
("==>", impl_ast_tr')]};


458 

18

459 
val syntax_types = [id, var, tfree, tvar, logic, "type", "types", "sort",


460 
"classes", args, "idt", "idts", "aprop", "asms"];

0

461 


462 
val constrainIdtC = "_idtyp";


463 
val constrainAbsC = "_constrainAbs";


464 
val apropC = "_aprop";


465 


466 


467 
end;


468 
