module examples::fun::Checker

rascal-0.34.0

typepal-0.8.10

Usage

import examples::fun::Checker;

Source code

http://github.com/usethesource/typepal/src/examples/fun/Checker.rsc

Dependencies

import examples::fun::Syntax;
extend analysis::typepal::TypePal;

data AType

data AType  
     = boolType()
     | intType()
     | strType()
     | functionType(AType from, AType to)
     ;

function prettyAType

str prettyAType(boolType()) = "bool";

str prettyAType(intType()) = "int";

str prettyAType(strType()) = "str";

str prettyAType(functionType(AType from, AType to)) = "fun <prettyAType(from)> -\> <prettyAType(to)>";

function collect

void collect(current: (Type) `bool`, Collector c){
    c.fact(current, boolType());
}

void collect(current: (Type) `int`, Collector c){
    c.fact(current, intType());
}

void collect(current: (Type) `str`, Collector c){
    c.fact(current, strType());
}

void collect(current: (Type) `<Type from> -\> <Type to>`, Collector c){
    c.calculate("function type", current, [from, to],
        AType(Solver s){ return functionType(s.getType(from), s.getType(to)); });
    collect(from, to, c);
}

void collect(current: (Expression) `fun <Id name> : <Type tp> { <Expression body> }`, Collector c) {   
     c.enterScope(current);
        c.define("<name>", variableId(), name, defType(tp));
        c.calculate("function declaration", current, [body], 
            AType(Solver s){ 
                s.requireEqual(tp, body, error(tp, "Declared type %t should be equal to type of body %t", tp, body));
                return functionType(s.getType(tp), s.getType(body)); 
            });
        collect(tp, body, c);
     c.leaveScope(current);
}

void collect(current: (Expression) `let <Id name> : <Type tp> = <Expression exp1> in <Expression exp2> end`, Collector c) {  
     c.enterScope(current);
         c.define("<name>", variableId(), name, defType(tp));
         c.calculate("let", current, [exp2], AType(Solver s) { return s.getType(exp2); } );
         collect(tp, exp1, exp2, c);  
     c.leaveScope(current);
}

void collect(current: (Expression) `<Id name>`,  Collector c){
     c.use(name, {variableId()});
}

void collect(current: (Expression) `<Expression exp1> (<Expression exp2>)`, Collector c) { 
     c.calculate("application", current, [exp1, exp2],
         AType (Solver s) {  
            if(functionType(tau1, tau2) := s.getType(exp1)){
                  s.requireEqual(exp2, tau1, error(exp2, "Incorrect type of actual parameter"));
                  return tau2;
               } else {
                  s.report(error(exp1, "Function type expected"));
                  return intType();
               }
        });
     collect(exp1, exp2, c);
}

void collect(current: (Expression) `if <Expression cond> then <Expression thenPart> else <Expression elsePart> fi`, Collector c){
     c.calculate("if", current, [cond, thenPart, elsePart],
        AType (Solver s) { 
            s.requireEqual(cond, boolType(), error(cond, "Condition should have type `bool`, found %t", cond));
            s.requireEqual(thenPart, elsePart, error(current, "thenPart and elsePart should have same type"));
            return s.getType(thenPart);
        }); 
      collect(cond, thenPart, elsePart, c);
}

void collect(current: (Expression) `<Expression lhs> + <Expression rhs>`, Collector c){
     c.calculate("addition", current, [lhs, rhs],
        AType (Solver s) { 
            switch(<s.getType(lhs), s.getType(rhs)>){
                case <intType(), intType()>: return intType();
                case <strType(), strType()>: return strType();
                default: {
                    s.report(error(current, "Arguments of type %t and %t not allowed for `+`", lhs, rhs));
                    return intType();
                  }
            }
        });
      collect(lhs, rhs, c);
}

void collect(current: (Expression) `<Expression lhs> && <Expression rhs>`, Collector c){
     c.calculate("and", current, [lhs, rhs],
        AType (Solver s) { 
            s.requireEqual(lhs, boolType(), error(lhs, "Left argument of `&&` should have type `bool`, found %t", lhs));
            s.requireEqual(rhs, boolType(), error(rhs, "Right argument of `&&` should have type `bool`, found %t", rhs));
            return boolType();
        });
      collect(lhs, rhs, c);
}

void collect(current: (Expression) `( <Expression exp> )`, Collector c){
     c.fact(current, exp);
     collect(exp, c);
}

void collect(current: (Expression) `<Boolean boolcon>`, Collector c){
     c.fact(current, boolType());
}

void collect(current: (Expression) `<Integer intcon>`, Collector c){
     c.fact(current, intType());
}

void collect(current: (Expression) `<String strcon>`, Collector c){
     c.fact(current, strType());
}