Mercurial > urweb

comparison src/elaborate.sml @ 71:6431b315a1e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborate efold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 11:09:30 -0400
parents 9f89f0b00b84
children 144d082b47ae
comparison
equal deleted inserted replaced
70:2e0f3b21fb85 71:6431b315a1e3
663 | L'.CRecord (k, (x, c) :: rest) => 663 | L'.CRecord (k, (x, c) :: rest) =>
664 hnormCon env 664 hnormCon env
665 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), 665 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
666 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), 666 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
667 (L'.CRecord (k, rest), loc)), loc)), loc) 667 (L'.CRecord (k, rest), loc)), loc)), loc)
668 | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') =>
669 let
670 val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc)
671 in
672 hnormCon env
673 (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc),
674 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc),
675 rest''), loc)), loc)
676 end
668 | _ => cAll) 677 | _ => cAll)
669 | _ => cAll) 678 | _ => cAll)
670 | _ => cAll) 679 | _ => cAll)
671 | _ => cAll) 680 | _ => cAll)
672 681
673 | L'.CConcat (c1, c2) => 682 | L'.CConcat (c1, c2) =>
674 (case (hnormCon env c1, hnormCon env c2) of 683 (case (hnormCon env c1, hnormCon env c2) of
675 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) => 684 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
676 (L'.CRecord (k, xcs1 @ xcs2), loc) 685 (L'.CRecord (k, xcs1 @ xcs2), loc)
686 | ((L'.CRecord (_, []), _), c2') => c2'
687 | ((L'.CConcat (c11, c12), loc), c2') =>
688 hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc)
677 | _ => cAll) 689 | _ => cAll)
678 690
679 | _ => cAll 691 | _ => cAll
680 692
681 and unifyCons' env c1 c2 = 693 and unifyCons' env c1 c2 =
755 767
756 | (L'.CRecord _, _) => isRecord () 768 | (L'.CRecord _, _) => isRecord ()
757 | (_, L'.CRecord _) => isRecord () 769 | (_, L'.CRecord _) => isRecord ()
758 | (L'.CConcat _, _) => isRecord () 770 | (L'.CConcat _, _) => isRecord ()
759 | (_, L'.CConcat _) => isRecord () 771 | (_, L'.CConcat _) => isRecord ()
772
773 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
774 (unifyKinds dom1 dom2;
775 unifyKinds ran1 ran2)
760 776
761 | _ => err CIncompatible 777 | _ => err CIncompatible
762 end 778 end
763 779
764 and unifyCons env c1 c2 = 780 and unifyCons env c1 c2 =
802 case p of 818 case p of
803 P.Int _ => !int 819 P.Int _ => !int
804 | P.Float _ => !float 820 | P.Float _ => !float
805 | P.String _ => !string 821 | P.String _ => !string
806 822
823 fun recCons (k, nm, v, rest, loc) =
824 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
825 rest), loc)
826
827 fun foldType (dom, loc) =
828 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
829 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
830 (L'.TCFun (L'.Explicit, "v", dom,
831 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
832 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
833 (L'.CApp ((L'.CRel 3, loc),
834 recCons (dom,
835 (L'.CRel 2, loc),
836 (L'.CRel 1, loc),
837 (L'.CRel 0, loc),
838 loc)), loc)), loc)),
839 loc)), loc)), loc),
840 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
841 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
842 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
843 loc)), loc)), loc)
844
807 fun typeof env (e, loc) = 845 fun typeof env (e, loc) =
808 case e of 846 case e of
809 L'.EPrim p => primType env p 847 L'.EPrim p => primType env p
810 | L'.ERel n => #2 (E.lookupERel env n) 848 | L'.ERel n => #2 (E.lookupERel env n)
811 | L'.ENamed n => #2 (E.lookupENamed env n) 849 | L'.ENamed n => #2 (E.lookupENamed env n)
834 | _ => raise Fail "typeof: Bad ECApp") 872 | _ => raise Fail "typeof: Bad ECApp")
835 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) 873 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
836 874
837 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) 875 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
838 | L'.EField (_, _, {field, ...}) => field 876 | L'.EField (_, _, {field, ...}) => field
877 | L'.EFold dom => foldType (dom, loc)
839 878
840 | L'.EError => cerror 879 | L'.EError => cerror
841 880
842 fun elabHead env (e as (_, loc)) t = 881 fun elabHead env (e as (_, loc)) t =
843 let 882 let
985 val rest = cunif ktype_record 1024 val rest = cunif ktype_record
986 in 1025 in
987 checkKind env c' ck kname; 1026 checkKind env c' ck kname;
988 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); 1027 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
989 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft) 1028 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
1029 end
1030
1031 | L.EFold =>
1032 let
1033 val dom = kunif ()
1034 in
1035 ((L'.EFold dom, loc), foldType (dom, loc))
990 end 1036 end
991 1037
992 1038
993 datatype decl_error = 1039 datatype decl_error =
994 KunifsRemainKind of ErrorMsg.span * L'.kind 1040 KunifsRemainKind of ErrorMsg.span * L'.kind