Mercurial > urweb

comparison src/elaborate.sml @ 312:f387d12193ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Datatype positivity check
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Sep 2008 09:15:00 -0400
parents 77a28e7430bf
children e457d8972ff1
comparison
equal deleted inserted replaced
311:9ad92047a499 312:f387d12193ba
1764 1764
1765 1765
1766 datatype decl_error = 1766 datatype decl_error =
1767 KunifsRemain of L'.decl list 1767 KunifsRemain of L'.decl list
1768 | CunifsRemain of L'.decl list 1768 | CunifsRemain of L'.decl list
1769 | Nonpositive of L'.decl
1769 1770
1770 fun lspan [] = ErrorMsg.dummySpan 1771 fun lspan [] = ErrorMsg.dummySpan
1771 | lspan ((_, loc) :: _) = loc 1772 | lspan ((_, loc) :: _) = loc
1772 1773
1773 fun declError env err = 1774 fun declError env err =
1776 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration"; 1777 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
1777 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)]) 1778 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1778 | CunifsRemain ds => 1779 | CunifsRemain ds =>
1779 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration"; 1780 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
1780 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)]) 1781 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1782 | Nonpositive d =>
1783 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
1784 eprefaces' [("Decl", p_decl env d)])
1781 1785
1782 datatype sgn_error = 1786 datatype sgn_error =
1783 UnboundSgn of ErrorMsg.span * string 1787 UnboundSgn of ErrorMsg.span * string
1784 | UnmatchedSgi of L'.sgn_item 1788 | UnmatchedSgi of L'.sgn_item
1785 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 1789 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
2737 end 2741 end
2738 2742
2739 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 2743 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
2740 2744
2741 2745
2746 fun positive self =
2747 let
2748 open L
2749
2750 fun none (c, _) =
2751 case c of
2752 CAnnot (c, _) => none c
2753
2754 | TFun (c1, c2) => none c1 andalso none c2
2755 | TCFun (_, _, _, c) => none c
2756 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2757 | TRecord c => none c
2758
2759 | CVar ([], x) => x <> self
2760 | CVar _ => true
2761 | CApp (c1, c2) => none c1 andalso none c2
2762 | CAbs _ => false
2763 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2764
2765 | CName _ => true
2766
2767 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
2768 | CConcat (c1, c2) => none c1 andalso none c2
2769 | CFold => true
2770
2771 | CUnit => true
2772
2773 | CTuple cs => List.all none cs
2774 | CProj (c, _) => none c
2775
2776 | CWild _ => false
2777
2778 fun pos (c, _) =
2779 case c of
2780 CAnnot (c, _) => pos c
2781
2782 | TFun (c1, c2) => none c1 andalso pos c2
2783 | TCFun (_, _, _, c) => pos c
2784 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2785 | TRecord c => pos c
2786
2787 | CVar _ => true
2788 | CApp (c1, c2) => pos c1 andalso none c2
2789 | CAbs _ => false
2790 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2791
2792 | CName _ => true
2793
2794 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
2795 | CConcat (c1, c2) => pos c1 andalso pos c2
2796 | CFold => true
2797
2798 | CUnit => true
2799
2800 | CTuple cs => List.all pos cs
2801 | CProj (c, _) => pos c
2802
2803 | CWild _ => false
2804 in
2805 pos
2806 end
2807
2742 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2808 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2743 let 2809 let
2744 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2810 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2745 2811
2746 val r = 2812 val r =
2758 2824
2759 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) 2825 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
2760 end 2826 end
2761 | L.DDatatype (x, xs, xcs) => 2827 | L.DDatatype (x, xs, xcs) =>
2762 let 2828 let
2829 val positive = List.all (fn (_, to) =>
2830 case to of
2831 NONE => true
2832 | SOME t => positive x t) xcs
2833
2763 val k = (L'.KType, loc) 2834 val k = (L'.KType, loc)
2764 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2835 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2765 val (env, n) = E.pushCNamed env x k' NONE 2836 val (env, n) = E.pushCNamed env x k' NONE
2766 val t = (L'.CNamed n, loc) 2837 val t = (L'.CNamed n, loc)
2767 val nxs = length xs - 1 2838 val nxs = length xs - 1
2795 ((x, n', to), (SS.add (used, x), env, gs')) 2866 ((x, n', to), (SS.add (used, x), env, gs'))
2796 end) 2867 end)
2797 (SS.empty, env, []) xcs 2868 (SS.empty, env, []) xcs
2798 2869
2799 val env = E.pushDatatype env n xs xcs 2870 val env = E.pushDatatype env n xs xcs
2871 val d' = (L'.DDatatype (x, n, xs, xcs), loc)
2800 in 2872 in
2801 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs' @ gs)) 2873 if positive then
2874 ()
2875 else
2876 declError env (Nonpositive d');
2877
2878 ([d'], (env, denv, gs' @ gs))
2802 end 2879 end
2803 2880
2804 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" 2881 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
2805 2882
2806 | L.DDatatypeImp (x, m1 :: ms, s) => 2883 | L.DDatatypeImp (x, m1 :: ms, s) =>