Custom base types

diff --git a/src/baseTypes.sig b/src/baseTypes.sig
new file mode 100644 (file)
index 0000000..ea7bef4
--- /dev/null
+++ b/src/baseTypes.sig
@@ -0,0 +1,23 @@
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+*)
+
+(* Add some base types *)
+
+signature BASE_TYPES = sig
+
+end

diff --git a/src/baseTypes.sml b/src/baseTypes.sml
new file mode 100644 (file)
index 0000000..c9e95ee
--- /dev/null
+++ b/src/baseTypes.sml
@@ -0,0 +1,31 @@
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+*)
+
+(* Add some base types *)
+
+structure BaseTypes :> BASE_TYPES = struct
+
+open Ast
+
+val _ = Env.registerType ("even", fn (EInt n, _) => n mod 2 = 0
+                                  | _ => false)
+
+val _ = Env.registerType ("digits", fn (EString s, _) => CharVector.all Char.isDigit s
+                                  | _ => false)
+
+end

diff --git a/src/domtool.cm b/src/domtool.cm
index fb9f9e1..4771582 100644 (file)
--- a/src/domtool.cm
+++ b/src/domtool.cm
@@ -30,5 +30,8 @@ tycheck.sml
 reduce.sig
 reduce.sml
 
+baseTypes.sig
+baseTypes.sml
+
 main.sig
 main.sml

diff --git a/src/env.sig b/src/env.sig
index cc68b53..795129a 100644 (file)
--- a/src/env.sig
+++ b/src/env.sig
@@ -20,6 +20,9 @@
 
 signature ENV = sig
 
+    val registerType : string * (Ast.exp -> bool) -> unit
+    val typeRule : string -> (Ast.exp -> bool) option
+
     type env
     val empty : env
 

diff --git a/src/env.sml b/src/env.sml
index b52ead1..d18a5a9 100644 (file)
--- a/src/env.sml
+++ b/src/env.sml
@@ -25,6 +25,10 @@ open Ast
 structure SS = StringSet
 structure SM = StringMap
 
+val typeRules : (exp -> bool) SM.map ref = ref SM.empty
+fun registerType (name, rule) = typeRules := SM.insert (!typeRules, name, rule)
+fun typeRule name = SM.find (!typeRules, name)
+
 type env = SS.set * (typ * exp option) SM.map
 val empty : env = (SS.add (SS.singleton "int", "string"),
                   SM.empty)

diff --git a/src/tycheck.sml b/src/tycheck.sml
index fa006df..30a1d86 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -281,6 +281,18 @@ fun whnorm (tAll as (t, loc)) =
        TUnif (_, ref (SOME tAll)) => whnorm tAll
       | _ => tAll
 
+fun hasTyp (e, t1, t2) =
+    case whnorm t2 of
+       (TBase name, _) =>
+       (case typeRule name of
+            NONE => subTyp (t1, t2)
+          | SOME rule =>
+            if rule e then
+                ()
+            else
+                subTyp (t1, t2))
+      | _ => subTyp (t1, t2)
+
 fun checkTyp G (tAll as (t, loc)) =
     let
        val err = ErrorMsg.error (SOME loc)
@@ -316,7 +328,7 @@ fun checkExp G (eAll as (e, loc)) =
                          let
                              val t' = checkExp G e'
                          in
-                             (subTyp (t', t);
+                             (hasTyp (eAll, t', t);
                               if isError t' then
                                   (TList (TError, loc), loc)
                               else
@@ -356,8 +368,8 @@ fun checkExp G (eAll as (e, loc)) =
                val tf = checkExp G func
                val ta = checkExp G arg
            in
-               (subTyp (tf, (TArrow (dom, ran), loc));
-                subTyp (ta, dom)
+               (hasTyp (func, tf, (TArrow (dom, ran), loc));
+                hasTyp (arg, ta, dom)
                 handle Unify ue =>
                        dte (WrongType ("Function argument",
                                        arg,
@@ -637,7 +649,7 @@ fun checkDecl G (d, _, loc) =
 
            val t = checkExp G e
        in
-           subTyp (t, to)
+           hasTyp (e, t, to)
            handle Unify ue =>
                   describe_type_error loc
                                       (WrongType ("Bound value",
@@ -658,7 +670,7 @@ fun checkFile G tInit (ds, eo) =
            let
                val t = checkExp G' e
            in
-               subTyp (t, tInit)
+               hasTyp (e, t, tInit)
                handle Unify ue =>
                       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
                        preface ("Actual:", p_typ t);

diff --git a/tests/base.dtl b/tests/base.dtl
new file mode 100644 (file)
index 0000000..23ce711
--- /dev/null
+++ b/tests/base.dtl
@@ -0,0 +1,11 @@
+extern type even;
+
+extern val frob : even -> [Root];
+extern val tweak : even -> even;
+
+extern type digits;
+
+extern val splat : digits -> [Root];
+
+frob (tweak 2);
+splat "1234"