Mercurial > urweb

comparison src/elaborate.sml @ 15:1e645beb3f3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Implicit constructor arguments
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 13:00:12 -0400
parents f1c36df29ed7
children 9bd8669d53c2
comparison
equal deleted inserted replaced
14:f1c36df29ed7 15:1e645beb3f3b
678 | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative") 678 | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative")
679 | E.Named (n, (L'.KType, _)) => L'.CNamed n 679 | E.Named (n, (L'.KType, _)) => L'.CNamed n
680 | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind") 680 | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind")
681 end 681 end
682 682
683 fun typeof env (e, loc) =
684 case e of
685 L'.EPrim p => (primType env p, loc)
686 | L'.ERel n => #2 (E.lookupERel env n)
687 | L'.ENamed n => #2 (E.lookupENamed env n)
688 | L'.EApp (e1, _) =>
689 (case #1 (typeof env e1) of
690 L'.TFun (_, c) => c
691 | _ => raise Fail "typeof: Bad EApp")
692 | L'.EAbs (x, t, e1) => (L'.TFun (t, typeof (E.pushERel env x t) e1), loc)
693 | L'.ECApp (e1, c) =>
694 (case #1 (typeof env e1) of
695 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
696 | _ => raise Fail "typeof: Bad ECApp")
697 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
698
699 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, e) => (x, typeof env e)) xes), loc), loc)
700 | L'.EField (_, _, {field, ...}) => field
701
702 | L'.EError => cerror
703
704 fun elabHead env (e as (_, loc)) t =
705 let
706 fun unravel (t, e) =
707 case hnormCon env t of
708 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
709 let
710 val u = cunif k
711 in
712 unravel (subConInCon (0, u) t',
713 (L'.ECApp (e, u), loc))
714 end
715 | _ => (e, t)
716 in
717 unravel (t, e)
718 end
719
683 fun elabExp env (e, loc) = 720 fun elabExp env (e, loc) =
684 case e of 721 case e of
685 L.EAnnot (e, t) => 722 L.EAnnot (e, t) =>
686 let 723 let
687 val (e', et) = elabExp env e 724 val (e', et) = elabExp env e
700 | E.Rel (n, t) => ((L'.ERel n, loc), t) 737 | E.Rel (n, t) => ((L'.ERel n, loc), t)
701 | E.Named (n, t) => ((L'.ENamed n, loc), t)) 738 | E.Named (n, t) => ((L'.ENamed n, loc), t))
702 | L.EApp (e1, e2) => 739 | L.EApp (e1, e2) =>
703 let 740 let
704 val (e1', t1) = elabExp env e1 741 val (e1', t1) = elabExp env e1
742 val (e1', t1) = elabHead env e1' t1
705 val (e2', t2) = elabExp env e2 743 val (e2', t2) = elabExp env e2
706 744
707 val dom = cunif ktype 745 val dom = cunif ktype
708 val ran = cunif ktype 746 val ran = cunif ktype
709 val t = (L'.TFun (dom, ran), dummy) 747 val t = (L'.TFun (dom, ran), dummy)
729 (L'.TFun (t', et), loc)) 767 (L'.TFun (t', et), loc))
730 end 768 end
731 | L.ECApp (e, c) => 769 | L.ECApp (e, c) =>
732 let 770 let
733 val (e', et) = elabExp env e 771 val (e', et) = elabExp env e
772 val (e', et) = elabHead env e' et
734 val (c', ck) = elabCon env c 773 val (c', ck) = elabCon env c
735 in 774 in
736 case #1 (hnormCon env et) of 775 case #1 (hnormCon env et) of
737 L'.CError => (eerror, cerror) 776 L'.CError => (eerror, cerror)
738 | L'.TCFun (_, _, k, eb) => 777 | L'.TCFun (_, _, k, eb) =>
830 val (c', ck) = elabCon env c 869 val (c', ck) = elabCon env c
831 val (env', n) = E.pushCNamed env x k' (SOME c') 870 val (env', n) = E.pushCNamed env x k' (SOME c')
832 in 871 in
833 checkKind env c' ck k'; 872 checkKind env c' ck k';
834 873
835 if kunifsInKind k' then 874 if ErrorMsg.anyErrors () then
836 declError env (KunifsRemainKind (loc, k')) 875 ()
837 else 876 else (
838 (); 877 if kunifsInKind k' then
839 878 declError env (KunifsRemainKind (loc, k'))
840 if kunifsInCon c' then 879 else
841 declError env (KunifsRemainCon (loc, c')) 880 ();
842 else 881
843 (); 882 if kunifsInCon c' then
883 declError env (KunifsRemainCon (loc, c'))
884 else
885 ()
886 );
844 887
845 (env', 888 (env',
846 (L'.DCon (x, n, k', c'), loc)) 889 (L'.DCon (x, n, k', c'), loc))
847 end 890 end
848 | L.DVal (x, co, e) => 891 | L.DVal (x, co, e) =>
854 val (e', et) = elabExp env e 897 val (e', et) = elabExp env e
855 val (env', n) = E.pushENamed env x c' 898 val (env', n) = E.pushENamed env x c'
856 in 899 in
857 checkCon env e' et c'; 900 checkCon env e' et c';
858 901
859 if kunifsInCon c' then 902 if ErrorMsg.anyErrors () then
860 declError env (KunifsRemainCon (loc, c')) 903 ()
861 else 904 else (
862 (); 905 if kunifsInCon c' then
863 906 declError env (KunifsRemainCon (loc, c'))
864 if cunifsInCon c' then 907 else
865 declError env (CunifsRemainCon (loc, c')) 908 ();
866 else 909
867 (); 910 if cunifsInCon c' then
868 911 declError env (CunifsRemainCon (loc, c'))
869 if kunifsInExp e' then 912 else
870 declError env (KunifsRemainExp (loc, e')) 913 ();
871 else 914
872 (); 915 if kunifsInExp e' then
873 916 declError env (KunifsRemainExp (loc, e'))
874 if cunifsInExp e' then 917 else
875 declError env (CunifsRemainExp (loc, e')) 918 ();
876 else 919
877 (); 920 if cunifsInExp e' then
921 declError env (CunifsRemainExp (loc, e'))
922 else
923 ());
878 924
879 (env', 925 (env',
880 (L'.DVal (x, n, c', e'), loc)) 926 (L'.DVal (x, n, c', e'), loc))
881 end) 927 end)
882 928