******************** * * * D E M O F I L E * * * * S n a k e v1.1 * * * ******************** This file contains many (non)trivial and tricky examples that can be runned immediately in the interpreter. Hoping you enjoy. For any comment please drop me a message. Luigi.Liquori@inria.fr as Constants e.g. a b x y foo2 as Constants with HOLE inside e.g. A B X Y FOO2 \ as Antiexpression e.g. \a \X \(X->X 3) \ as Guarded Costants with HOLE e.g. X\a X\Y X\(a->a b) ;; as the Symbol of Top Level e.g. 3;; , as the Symbol of Structures e.g. (3,X,foo) -> as the Symbol of Rule e.g. X->X ->| as the Symbol of Resultless Rule e.g. X->| as the Symbol of Rule Application e.g.(X->X 4) ^ as the Symbol of Pointer e.g. ^X ! as the Symbol of Access Pointers e.g. !X <- as Assign to e.g. X<-0 [ | ...| ] define a Term Rewriting System ; Eval first , and then <-? ?-> Conditional -) Declare Exception + Handler (- Raise Exception = bind to e.g. X = 0 $ to Switch Theory (Noeffect vs Syntactical) # to Clean Namespace @ to Exit Snake Before the End of the Summer .... The First Ascii-oriented White Paper on Snake Snake >> ~~> W h i t e ~ S n a k e.pdf <~~ *** Heating *** foo;; FOO;; (foo,FOO);; (pair foo doo);; (foo -> doo foo);; (foo -> doo doo);; (FOO -> FOO doo);; ((foo->foo,foo->doo) foo);; _The Rho-ationale: Pattern Matching is hexaustive_ _In contrast with the ML vision that is selective ** Breacking the hole of a Constant *** X;; X = 3;; X;; #;; *** Your first TERM REWRITING SYSTEM *** [PLUS = ((0,N) -> N, ((succ N),M) -> (succ (PLUS (N,M))))];; ZERO = 0;; ONE = (succ 0);; TWO = (succ ONE);; THREE = (succ TWO);; (PLUS (THREE,THREE));; *** About alpha conversion *** (VAR -> VAR -> VAR 2 2);; (VAR -> VAR -> VAR 2 3);; _The rationale is: no REAL variables no REAL alpha bureaucracy _ *** If-then-else *** ELSE <-? COND ?-> THEN (PLUS (TWO,TWO)) <-? true ?-> (PLUS (THREE,THREE));; (PLUS (TWO,TWO)) <-? false ?-> (PLUS (THREE,THREE));; *** Imperative Features *** ^X;; !^X;; (^X -> X ^3);; _The rationale is : ! is just SUGAR_ ** YOUR FIRST ASSIGNMENT ** ((LOC,VAL) -> (LOC<-VAL;!LOC) (^dummy,4));; *** Swapping Two Variables *** SWAP = ((X,Y) -> ((AUX -> (AUX<-!X ; X<-!Y ; Y<-!AUX ; (!X,!Y))) (^0)));; (SWAP (^4 , ^5));; *** Your second term rewriting system: Negation Normal Form *** [NNF = ( p -> p, q -> q, (not (not X)) -> (NNF X), (not (or (X,Y))) -> (and ((not (NNF X)),(not (NNF Y)))), (not (and (X,Y))) -> (or ((not (NNF X)),(not (NNF Y)))), (and (X,Y)) -> (and ((NNF X),(NNF Y))), (or (X,Y)) -> (or ((NNF X),(NNF Y))))];; PHI = (and ((not (and (p,q))),(not (and (p,q)))));; (NNF PHI);; ************** * * Peano's Toys * ************** ZERO = 0;; ONE = (succ 0);; TWO = (succ ONE);; THREE = (succ TWO);; FOUR = (succ THREE);; FIVE = (succ FOUR);; SIX = (succ FIVE);; SEVEN = (succ SIX);; EIGHT = (succ SEVEN);; NINE = (succ EIGHT);; TEN = (succ NINE);; TENONE = (succ TEN);; TENTWO = (succ TENONE);; TENTHREE = (succ TENTWO);; TENFOUR = (succ TENTHREE);; TENFIVE = (succ TENFOUR);; TENSIX = (succ TENFIVE);; TENSEVEN = (succ TENSIX);; TENEIGHT = (succ TENSEVEN);; TENNINE = (succ TENEIGHT);; TWE = (succ TENNINE);; *** Multiplication (use Plus) *** Your first composite term rewriting system (N.B. note the introduction of "|" as a TRS separator) [PLUS = ((0,N) -> N, ((succ N),M) -> (succ (PLUS (N,M)))) | MULT = ((0,M) -> 0, ((succ 0),M) -> M, ((succ N\0),M) -> (PLUS (M,(MULT (N,M)))))];; (MULT (FIVE,FIVE));; *** Fibonacci (use Plus) *** [PLUS = ((0,N) -> N, ((succ N),M) -> (succ (PLUS (N,M)))) | FIB = (0 -> (succ 0) , (succ 0) -> (succ 0) , (succ (succ X)) -> (PLUS ((FIB (succ X)),(FIB X))))];; (FIB TWE);; *** Power (use Plus and Mult ) *** [PLUS = ((0,N) -> N, ((succ N),M) -> (succ (PLUS (N,M)))) | MULT = ((0,M) -> 0, ((succ 0),M) -> M, ((succ N\0),M) -> (PLUS (M,(MULT (N,M))))) | POW = ((N,0) -> (succ 0), (N,(succ M)) -> (MULT (N,(POW (N,M)))))];; (POW (TWO,TEN));; *** Ackermann *** [ACK = ((0,N) -> (succ N), ((succ M),0) -> (ACK (M,(succ 0))), ((succ M),(succ N)) -> (ACK (M,(ACK ((succ M),N)))))];; (ACK (THREE,FIVE));; *** Findn : Find the nth Element in a list *** LIST = (gigi,claude,maribel,bonny,elvis,klyde,nil);; [FINDN = ((0,nil) -> fail, ((succ N),nil) -> fail, ((succ 0),(X,Y)) -> X, ((succ N),(X,Y)) -> (FINDN (N,Y)))];; (FINDN (SIX,LIST));; *** Killanat: *** LIST = (ONE,TWO,THREE,FOUR,TEN,nil);; [EQNAT = ((0,0) -> true, (0,(succ X)) -> false, ((succ X),0) -> false, ((succ X),(succ Y)) -> (EQNAT (X,Y))) | KILL = ((ELM,(nil)) -> (nil), (ELM,(E,X)) -> ((E,(KILL (ELM,(X)))) <-? (EQNAT (ELM,E)) ?-> (KILL (ELM,(X)))))];; (KILL (TEN,LIST));; *** Antipatterns and antivariables *** \foo = match with everything but foo \\foo = foo (double negation) antivariables \X = match only with an antipattern, otherwise it block the computation. \\X = X double negation \foo;; \\foo;; (\foo ->ok doo);; (\foo ->ok \foo);; (\BLACKHOLE ->never any);; X\0;; X=0;; X\0;; Antipatterns @ work : Boolean Operators AND = ( (true, true) -> true, \(true,true) -> false);; OR = ( (false,false) -> false, \(false,false) -> true);; ( (f X \X) -> X (f 2 3));; # 2 ( (f \X X) -> X (f 2 3));; # 3 ( (f X Y\X) -> X (f 2 3));; # 2 ( (f Y\X X) -> X (f 2 3));; # 2 ( \(X, X) -> ok (true, false));; ((f (\g X)) ->ok (f (g a)));; *** Guarded variables *** X\a = X such that is not equal to a X\Y = X such that is not equal to Y (if Y is bound before) VAR\(2->3 4);; (VAR\foo->VAR foo);; (VAR\foo->VAR doo);; (GUARD->(VAR\GUARD ->true 3) 3);; (GUARD->(VAR\GUARD ->true 3) 4);; ((f \X X) -> OK (f 2 2));; *** cool: Patterns can be linear and checked during matching phase under \equiv (as in the Huet 76 Thesis) *** ((f Z Z) -> Z (f a a));; ((f Z Z) -> Z (f a b));; *** cool: Pattern can be evaluated!!! *** ((V->V foo) -> doo foo);; ((MULT (FOUR,FIVE)) -> yeahsnakeisgood (MULT (TWO,TEN)));; ((MULT (X,TEN)) -> yeahsnakeisverygood (MULT (FOUR,FIVE)));; *** Extra cool : pattern can be FUNCTIONS!! *** ((V->V) ->yeahverygood (V->V));; X=0;Y=0;; ((X->X) ->storegood (Y->Y));; Y=1;; ((X->X) ->matchgood (Y->Y));; *** Fastest Pair selection in Lambda Calculus * van Oostroom 90 (BOOL->(BOOL FIRST SECOND));; ((BOOL->(BOOL FIRST SECOND)) -> FIRST (B->(B foo doo)));; ******************************* * * * Small XML-oriented Galleria * * * ******************************* *** Some list of friends and the DB *** ZERO = 0;; ONE = (succ 0);; TWO = (succ ONE);; THREE= (succ TWO);; FOUR = (succ THREE);; ME = (person ((first luigi) ,(nat it) ,(cat ONE)));; YOU = (person ((first jessica) ,(nat usa),(cat TWO)));; SHE = (person ((first therese) ,(nat fr) ,(cat ZERO)));; HIM = (person ((first claude) ,(nat fr) ,(cat THREE)));; HER = (person ((first uma) ,(nat usa),(cat FOUR)));; BIG = (person ((first sidarth) ,(nat ind),(cat TWO)));; HEAD = (person ((first moreno) ,(nat it) ,(cat TWO)));; BOSS = (person ((first furio) ,(nat it) ,(cat THREE)));; JEFE = (person ((first maribel) ,(nat arg),(cat ZERO)));; GURU = (person ((first salvador),(nat es) ,(cat TWO)));; DB = (group (ME,YOU,SHE,HIM,HER,BIG,HEAD,JEFE,BOSS,GURU,nil));; *** FINDN : Find the nth Element in a xml catalogue *** [FINDN = ((0,nil) -> fail, ((succ N),(group nil)) -> fail, ((succ 0),(group (A,B))) -> A, ((succ N),(group (A,B))) -> (FINDN (N,(group B))))];; (FINDN (THREE,DB));; *** SELECTIT: Select in a DB the all the items of "it" nationality *** [SELECTIT = ((group (nil)) -> (nil), (group ((person (X, (nat it) ,V)),Z)) -> ((person (X,(nat it) ,V)),(SELECTIT (group Z))), (group ((person (X,\(nat it) ,V)),Z)) -> (SELECTIT (group Z)))];; (SELECTIT DB);; *** DROPIT: Kill in a DB the all the items of "it" nationality *** [DROPIT =((group (nil)) -> (nil), (group ((person (X, (nat it),V)),Z)) -> (DROPIT (group Z)), (group ((person (X,Y\(nat it),V)),Z)) -> ((person (X,Y,V)),(DROPIT (group Z))))];; (DROPIT DB);; *** Right-widow rewriting rules Pattern ->| This rule fire, an "effect" (e.g. a I/O operation) is performed. All effects are treated as pattern-matching failures with the NoEffect theory. Examples: (V->| foo);; ******************************** * * * One HTML-oriented RHOUTINE * * * ******************************* LINK = rhodotinriadotfr;; INDEX = L -> (ohyeahpleaseindex L);; LOAD = (gigdotinriadotfr -> GIG, cladotinriadotfr -> CLA, hordotinriadotfr -> HOR, rhodotinriadotfr -> RHO);; GIG = (html ((markup ((markup pc),(markup pc))),(markup ((markup pc),(href rhodotinriadotfr)))));; HOR = (html ((markup (href gigdotinriadotfr),(markup pc)),(markup (markup pc),(markup pc))));; CLA = (html ((markup (markup pc),(markup pc)),(markup (href hordotinriadotfr),(markup pc))));; DCM = (html ((markup (markup pc),(href cladotinriadotfr)),(markup (markup pc),(markup pc))));; *** FINDLINK: find in a web page (recursively) a LINK*** [FINDLINK = (html BODY) -> (FIND BODY) | FIND = ( pc ->|, (markup X) -> (FIND X) , (href LINK) -> (INDEX LINK), (href L\LINK) -> (FINDLINK (LOAD L)), ((href LINK) ,BODY) -> (INDEX LINK), ((href L\LINK) ,BODY) -> ((FINDLINK (LOAD L)),(FIND BODY)), ((markup X) ,BODY) -> ((FIND X) ,(FIND BODY))) ];; (FINDLINK DCM);; [FINDALINK = (html BODY) -> (FIND BODY) | FIND = ( pc ->|, (markup X) -> (FIND X) , (href LINK) -> (INDEX LINK), (href L\LINK) -> (FINDALINK (LOAD L)), (X,BODY) -> ((FIND X) ,(FIND BODY))) ];; (FINDALINK DCM);; *** Exceptions !!! Two simple constructions: Handler-Function :-) Protected-Expression and (-: raise-value as a result of evaluating a Protected expression....x *** REVERSE TWICE BUT ZERO *** LIST = (1,2,3,4,5,7,8,9,10,nil);; LIST = (1,2,3,0,5,7,8,9,10,nil);; [HAND = P -> (founda P) | REV = ( (nil,R) -> R, ((X\0,T),R) -> (REV (T,(X,R))), ((0,T),R) -> (-: 0)];; HAND :-) (REV ((REV (LIST,(nil))),(nil)));; HAND :-) (REV (LIST,(nil)));; ( (f Y X\Y) -> nonlin (f 3 3));; LIST = (1,2,3,4,5,0,7,8,9,10,nil);; [HAND = P -> (REV (P,(nil))) | REV = ( (nil,R) -> R, ((X\0,T),R) -> (REV (T,(X,R))), ((0,T),R) -> (-: R)];; HAND :-) (REV ((REV (LIST,(nil))),(nil)));; [REVERSE = ( (nil,R) -> R, ((0,T),R) -> (REVERSE (R,(nil))), ((X\0,T),R) -> (REVERSE (T,(X,R))))];; (REVERSE ((REVERSE (LIST,(nil))),(nil)));; **** GRAN FINALE: OPTIONAL TYPE SYSTEMS **** A type (inference) system can be used on demand by the user. DATA = 0;; PROGRAM = N ->(succ N);; INFER = (P,D) -> false;; HAND = X -> (doesnotcheck (X dummy));; HAND :-) (-: (PROGRAM,DATA) <-? (INFER (PROGRAM,DATA)) ?-> (ihaverun (PROGRAM DATA));; ***WHAT'S NEXT BEFORE SUMMER (V2.0) - IMPLEMENT SECOND ORDER TYPE INFERENCE (FOLLOWING WRLA-04) - GENERAL LIBRARY (ala HASKELL PRELUDE.SNK) - OPEN TO OTHER LANGUAGES (WRAPPERS) (FUN~ARG) *FUN.py is a python function* (FUN#ARG) *FUN.cs is a (compiled) c# function* (FUN$ARG) *FUN.java/class is a java standalone function or just javascript* (PATT ~> BODY) *BODY.py is a python function* (PATT #> BODY) *BODY.cs is a (compiled) c# function* (PATT $> BODY) *BODY.class is a (compiled) java standalone function (or maybe javascript)* ======================== Hoping you enjoyed Luigi Liquori Copyright INRIA 2005 ======================== ----------------------------------------------------------- | /^\/^\ | | _|__| O| | | \/ /~ \_/ \ | | \____|__________/ \ | | \_______ \ | | `\ \ \ | | | | \ | | / / \ | | / / \\ | | / / \ \ | | / / \ \ | | / / _----_ \ \ | | / / _-~ ~-_ | | | | ( ( _-~ _--_ ~-_ _/ | | | \ ~-____-~ _-~ ~-_ ~-_-~ / | | ~-_ _-~ ~-_ _-~ | | ~--______-~ ~-___-~ | | | | S N A K E | -------------------------------------------------------------