Create a new input syntax for function.

src/haz3lcore/lang/Form.re

@@ -300,6 +300,7 @@ let forms: list((string, t)) = [
   ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))),
   ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))),
   ("test", mk(ds, ["test", "end"], mk_op(Exp, [Exp]))),
+  // This is a potential place for modification
   ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   (
     "rule",

src/haz3lcore/statics/Statics.re

@@ -636,3 +636,63 @@ let collect_errors = (map: Map.t): list((Id.t, Info.error)) =>
     map,
     [],
   );
+
+/*
+ * Unwrap the input funtion's args (more than 1) into format check and types
+ */
+let caf_argtrans = (args: list(UPat.t)): option(list(UTyp.t)) =>
+  List.fold_right(
+    (item: UPat.t, partial: option(list(UTyp.t))) =>
+      switch (partial) {
+      | Some(lst_typ) =>
+        switch (item.term) {
+        | TypeAnn({ids: _, term: Var(_)}, t) => Some([t, ...lst_typ])
+        | Var(_) => Some([{ids: item.ids, term: EmptyHole}, ...lst_typ])
+        | _ => None
+        }
+      | _ => None
+      },
+    args,
+    Some([]),
+  );
+
+let check_annotated_function_helper =
+    (pat: UPat.t, ret_type: UTyp.t): option((Var.t, UPat.t, UTyp.t)) =>
+  switch (pat.term) {
+  | Ap({ids: _, term: Var(func_name)}, args) =>
+    let in_type_opt: option(UTyp.t) =
+      switch (args.term) {
+      | Var(_) => Some({ids: args.ids, term: EmptyHole})
+      | TypeAnn({ids: _, term: Var(_)}, t) => Some(t)
+      | Tuple(ps) =>
+        switch (caf_argtrans(ps)) {
+        | None => None
+        | Some(in_type) => Some({ids: args.ids, term: Tuple(in_type)})
+        }
+      | _ => None
+      };
+    switch (in_type_opt) {
+    | None => None
+    | Some(in_type) =>
+      Some((
+        func_name,
+        args,
+        {ids: pat.ids, term: Arrow(in_type, ret_type)},
+      ))
+    };
+  | _ => None
+  };
+
+/*
+ * Check whether a particular let binding is an annotated function under the new syntax.
+ * It is parsed as a constructor syntax.
+ * I am not sure what is the top-level pattern; the only thing similar seems to be UPat.Ap.
+ */
+let check_annotated_function =
+    (pat: UPat.t): option((Var.t, UPat.t, UTyp.t)) =>
+  switch (pat.term) {
+  | TypeAnn(inner_pat, ret_type) =>
+    check_annotated_function_helper(inner_pat, ret_type)
+  | _ =>
+    check_annotated_function_helper(pat, {ids: pat.ids, term: EmptyHole})
+  };