diff src/termination.sml @ 623:588b9d16b00a

Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents ae03d09043c1
children 7f871c03e3a1
line wrap: on
line diff
--- a/src/termination.sml	Sat Feb 21 16:11:56 2009 -0500
+++ b/src/termination.sml	Sun Feb 22 16:10:25 2009 -0500
@@ -190,6 +190,7 @@
                                     in
                                         (p, ps, calls)
                                     end
+                                  | EKApp (e, _) => combiner calls e
                                   | _ =>
                                     let
                                         val (p, calls) = exp parent (penv, calls) e
@@ -239,6 +240,13 @@
                         in
                             (Rabble, calls)
                         end
+                      | EKApp _ => apps ()
+                      | EKAbs (_, e) =>
+                        let
+                            val (_, calls) = exp parent (penv, calls) e
+                        in
+                            (Rabble, calls)
+                        end
 
                       | ERecord xets =>
                         let
@@ -278,7 +286,6 @@
                         in
                             (Rabble, calls)
                         end
-                      | EFold _ => (Rabble, calls)
 
                       | ECase (e, pes, _) =>
                         let