Mercurial > urweb
comparison src/elab_env.sml @ 403:8084fa9216de
New implicit argument handling
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 21 Oct 2008 16:41:11 -0400 |
parents | 389399d65331 |
children | cb5897276abf |
comparison
equal
deleted
inserted
replaced
402:ebf27030ae3b | 403:8084fa9216de |
---|---|
356 | 356 |
357 renameSgn = #renameSgn env, | 357 renameSgn = #renameSgn env, |
358 sgn = #sgn env, | 358 sgn = #sgn env, |
359 | 359 |
360 renameStr = #renameStr env, | 360 renameStr = #renameStr env, |
361 str = #str env} | 361 str = #str env} |
362 | 362 |
363 fun class_name_in (c, _) = | 363 fun class_name_in (c, _) = |
364 case c of | 364 case c of |
365 CNamed n => SOME (ClNamed n) | 365 CNamed n => SOME (ClNamed n) |
366 | CModProj x => SOME (ClProj x) | 366 | CModProj x => SOME (ClProj x) |
367 | CUnif (_, _, _, ref (SOME c)) => class_name_in c | 367 | CUnif (_, _, _, ref (SOME c)) => class_name_in c |
368 | _ => NONE | 368 | _ => NONE |
369 | |
370 fun isClass (env : env) c = | |
371 let | |
372 fun find NONE = false | |
373 | find (SOME c) = Option.isSome (CM.find (#classes env, c)) | |
374 in | |
375 find (class_name_in c) | |
376 end | |
369 | 377 |
370 fun class_key_in (c, _) = | 378 fun class_key_in (c, _) = |
371 case c of | 379 case c of |
372 CRel n => SOME (CkRel n) | 380 CRel n => SOME (CkRel n) |
373 | CNamed n => SOME (CkNamed n) | 381 | CNamed n => SOME (CkNamed n) |
403 ground = KM.map liftExp (#ground class) | 411 ground = KM.map liftExp (#ground class) |
404 }) (#classes env) | 412 }) (#classes env) |
405 val classes = case class_pair_in t of | 413 val classes = case class_pair_in t of |
406 NONE => classes | 414 NONE => classes |
407 | SOME (f, x) => | 415 | SOME (f, x) => |
408 let | 416 case CM.find (classes, f) of |
409 val class = Option.getOpt (CM.find (classes, f), empty_class) | 417 NONE => classes |
410 val class = { | 418 | SOME class => |
411 ground = KM.insert (#ground class, x, (ERel 0, #2 t)) | 419 let |
412 } | 420 val class = { |
413 in | 421 ground = KM.insert (#ground class, x, (ERel 0, #2 t)) |
414 CM.insert (classes, f, class) | 422 } |
415 end | 423 in |
424 CM.insert (classes, f, class) | |
425 end | |
416 in | 426 in |
417 {renameC = #renameC env, | 427 {renameC = #renameC env, |
418 relC = #relC env, | 428 relC = #relC env, |
419 namedC = #namedC env, | 429 namedC = #namedC env, |
420 | 430 |
442 let | 452 let |
443 val classes = #classes env | 453 val classes = #classes env |
444 val classes = case class_pair_in t of | 454 val classes = case class_pair_in t of |
445 NONE => classes | 455 NONE => classes |
446 | SOME (f, x) => | 456 | SOME (f, x) => |
447 let | 457 case CM.find (classes, f) of |
448 val class = Option.getOpt (CM.find (classes, f), empty_class) | 458 NONE => classes |
449 val class = { | 459 | SOME class => |
450 ground = KM.insert (#ground class, x, (ENamed n, #2 t)) | 460 let |
451 } | 461 val class = { |
452 in | 462 ground = KM.insert (#ground class, x, (ENamed n, #2 t)) |
453 CM.insert (classes, f, class) | 463 } |
454 end | 464 in |
465 CM.insert (classes, f, class) | |
466 end | |
455 in | 467 in |
456 {renameC = #renameC env, | 468 {renameC = #renameC env, |
457 relC = #relC env, | 469 relC = #relC env, |
458 namedC = #namedC env, | 470 namedC = #namedC env, |
459 | 471 |
738 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of | 750 case class_key_in (sgnS_con' (m1, ms, fmap) (#1 a), #2 a) of |
739 NONE => default () | 751 NONE => default () |
740 | SOME ck => | 752 | SOME ck => |
741 let | 753 let |
742 val cn = ClProj (m1, ms, fx) | 754 val cn = ClProj (m1, ms, fx) |
743 val class = Option.getOpt (CM.find (classes, cn), empty_class) | 755 |
744 val class = { | 756 val classes = |
745 ground = KM.insert (#ground class, ck, | 757 case CM.find (classes, cn) of |
746 (EModProj (m1, ms, x), #2 sgn)) | 758 NONE => classes |
747 } | 759 | SOME class => |
748 | 760 let |
761 val class = { | |
762 ground = KM.insert (#ground class, ck, | |
763 (EModProj (m1, ms, x), #2 sgn)) | |
764 } | |
765 in | |
766 CM.insert (classes, cn, class) | |
767 end | |
749 in | 768 in |
750 (CM.insert (classes, cn, class), | 769 (classes, |
751 newClasses, | 770 newClasses, |
752 fmap, | 771 fmap, |
753 env) | 772 env) |
754 end) | 773 end) |
755 | SgiVal _ => default () | 774 | SgiVal _ => default () |