--- /dev/null
+(* 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
--- /dev/null
+(* 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
reduce.sig
reduce.sml
+baseTypes.sig
+baseTypes.sml
+
main.sig
main.sml
signature ENV = sig
+ val registerType : string * (Ast.exp -> bool) -> unit
+ val typeRule : string -> (Ast.exp -> bool) option
+
type env
val empty : env
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)
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)
let
val t' = checkExp G e'
in
- (subTyp (t', t);
+ (hasTyp (eAll, t', t);
if isError t' then
(TList (TError, loc), loc)
else
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,
val t = checkExp G e
in
- subTyp (t, to)
+ hasTyp (e, t, to)
handle Unify ue =>
describe_type_error loc
(WrongType ("Bound value",
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);
--- /dev/null
+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"