Setepenre pushed to branch master at Stefan / Typer

Commits: bae92e62 by Pierre Delaunay at 2016-09-08T09:50:00-04:00 updated the type_ macro. - Formal args were not processed correctly. - Added new examples - Modfied style

Changes to be committed: * samples/inductive.typer

- - - - -

2 changed files:

- samples/inductive.typer - src/lexp.ml

Changes:

===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -28,54 +28,56 @@ type-impl = lambda (x : List Sexp) -> % x follow the mask -> (_|_ Nat zero (succ Nat)) % Type name --^ ^------^ constructors

- % Get expression - let expr = head (a := Sexp) x in let sexp_nil = (nil (a := Sexp)) in

- % Expression is node_ (symbol_ "|") (list) - % we only care about the list bit - - let get-list = (lambda (node : Sexp) -> - sexp_dispatch_ (a := List Sexp) node - (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> lst)) % Nodes - (lambda (str : String) -> sexp_nil) % Symbol - (lambda (str : String) -> sexp_nil) % String - (lambda (int : Int) -> sexp_nil) % Integer - (lambda (float : Float) -> sexp_nil) % Float - (lambda (lst : List Sexp) -> sexp_nil)) in % List of Sexp + % Return a list contained inside a node sexp + let get-list : Sexp -> List Sexp; + get-list node = sexp_dispatch_ (a := List Sexp) node + (lambda op lst -> lst) % Nodes + (lambda _ -> sexp_nil) % Symbol + (lambda _ -> sexp_nil) % String + (lambda _ -> sexp_nil) % Integer + (lambda _ -> sexp_nil) % Float + (lambda _ -> sexp_nil) in % List of Sexp

% Get a name from a sexp - % (name t) -> name - % name -> name + % - (name t) -> name + % - name -> name let get-name : Sexp -> Sexp; get-name sxp = sexp_dispatch_ (a := Sexp) sxp - (lambda (op : Sexp) -> (lambda (lst : List Sexp) -> get-name op)) % Nodes - (lambda (str : String) -> symbol_ str) % Symbol - (lambda (str : String) -> symbol_ str) % String - (lambda (int : Int) -> symbol_ "error") % Integer - (lambda (float : Float) -> symbol_ "error") % Float - (lambda (lst : List Sexp) -> symbol_ "error") in % List of Sexp + (lambda op lst -> get-name op) % Nodes + (lambda str -> symbol_ str) % Symbol + (lambda _ -> symbol_ "error") % String + (lambda _ -> symbol_ "error") % Integer + (lambda _ -> symbol_ "error") % Float + (lambda _ -> symbol_ "error") in % List of Sexp

+ % Get expression + let expr = head (a := Sexp) x in + + % Expression is node_ (symbol_ "|") (list) + % we only care about the list bit let lst = get-list expr in

- let name = head (a := Sexp) lst in - let ctor = tail (a := Sexp) lst in + % head is (node_ type-name (arg list)) + let name = head (a := Sexp) lst; + ctor = tail (a := Sexp) lst in

let type-name = get-name name in

% Create the inductive type definition let inductive = node_ (symbol_ "inductive_") - (cons (a := Sexp) type-name ctor) in + (cons (a := Sexp) name ctor) in

% Create a forward declaration in case the declaration is recursive - let fdecl = make-ann type-name (symbol_ "Type") in + % let fdecl = make-ann type-name (symbol_ "Type") in let decl = make-decl type-name inductive in

% Add constructors let ctors = let for-each : List Sexp -> List Sexp -> List Sexp; - for-each ctor acc = case ctor + for-each ctr acc = case ctr | cons hd tl => ( let acc2 = cons (a := Sexp) (make-cons (get-name hd) type-name) acc in for-each tl acc2) @@ -83,15 +85,38 @@ type-impl = lambda (x : List Sexp) -> in for-each ctor (nil (a := Sexp)) in

% return decls - cons (a := Sexp) fdecl % Forward declaration + % cons (a := Sexp) fdecl % Forward declaration (cons (a := Sexp) decl % inductive type declaration ctors); % constructor declarations

type_ = Macro_ type-impl;

-% (type_ (_|_ (Nat t) zero (succ Nat))) -% (type_ (_|_ Nat zero (succ Nat))) -type Nat t - | succ Nat - | zero; +% (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) +type Either t1 t2 + | either-first t1 + | either-second t2; + +type Pair t1 t2 + | pair t1 t2; + +type Point t + | point (x : t) (y : t); + +get-first : (a : Type) => (b : Type) => Pair -> a; +get-second : (a : Type) => (b : Type) => Pair -> b; + +get-first p = case p | pair a b => a; +get-second p = case p | pair a b => b; + +get-x : (a : Type) => Point -> a; +get-y : (a : Type) => Point -> a; +get-x p = case p | point x y => x; +get-y p = case p | point x y => y; + + +% transformed to: +% Nat : Type; +% Nat = inductive_ (Nat) (succ Nat) (zero); +% zero = inductive-cons Nat zero; +% succ = inductive-cons Nat succ; \ No newline at end of file

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -511,6 +511,26 @@ let debug_ppctx = ref (false, 0, true, true , false, 4, true) let rec lexp_print e = _lexp_print (!debug_ppctx) e and _lexp_print ctx e = print_string (_lexp_to_str ctx e)

+(*) +type print_context2 = int SMap.t + +let default_print_context = + List.fold (fun map (key, v) -> SMap.add key v map) + [ + (* true options *) + ("pretty", 1); + ("print_type", 1); + ("print_dbi", 1); + ("indent_size", 2); + ("color", 1); + ("separate_decl", 1); + + (* State information *) + ("indent_level", 0); + ("previous node", 0) + ] + SMap.empty *) + (* Print a lexp into its typer equivalent *) (* Depending on the print_context the output can be correct typer code *) (* This function will be very useful when debugging generated code *)

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