; *** MONICA *** ; ; This program implements MONICA, Miranda's little sister, a strongly typed ; lazy functional language. You invoke the interpreter by asking ? monica. ; The prompt >> asks for an expression to be evaluated. ; Being an interpreter written in an interpreted language it is ; of course extremely slow, but it can give you an idea of what such ; languages are like. ; there are two basic types: num and truval, and one type constructor list: ; 77 has type num, false has type truval and [66] type list(num). ; function application is written as f:X ; plus:8:8 has type num, plus:8 has type num -> num ("currying") ,plus has type ; num -> num -> num. X+Y is shorthand for plus:X:Y. ; Examples: ; >> 7*7. gives: TYPE: num, VALUE: 49. ; >> X*X where X eq 7. gives the same result. ; >> define [fac:0 => 1, fac:N => N*fac:(N-1)]. ; defines fac: num -> num, the well-known factorial function: ; >> fac:4. gives TYPE: num, VALUE: 24. ; >> fac:[4]. does nothing (type error) ; #Goal has type truval. It is evaluated by invoking the Prolog goal Goal and ; gives true or false depending on success or failure. Similarly #[Goal|Goals]. ; >>#[ink(Red), cls] where Red eq 2. gives TYPE: truval, VALUE: true. ; define [map:F:[] => [], map:F:[X|Xs] => [F:X|map:F:Xs]]. ; defines map: (Alpha -> Alpha') -> list (Alpha) -> list (Alpha') ; (Alpha and Alpha' are type variables, map has a 'polymorphic type') ; >> map:(plus:8):[1,2,3] gives TYPE: list(num), VALUE: [9|map:(plus:8):[2,3]] ; because of Monica's lazy evaluation (only the first list element is evaluated). ; define [from:N => [N|from:(N+1)], define [num => from:0]. defines ; an infinite list [1,2,3,4,5,......] ; User-defined types are also possible : ; >> # typedef [ ; empty : bintree(Alpha) ; node : (Alpha -> bintree(Alpha) -> bintree(Alpha) -> bintree (Alpha) ; ]. ? seeing (ThisProgram), assert ([anew, new(ThisProgram)]). ? op (90, ":"), op (1, "->"), op (101,"lambda"), op (11, "if"). ? op (12, "then"), op (13, "else"), op (15, "#"), op (20, "eq"). ? op (7, "where"), op (2, "and"), op (101, "define"). ? op (101, "forget"), op (101, "typedef"). X and Y <- X,Y. ; ***************************** THE INTERPRETER **************************** monica <- ; the main interpreter loop repeat, ; repeat write(">>"), ; ask the user for a term .... read (T), ; ..... read it into T >> T, ; >>T type-checks and evaluates T T = 0, ; until T was 0 !, fail. ; in the following two definitions the following trick is used: if you want to ; know whether a goal G succeeds but you want to prevent its variables from ; becoming bound, you call 'not not G' instead of G itself. ; this is necessary here because 'type (Term, type (ItsType))' uses ; Term's variables to store their inferred types. Try for example: ; ? Term = [plus:N:8], type (Term, ItsType). >> X <- translate (X,X'), !, ; translate X into unique X' not not ( ; solve the following query: type (X', type (T)) and ; find X' most general type write ("TYPE: ") and ; write it write (T) ), ; forget substitutions made in X' eval (X', Value), ; find X's value write (" VALUE: "), write (Value), nl, !. ; at most one solution. ; ***************************** DEFINING CONSTANTS ************************* define Def <- ; define a new constant translate (Def, Def'), ; translate definition transform (Def', [ F => NewDef]), ; 'normalize' it not not ( assert ([type (F, type ( _ ))]) and ; assert 'any type possible' type (NewDef, type (TypF)) and ; find most general type push (TypF) and ; remember it retract ([type(F, type ( _ ))]) ; retract 'any type possible' ), ; forget substitutions in F assert ([F >> NewDef, true]), ; store definition ... pop (TypF), ; ... recall type .... assert ([type (F, type (TypF)),true]), ; ...... store it. writeln ([" ", F, ": ", TypF]), ; announce birth of F !. ; only one definition. forget Const <- ; forget a constant retract ([type (Const, _ ), true]), ; forget its type retract ([Const >> _ , true]). ; forget definition typedef ([Def|Defs]) <- Def = NewConst : ItsType, atom (NewConst), assert ([type (NewConst, type (ItsType)), true]), writeln([" ",NewConst,": ", ItsType]), typedef (Defs). typedef ([]). ;***************************** EVALUATION ************************************ eval (T, Value) <- T >> T', !, eval (T', Value). eval (T,T). lambda [X => T]:X >> T <- !. lambda List:Y >> T <- eval (Y,X), member (X => T, List). cond:C:X:Y >> Y' <- eval (C, false), eval (Y,Y'). cond:C:X:Y >> X' <- eval (X,X'). en:X:Y >> true <- eval (X,true), eval (Y,true). en:X:Y >> false. niet:X >> true <- eval (X, false). niet:X >> false. plus:K:L >> M <- eval (K, Kval), eval (L, Lval), M := Kval + Lval. min:K:L >> M <- eval (K, Kval), eval (L, Lval), M := Kval - Lval. times:K:L >> M <- eval (K, Kval), eval (L, Lval), M := Kval * Lval. less:K:L >> true <- eval (K, Kval), eval (L, Lval), K < L. less:K:L >> false. is:X:Y >> true <- eval (X,X'),eval (Y,Y'), X' = Y'. is:X:Y >> false. # [Goal|Goals] >> true <- # Goal >> true, # Goals >> true. # [] >> true. # Goal >> true <- Goal. # Goal >> false. define D >> true <- define D, !. define D >> false. X:Y >> X':Y <- X >> X'. [X|Y] >> [X'|Y] <- X >> X'. ;**************************** TYPE INFERENCE ******************************* type (type(T), type(T)) <- T = Alpha, !. type (plus , type (num -> num -> num)). type (min , type (num -> num -> num)). type (times, type (num -> num -> num)). type (less, type (num -> num -> truval)). type (cond, type (truval -> Alpha -> Alpha -> Alpha)). type (en, type (truval -> truval -> truval)). type (niet, type (truval -> truval)). type (true, type (truval)). type (false, type (truval)). type (is, type (Alpha -> Alpha -> truval)). type (X : Y, type(Beta)) <- type (X, type (Alpha -> Beta)), type (Y, type (Alpha)). type (lambda [X => T|Rest], type(Alpha -> Beta) ) <- type (X, type(Alpha)), type (T, type(Beta)), type (lambda Rest, type (Alpha -> Beta)). type (lambda [], type (Alpha -> Beta)). type (X, type(num)) <- integer (X). type ([X|Xs], type(list (Alpha))) <- type (X, type(Alpha)), type (Xs, type(list (Alpha))). type ([], type(list (Alpha))). type (# Goal, type(truval)). type (define D, type(truval)). ;************************** TRANSLATION ************************************** translate (X,X) <- var (X),!. translate (X+Y,plus:X':Y') <- translate ([X,Y],[X',Y']). translate (X-Y,min:X':Y') <- translate ([X,Y],[X',Y']). translate (X*Y,times:X':Y') <- translate ([X,Y],[X',Y']). translate (X eq Y,is:X':Y') <- translate ([X,Y],[X',Y']). translate (X < Y,less:X':Y') <- translate ([X,Y],[X',Y']). translate (if C then X else Y, cond:C':X':Y') <- translate([C,X,Y],[C',X',Y']). translate (X and Y, en:X':Y') <- translate ([X,Y],[X',Y']). translate (not X, niet:X') <- translate (X,X'). translate (X:Y, X':Y') <- translate ([X,Y],[X',Y']). translate (X => Y, X' => Y') <- translate ([X,Y],[X',Y']). translate ([X|Xs], [X'|Xs']) <- translate (X,X'), translate (Xs, Xs'). translate ([],[]). translate (lambda List, lambda List') <- translate (List, List'). translate (X => T, X' => T') <- translate ([X,T],[X',T']), !. translate (T where X eq S, lambda [X' => T']:S') <- translate ([T,X,S],[T',X',S']). translate (#G,#G). translate (X,X) <- atomic (X),!. translate (define D, define D') <- translate (D, D'). push (T) <- asserta ([$stack(T)]). pop (T) <- retract ([$stack(T)]). collect ([F:X => Y| Rest_def], T, Rest, F' => lambda Body) <- F == F', !, append (Body, [X => Y], New_body), collect (Rest_def, T, Rest, F => lambda New_body). collect (R, Def, R, Def). group (Def, [T|Ts]) <- Def = [F:X => Y| Rest_def], collect (Def, T, Rest, F => lambda []), group (Rest, Ts). group ([],[]). transform (Def, T) <- group (Def, NewDef), transform (NewDef, T). transform (T,T) <- !. ; exactly one solution test (X) <- translate (X,X'), transform (X', X''), writeln ([X'']),!.