121 |
121 |
122 (* this code is a bit of a mess. add_cterm could be simplified greatly if |
122 (* this code is a bit of a mess. add_cterm could be simplified greatly if |
123 simultaneous instantiations were read or at least type checked |
123 simultaneous instantiations were read or at least type checked |
124 simultaneously rather than one after the other. This would make the tricky |
124 simultaneously rather than one after the other. This would make the tricky |
125 composition of implicit type instantiations (parameter tye) superfluous. |
125 composition of implicit type instantiations (parameter tye) superfluous. |
126 *) |
126 |
127 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = |
127 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = |
128 let val {tsig,...} = Sign.rep_sg sign |
128 let val {tsig,...} = Sign.rep_sg sign |
129 fun split([],tvs,vs) = (tvs,vs) |
129 fun split([],tvs,vs) = (tvs,vs) |
130 | split((sv,st)::l,tvs,vs) = (case explode sv of |
130 | split((sv,st)::l,tvs,vs) = (case explode sv of |
131 "'"::cs => split(l,(indexname cs,st)::tvs,vs) |
131 "'"::cs => split(l,(indexname cs,st)::tvs,vs) |
150 in (map inst cts',tye2 @ tye,used') end |
150 in (map inst cts',tye2 @ tye,used') end |
151 val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); |
151 val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); |
152 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', |
152 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', |
153 map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) |
153 map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) |
154 end; |
154 end; |
|
155 *) |
|
156 |
|
157 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = |
|
158 let val {tsig,...} = Sign.rep_sg sign |
|
159 fun split([],tvs,vs) = (tvs,vs) |
|
160 | split((sv,st)::l,tvs,vs) = (case explode sv of |
|
161 "'"::cs => split(l,(indexname cs,st)::tvs,vs) |
|
162 | cs => split(l,tvs,(indexname cs,st)::vs)); |
|
163 val (tvs,vs) = split(insts,[],[]); |
|
164 fun readT((a,i),st) = |
|
165 let val ixn = ("'" ^ a,i); |
|
166 val S = case rsorts ixn of Some S => S | None => absent ixn; |
|
167 val T = Sign.read_typ (sign,sorts) st; |
|
168 in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) |
|
169 else inst_failure ixn |
|
170 end |
|
171 val tye = map readT tvs; |
|
172 fun mkty(ixn,st) = (case rtypes ixn of |
|
173 Some T => (ixn,(st,typ_subst_TVars tye T)) |
|
174 | None => absent ixn); |
|
175 val ixnsTs = map mkty vs; |
|
176 val ixns = map fst ixnsTs |
|
177 and sTs = map snd ixnsTs |
|
178 val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs; |
|
179 fun mkcVar(ixn,T) = |
|
180 let val U = typ_subst_TVars tye2 T |
|
181 in cterm_of sign (Var(ixn,U)) end |
|
182 val ixnTs = ListPair.zip(ixns, map snd sTs) |
|
183 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye), |
|
184 ListPair.zip(map mkcVar ixnTs,cts)) |
|
185 end; |
155 |
186 |
156 |
187 |
157 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term |
188 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term |
158 Used for establishing default types (of variables) and sorts (of |
189 Used for establishing default types (of variables) and sorts (of |
159 type variables) when reading another term. |
190 type variables) when reading another term. |