Re: Asserting a fact when triggering a rule

On 19/12/2013, at 10:15 PM, Baltasar García Perez-Schofield wrote:

> 	My objective is to infer types from an AST.


The usual way to do that is to create your AST with slots
for the types, leaving them as unbound variables in your
syntax pass, and then walk over the tree filling them in.


:- type stmt
   ---> begin(list(var_decl), list(stmt))
      ; if(expr, stmt, stmt)
      ; while(expr, stmt)
      ; assign(var, expr)
      .
:- type var
   ---> var(atom, type)
      .
:- type expr
   ---> var(atom, type)
      ; num(number, type)
      ; plus(expr, type, expr)
      ; less(expr, type, expr)
      ; and(expr, type, expr)
      .
:- type var_decl
   ---> var(atom, type)
      .
:- type (type)
   ---> bool
      ; int
      .
check(Program) :-
    check_stmt(Program, []).

check_stmt(begin(Decls, Stmts), Env) :-
    check_stmt_list(Stmts, [Decls|Env]).
check_stmt(if(Expr, T, F), Env) :-
    check_expr(Expr, bool, Env),
    check_stmt(T, Env),
    check_stmt(F, Env).
check_stmt(while(Expr, Body), Env) :-
    check_expr(Expr, bool, Env),
    check_stmt(Body, Env).
check_stmt(assign(Var, Expr), Env) :-
    check_var(Var, Type, Env),
    check_expr(Expr, Type, Env).

check_var(var(V,T), T, Env) :-
    member(Level, Env),
    member(var(V,X), Level),
    !,
    T = X.

check_expr(var(V,T), T, Env) :-
    check_var(var(V,T), T, Env).
check_expr(num(_,T), T, _).
check_expr(plus(E1,int,E2), int, Env) :-
    check_expr(E1, int, Env),
    check_expr(E2, int, Env).
check_expr(less(E1,bool,E2), bool, Env) :-
    check_expr(E1, int, Env),
    check_expr(E2, int, Env).
check_expr(and(E1,bool,E2), bool, Env) :-
    check_expr(E1, bool, Env),
    check_expr(E2, bool, Env).

Note that this can handle surface syntax like
	begin var x; x := 1+1 end
and infer the types.

Obviously this is a bit oversimplified;
you can make it table-driven, and you can (and should)
do something a bit cleverer like

	unify_types(T, T) :- !.
	unify_types(Actual, Expected, _) :-
	    ... write an error message that Actual
	    ... and Expected don't match.

and use e.g.

	check_expr(var(V,T1), T, Env) :-
	    check_var(var(V,T1)),
	    unify_types(T1, T).
	check_expr(num(_,T1), T, Env) :-
	    unify_types(T1, T).


> The rule of concern is of the form:
> 
> 	% VBLE = EXPR2
> 	isType( EXPR1, TYPE ) :-
> 			node( EXPR1, asg, VBLE, EXPR2 ),
>                        isType( EXPR2, TYPE ).

There's your problem right there.
You have a node/4 predicate instead of
using a tree in which variables can be shared.

By the way, I would normally expect "isType(X, Y)" to mean
"X is a type" and then I'd be puzzled about Y.  Wouldn't
"node_type(Node, Type)" be better?

> 	The problem is that this rule gives you the type of the node, as expected, but not the type of the variable (VBLE).

Indeed, the rule as shown to us doesn't do anything whatever
with the variable.

Note that

	expr_type(asg(VBLE, Expr), Type) :-
	    vble_type(VBLE, Type),
	    expr_type(Expr, Type).

would not only make your life easier, it would make your
program a whole lot faster (and take less memory).

Why on earth are you representing an AST as a bunch of
facts instead of a simple tree?