RiSE4fun samples for FastList of built-in samples for the Fast in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Fasthttp://rise4fun.com/Fast/functionsfunctions//Constants and functions in Fast Const five : int := 5 Fun f (i:int) : int := (+ i 1) Const six : int := (f five) Fun f1 (i:int) (b:bool) : int := (if (and (= (f i) 3) b) 1 2) Alphabet A[i : int]{zero(0),one(1),two(2)} Public Trans t : A -> A { two(x,y) where (and (= (mod five (f i)) 1)) to (two [i] (t x) (t y)) | zero() where (and (>= six (f1 five true))) to (zero [(f i)]) } Print thttp://rise4fun.com/Fast/complementcomplement//Language complement Alphabet BTree[]{Zero(0),One(1),Two(2)} Public Lang q1 : BTree { Zero() | Two(x,y) given (q1 x) (q1 y) } //The language of all trees Public Lang tot : BTree { Zero() | One(x) | Two(x,y) } //Complement q1 Def complement_q1 : BTree := (complement q1) Print complement_q1 //Analysis Def c_complement_q1 : BTree := (complement complement_q1) //Show correctness Def unionq1cq1 : BTree := (union complement_q1 q1) //the union of q1 and its complement is the same as the language of all trees AssertTrue (eq_lang unionq1cq1 tot) http://rise4fun.com/Fast/treestrees//Example of trees usage //Normal tree Tree t_1 : A := (B [1.5] (Z [1.5]) (Z [1.4])) //Result of function appliction Tree t_2 : A := (apply t1 t_1) //Witness generation from langauge Tree t_3 : A := (get_witness l1) //Output Print t_1 Print t_2 Print t_3 //Language we use for restriction Public Lang l1 : A { Z() where (> r 1.0) | B(x,y) where (> r 1.0) given (l1 x) } //Transformation Public Trans t1 : A -> A { Z() where (< r 3.0) to (Z [(- r 0.5)]) | B(x,y) where (< r 3.0) to (B [(- r 0.5)] (t2 x) (t2 y)) } Trans t2 : A -> A { Z() where (< r 3.0) to (Z [(- r 0.5)]) | B(x,y) where (< r 3.0) to (B [(- r 0.5)] (t1 x) (t1 y)) } Alphabet A[r:real]{Z(0),B(2)}http://rise4fun.com/Fast/constantsconstants//Constants definitions in Fast //Enum definitions (enum types in Fast are required to start with a capital letter) Enum Color {red, blue, green} //Constants Const pi : real := 3.14159 Const piby4 : real := (/ pi 4.0) Const red : Color := Color.red Alphabet A[r:real, c:Color]{zero(0),one(1),two(2)} //Language where every leaf is labeled with Color.red Lang l (a: A) { two(x,y) given (l x) (l y) | zero() where (= a.c Color.red) } //Example of transformation Public Trans t (a: A) : A { two(x,y) where (and (<= pi 3.4) (= a.c Color.red)) given (l x) (l y) to (two [(+ a.r 0.1), a.c] (t y) (t x)) | zero() to (zero [(+ piby4 5/2), a.c]) } // Output the transducer Print thttp://rise4fun.com/Fast/deforestationdeforestation//Auxiliary functions Fun even (x:int) : bool := (= (mod x 2) 0) Fun odd (x:int) : bool := (not (even x)) Fun inc (x:int) : int := (+ x 1) //Lists of integers Alphabet IntList[i:int]{nil(0),cons(1)} //Increments all the elements of the list by 1 Public Trans map_inc : IntList -> IntList { nil() to (nil [0]) | cons(x) to (cons [(inc i)] (map_inc x)) } //Removes all the odd elements from the list Public Trans filter_ev : IntList -> IntList { nil() to (nil [0]) | cons(x) where (odd i) to (filter_ev x) | cons(x) where (even i) to (cons [i] (filter_ev x)) } //Compose the two functions into a single one Def map_filt : IntList -> IntList := (compose map_inc filter_ev) Print "Single function equivalent to composition of map_inc and filter_ev" Print map_filthttp://rise4fun.com/Fast/preimagepreimage//Example of preimage computation Def preim : BT := (pre_image mapInc oddTree) AssertTrue (eq_lang evenTree preim) //Output the minimized language for the preimage Def p : BT := (minimize preim) Print p //Trees with even elements Lang evenTree : BT { Nil() where (even i) | Bin(l,r) where (even i) given (evenTree l) (evenTree r) } //Trees with odd elements Lang oddTree : BT { Nil() where (odd i) | Bin(l,r) where (odd i) given (oddTree l) (oddTree r) } //Increment every node in the tree by 1 Public Trans mapInc : BT -> BT { Nil() to (Nil [(+ i 1)]) | Bin(l,r) to (Bin [(+ i 1)] (mapInc l) (mapInc r)) } //Functions and alphabet Fun even (i:int) : bool := (= (mod i 2) 0) Fun odd (i:int) : bool := (not (even i)) Alphabet BT [i:int] {Nil(0),Bin(2)}http://rise4fun.com/Fast/equivalenceequivalence//Language equivalence Alphabet A[r:real]{Z(0),O(1),B(2)} //Language definitions Public Lang q1 : A { Z() where (> r 1.0) | O(x) where (> r 1.0) given (q2 x) | B(x,y) where (> r 1.0) given (q2 x) (q2 y) } Lang q2 : A { Z() where (> r 1.0) | O(x) where (> r 1.0) given (q1 x) | B(x,y) where (> r 1.0) given (q1 x) (q1 y) } Public Lang r1 : A { Z() where (< r 2.0) | O(x) where (< r 2.0) given (r2 x) | B(x,y) where (< r 2.0) given (r2 x) (r2 y) } Lang r2 : A { Z() where (< r 2.0) | O(x) where (< r 2.0) given (r1 x) | B(x,y) where (< r 2.0) given (r1 x) (r1 y) } //Checks whether the intersection is commutative using equivalence Def intersect_q1r1 : A := (intersect q1 r1) Def intersect_r1q1 : A := (intersect r1 q1) AssertTrue (eq_lang intersect_q1r1 intersect_r1q1) //In case of inequivalence Fast provides a counter example Print (eq_lang intersect_q1r1 q1)http://rise4fun.com/Fast/typecheckingtypechecking//Typechecking operations in FAST //Every even tree produces and odd tree AssertTrue (typecheck evenTree mapInc oddTree) //Every odd tree produces and even tree AssertTrue (typecheck oddTree mapInc evenTree) //Not true for the buggy version that doesn't do recursion on right child AssertFalse (typecheck evenTree mapIncBuggy oddTree) AssertFalse (typecheck oddTree mapIncBuggy evenTree) Print "typechecking succeeded" //Definitions Fun even (i:int) : bool := (= (mod i 2) 0) Fun odd (i:int) : bool := (not (even i)) Alphabet BT [i:int] {Nil(0),Bin(2)} Lang evenTree : BT { Nil() where (even i) | Bin(l,r) where (even i) given (evenTree l) (evenTree r) } Lang oddTree : BT { Nil() where (odd i) | Bin(l,r) where (odd i) given (oddTree l) (oddTree r) } Public Trans mapInc : BT -> BT { Nil() to (Nil [(+ i 1)]) | Bin(l,r) to (Bin [(+ i 1)] (mapInc l) (mapInc r)) } Public Trans mapIncBuggy : BT -> BT { Nil() to (Nil [(+ i 1)]) | Bin(l,r) to (Bin [(+ i 1)] (mapInc l) r) } http://rise4fun.com/Fast/languageoperationslanguageoperations//Union and Intersection Def intersect_q1r1 : A := (intersect q1 r1) Def union_q1r1 : A := (union q1 r1) Def complement_q1 : A := (complement q1) Def min_cq1 : A := (minimize complement_q1) Print "" Print "Equivalence" Print (eq_lang q1 r1) Print (eq_lang q1 (complement complement_q1)) Print "" Print "Intersection" Print intersect_q1r1 Print "" Print "Union" Print union_q1r1 Print "" Print "Complement" Print complement_q1 Print "" Print "Minimization" Print min_cq1 //Other definitions Alphabet A[r:real]{Z(0),O(1),B(2)} Public Lang q1 : A { Z() where (> r 1.0) | O(x) where (> r 1.0) given (q2 x) | B(x,y) where (> r 1.0) given (q2 x) (q2 y) } Lang q2 : A { Z() where (> r 1.0) | O(x) where (> r 1.0) given (q1 x) | B(x,y) where (> r 1.0) given (q1 x) (q1 y) } Public Lang r1 : A { Z() where (< r 2.0) | O(x) where (< r 2.0) given (r2 x) | B(x,y) where (< r 2.0) given (r2 x) (r2 y) } Lang r2 : A { Z() where (< r 2.0) | O(x) where (< r 2.0) given (r1 x) | B(x,y) where (< r 2.0) given (r1 x) (r1 y) } http://rise4fun.com/Fast/restrictrestrictAlphabet A[r:real]{Z(0),B(2)} //Example of restriction over input and output Def t1resi : A -> A := (restrict_inp t1 l1) Def t1reso : A -> A := (restrict_out t1 l1) Def t1resio : A -> A := (restrict_out (restrict_inp t1 l1) l1) Tree t_1 : A := (B [1.5] (Z [1.5]) (Z [1.4])) Tree t_1norm : A := (apply t1 t_1) Tree t_1resi : A := (apply t1resi t_1) Tree t_1reso : A := (apply t1reso t_1) Tree t_1resio : A := (apply t1resio t_1) Tree t_2 : A := (B [1.0] (Z [1.0]) (Z [1.0])) Tree t_2norm : A := (apply t1 t_2) Tree t_2resi : A := (apply t1resi t_2) Tree t_2reso : A := (apply t1reso t_2) Tree t_2resio : A := (apply t1resio t_2) //Output Print t_1norm Print t_1resi Print t_1reso Print t_1resio Print t_2norm Print t_2resi Print t_2reso Print t_2resio //Language we use for restriction Public Lang l1 : A { Z() where (> r 1.0) | B(x,y) where (> r 1.0) given (l1 x) } //Transformation Public Trans t1 : A -> A { Z() where (< r 3.0) to (Z [(- r 0.5)]) | B(x,y) where (< r 3.0) to (B [(- r 0.5)] (t2 x) (t2 y)) } Trans t2 : A -> A { Z() where (< r 3.0) to (Z [(- r 0.5)]) | B(x,y) where (< r 3.0) to (B [(- r 0.5)] (t1 x) (t1 y)) }http://rise4fun.com/Fast/htmlSanitizerhtmlSanitizer// A simple HTML sanitizer written in Fast //Basic sanitizer Def s1 : HTML -> HTML := (compose removeBadNodes prefixIds) Def s2 : HTML -> HTML := (compose s1 convertDeprecated) Def sanitizer : HTML -> HTML := (restrict_inp s2 wellFormedTree) Print "Uncomment line 9 for C# generated code" Print sanitizer //Print (gen_csharp) // Auxiliary functions Fun isSafeNode (name:string) : bool := (or (= name "div") (= name "style") (= name "p") (= name "b") (= name "span") (= name "caption") (= name "tr") (= name "td") (= name "table") (= name "tfoot") (= name "th") (= name "center") (= name "svg") (= name "textarea") (= name "circle") (= name "img") (= name "a") (= name "html") (= name "body") (= name "input")) Fun isSafeAttribute (name:string) : bool := (or (= name "style") (= name "href") (= name "id") (= name "name") (= name "align") (= name "width") (= name "height") (= name "type")) Fun needsPrefix (name:string) : bool := (or (= name "name") (= name "id")) Fun needsURLWhiteList (name:string) : bool := (or (= name "src") (= name "style") (= name "href")) Alphabet HTML[tag:string]{empty(0),value(1),attr(2),node(3)} // Language of HTML trees Lang wellFormedTree : HTML{ node(fa,fc,ns) given (wellFormedAttributeTree fa) (wellFormedTree fc) (wellFormedTree ns) | empty() where (= tag "") } Lang wellFormedAttributeTree : HTML { attr(attVal,na) given (attributeValue attVal) (wellFormedAttributeTree na) | empty() where (= tag "") } Lang attributeValue : HTML { value(nv) given (attributeValue nv) | empty() where (= tag "") } // Transformations Trans removeBadNodes : HTML -> HTML { node(fa,fc,ns) where (isSafeNode tag) to (node [tag] fa (removeBadNodes fc) (removeBadNodes ns)) | node(fa,fc,ns) where (not (isSafeNode tag)) to (removeBadNodes ns) | empty() to (empty [tag]) } Trans prefixIds : HTML -> HTML { node(fa,fc,ns) to (node [tag] (prefixIds fa) (prefixIds fc) (prefixIds ns)) | attr(attVal,na) where (needsPrefix tag) to (attr [tag] (value ["p"] (value ["r"] (value ["e"] (value ["f"] (value ["0"] (value ["1"] na ) ) ) ) ) ) (prefixIds na) ) | empty() to (empty [tag]) } Trans removeBadAttributes : HTML -> HTML { node(fa,fc,ns) to (node [tag] (removeBadAttributes fa) (removeBadAttributes fc) (removeBadAttributes ns)) | attr(v,na) where (isSafeAttribute tag) to (attr [tag] v (removeBadAttributes na)) | attr(v,na) where (not (isSafeAttribute tag)) to (removeBadAttributes na) | empty() to (empty [tag]) } // text-align:center will in the future be encoded as a sequence of values Trans convertDeprecated : HTML -> HTML { node(fa,fc,ns) where (= tag "center") to (node ["div"] (attr ["style"] (value ["text-align:center;"] (empty [""]) ) (empty [""]) ) (convertDeprecated fc) (convertDeprecated ns) ) | empty() to (empty [tag]) } Trans whiteListURL : HTML -> HTML { node(fa,fc,ns) to (node [tag] (whiteListURL fa) (whiteListURL fc) (whiteListURL ns)) | attr(x,y) where (needsURLWhiteList tag) to (attr [tag] x y) //TODO deletion based on given } http://rise4fun.com/Fast/bodytreebodytree// A Kinect skeleton Animator Enum Side {C, L, R} Alphabet BodyPart[s:Side, x:real, y:real, color:string]{Spine(2), Shoulder(1), ShoulderCenter(3), Head, Elbow(1), Wrist(1), Hand, HipCenter(2), Hip(1), Knee(1), Ankle(1), Foot} //Create complex moves out of simpler ones Def MoveArmLeg : BodyPart -> BodyPart := (compose DownLeftArm DownRightArm) //Restrict to only start from a well defined body Def ResMoveArmLeg : BodyPart -> BodyPart := (restrict_inp DownLeftArm body) //Domain of DownLeftArm Def DownLeftArmDom : BodyPart := (domain DownLeftArm) //Intersect with the language body Def IntersTest : BodyPart := (intersect DownLeftArmDom body) Print IntersTest //LANGUAGES //Defines what a correct body_tree is Public Lang body : BodyPart { Spine(u,d) where (= s Side.C) given (upperBody u) (lowerBody d) } Lang upperBody : BodyPart { ShoulderCenter(h,l,r) where (and (= s Side.C)) given (head h) (arm l) (arm r) (leftJ l) (rightJ r) } Lang arm : BodyPart { Shoulder(e) given (lowerArm e) } Lang lowerArm : BodyPart { Elbow(w) given (wrist w) } Lang wrist : BodyPart{ Wrist(h) given (hand h) } Lang hand : BodyPart{ Hand() } Lang head : BodyPart{ Head() } Lang lowerBody : BodyPart { HipCenter(l,r) where (= s Side.C) given (leg l) (leg r) (leftJ l) (rightJ r) } Lang leg : BodyPart { Hip(k) given (lowerLeg k) } Lang lowerLeg : BodyPart { Knee(a) given (ankle a) } Lang ankle : BodyPart{ Ankle(h) given (foot h) } Lang foot : BodyPart{ Foot() } //Left joint Lang leftJ : BodyPart{ Hip(c) where (= s Side.L) given (leftJ c) | Knee(c) where (= s Side.L) given (leftJ c) | Ankle(c) where (= s Side.L) given (leftJ c) | Foot() where (= s Side.L) | Shoulder(c) where (= s Side.L) given (leftJ c) | Elbow(c) where (= s Side.L) given (leftJ c) | Wrist(c) where (= s Side.L) given (leftJ c) | Hand() where (= s Side.L) } //Right joint Lang rightJ : BodyPart{ Hip(c) where (= s Side.R) given (rightJ c) | Knee(c) where (= s Side.R) given (rightJ c) | Ankle(c) where (= s Side.R) given (rightJ c) | Foot() where (= s Side.R) | Shoulder(c) where (= s Side.R) given (rightJ c) | Elbow(c) where (= s Side.R) given (rightJ c) | Wrist(c) where (= s Side.R) given (rightJ c) | Hand() where (= s Side.R) } //Auxiliary functions Fun rotateXR (x:real) (y:real):real:= (- (* 0.9848 x) (* (- 0.0 0.1736) y)) Fun rotateYR (x:real) (y:real):real:= (+ (* (- 0.0 0.1736) x) (* 0.9848 y)) Fun rotateXL (x:real) (y:real):real:= (- (* 0.9848 x) (* 0.1736 y)) Fun rotateYL (x:real) (y:real):real:= (+ (* 0.1736 x) (* 0.9848 y)) Fun liftXR (x:real) (y:real):real:= (- (* 0.7071 x) (* (- 0.0 0.7071) y)) Fun liftYR (x:real) (y:real):real:= (+ (* (- 0.0 0.7071) x) (* 0.7071 y)) Fun liftXL (x:real) (y:real):real:= (- (* 0.7071 x) (* 0.7071 y)) Fun liftYL (x:real) (y:real):real:= (+ (* 0.7071 x) (* 0.7071 y)) Fun stepXL (x:real):real:= (- x 34.0) Fun stepYU (x:real):real:= (+ x 7.0) Fun stepXR (x:real):real:= (+ x 34.0) Fun stepYD (x:real):real:= (+ x 7.0) //TRANSDUCTIONS Trans Step : BodyPart -> BodyPart { HipCenter(c1,c2) where true to (HipCenter [s,x,y,color] (Step c1) (Step c2)) | Hip(c) where true to (Hip [s,x,y,color] (Step c)) | Knee(c) where (= s Side.R) to (Knee [s,(rotateXR x y),(rotateYR x y),color] (Step c)) | Knee(c) where (= s Side.L) to (Knee [s,(rotateXL x y),(rotateYL x y), color] (Step c)) | Ankle(c) where (= s Side.R) to (Ankle [s,(rotateXR x y),(rotateYR x y),color] c) | Ankle(c) where (= s Side.L) to (Ankle [s,(rotateXL x y),(rotateYL x y), color] c) } Public Trans StepLeft : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, (stepXL x), (stepYD y), color] c1 (Step c2)) } Public Trans StepRight : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, (stepXR x), (stepYD y), color] c1 (Step c2)) } Trans Collect : BodyPart -> BodyPart { HipCenter(c1,c2) where true to (HipCenter [s,x,y,color] (Collect c1) (Collect c2)) | Hip(c) where true to (Hip [s,x,y,color] (Collect c)) | Knee(c) where (= s Side.L) to (Knee [s,(rotateXR x y),(rotateYR x y),color] (Collect c)) | Knee(c) where (= s Side.R) to (Knee [s,(rotateXL x y),(rotateYL x y), color] (Collect c)) | Ankle(c) where (= s Side.L) to (Ankle [s,(rotateXR x y),(rotateYR x y),color] c) | Ankle(c) where (= s Side.R) to (Ankle [s,(rotateXL x y),(rotateYL x y), color] c) } Public Trans CollectLeft : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, (stepXR x), (stepYU y), color] c1 (Collect c2)) } Public Trans CollectRight : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, (stepXL x), (stepYU y), color] c1 (Collect c2)) } Trans LiftArm : BodyPart -> BodyPart { Shoulder(c) where true to (Shoulder [s,x,y,color] (LiftArm c)) | Elbow(c) where (= s Side.R) to (Elbow [s,(liftXR x y),(liftYR x y),color] (LiftArm c)) | Elbow(c) where (= s Side.L) to (Elbow [s,(liftXL x y),(liftYL x y),color] (LiftArm c)) | Wrist(c) where (= s Side.R) to (Wrist [s,(liftXR x y),(liftYR x y),color] c) | Wrist(c) where (= s Side.L) to (Wrist [s,(liftXL x y),(liftYL x y),color] c) } Public Trans LiftLeftArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (LiftLeftArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h (LiftArm l) r) } Public Trans LiftRightArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (LiftRightArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h l (LiftArm r)) } Public Trans LiftLeftLowerArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (LiftLeftLowerArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h (LiftLowerArm l) r) } Public Trans LiftRightLowerArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (LiftRightLowerArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h l (LiftLowerArm r)) } Trans LiftLowerArm : BodyPart -> BodyPart { Shoulder(c) where true to (Shoulder [s,x,y,color] (LiftLowerArm c)) | Elbow(c) where (= s Side.L) to (Elbow [s,x,y,color] (LiftArm c)) | Elbow(c) where (= s Side.R) to (Elbow [s,x,y,color] (LiftArm c)) } Trans DownArm : BodyPart -> BodyPart { Shoulder(c) where true to (Shoulder [s,x,y,color] (DownArm c)) | Elbow(c) where (= s Side.L) to (Elbow [s,(liftXR x y),(liftYR x y),color] (DownArm c)) | Elbow(c) where (= s Side.R) to (Elbow [s,(liftXL x y),(liftYL x y),color] (DownArm c)) | Wrist(c) where (= s Side.L) to (Wrist [s,(liftXR x y),(liftYR x y),color] c) | Wrist(c) where (= s Side.R) to (Wrist [s,(liftXL x y),(liftYL x y),color] c) } Public Trans DownLeftArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (DownLeftArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h (DownArm l) r) } Public Trans DownRightArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (DownRightArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h l (DownArm r)) } Public Trans DownLeftLowerArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (DownLeftLowerArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h (DownLowerArm l) r) } Public Trans DownRightLowerArm : BodyPart -> BodyPart { Spine(c1,c2) where true to (Spine [s, x,y,color] (DownRightLowerArm c1) c2) | ShoulderCenter(h,l,r) where true to (ShoulderCenter [s, x,y,color] h l (DownLowerArm r)) } Trans DownLowerArm : BodyPart -> BodyPart { Shoulder(c) where true to (Shoulder [s,x,y,color] (DownLowerArm c)) | Elbow(c) where (= s Side.L) to (Elbow [s,x,y,color] (DownArm c)) | Elbow(c) where (= s Side.R) to (Elbow [s,x,y,color] (DownArm c)) }