[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v #275

JasonGross · 2017-11-24T20:25:39Z

It's rather verbose, unfortunately. The reification also doesn't have
any of the nice debugging features of the version of reification in
Compilers, because that's even more boilerplate. Not sure if I should
add that back in, at the moment.

Also, for some strange reason, places where constrs fail to typecheck
seem to induce backtracking where I don't think they should, and I'm not
sure what's going on...

andres-erbsen

Overall strategy looks good as expected. I still scribbled all over this, mostly to make sure I am actually reading it. I think the machinery for substituting type arguments during reification warrants some more explanation. I would also like you to consider the namespacing suggestions I made. However, don't try to address every individual scribble that I made, just take the overall sense of what caused me to do a double-take into consideration. If I don't respond for a day after you make changes (or decide not to), feel free to merge this anyway and move on with whatever you are doing.

andres-erbsen · 2017-11-24T21:35:43Z

src/Experiments/SimplyTypedArithmetic.v

@@ -178,22 +179,435 @@ Module Positional. Section Positional.
  End mulmod.
 End Positional. End Positional.

-Import Associational Positional.
+Module Compilers.
+  Inductive type := Unit | Prod (A B : type) | Arrow (s d : type) | List (A : type) | TNat | TZ | TBool.


What are your thoughts on putting constructors in a namespace named after the type, as in Lean? I think I have an easier time remembering Compilers.type.nat vs Compilers.TNat (and obviously I would import Compilers if I used it alot).

Sure, seems fine. I'll do that. Should I also call it type.interp rather than interp_type?

andres-erbsen · 2017-11-24T21:36:15Z

src/Experiments/SimplyTypedArithmetic.v

-Import Associational Positional.
+Module Compilers.
+  Inductive type := Unit | Prod (A B : type) | Arrow (s d : type) | List (A : type) | TNat | TZ | TBool.
+  Delimit Scope ctype_scope with ctype.


What does ctype stand for?

c stands for compilers or compiler or compiled. The issue is that type_scope is already taken by Coq, and scopes aren't namespaced.

andres-erbsen · 2017-11-24T21:36:56Z

src/Experiments/SimplyTypedArithmetic.v

+  Inductive type := Unit | Prod (A B : type) | Arrow (s d : type) | List (A : type) | TNat | TZ | TBool.
+  Delimit Scope ctype_scope with ctype.
+  Bind Scope ctype_scope with type.
+  Notation "()" := Unit : ctype_scope.


Would ( ) parse as Unit?

No, but I can fix that. Shall I?

andres-erbsen · 2017-11-24T21:41:54Z

src/Experiments/SimplyTypedArithmetic.v

+  | BoolRect {T} : op (T * T * TBool) T
+  | NatRect {P} : op (P * (TNat -> P -> P) * TNat) P
+  | Seq : op (TNat * TNat) (List TNat)
+  | Repeat {A} : op (A * TNat) (List A)


I read Repeat as while (1) { ... } at first. Hmm. ListRepeat could be an ad-hoc solution, though the real issue here is lack of namespacing of op values themselves...

Renamed to List_repeat, added some namespacing

andres-erbsen · 2017-11-24T21:42:23Z

src/Experiments/SimplyTypedArithmetic.v

+  | Zmodulo : op (TZ * TZ) TZ
+  | Zeqb : op (TZ * TZ) TBool
+  | ZofNat : op TNat TZ
+  | App {s d} : op ((s -> d) * s) d.


Yeah, ListApp is above already...

andres-erbsen · 2017-11-24T22:12:56Z

src/Experiments/SimplyTypedArithmetic.v

+                          end) in
+         lazymatch rest with
+         | (fun _ => ?rest)
+           => constr:((tt, rest))


Does this function just return a (tt, (tt, (tt, ...))) according to the arity of the input? If so, why is it useful?

Yes. It's useful because some other code relies on the "delayed arguments" list exactly matching the shape of the type. We could instead add some extra cases to deal separately with tt as dummy, and (tt, _) as dummy, but I decided to pay the cost in this one place, rather than in all the places where I use it.

The problem I'm solving is that some applications need to stay as Gallina applications, and not turn into PHOAS application nodes. I could throw an error if not all such applications came at the head of the term (i.e., if there was anything of type nat -> forall T : Type, ....), but I currently support such cases. So I need to save the arguments that need to be plugged in as Gallina applications, and mark the ones that become PHOAS applications.

Do we actually support these, though? I don't know what would be passed to reify_op for something like this.

These = nat -> forall T : Type, ...? Or just type arguments? For type arguments, we need something like this for List.map, etc. For things like nat -> forall T : Type, ..., we nominally support them. We can reify something silly like

(fun (n : nat) (T : Type) (f : T -> nat) (x : T) => n + f x) 0 nat (fun x => x) 1

But we don't need to support these things. Would it be better to drop support for them?

Oh, so this is about being insensitive to ordering of arguments / section variables. That seems like a good property.

andres-erbsen · 2017-11-24T22:16:51Z

src/Experiments/SimplyTypedArithmetic.v

+    | (tt, ?delayed_arguments) => check_delayed_arguments_dummy delayed_arguments if_dummy if_not_dummy
+    | (_, _) => if_not_dummy ()
+    end.
+  Ltac plug_delayed_arguments f delayed_arguments :=


Okay, I now understand here that we are doing substituting in some arguments of a function and not others. However, it is not clear how the bindings being substitutied are encoded. Part of this might be me having trouble reading tactics-in-terms.

The encoding is that there is a tuple of arguments. tt means "this becomes a PHOAS application node", anything else means "this should be substituted in Gallina". (This is safe, because only things of type Type, Set, Prop, or _ -> _ -> ... _ -> {Type,Set,Prop} get substituted.) Terms are eta-expanded as necessary to fill in arguments, but, importantly, are not eta-expanded if all remaining arguments are dummy (tt). Perhaps there is a cleaner way to do all of this.

Why do we pass arguments in tuples anyway? Why does that transformation need to happen during reification?

There are two cases:

Somehow, reification needs to know to reify @List.map ?A ?B, not @List.map. This could be solved by cps-ing reify_op, and then having reification try reify_op first, and only try other things if reify_op fails. However, this will stop working if we want to, e.g., define List.map in terms of list_rect and remove List.map from reification in favor of an initial cbv delta [List.map], in which case we'll have:

reification of (fun (A B : Type) => ...) T U

Because we're not doing cbv beta, we need to either commit to never having lambdas that take type arguments, or we need to pass types around in tuples to do controlled beta reduction ourselves, or we need to write special cases for all of the numbers and kinds of type arguments we want to handle.

I agree that we do need to implement beta reduction of type arguments.

andres-erbsen · 2017-11-24T22:17:40Z

src/Experiments/SimplyTypedArithmetic.v

+         Uncurry0 (@OpConst rT term)
+    end.
+
+  Inductive context_var_map {var : type -> Type} :=


Again, how about namespacing the constructors? I actually had to look them up when I encountered them below.

andres-erbsen · 2017-11-24T22:19:37Z

src/Experiments/SimplyTypedArithmetic.v

+        | ?f ?x
+          =>
+          let x_ty := type of x in
+          let x_type_arg := is_type_arg x_ty in


is_type_arg -> is_type or is_sort or something like that?

Yeah, basically

andres-erbsen · 2017-11-24T22:20:38Z

src/Experiments/SimplyTypedArithmetic.v

+          lazymatch x_type_arg with
+          | true
+            => (* we can't reify things of type [Type], so we save it for later to plug in *)
+            reify_helper var f ctx (x, delayed_arguments)


Is delayed_arguments a list of substitutions to be made during reification?

Yes, with tt marking places where substitutions are reified as applications rather than made

JasonGross · 2017-11-25T00:42:14Z

Eh, responding to the scribbles was not hard. I appreciate them. I think you did a double-take at all of the places where my abstraction barriers are leaky, painful, or unclean. There are still some design questions to be answered (around currying of functions and around what the right interface is for delayed arguments), so I'll wait on your feedback. (Note also that I made delayed arguments more general than it needs to be for me to use it here. Perhaps I should just assume/enforce the invariant that all type arguments come first, and that will simplify code a decent amount?)

andres-erbsen · 2017-11-25T01:53:00Z

src/Experiments/SimplyTypedArithmetic.v

+      Notation op := op.
+    End Notations.
+  End op.
+  Export op.Notations.


is Export actually necessary here? could the alias just be after the end of the module?

Alias could be after the end of the module, but I imagine op may get it's own file, or something, and this is preempting that. Is that a bad idea?

andres-erbsen · 2017-11-25T02:12:38Z

src/Experiments/SimplyTypedArithmetic.v

+    let n' := fresh n' in
+    n'.
+
+  Ltac is_type_arg arg_ty :=


Why do we need to do beta-reduction here at all?

I would rename to is_template_parameter parameter_type (even though we call it on argument types).

andres-erbsen · 2017-11-25T02:57:25Z

src/Experiments/SimplyTypedArithmetic.v

+                          end) in
+         lazymatch rest with
+         | (fun _ => ?rest)
+           => constr:((tt, rest))


Do we actually support these, though? I don't know what would be passed to reify_op for something like this.

As per mit-plv#275 (comment)

andres-erbsen · 2017-11-25T14:15:51Z

I am still confused why we need to mark non-template arguments with tt -- they should be obvious from the function itself. Is this somehow because we do currying in the same pass?

andres-erbsen · 2017-11-25T15:32:34Z

I think I am now convinced that the reification should indeed be doing what it is doing right now. However, it seems sketchy that we need to insert tt in the list of type arguments to keep things in sync -- I am guessing it is duplicating some other information already available in the context where it is used, and the code would be nicer without it. E.g. we could just keep an ordered list of template arguments, using them on demand.

andres-erbsen · 2017-11-25T15:37:40Z

src/Experiments/SimplyTypedArithmetic.v

+             reify_rec (@Let_In A B a b)
+        | ?f ?x
+          =>
+          let x_ty := type of x in


actually, we could just inspect the type of f here instead of x to make parameter/argument naming less confusing.

Ah, that seems wise, I'll do that.

andres-erbsen · 2017-11-25T15:40:18Z

src/Experiments/SimplyTypedArithmetic.v

+        | (fun x : ?T => ?f)
+          =>
+          (*let dummy := match goal with _ => idtac "funcase delaying" delayed_arguments end in*)
+          lazymatch delayed_arguments with


Could we branch on T here instead, only consuming the arguments list when T is a template parameter?

Yes, though then I should change cbv beta to something stronger like hnf, because we need to avoid the case where the type of the binder unifies with the type of the argument, but is syntactically different in a way that causes us to delay the argument and then miss it here, or vice versa (e.g., if we ever do Definition Type1 := Type.).

Could we change to consistently inspecting the function binder type, not the argument type?

Sure, but that's not enough for all cases (e.g., ((fun (T : Type) (x : T) => x) : forall T : Type1, T -> T) nat 0)). I think I have a decent way of switching to using unify, though.

Okay, it really does seem that alias unification (in the same sense as it came up for section records) is what we want here. I think I might be okay with just not supporting aliases for Type and Set, though. Also happy to look at your unify solution.

Unify solution presently at https://github.com/mit-plv/fiat-crypto/pull/275/files#diff-d6d787cba38e2097ad545be3240b32feR484

As per mit-plv#275 (comment)

JasonGross · 2017-11-26T19:22:47Z

E.g. we could just keep an ordered list of template arguments, using them on demand.

Updated to do that

andres-erbsen · 2017-11-26T19:28:16Z

src/Experiments/SimplyTypedArithmetic.v

+    first [ unify parameter_type Prop
+          | unify parameter_type Set
+          | unify parameter_type Type
+          | lazymatch eval hnf in parameter_type with


Could we ask for more fine-grained reduction here by trying to unify with the match pattern instead of calling hnf and then doing a syntactic check?

unify doesn't work on uconstrs, so unify parameter_type (_ -> _) will always fail. I could make an open_constr first, but that's clunky and not exactly fine-grained; I guess one way is:

let T := open_constr:(_) in let arrow := open_constr:(_ -> T) in unify parameter_type arrow; require_template_parameter T

Is that better?

What is the difference beteewen uconstr and openconstr? What does the change from one to another require? Is using an arrow instead of a forall intentional?

If I write unify p (_ -> _), _ -> _ gets interpreted as a ... constr, I think? The implicit cast from uconstr to constr requires that all holes be fillable by type inference. The "cast" from uconstr to open_constr fills uninferrable holes with evars. (constr and uconstr roughly correspond to actual datatypes, while open_constr is just a description of how to fill holes, roughly) What I am saying here is that I need the extra two let lines because the default unify syntax will try to fill the holes too early.

The change from a forall to an arrow is suboptimal, but we already can't handle any of the cases where I can imagine it coming up (things that look like recursion principles of length-indexed lists). If we use forall, then we need to reintroduce tactics in terms. I'm confused by your objection to hnf + match, though; can you add a bit more?

hnf is one of the things I assume to be arbitrarily slow (in case the next match fails, in particular). Unification too, but I am less angry at unification in types. Feel free to change back to hnf if you feel better about it.

hnf is differently arbitrarily slow than unification. (Note that I am doing hnf in a type, here. It'd probably even be safe to do cbv / compute.) In particular, if unify is faster than hnf in this case, it will be because unify performs more beta reduction and leaves over fewer things of the form (fun _ => <small term>) <big term>. In this case, I'm making use of the fact that I absolutely need to know whether or not the term is headed by forall, and that hnf stops evaluating when it hits forall.

Yeah, I think what I was saying is that we don't need to know what the head symbol is if it is not a function type constructor. Use your judgement for which command to use.

Sure. I'm leaving it as hnf. I think I see the algorithm you're proposing (first check if it's a forall, which should be fast, since you only need a very limited form of beta, then, if it is, pull out the type). However, there isn't actually a primitive for this, and unify doesn't follow this strategy, I believe.

andres-erbsen · 2017-11-26T19:29:24Z

src/Experiments/SimplyTypedArithmetic.v

+                 idtac
+            end ].
+  Ltac is_template_parameter parameter_type :=
+    run_tactic_as_bool ltac:(fun _ => require_template_parameter parameter_type).


run_tactic_as_bool -> is_success or is_succeeding or sth?

Mmm, I'm not sure about this. The semantics are that it runs a tactic during tactic expression evaluation, and returns a constr indicating success or failure. I use it to build a more general constr_tryif_then_else:

fiat-crypto/src/Util/Tactics/RunTacticAsConstr.v

Lines 16 to 23 in 6c7913c

(** Runs a tactic during expression evaluation phase; on success,

returns [then_tac ()], otherwise returns [else_tac ()] *)

Ltac constr_tryif_then_else tac then_tac else_tac :=

let success := run_tactic_as_bool tac in

lazymatch success with

| true => then_tac ()

| false => else_tac ()

end.

I could use this (though it may be a bit awkward). Or maybe is_success_run_tactic?

is_success_run_tactic sounds okay, I also don't really care

andres-erbsen · 2017-11-26T21:46:48Z

src/Experiments/SimplyTypedArithmetic.v

+
+  Ltac plug_delayed_arguments f delayed_arguments :=
+    lazymatch delayed_arguments with
+    | tt => f


Is tt acting as a list nil here?

Please document the delayed_arguments substitution context representation in a comment.

andres-erbsen · 2017-11-26T21:58:13Z

src/Experiments/SimplyTypedArithmetic.v

+                   constr:(I : I)
+            end
+          end
+        | _


Please add a comment explaining why this needs to be the default case.

I'm not sure what to say in the comment. "This must come last because we're using lazymatch"? Or "This must be here because we do in fact need to reify [op]s"? Or something else? I'm not sure what I'm explaining: that this case is present, that it's last, that it's run whenever the only cases don't match, that it's run only when the other cases don't match, or that there's no other cases to handle when none of the others match (or something else)

Why can't we write an actual pattern in this case, instead of _? Why do we need to use a catch-all instead of something more specific.

andres-erbsen · 2017-11-26T21:59:42Z

src/Experiments/SimplyTypedArithmetic.v

+            lazymatch rf0 with
+            | (fun _ => ?rf)
+              => constr:(@Abs var rT _ rf)
+            | _ => let dummy := match goal with


Please add a comment explaining when this case might happen.

andres-erbsen · 2017-11-26T22:03:38Z

src/Experiments/SimplyTypedArithmetic.v

+      end
+    end.
+
+  Ltac reify_helper var term ctx delayed_arguments :=


Proposed rename: value_ctx and template_ctx

andres-erbsen · 2017-11-26T22:04:31Z

src/Experiments/SimplyTypedArithmetic.v

+             reify_rec (@Let_In A B a b)
+        | ?f ?x
+          =>
+          let ty := get_first_argument_type f in


type_of_first_argument_of

andres-erbsen · 2017-11-26T22:08:22Z

This might be the last set of comments I have. I think at this point handling of template-arguments is essentially as systematic as the handling of runtime arguments in ctx, and what remains is to make that convention obvious from code and comments.

As per #275 (comment)

It's rather verbose, unfortunately. The reification also doesn't have any of the nice debugging features of the version of reification in Compilers, because that's even more boilerplate. Not sure if I should add that back in, at the moment. Also, for some strange reason, places where `constr`s fail to typecheck seem to induce backtracking where I don't think they should, and I'm not sure what's going on...

As per code review suggestions

As per mit-plv#275 (comment)

We no longer pass around dummy markers in the tuple of arguments.

This time without exponential slowdown in failure cases and without needing to manually think up all of the possible errors and write them out. Possible thanks to Hugo's comment at coq/coq#6252 (comment)

andres-erbsen · 2017-11-26T23:04:23Z

src/Experiments/SimplyTypedArithmetic.v

+    | forall x : ?T, _ => T
+    end.
+
+  (** Template parameters (things whose type or codomain is [Type],


Suggestion: Forms of abstraction in Gallina that our reflective language cannot handle get handled by specializing the code "template" to each particular application of that abstraction. In particular, type arguments (Type, Set, Prop) get substituted into lambdas and treated as a integral part of primitive operations (such as @List.app T). During reification...

Updated to

- (** Template parameters (things whose type or codomain is [Type], - [Set] or [Prop]) get handled specially, because our PHOAS - representation does not support dependent types. During + (** Forms of abstraction in Gallina that our reflective language + cannot handle get handled by specializing the code "template" to + each particular application of that abstraction. In particular, + type arguments (nat, Z, (λ _, nat), etc) get substituted into + lambdas and treated as a integral part of primitive operations + (such as [@List.app T], [@list_rect (λ _, nat)]). During

andres-erbsen · 2017-11-26T23:14:31Z

src/Experiments/SimplyTypedArithmetic.v

+              => constr:(@Abs var rT _ rf)
+            | _
+              => (* This will happen if the reified term still
+              mentions the non-var variable.  By chance, [cbv delta]


What do casts have to do with this?

If you do something really silly like try to reify (fun x : nat => S (O : (fun _ => nat) x)), by chance, cbv delta strips away the cast and has us reifying S O under the binder. If instead we passed S (O : (fun _ => nat) x) to reify_op, the term we get back is @op.Const type.nat (S (O : (fun _ => nat) x)). This term would trigger this error message, because it would still mention the binder x.

I can't think of any other way to get x into the reified term, because we pull everything except for constants apart to reify them, but that doesn't mean I thought of everything.

andres-erbsen · 2017-11-26T23:17:01Z

Feel free to change comments as you wish / in response to things I may have said and forgotten about, but I think it is also fair to call this done. I am actually really happy with how this turned out, including the initial version which was much more digestible than what I was afraid of at last meeting.

JasonGross requested a review from andres-erbsen November 24, 2017 20:25

JasonGross added this to To Do in Pipeline without CPS via automation Nov 24, 2017

andres-erbsen reviewed Nov 24, 2017

View reviewed changes

andres-erbsen reviewed Nov 25, 2017

View reviewed changes

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Nov 25, 2017

Rename is_type_arg to is_template_parameter

8cbf403

As per mit-plv#275 (comment)

andres-erbsen reviewed Nov 25, 2017

View reviewed changes

JasonGross force-pushed the reification-in-demo branch from 8cbf403 to 17f2fba Compare November 26, 2017 19:22

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Nov 26, 2017

Rename is_type_arg to is_template_parameter

f30191e

As per mit-plv#275 (comment)

andres-erbsen reviewed Nov 26, 2017

View reviewed changes

JasonGross added a commit that referenced this pull request Nov 26, 2017

Rename run_tactic_as_bool to is_success_run_tactic

b165133

As per #275 (comment)

JasonGross added 6 commits November 26, 2017 17:41

[demo] Add more namespacing

8a51550

Update llet notation, update is_known_const name

055b3c2

As per code review suggestions

Namespace var_context, add some coqbug references

547c195

Rename is_type_arg to is_template_parameter

fd27382

As per mit-plv#275 (comment)

Simplify the logic around delayed arguments a bit

a11ceeb

We no longer pass around dummy markers in the tuple of arguments.

JasonGross force-pushed the reification-in-demo branch from 71b415c to 1077e4f Compare November 26, 2017 22:57

JasonGross added 2 commits November 26, 2017 18:00

[demo] More informative reification error messages

3bf1476

This time without exponential slowdown in failure cases and without needing to manually think up all of the possible errors and write them out. Possible thanks to Hugo's comment at coq/coq#6252 (comment)

[demo] respond to code review, add comments

7a6a548

JasonGross force-pushed the reification-in-demo branch from 1077e4f to 7a6a548 Compare November 26, 2017 23:00

andres-erbsen reviewed Nov 26, 2017

View reviewed changes

Update documentation with suggestions from Andres

ba9f695

andres-erbsen reviewed Nov 26, 2017

View reviewed changes

andres-erbsen approved these changes Nov 26, 2017

View reviewed changes

JasonGross merged commit 499b76f into mit-plv:master Nov 26, 2017

Pipeline without CPS automation moved this from To Do to Done Nov 26, 2017

JasonGross deleted the reification-in-demo branch November 26, 2017 23:25

	(** Runs a tactic during expression evaluation phase; on success,
	returns [then_tac ()], otherwise returns [else_tac ()] *)
	Ltac constr_tryif_then_else tac then_tac else_tac :=
	let success := run_tactic_as_bool tac in
	lazymatch success with
	\| true => then_tac ()
	\| false => else_tac ()
	end.

[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v #275

[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v #275

Conversation

JasonGross commented Nov 24, 2017

andres-erbsen left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JasonGross commented Nov 25, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

andres-erbsen commented Nov 25, 2017

andres-erbsen commented Nov 25, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JasonGross commented Nov 26, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

andres-erbsen commented Nov 26, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment