Param types update

src/haz3lcore/dynamics/DH.re

@@ -21,9 +21,9 @@ module rec DHExp: {
     | Let(DHPat.t, t, t)
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
+    | Ap(t, t)
     | TypFun(Term.UTPat.t, t)
     | TypAp(t, Typ.t)
-    | Ap(t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)
@@ -82,9 +82,9 @@ module rec DHExp: {
     | Let(DHPat.t, t, t)
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
+    | Ap(t, t)
     | TypFun(Term.UTPat.t, t)
     | TypAp(t, Typ.t)
-    | Ap(t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)

src/haz3lcore/dynamics/Elaborator.re

@@ -27,7 +27,7 @@ let fixed_pat_typ = (m: Statics.Map.t, p: Term.UPat.t): option(Typ.t) =>
   | _ => None
   };
 
-let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
+let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) => {
   switch (mode) {
   | Syn => d
   | SynFun =>
@@ -75,12 +75,13 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
       | _ => d
       }
     | Ap(NonEmptyHole(_, _, _, Constructor(_)), _)
-    | Ap(Constructor(_), _)
+    | Ap(Constructor(_) | TypAp(_), _)
     | TypAp(Constructor(_), _)
     | Constructor(_) =>
       switch (ana_ty, self_ty) {
       | (Unknown(prov), Rec(_, Sum(_)))
-      | (Unknown(prov), Sum(_)) => DHExp.cast(d, self_ty, Unknown(prov))
+      | (Unknown(prov), Ap(_) | Sum(_)) =>
+        DHExp.cast(d, self_ty, Unknown(prov))
       | _ => d
       }
     /* Forms with special ana rules but no particular typing requirements */
@@ -122,7 +123,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
       DHExp.cast(d, self_ty, ana_ty)
     };
   };
-
+};
 /* Handles cast insertion and non-empty-hole wrapping
    for elaborated expressions */
 let wrap = (ctx: Ctx.t, u: Id.t, mode: Mode.t, self, d: DHExp.t): DHExp.t =>
@@ -253,13 +254,13 @@ let rec dhexp_of_uexp =
           DHExp.Let(dp, add_name(Term.UPat.get_var(p), ddef), dbody)
         | Some([f]) =>
           /* simple recursion */
-          Let(dp, FixF(f, ty, add_name(Some(f), ddef)), dbody)
+          Let(dp, FixF(f, ty, add_name(Some(f ++ "+"), ddef)), dbody)
         | Some(fs) =>
           /* mutual recursion */
           let ddef =
             switch (ddef) {
             | Tuple(a) =>
-              DHExp.Tuple(List.map2(s => add_name(Some(s)), fs, a))
+              DHExp.Tuple(List.map2(s => add_name(Some(s ++ "+")), fs, a))
             | _ => ddef
             };
           let uniq_id = List.nth(def.ids, 0);

src/haz3lcore/dynamics/Stepper.re

@@ -417,6 +417,7 @@ let get_justification: step_kind => string =
   | VarLookup => "variable lookup"
   | CastAp
   | Cast => "cast calculus"
+  | FixClosure => "fixpoint closure"
   | CompleteFilter => "complete filter"
   | CompleteClosure => "complete closure"
   | FunClosure => "function closure"

src/haz3lcore/dynamics/Transition.re

@@ -52,6 +52,7 @@ type step_kind =
   | LetBind
   | FunClosure
   | FixUnwrap
+  | FixClosure
   | UpdateTest
   | TypFunAp
   | FunAp
@@ -131,6 +132,7 @@ module CastHelpers = {
     | Arrow(_, _) => grounded_Arrow
     | Forall(_) => grounded_Forall
     | List(_) => grounded_List
+    | Ap(_) => NotGroundOrHole(Ap(Unknown(Internal), Unknown(Internal)))
     };
   };
 };
@@ -229,15 +231,15 @@ module Transition = (EV: EV_MODE) => {
         kind: FunClosure,
         value: true,
       });
+    | FixF(f, _, Closure(env, d1)) =>
+      let. _ = otherwise(env, d);
+      let env' = evaluate_extend_env(Environment.singleton((f, d)), env);
+      Step({apply: () => Closure(env', d1), kind: FixUnwrap, value: false});
     | FixF(f, t, d1) =>
       let. _ = otherwise(env, FixF(f, t, d1));
       Step({
-        apply: () =>
-          Closure(
-            evaluate_extend_env(Environment.singleton((f, d1)), env),
-            d1,
-          ),
-        kind: FixUnwrap,
+        apply: () => FixF(f, t, Closure(env, d1)),
+        kind: FixClosure,
         value: false,
       });
     | Test(id, d) =>
@@ -278,6 +280,9 @@ module Transition = (EV: EV_MODE) => {
           /* Treat a hole or invalid tyvar name as a unique type variable that doesn't appear anywhere else. Thus instantiating it at anything doesn't produce any substitutions. */
           Step({apply: () => tfbody, kind: TypFunAp, value: false})
         }
+      | Constructor(name) =>
+        /* Rule ITTCon */
+        Step({apply: () => Constructor(name), kind: TypFunAp, value: false})
       | Cast(d'', Forall(x, t), Forall(x', t')) =>
         /* Rule ITTApCast */
         Step({
@@ -712,9 +717,10 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) =>
   | VarLookup => !settings.show_lookup_steps
   | CastAp
   | Cast => !settings.show_casts
+  | FixUnwrap => !settings.show_fixpoints
   | CaseNext
   | CompleteClosure
   | CompleteFilter
-  | FixUnwrap
   | BuiltinWrap
-  | FunClosure => true;
+  | FunClosure
+  | FixClosure => true;

src/haz3lcore/lang/Form.re

@@ -161,6 +161,7 @@ let is_var = str =>
      );
 let is_capitalized_name = regexp("^[A-Z][A-Za-z0-9_]*$");
 let is_ctr = is_capitalized_name;
+let is_type_input = regexp("^[a-z]*$");
 let base_typs = ["String", "Int", "Float", "Bool"];
 let is_base_typ = regexp("^(" ++ String.concat("|", base_typs) ++ ")$");
 let is_typ_var = str => is_var(str) || is_capitalized_name(str);
@@ -216,6 +217,10 @@ let bad_token_cls: string => bad_token_cls =
    Order in this list determines relative remolding
    priority for forms with overlapping regexps */
 let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
+  ("ty_var", (is_typ_var, [mk_op(Typ, [])])),
+  ("ty_var_p", (is_typ_var, [mk_op(TPat, [])])),
+  ("ctr", (is_ctr, [mk_op(Exp, []), mk_op(Pat, [])])),
+  ("type", (is_base_typ, [mk_op(Typ, [])])),
   ("var", (is_var, [mk_op(Exp, []), mk_op(Pat, [])])),
   (
     "explicit_hole",
@@ -297,9 +302,11 @@ let forms: list((string, t)) = [
   ("parens_exp", mk(ii, ["(", ")"], mk_op(Exp, [Exp]))),
   ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))),
   ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))),
+  ("parens_tpat", mk(ii, ["(", ")"], mk_op(TPat, [TPat]))),
   ("ap_exp_empty", mk(ii, ["()"], mk_post(P.ap, Exp, []))),
   ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))),
   ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))),
+  ("ap_tpat", mk(ii, ["(", ")"], mk_post(P.ap, TPat, [TPat]))),
   ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))),
   ("ap_exp_typ", mk(ii, ["@<", ">"], mk_post(P.ap, Exp, [Typ]))),
   ("at_sign", mk_nul_infix("@", P.eqs)), // HACK: SUBSTRING REQ

src/haz3lcore/statics/Info.re

@@ -179,7 +179,8 @@ type error_tpat =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type ok_tpat =
   | Empty
-  | Var(TypVar.t);
+  | Var(TypVar.t)
+  | Ap(TypVar.t, TypVar.t);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_tpat =
@@ -366,7 +367,7 @@ let rec status_common =
     InHole(Inconsistent(Internal(Typ.of_source(tys))))
   };
 
-let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
+let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat => {
   switch (mode, self) {
   | (Syn | SynTypFun | Ana(_), Common(self_pat))
   | (SynFun, Common(IsConstructor(_) as self_pat)) =>
@@ -376,13 +377,22 @@ let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
        we catch them here, diverting to an ExpectedConstructor error. But we
        avoid capturing the second case above, as these will ultimately
        get a (more precise) unbound ctr  via status_common */
+    let self_pat: Self.t =
+      switch (self_pat) {
+      | IsConstructor({name, syn_ty: Some(Forall(name2, ty))}) =>
+        IsConstructor({
+          name,
+          syn_ty: Some(Typ.subst(Unknown(Internal), name2, ty)),
+        })
+      | _ => self_pat
+      };
     switch (status_common(ctx, mode, self_pat)) {
     | NotInHole(ok_exp) => NotInHole(ok_exp)
     | InHole(err_pat) => InHole(Common(err_pat))
-    }
+    };
   | (SynFun, _) => InHole(ExpectedConstructor)
   };
-
+};
 /* Determines whether an expression or pattern is in an error hole,
    depending on the mode, which represents the expectations of the
    surrounding syntactic context, and the self which represents the
@@ -406,7 +416,7 @@ let status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp =>
    free, and whether a ctr name is a dupe. */
 let status_typ =
     (ctx: Ctx.t, expects: typ_expects, term: TermBase.UTyp.t, ty: Typ.t)
-    : status_typ =>
+    : status_typ => {
   switch (term.term) {
   | Invalid(token) => InHole(BadToken(token))
   | EmptyHole => NotInHole(Type(ty))
@@ -422,9 +432,10 @@ let status_typ =
     | TypeExpected =>
       switch (Ctx.is_alias(ctx, name)) {
       | false =>
-        switch (Ctx.is_abstract(ctx, name)) {
+        switch (Ctx.is_tyVar(ctx, name)) {
         | false => InHole(FreeTypeVariable(name))
-        | true => NotInHole(Type(Var(name)))
+        | true =>
+          NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty)))
         }
       | true => NotInHole(TypeAlias(name, Typ.weak_head_normalize(ctx, ty)))
       }
@@ -439,7 +450,17 @@ let status_typ =
       | _ => NotInHole(VariantIncomplete(Arrow(ty_in, ty_variant)))
       };
     | ConstructorExpected(_) => InHole(WantConstructorFoundAp)
-    | TypeExpected => InHole(WantTypeFoundAp)
+    | TypeExpected =>
+      let constructor =
+        switch (t1.term) {
+        | Var(s) => s
+        | _ => ""
+        };
+      switch (Ctx.is_tyVar(ctx, constructor)) {
+      | false => InHole(FreeTypeVariable(constructor))
+      | true =>
+        NotInHole(TypeAlias(constructor, Typ.weak_head_normalize(ctx, ty)))
+      };
     }
   | _ =>
     switch (expects) {
@@ -448,7 +469,7 @@ let status_typ =
     | VariantExpected(_) => InHole(WantConstructorFoundType(ty))
     }
   };
-
+};
 let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat =>
   switch (utpat.term) {
   | EmptyHole => NotInHole(Empty)
@@ -464,26 +485,43 @@ let status_tpat = (ctx: Ctx.t, utpat: UTPat.t): status_tpat =>
   | Var(name) => NotInHole(Var(name))
   | Invalid(_) => InHole(NotAVar(NotCapitalized))
   | MultiHole(_) => InHole(NotAVar(Other))
+  | Ap({term: Var(name), _}, {term: Var(_), _})
+      when Form.is_base_typ(name) || Ctx.lookup_alias(ctx, name) != None =>
+    let f = src => InHole(ShadowsType(name, src));
+    if (Form.is_base_typ(name)) {
+      f(BaseTyp);
+    } else if (Ctx.is_alias(ctx, name)) {
+      f(TyAlias);
+    } else {
+      f(TyVar);
+    };
+  | Ap({term: Var(name1), _}, {term: Var(name2), _}) =>
+    NotInHole(Ap(name1, name2))
+
+  | Ap(_) => InHole(NotAVar(Other))
   };
 
 /* Determines whether any term is in an error hole. */
 let is_error = (ci: t): bool => {
   switch (ci) {
   | InfoExp({mode, self, ctx, _}) =>
-    switch (status_exp(ctx, mode, self)) {
+    let status = status_exp(ctx, mode, self);
+    switch (status) {
     | InHole(_) => true
     | NotInHole(_) => false
-    }
+    };
   | InfoPat({mode, self, ctx, _}) =>
-    switch (status_pat(ctx, mode, self)) {
+    let status = status_pat(ctx, mode, self);
+    switch (status) {
     | InHole(_) => true
     | NotInHole(_) => false
-    }
+    };
   | InfoTyp({expects, ctx, term, ty, _}) =>
-    switch (status_typ(ctx, expects, term, ty)) {
+    let status = status_typ(ctx, expects, term, ty);
+    switch (status) {
     | InHole(_) => true
     | NotInHole(_) => false
-    }
+    };
   | InfoTPat({term, ctx, _}) =>
     switch (status_tpat(ctx, term)) {
     | InHole(_) => true