From 75d4c2d6fb7996625d062f5949ceb2e66c0a70ab Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 15 Dec 2007 19:52:21 +0000 Subject: [PATCH 1/1] Add if..then..else --- src/ast.sml | 2 ++ src/domtool.grm | 2 ++ src/domtool.lex | 4 ++++ src/order.sml | 3 +++ src/printFn.sml | 3 +++ src/reduce.sml | 16 ++++++++++++++++ src/tycheck.sml | 27 +++++++++++++++++++++++++++ 7 files changed, 57 insertions(+) diff --git a/src/ast.sml b/src/ast.sml index ead8531..6668b4b 100644 --- a/src/ast.sml +++ b/src/ast.sml @@ -91,6 +91,8 @@ datatype exp' = (* Apply a TNested to an action *) | EALam of string * pred * exp (* Abstraction for building TNested values *) + | EIf of exp * exp * exp + (* If..then..else *) withtype exp = exp' * position datatype decl' = diff --git a/src/domtool.grm b/src/domtool.grm index 532dad9..c9cd837 100644 --- a/src/domtool.grm +++ b/src/domtool.grm @@ -32,6 +32,7 @@ open Ast | COLON | CARET | BANG | AND | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | BSLASH | BSLASHBSLASH | SEMI | LET | IN | BEGIN | END + | IF | THEN | ELSE | ROOT | EXTERN | TYPE | VAL | WITH | WHERE | CONTEXT @@ -128,6 +129,7 @@ exp : apps (apps) | exp SEMI (exp) | SYMBOL LARROW CSYMBOL SEMI exp (EGet (SYMBOL, NONE, CSYMBOL, exp), (SYMBOLleft, expright)) | SYMBOL COLON typ LARROW CSYMBOL SEMI exp (EGet (SYMBOL, SOME typ, CSYMBOL, exp), (SYMBOLleft, expright)) + | IF exp THEN exp ELSE exp (EIf (exp1, exp2, exp3), (IFleft, exp3right)) apps : term (term) | apps term (EApp (apps, term), (appsleft, termright)) diff --git a/src/domtool.lex b/src/domtool.lex index 99449ca..dd4391b 100644 --- a/src/domtool.lex +++ b/src/domtool.lex @@ -130,6 +130,10 @@ lineComment = #[^\n]*\n; "with" => (Tokens.WITH (yypos, yypos + size yytext)); "where" => (Tokens.WHERE (yypos, yypos + size yytext)); + "if" => (Tokens.IF (yypos, yypos + size yytext)); + "then" => (Tokens.THEN (yypos, yypos + size yytext)); + "else" => (Tokens.ELSE (yypos, yypos + size yytext)); + "extern" => (Tokens.EXTERN (yypos, yypos + size yytext)); "type" => (Tokens.TYPE (yypos, yypos + size yytext)); "val" => (Tokens.VAL (yypos, yypos + size yytext)); diff --git a/src/order.sml b/src/order.sml index 08db062..599c62a 100644 --- a/src/order.sml +++ b/src/order.sml @@ -120,6 +120,9 @@ fun expNeeded G (e, loc) = empty es | ELocal (e1, e2) => unionCTE (expNeeded G e1, expNeeded G e2) | EWith (e1, e2) => unionCTE (expNeeded G e1, expNeeded G e2) + | EIf (e1, e2, e3) => unionCTE (expNeeded G e1, + unionCTE (expNeeded G e2, + expNeeded G e3)) fun declNeeded G (d, _, _) = case d of diff --git a/src/printFn.sml b/src/printFn.sml index 05172da..decc2bc 100644 --- a/src/printFn.sml +++ b/src/printFn.sml @@ -132,6 +132,9 @@ fun p_exp' pn (e, _) = keyword "end"] | EWith (e1, (ESkip, _)) => dBox [p_exp e1, space 1, keyword "with", space 1, keyword "end"] | EWith (e1, e2) => dBox [p_exp e1, space 1, keyword "with", p_exp e2, space 1, keyword "end"] + | EIf (e1, e2, e3) => dBox [keyword "if", space 1, p_exp e1, + space 1, keyword "then", space 1, p_exp e2, + space 1, keyword "else", space 1, p_exp e2] and p_exp e = p_exp' false e fun p_decl d = diff --git a/src/reduce.sml b/src/reduce.sml index 525d713..9e538d6 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -42,6 +42,8 @@ fun freeIn x (b, _) = | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2 | EALam (x', _, b') => x <> x' andalso freeIn x b' + | EIf (e1, e2, e3) => freeIn x e1 orelse freeIn x e2 orelse freeIn x e3 + local val freshCount = ref 0 in @@ -106,6 +108,8 @@ fun subst x e (bAll as (b, loc)) = else (EALam (x', p, subst x e b'), loc) + | EIf (b1, b2, b3) => (EIf (subst x e b1, subst x e b2, subst x e b3), loc) + fun findPrim (e, _) = case e of EApp (f, x) => @@ -179,4 +183,16 @@ fun reduceExp G (eAll as (e, loc)) = (EALam (x, p, reduceExp G' e), loc) end + | EIf (e1, e2, e3) => + let + val e1' = reduceExp G e1 + fun e2' () = reduceExp G e2 + fun e3' () = reduceExp G e3 + in + case e1' of + (EVar "true", _) => e2' () + | (EVar "false", _) => e3' () + | _ => (EIf (e1', e2' (), e3' ()), loc) + end + end diff --git a/src/tycheck.sml b/src/tycheck.sml index def1463..f68100f 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -571,6 +571,33 @@ fun checkExp G (eAll as (e, loc)) = | ESkip => (TAction ((CPrefix (CRoot, loc), loc), SM.empty, SM.empty), loc) + + | EIf (e1, e2, e3) => + let + val t = (newUnif (), loc) + + val t1 = checkExp G e1 + val t2 = checkExp G e2 + val t3 = checkExp G e3 + val bool = (TBase "bool", loc) + in + (subTyp (t1, bool)) + handle Unify ue => + dte (WrongType ("\"If\" test", + e1, + t1, + bool, + SOME ue)); + subTyp (t2, t); + (subTyp (t3, t)) + handle Unify ue => + dte (WrongType ("\"Else\" case", + eAll, + t3, + t2, + SOME ue)); + t + end end exception Ununif -- 2.20.1