Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: a1747386 by Jonathan Graveline at 2018-08-30T20:16:35Z Removed "debug output" in `Ref_make` from src/eval.ml

samples/decltype.typer: another version of `decltype` implemented in Typer

samples/math.typer: a toy math library

- - - - -

3 changed files:

- + samples/decltype.typer - + samples/math.typer - src/eval.ml

Changes:

===================================== samples/decltype.typer ===================================== @@ -0,0 +1,57 @@ +%%%% +%%%% Declaring the type of an expression +%%%% directly in Typer +%%%% + +%% +%% It mostly work as exemples below work fine +%% but I can't do somethings like: +%% y = decl-type x; +%% + +decl-type = lambda (t : Type) => lambda (_ : t) -> t; + +%% +%% Some tests and exemples +%% + +int-var : Int; +int-var = 100; + +%% +%% Error "Metavar in erase_type": +%% int = decl-type int-var; +%% + +flt-var : Float; +flt-var = 0.1; + +str-var : String; +str-var = "abc"; + +bool-var : Bool; +bool-var = true; + +take-int : (decl-type int-var) -> (decl-type 1); +take-int n = n + n; + +take-flt : (decl-type flt-var) -> (decl-type 1.0); +take-flt x = Float_+ x x; + +take-str : (decl-type str-var) -> (decl-type "123"); +take-str s = String_concat s s; + +%% +%% This is the first exemple where we really need +%% type annotation (with current `##case_`) +%% +take-bool : (decl-type bool-var) -> (decl-type true); +take-bool b = case b + | true => false + | false => true; + +rec-int : (decl-type int-var) -> (decl-type int-var); +rec-int n = if (Int_> n 0) then + (n + rec-int (n - 1)) + else + (0);

===================================== samples/math.typer ===================================== @@ -0,0 +1,244 @@ +%%%% +%%%% Sample math library. +%%%% +%%%% Basic math function, constant, etc. +%%%% +%%%% This file is only an exemple. There is probably multiple +%%%% design errors (precision lost, bad algorithm choice, etc). +%%%% + +%% +%% Get the string decimal representation of an Int +%% +%% With this function we could remove built-in function Int->String +%% + +Int2String : Int -> String; +Int2String x = let + + lut : List String; + lut = cons "0" (cons "1" (cons "2" (cons "3" (cons "4" + (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) + )))))))); + + helper : Int -> String; + helper x = + if (Int_eq x 0) then + ("") + else + (String_concat (helper (x / 10)) (List_nth (Int_mod x 10) lut "error")); + +in if (Int_eq x 0) then + ("0") + else + (helper x); + +%% +%% Factorial +%% +%% Shouldn't be calculated recursively but an Int isn't bigger than `fact 20;` +%% This function isn't safe +%% + +fact : Int -> Int; +fact n = + if (Int_eq 1 n) then 1 else (n * (fact (n - 1))); + +Int_abs : Int -> Int; +Int_abs n = if (Int_< n 0) then (0 - n) else n; + +Float_abs : Float -> Float; +Float_abs x = if (Float_< x 0.0) then (Float_- 0.0 x) else x; + +Float_mod : Float -> Float -> Float; +Float_mod x y = Float_- x (Float_* (Float_trunc (Float_/ x y)) y); + +%% +%% Cool math constant +%% + +pi : Float; +e : Float; + +pi = 3.141592653589793; +e = 2.718281828459045; + +%% +%% Get square root of number 'a' +%% + +sqrt : Float -> Float; +sqrt a = let + + x : Float; + x = (Float_/ a 4.0); + + sqrtp : Int -> Float -> Float; + sqrtp n x = + let xp = (Float_/ (Float_+ x (Float_/ a x)) 2.0) in + if (Int_eq n 32) then % maybe 32 isn't enough iteration ? + xp + else + (sqrtp (n + 1) xp); + +in sqrtp 0 x; + +%% +%% Power +%% +%% Only for positive integer exponent +%% +%% (Using a divide-and-conquer algorithm) +%% + +Floatpow : Float -> Int -> Float; +Floatpow x n = let + + powp : Float -> Int -> Float; + powp xp np = + if (Int_eq np 1) then + xp + else + (if (Int_eq (Int_mod np 2) 0) then + (powp (Float_* xp xp) (np / 2)) + else + (Float_* xp (powp (Float_* xp xp) ((np - 1) / 2)))); + +in powp x n; + +Intpow : Int -> Int -> Int; +Intpow x n = let + + powp : Int -> Int -> Int; + powp xp np = + if (Int_eq np 1) then + xp + else + (if (Int_eq (Int_mod np 2) 0) then + (powp (xp * xp) (np / 2)) + else + (xp * (powp (xp * xp) ((np - 1) / 2)))); + +in powp x n; + +%% +%% Sinus and Cosinus +%% +%% (Using Taylor series...) +%% +%% (Probably not the best algorithm for this) +%% + +%% +%% truncRadian keep `x` between 0 and 2pi +%% (It "trunc" all complete circle) +%% +truncRadian : Float -> Float; +truncRadian x = Float_mod x (Float_* 2.0 pi); + +%% +%% Implementation of both sinus and cosinus +%% (they just have different parameters) +%% +sinusoidaleTaylor : Int -> Float -> Float -> Float -> Float -> Float -> Float; +sinusoidaleTaylor iter y xp x n i = let + + _fact : Float -> Float; + _fact n = + if (Float_eq 1.0 n) then + 1.0 + else + (Float_* n (_fact (Float_- n 1.0))); + + ii : Float; + ii = Float_- 0.0 1.0; + + x2 : Float; + x2 = Float_* y y; + + sinusoidaleTaylorp : Int -> Float -> Float -> Float -> Float -> Float; + sinusoidaleTaylorp iter xx xp n i = + let + xxp : Float; xxp = Float_* xx x2; + np : Float; np = Float_+ n 2.0; + in if (Int_eq iter 0) then + xp + else + (sinusoidaleTaylorp (iter - 1) + xxp + (Float_+ xp (Float_* i (Float_/ xxp (_fact np)))) + np + (Float_* i ii)); + +in sinusoidaleTaylorp iter xp x n i; + +sin : Float -> Float; +sin x = let + + %% + %% I got error with value outside [0,360] + %% (It could be a precision lost or an error in sinusoidaleTaylor) + %% + xp : Float; + xp = truncRadian x; + +in sinusoidaleTaylor 20 xp xp xp 1.0 (-1.0); + +%% +%% cos is exactly like sin but start somewhere else +%% +cos : Float -> Float; +cos x = let + + %% + %% I got error with value outside [0,360] + %% (It could be a precision lost or an error in sinusoidaleTaylor) + %% + xp : Float; + xp = truncRadian x; + +in sinusoidaleTaylor 20 xp 1.0 1.0 0.0 (-1.0); + +%% +%% Random number generator +%% +%% Linear congruential +%% + +type Rand-Data + | rand-data (last : Int) (fun : (Int -> Int)); + +rand-gen : Int -> Int -> Int -> IO (Ref Rand-Data); +rand-gen min max seed = let + + a : Int; a = 1664525; + b : Int; b = 1013904223; + c : Int; c = 123456789; % probably a bad choice (reduce the period length?) + + range : Int; + range = max - min + 1; + + inrange : Int -> Int; + inrange s = min + (Int_mod (Int_abs s) range); + + randp : Int -> Int; + randp r = inrange ((a * r + b) * c); + +in Ref_make (rand-data seed randp); + +rand-next : Ref Rand-Data -> IO Int; +rand-next ref-data = do { + data <- Ref_read ref-data; + + last <- IO_return ( case data + | rand-data last _ => last ); + + f <- IO_return ( case data + | rand-data _ f => f ); + + rand <- IO_return (f last); + + Ref_write (rand-data rand f) ref-data; + + IO_return rand; +};

===================================== src/eval.ml ===================================== @@ -723,7 +723,7 @@ let nop_fun loc _ vs = match vs with | _ -> error loc "Wrong number of argument to nop"

let ref_make loc depth args_val = match args_val with - | [v] -> Vcommand (fun () -> print_string "\n\tIN REF_MAKE\n\n"; Vref (ref v)) + | [v] -> Vcommand (fun () -> Vref (ref v)) | _ -> error loc "Ref.make takes a single value as argument"

let ref_read loc depth args_val = match args_val with

View it on GitLab: https://gitlab.com/monnier/typer/commit/a17473862e54f2452061c3f34d688277726a...