313 let |
313 let |
314 fun of_iterm match_cont t = |
314 fun of_iterm match_cont t = |
315 let |
315 let |
316 val (t', ts) = Code_Thingol.unfold_app t |
316 val (t', ts) = Code_Thingol.unfold_app t |
317 in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end |
317 in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end |
318 and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts |
318 and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts |
319 | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts |
319 | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts |
320 | of_iapp match_cont ((v, _) `|=> t) ts = |
320 | of_iapp match_cont ((v, _) `|=> t) ts = |
321 nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts |
321 nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts |
322 | of_iapp match_cont (ICase (((t, _), cs), t0)) ts = |
322 | of_iapp match_cont (ICase (((t, _), cs), t0)) ts = |
323 nbe_apps (ml_cases (of_iterm NONE t) |
323 nbe_apps (ml_cases (of_iterm NONE t) |
423 let |
423 let |
424 val names = map snd super_classes @ map fst classparams; |
424 val names = map snd super_classes @ map fst classparams; |
425 val params = Name.invent Name.context "d" (length names); |
425 val params = Name.invent Name.context "d" (length names); |
426 fun mk (k, name) = |
426 fun mk (k, name) = |
427 (name, ([(v, [])], |
427 (name, ([(v, [])], |
428 [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params], |
428 [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params], |
429 IVar (SOME (nth params k)))])); |
429 IVar (SOME (nth params k)))])); |
430 in map_index mk names end |
430 in map_index mk names end |
431 | eqns_of_stmt (_, Code_Thingol.Classrel _) = |
431 | eqns_of_stmt (_, Code_Thingol.Classrel _) = |
432 [] |
432 [] |
433 | eqns_of_stmt (_, Code_Thingol.Classparam _) = |
433 | eqns_of_stmt (_, Code_Thingol.Classparam _) = |
434 [] |
434 [] |
435 | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) = |
435 | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) = |
436 [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$ |
436 [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$ |
437 map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances |
437 map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances |
438 @ map (IConst o snd o fst) classparam_instances)]))]; |
438 @ map (IConst o snd o fst) classparam_instances)]))]; |
439 |
439 |
440 |
440 |
441 (* compile whole programs *) |
441 (* compile whole programs *) |
442 |
442 |