Setepenre pushed to branch master at Stefan / Typer

Commits: 05b1ad07 by Pierre Delaunay at 2016-12-18T23:18:58-05:00 * src/lexp.ml: modified lexp_string so metavar's result is printed instead of metavar. Helps when debug printing * src/lparse.ml: moved `global_substitution` to `src/lexp.ml` so the context can be used when printing lexp * samples/dependent.typer: fixed some issues, the example is almost working (inference issue I think) * samples/acc.typer: new list functions

- - - - - 8cc696db by Pierre Delaunay at 2016-12-20T16:43:45-05:00 Merge

- - - - - c7ec8cf2 by Pierre Delaunay at 2016-12-26T11:54:38-05:00 added a new example `samples/io.typer`

- - - - -

3 changed files:

- + samples/acc.typer - + samples/io.typer - src/lexp.ml

Changes:

===================================== samples/acc.typer ===================================== --- /dev/null +++ b/samples/acc.typer @@ -0,0 +1,23 @@ +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); \ No newline at end of file

===================================== samples/io.typer ===================================== --- /dev/null +++ b/samples/io.typer @@ -0,0 +1,70 @@ +type Location + | location (line : col) (col : Int) (file : String); + +% Symbolic Expression +Sexp : Type; +type Sexp + | epsilon + | block (loc_start : Location) (tok : List Pretoken) (loc_end : Location) + | symbol (loc : Location) (name : String) + | string (loc : Location) (value : String) + | integer (loc : Location) (value : Int) + | float (loc : Location) (value : Float) + | node (op : Sexp) (args : List Sexp); + +sexp_loc : Sexp -> Location; +sexp_loc s = + case s + | block loc _ _ => loc + | symbol loc _ => loc + | string loc _ => loc + | integer loc _ => loc + | float loc _ => loc + | node loc _ => sexp_loc op + | _ => dummy_location; + +sexp_name : Sexp -> String; +sexp_name s = + case s + | epsilon => "Epsilon" + | block _ _ _ => "Block" + | symbol _ _ => "Symbol" + | string _ _ => "String" + | integer _ _ => "Integer" + | float _ _ => "Float" + | node _ _ => "Node"; + +sexp_string : Sexp -> String; +sexp_string s = + case s + | epsilon => "ε" + | symbol _ v => v + | string _ v => v + | integer _ v => to-string v + | float _ v => to-string v + | block _ v _ => "{" ++ (pretokens_string v) ++ "}" + | node op args => + let args = accumulate + (lambda str val -> str ++ " " ++ sexp_string val) "" args in + "(" ++ (sexp_string op) ++ args ++ ")"; + +% is there a simplier way ? +sexp_equal : Sexp -> Sexp -> Bool; +sexp_equal a b = + case a + | epsilon => case b | + epsilon => true | _ => false + | symbol _ v => case b | + symbol _ v' => v = v' | _ => false + | string _ v => case b | + string _ v' => v = v' | _ => false + | integer _ v => case b | + integer _ v' => v = v' | _ => false + | float _ v => case b | + float _ v' => v = v' | _ => false + | block _ lst _ => case b | + block _ lst' _ => (lst = lst) | _ => false + | node op args => case b | + node op' args' => (op = op') && (args = args') | _ => false; + +

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -545,7 +545,6 @@ let pp_append_string buffer ctx str = let n = (String.length str) in Buffer.add_string buffer str; add_col_size n ctx - let pp_newline buffer ctx = Buffer.add_char buffer '\n'; reset_col_size ctx

View it on GitLab: https://gitlab.com/monnier/typer/compare/bd953f6da7ec2d2df739603e363a86d60a7...