From 6be996d467429cc09f81becd3fd4e294ae1871ae Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 30 Jul 2006 01:26:25 +0000 Subject: [PATCH] Custom base types --- src/baseTypes.sig | 23 +++++++++++++++++++++++ src/baseTypes.sml | 31 +++++++++++++++++++++++++++++++ src/domtool.cm | 3 +++ src/env.sig | 3 +++ src/env.sml | 4 ++++ src/tycheck.sml | 22 +++++++++++++++++----- tests/base.dtl | 11 +++++++++++ 7 files changed, 92 insertions(+), 5 deletions(-) create mode 100644 src/baseTypes.sig create mode 100644 src/baseTypes.sml create mode 100644 tests/base.dtl diff --git a/src/baseTypes.sig b/src/baseTypes.sig new file mode 100644 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 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 --- 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 --- 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 --- 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 --- 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 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" -- 2.20.1