comparison src/elaborate.sml @ 362:24a31b35e08f

Reusable column handlers for Crud
author Adam Chlipala <adamc@hcoop.net>
date Tue, 14 Oct 2008 17:18:59 -0400
parents beb72f8a7218
children 4d519baf357c
comparison
equal deleted inserted replaced
361:260b680a6a04 362:24a31b35e08f
2165 (L'.SgnError, _) => () 2165 (L'.SgnError, _) => ()
2166 | (_, L'.SgnError) => () 2166 | (_, L'.SgnError) => ()
2167 2167
2168 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 2168 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
2169 let 2169 let
2170 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2171 ("sgn2", p_sgn env sgn2),
2172 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
2173 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
2174
2170 fun folder (sgi2All as (sgi, loc), (env, denv)) = 2175 fun folder (sgi2All as (sgi, loc), (env, denv)) =
2171 let 2176 let
2177 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
2178
2172 fun seek p = 2179 fun seek p =
2173 let 2180 let
2174 fun seek (env, denv) ls = 2181 fun seek (env, denv) ls =
2175 case ls of 2182 case ls of
2176 [] => (sgnError env (UnmatchedSgi sgi2All); 2183 [] => (sgnError env (UnmatchedSgi sgi2All);
2356 | L'.SgiVal (x, n2, c2) => 2363 | L'.SgiVal (x, n2, c2) =>
2357 seek (fn sgi1All as (sgi1, _) => 2364 seek (fn sgi1All as (sgi1, _) =>
2358 case sgi1 of 2365 case sgi1 of
2359 L'.SgiVal (x', n1, c1) => 2366 L'.SgiVal (x', n1, c1) =>
2360 if x = x' then 2367 if x = x' then
2361 (case unifyCons (env, denv) c1 c2 of 2368 ((*prefaces "Pre" [("c1", p_con env c1),
2369 ("c2", p_con env c2)];*)
2370 case unifyCons (env, denv) c1 c2 of
2362 [] => SOME (env, denv) 2371 [] => SOME (env, denv)
2363 | _ => NONE) 2372 | _ => NONE)
2364 handle CUnify (c1, c2, err) => 2373 handle CUnify (c1, c2, err) =>
2365 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2374 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2366 SOME (env, denv)) 2375 SOME (env, denv))
2844 val (c', gs4) = normClassConstraint (env, denv) c' 2853 val (c', gs4) = normClassConstraint (env, denv) c'
2845 val (env', n) = E.pushENamed env x c' 2854 val (env', n) = E.pushENamed env x c'
2846 val c' = makeInstantiable c' 2855 val c' = makeInstantiable c'
2847 in 2856 in
2848 (*prefaces "DVal" [("x", Print.PD.string x), 2857 (*prefaces "DVal" [("x", Print.PD.string x),
2849 ("c'", p_con env c')];*) 2858 ("c'", p_con env c')];*)
2850 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 2859 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
2851 end 2860 end
2852 | L.DValRec vis => 2861 | L.DValRec vis =>
2853 let 2862 let
2854 fun allowable (e, _) = 2863 fun allowable (e, _) =