Create a new input syntax for function.

[DavidFangWJ]

Motivation

Add a more compact syntax to function, such that

let f(x : A, y: B) = e

should behave the same as below:

let f : (A, B) = fun (x, y) -> e

This new function syntax is more analogous to other programming languages with strong data types, and is therefore easier to learn.

Implementation Details

According to the current structure, there following files are modified.

• For Info.re, a new field rewrite_id is introduced, which registers the correspondence between the rewritten Exp.t and the original one.
• For StaticsBase.re, check_annotated_function is introduced to check whether the function is in the new specified syntax, passed as Let(Ap, ...).
• For Statics.re and Elaborator.re, additional code are introduced to process the new syntax.
• For ExplainThis.re and AppPat.re, additional explanation categories are introduced.

[cyrus-]

@DavidFangWJ We shouldn't actually need to modify Form.re to accomplish this, since the syntax of patterns already includes application and annotations:

We will need to change how patterns in let bindings are processed in the statics and elaboration to special case the situation where the top-level pattern is x(p1[: t1], ..., pn[: tn])[ : t].

[cyrus-]

Regarding the type error, take a look at the definition of UPat.t -- it is a record type, because terms have unique IDs, so you need to decompose it like the other functions working on UPat's do.

Regarding the function itself, you should be looking for the application of a variable, rather than a constructor. Constructors are capitalized.

You also do not need to check that all arguments have type annotations -- it is okay to leave an argument unannotated, it will just get the unknown type.

You also need to handle optional return type annotations (which will require changing the return type of your function overall).

Please write some additional examples in your PR message to handle both functions with missing type annotations on arguments and missing return types, so make it clear these are all valid. We'll turn these into tests as well.

[DavidFangWJ]

Cannot fully understand the part in Statics.re/uexp_to_info_map regarding the process of let binding, which looks like this:

  | Let(p, def, body) =>
    let (p_syn, _) =
      go_pat(~is_synswitch=true, ~co_ctx=CoCtx.empty, ~mode=Syn, p, m);
    let (def, p_ana_ctx, m, ty_p_ana) =
      if (!is_recursive(ctx, p, def, p_syn.ty)) {
        let (def, m) = go(~mode=Ana(p_syn.ty), def, m);
        let ty_p_ana = def.ty;
        let (p_ana', _) =
          go_pat(
            ~is_synswitch=false,
            ~co_ctx=CoCtx.empty,
            ~mode=Ana(ty_p_ana),
            p,
            m,
          );
        (def, p_ana'.ctx, m, ty_p_ana);
      } else {
        let (def_base, _) =
          go'(~ctx=p_syn.ctx, ~mode=Ana(p_syn.ty), def, m);
        let ty_p_ana = def_base.ty;
        /* Analyze pattern to incorporate def type into ctx */
        let (p_ana', _) =
          go_pat(
            ~is_synswitch=false,
            ~co_ctx=CoCtx.empty,
            ~mode=Ana(ty_p_ana),
            p,
            m,
          );
        let def_ctx = p_ana'.ctx;
        let (def_base2, _) = go'(~ctx=def_ctx, ~mode=Ana(p_syn.ty), def, m);
        let ana_ty_fn = ((ty_fn1, ty_fn2), ty_p) => {
          ty_p == Typ.Unknown(SynSwitch) && !Typ.eq(ty_fn1, ty_fn2)
            ? ty_fn1 : ty_p;
        };
        let ana =
          switch ((def_base.ty, def_base2.ty), p_syn.ty) {
          | ((Prod(ty_fns1), Prod(ty_fns2)), Prod(ty_ps)) =>
            let tys =
              List.map2(ana_ty_fn, List.combine(ty_fns1, ty_fns2), ty_ps);
            Typ.Prod(tys);
          | ((ty_fn1, ty_fn2), ty_p) => ana_ty_fn((ty_fn1, ty_fn2), ty_p)
          };
        let (def, m) = go'(~ctx=def_ctx, ~mode=Ana(ana), def, m);
        (def, def_ctx, m, ty_p_ana);
      };
    let (body, m) = go'(~ctx=p_ana_ctx, ~mode, body, m);
    /* add co_ctx to pattern */
    let (p_ana, m) =
      go_pat(
        ~is_synswitch=false,
        ~co_ctx=body.co_ctx,
        ~mode=Ana(ty_p_ana),
        p,
        m,
      );
    add(
      ~self=Just(body.ty),
      ~co_ctx=
        CoCtx.union([def.co_ctx, CoCtx.mk(ctx, p_ana.ctx, body.co_ctx)]),
      m,
    );

[cyrus-]

@DavidFangWJ there is a small merge conflict + the following has an error on f:

[cyrus-]

@DavidFangWJ The ExplainThis description for function definition should say something like "Defines a function f with arguments x", not the same message as constructor binding.

[cyrus-]

@DavidFangWJ functionality looks good, but take a look at my comments. please write up an explanation for how the rewriting works in general as well in the PR description.