Mercurial > urweb

comparison src/elab_env.sml @ 403:8084fa9216de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ()