23 |
27 |
24 functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT = |
28 functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT = |
25 struct |
29 struct |
26 |
30 |
27 structure Extension = Extension; |
31 structure Extension = Extension; |
28 open Extension Extension.XGram.Ast; |
32 open Extension Extension.XGram Extension.XGram.Ast Lexicon; |
29 |
33 |
30 |
34 |
31 (** typ_of_term **) (* FIXME check *) |
35 (** typ_of_term **) |
32 |
36 |
33 fun typ_of_term def_sort t = |
37 fun typ_of_term def_sort t = |
34 let |
38 let |
35 fun sort_err (xi as (x, i)) = |
39 fun sort_err (xi as (x, i)) = |
36 error ("typ_of_term: inconsistent sort constraints for type variable " ^ |
40 error ("Inconsistent sort constraints for type variable " ^ |
37 (if i < 0 then x else Lexicon.string_of_vname xi)); |
41 quote (if i < 0 then x else string_of_vname xi)); |
38 |
|
39 fun is_tfree name = |
|
40 (case explode name of |
|
41 "'" :: _ :: _ => true |
|
42 | _ :: _ => false |
|
43 | _ => error ("typ_of_term: bad var name " ^ quote name)); |
|
44 |
42 |
45 fun put_sort scs xi s = |
43 fun put_sort scs xi s = |
46 (case assoc (scs, xi) of |
44 (case assoc (scs, xi) of |
47 None => (xi, s) :: scs |
45 None => (xi, s) :: scs |
48 | Some s' => if s = s' then scs else sort_err xi); |
46 | Some s' => if s = s' then scs else sort_err xi); |
49 |
47 |
50 fun classes (Const (s, _)) = [s] |
48 fun insert x [] = [x: string] |
51 | classes (Free (s, _)) = [s] |
49 | insert x (lst as y :: ys) = |
52 | classes (Const ("_sortcons", _) $ Const (s, _) $ cls) = s :: classes cls |
50 if x > y then y :: insert x ys |
53 | classes (Const ("_sortcons", _) $ Free (s, _) $ cls) = s :: classes cls |
51 else if x = y then lst |
54 | classes tm = raise (TERM ("typ_of_term: bad encoding of classes", [tm])); |
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]; |
55 |
61 |
56 fun sort (Const ("_emptysort", _)) = [] |
62 fun sort (Const ("_emptysort", _)) = [] |
57 | sort (Const (s, _)) = [s] |
63 | sort (Const (s, _)) = [s] |
58 | sort (Free (s, _)) = [s] |
64 | sort (Free (s, _)) = [s] |
59 | sort (Const ("_classes", _) $ cls) = classes cls |
65 | sort (Const ("_sort", _) $ cls) = classes cls |
60 | sort tm = raise (TERM ("typ_of_term: bad encoding of sort", [tm])); |
66 | sort tm = raise_term "typ_of_term: bad encoding of sort" [tm]; |
61 |
67 |
62 fun typ (Free (x, _), scs) = |
68 fun typ (Free (x, _), scs) = |
63 (if is_tfree x then TFree (x, []) else Type (x, []), scs) |
69 (if is_tfree x then TFree (x, []) else Type (x, []), scs) |
64 | typ (Var (xi, _), scs) = (TVar (xi, []), scs) |
70 | typ (Var (xi, _), scs) = (TVar (xi, []), scs) |
65 | typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) = |
71 | typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) = |
66 (TFree (x, []), put_sort scs (x, ~1) (sort st)) |
72 (TFree (x, []), put_sort scs (x, ~1) (sort st)) |
67 | typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) = |
73 | typ (Const ("_ofsort", _) $ Var (xi, _) $ st, scs) = |
68 (TVar (xi, []), put_sort scs xi (sort st)) |
74 (TVar (xi, []), put_sort scs xi (sort st)) |
69 | typ (Const (a, _), scs) = (Type (a, []), scs) |
75 | typ (Const (a, _), scs) = (Type (a, []), scs) |
70 | typ (tm as (_ $ _), scs) = |
76 | typ (tm as _ $ _, scs) = |
71 let |
77 let |
72 val (t, ts) = strip_comb tm; |
78 val (t, ts) = strip_comb tm; |
73 val a = |
79 val a = |
74 case t of |
80 (case t of |
75 Const (x, _) => x |
81 Const (x, _) => x |
76 | Free (x, _) => x |
82 | Free (x, _) => x |
77 | _ => raise (TERM ("typ_of_term: bad type application", [tm])); |
83 | _ => raise_term "typ_of_term: bad type application" [tm]); |
78 val (tys, scs') = typs (ts, scs); |
84 val (tys, scs') = typs (ts, scs); |
79 in |
85 in |
80 (Type (a, tys), scs') |
86 (Type (a, tys), scs') |
81 end |
87 end |
82 | typ (tm, _) = raise (TERM ("typ_of_term: bad encoding of typ", [tm])) |
88 | typ (tm, _) = raise_term "typ_of_term: bad encoding of typ" [tm] |
83 and typs (t :: ts, scs) = |
89 and typs (t :: ts, scs) = |
84 let |
90 let |
85 val (ty, scs') = typ (t, scs); |
91 val (ty, scs') = typ (t, scs); |
86 val (tys, scs'') = typs (ts, scs'); |
92 val (tys, scs'') = typs (ts, scs'); |
87 in (ty :: tys, scs'') end |
93 in (ty :: tys, scs'') end |
107 (** term_of_typ **) |
113 (** term_of_typ **) |
108 |
114 |
109 fun term_of_typ show_sorts ty = |
115 fun term_of_typ show_sorts ty = |
110 let |
116 let |
111 fun const x = Const (x, dummyT); |
117 fun const x = Const (x, dummyT); |
|
118 fun free x = Free (x, dummyT); |
|
119 fun var xi = Var (xi, dummyT); |
112 |
120 |
113 fun classes [] = raise Match |
121 fun classes [] = raise Match |
114 | classes [s] = const s |
122 | classes [c] = free c |
115 | classes (s :: ss) = const "_sortcons" $ const s $ classes ss; |
123 | classes (c :: cs) = const "_classes" $ free c $ classes cs; |
116 |
124 |
117 fun sort [] = const "_emptysort" |
125 fun sort [] = const "_emptysort" |
118 | sort [s] = const s |
126 | sort [s] = free s |
119 | sort ss = const "_classes" $ classes ss; |
127 | sort ss = const "_sort" $ classes ss; |
120 |
128 |
121 fun of_sort t ss = |
129 fun of_sort t ss = |
122 if show_sorts then const "_ofsort" $ t $ sort ss else t; |
130 if show_sorts then const "_ofsort" $ t $ sort ss else t; |
123 |
131 |
124 fun typ (Type (a, tys)) = list_comb (const a, map typ tys) |
132 fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys) |
125 | typ (TFree (x, ss)) = of_sort (Free (x, dummyT)) ss |
133 | term_of (TFree (x, ss)) = of_sort (free x) ss |
126 | typ (TVar (xi, ss)) = of_sort (Var (xi, dummyT)) ss; |
134 | term_of (TVar (xi, ss)) = of_sort (var xi) ss; |
127 in |
135 in |
128 typ ty |
136 term_of ty |
129 end; |
137 end; |
130 |
138 |
131 |
139 |
132 |
140 |
133 (** the type syntax **) |
141 (** the type syntax **) |
134 |
142 |
135 (* parse translations *) |
143 (* parse ast translations *) |
136 |
144 |
137 fun tappl_ast_tr (*"_tappl"*) [types, f] = Appl (f :: unfold_ast "_types" types) |
145 fun tappl_ast_tr (*"_tapp(l)"*) [types, f] = |
138 | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts; |
146 Appl (f :: unfold_ast "_types" types) |
|
147 | tappl_ast_tr (*"_tapp(l)"*) asts = raise_ast "tappl_ast_tr" asts; |
139 |
148 |
140 fun bracket_ast_tr (*"_bracket"*) [dom, cod] = |
149 fun bracket_ast_tr (*"_bracket"*) [dom, cod] = |
141 fold_ast_p "fun" (unfold_ast "_types" dom, cod) |
150 fold_ast_p "fun" (unfold_ast "_types" dom, cod) |
142 | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts; |
151 | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts; |
143 |
152 |
144 |
153 |
145 (* print translations *) |
154 (* print ast translations *) |
146 |
155 |
147 fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f] |
156 fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f] |
148 | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f] |
157 | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f] |
149 | tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f]; |
158 | tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f]; |
150 |
159 |
151 fun fun_ast_tr' (*"fun"*) asts = |
160 fun fun_ast_tr' (*"fun"*) asts = |
152 (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of |
161 (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of |
153 (dom as (_ :: _ :: _), cod) |
162 (dom as _ :: _ :: _, cod) |
154 => Appl [Constant "_bracket", fold_ast "_types" dom, cod] |
163 => Appl [Constant "_bracket", fold_ast "_types" dom, cod] |
155 | _ => raise Match); |
164 | _ => raise Match); |
156 |
165 |
157 |
166 |
158 (* type_ext *) |
167 (* type_ext *) |
163 |
172 |
164 val type_ext = |
173 val type_ext = |
165 Ext { |
174 Ext { |
166 roots = [logic, "type"], |
175 roots = [logic, "type"], |
167 mfix = [ |
176 mfix = [ |
168 Mfix ("_", idT --> sortT, "", [], max_pri), |
|
169 Mfix ("{}", sortT, "_emptysort", [], max_pri), |
|
170 Mfix ("{_}", classesT --> sortT, "_classes", [], max_pri), |
|
171 Mfix ("_", idT --> classesT, "", [], max_pri), |
|
172 Mfix ("_,_", [idT, classesT] ---> classesT, "_sortcons", [], max_pri), |
|
173 Mfix ("_", tfreeT --> typeT, "", [], max_pri), |
177 Mfix ("_", tfreeT --> typeT, "", [], max_pri), |
174 Mfix ("_", tvarT --> typeT, "", [], max_pri), |
178 Mfix ("_", tvarT --> typeT, "", [], max_pri), |
175 Mfix ("_", idT --> typeT, "", [], max_pri), |
179 Mfix ("_", idT --> typeT, "", [], max_pri), |
176 Mfix ("_::_", [tfreeT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
180 Mfix ("_::_", [tfreeT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
177 Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
181 Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), |
178 Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), |
182 Mfix ("_", idT --> sortT, "", [], max_pri), |
179 Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT, "_tappl", [], 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 *) |
180 Mfix ("_", typeT --> typesT, "", [], max_pri), |
189 Mfix ("_", typeT --> typesT, "", [], max_pri), |
181 Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), |
190 Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), |
182 Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0), |
191 Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0), |
183 Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)], |
192 Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)], |
184 extra_consts = ["fun"], |
193 extra_consts = ["_K"], |
185 parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), |
194 parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), |
186 ("_bracket", bracket_ast_tr)], |
195 ("_bracket", bracket_ast_tr)], |
187 parse_preproc = None, |
|
188 parse_postproc = None, |
|
189 parse_translation = [], |
196 parse_translation = [], |
190 print_translation = [], |
197 print_translation = [], |
191 print_preproc = None, |
|
192 print_postproc = None, |
|
193 print_ast_translation = [("fun", fun_ast_tr')]}; |
198 print_ast_translation = [("fun", fun_ast_tr')]}; |
194 |
199 |
195 |
200 |
196 end; |
201 end; |
197 |
202 |