18

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

0

2 
ID: $Id$


3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen


4 

18

5 
The concrete syntax of types (used to bootstrap Pure).


6 


7 
TODO:


8 
term_of_typ: prune sorts


9 
move "_K" (?)

0

10 
*)


11 


12 
signature TYPE_EXT0 =


13 
sig


14 
val typ_of_term: (indexname > sort) > term > typ


15 
end;


16 


17 
signature TYPE_EXT =


18 
sig


19 
include TYPE_EXT0


20 
structure Extension: EXTENSION


21 
local open Extension Extension.XGram.Ast in


22 
val term_of_typ: bool > typ > term


23 
val tappl_ast_tr': ast * ast list > ast


24 
val type_ext: ext


25 
end


26 
end;


27 


28 
functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT =


29 
struct


30 


31 
structure Extension = Extension;

18

32 
open Extension Extension.XGram Extension.XGram.Ast Lexicon;

0

33 


34 

18

35 
(** typ_of_term **)

0

36 


37 
fun typ_of_term def_sort t =


38 
let


39 
fun sort_err (xi as (x, i)) =

18

40 
error ("Inconsistent sort constraints for type variable " ^


41 
quote (if i < 0 then x else string_of_vname xi));

0

42 


43 
fun put_sort scs xi s =


44 
(case assoc (scs, xi) of


45 
None => (xi, s) :: scs


46 
 Some s' => if s = s' then scs else sort_err xi);


47 

18

48 
fun insert x [] = [x: string]


49 
 insert x (lst as y :: ys) =


50 
if x > y then y :: insert x ys


51 
else if x = y then lst


52 
else x :: lst;


53 


54 
fun classes (Const (c, _)) = [c]


55 
 classes (Free (c, _)) = [c]


56 
 classes (Const ("_classes", _) $ Const (c, _) $ cls) =


57 
insert c (classes cls)


58 
 classes (Const ("_classes", _) $ Free (c, _) $ cls) =


59 
insert c (classes cls)


60 
 classes tm = raise_term "typ_of_term: bad encoding of classes" [tm];

0

61 


62 
fun sort (Const ("_emptysort", _)) = []


63 
 sort (Const (s, _)) = [s]


64 
 sort (Free (s, _)) = [s]

18

65 
 sort (Const ("_sort", _) $ cls) = classes cls


66 
 sort tm = raise_term "typ_of_term: bad encoding of sort" [tm];

0

67 


68 
fun typ (Free (x, _), scs) =


69 
(if is_tfree x then TFree (x, []) else Type (x, []), scs)


70 
 typ (Var (xi, _), scs) = (TVar (xi, []), scs)


71 
 typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) =


72 
(TFree (x, []), put_sort scs (x, ~1) (sort st))


73 
 typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) =


74 
(TVar (xi, []), put_sort scs xi (sort st))


75 
 typ (Const (a, _), scs) = (Type (a, []), scs)

18

76 
 typ (tm as _ $ _, scs) =

0

77 
let


78 
val (t, ts) = strip_comb tm;


79 
val a =

18

80 
(case t of

0

81 
Const (x, _) => x


82 
 Free (x, _) => x

18

83 
 _ => raise_term "typ_of_term: bad type application" [tm]);

0

84 
val (tys, scs') = typs (ts, scs);


85 
in


86 
(Type (a, tys), scs')


87 
end

18

88 
 typ (tm, _) = raise_term "typ_of_term: bad encoding of typ" [tm]

0

89 
and typs (t :: ts, scs) =


90 
let


91 
val (ty, scs') = typ (t, scs);


92 
val (tys, scs'') = typs (ts, scs');


93 
in (ty :: tys, scs'') end


94 
 typs ([], scs) = ([], scs);


95 


96 


97 
val (ty, scs) = typ (t, []);


98 


99 
fun get_sort xi =


100 
(case assoc (scs, xi) of


101 
None => def_sort xi


102 
 Some s => s);


103 


104 
fun add_sorts (Type (a, tys)) = Type (a, map add_sorts tys)


105 
 add_sorts (TVar (xi, _)) = TVar (xi, get_sort xi)


106 
 add_sorts (TFree (x, _)) = TFree (x, get_sort (x, ~1));


107 
in


108 
add_sorts ty


109 
end;


110 


111 


112 


113 
(** term_of_typ **)


114 


115 
fun term_of_typ show_sorts ty =


116 
let


117 
fun const x = Const (x, dummyT);

18

118 
fun free x = Free (x, dummyT);


119 
fun var xi = Var (xi, dummyT);

0

120 


121 
fun classes [] = raise Match

18

122 
 classes [c] = free c


123 
 classes (c :: cs) = const "_classes" $ free c $ classes cs;

0

124 


125 
fun sort [] = const "_emptysort"

18

126 
 sort [s] = free s


127 
 sort ss = const "_sort" $ classes ss;

0

128 


129 
fun of_sort t ss =


130 
if show_sorts then const "_ofsort" $ t $ sort ss else t;


131 

18

132 
fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)


133 
 term_of (TFree (x, ss)) = of_sort (free x) ss


134 
 term_of (TVar (xi, ss)) = of_sort (var xi) ss;

0

135 
in

18

136 
term_of ty

0

137 
end;


138 


139 


140 


141 
(** the type syntax **)


142 

18

143 
(* parse ast translations *)

0

144 

18

145 
fun tappl_ast_tr (*"_tapp(l)"*) [types, f] =


146 
Appl (f :: unfold_ast "_types" types)


147 
 tappl_ast_tr (*"_tapp(l)"*) asts = raise_ast "tappl_ast_tr" asts;

0

148 


149 
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =


150 
fold_ast_p "fun" (unfold_ast "_types" dom, cod)


151 
 bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;


152 


153 

18

154 
(* print ast translations *)

0

155 


156 
fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]


157 
 tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]


158 
 tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f];


159 


160 
fun fun_ast_tr' (*"fun"*) asts =


161 
(case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of

18

162 
(dom as _ :: _ :: _, cod)

0

163 
=> Appl [Constant "_bracket", fold_ast "_types" dom, cod]


164 
 _ => raise Match);


165 


166 


167 
(* type_ext *)


168 


169 
val sortT = Type ("sort", []);


170 
val classesT = Type ("classes", []);


171 
val typesT = Type ("types", []);


172 


173 
val type_ext =


174 
Ext {


175 
roots = [logic, "type"],


176 
mfix = [


177 
Mfix ("_", tfreeT > typeT, "", [], max_pri),


178 
Mfix ("_", tvarT > typeT, "", [], max_pri),


179 
Mfix ("_", idT > typeT, "", [], max_pri),


180 
Mfix ("_::_", [tfreeT, sortT] > typeT, "_ofsort", [max_pri, 0], max_pri),


181 
Mfix ("_::_", [tvarT, sortT] > typeT, "_ofsort", [max_pri, 0], max_pri),

18

182 
Mfix ("_", idT > sortT, "", [], max_pri),


183 
Mfix ("{}", sortT, "_emptysort", [], max_pri),


184 
Mfix ("{_}", classesT > sortT, "_sort", [], max_pri),


185 
Mfix ("_", idT > classesT, "", [], max_pri),


186 
Mfix ("_,_", [idT, classesT] > classesT, "_classes", [], max_pri),


187 
Mfix ("_ _", [typeT, idT] > typeT, "_tapp", [max_pri, 0], max_pri), (* FIXME ambiguous *)


188 
Mfix ("((1'(_'))_)", [typesT, idT] > typeT, "_tappl", [], max_pri), (* FIXME ambiguous *)

0

189 
Mfix ("_", typeT > typesT, "", [], max_pri),


190 
Mfix ("_,/ _", [typeT, typesT] > typesT, "_types", [], max_pri),


191 
Mfix ("(_/ => _)", [typeT, typeT] > typeT, "fun", [1, 0], 0),


192 
Mfix ("([_]/ => _)", [typesT, typeT] > typeT, "_bracket", [0, 0], 0)],

18

193 
extra_consts = ["_K"],

0

194 
parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr),


195 
("_bracket", bracket_ast_tr)],


196 
parse_translation = [],


197 
print_translation = [],


198 
print_ast_translation = [("fun", fun_ast_tr')]};


199 


200 


201 
end;


202 
