Remove useless [params] argument in [convert].

introduce-rigid
Olivier 3 months ago
parent ffa2926759
commit 4871534e80

@ -253,12 +253,12 @@ let rec map_co (f : 'a -> 'b co) : 'a list -> 'b list co
and+ ys = map_co f xs
in y :: ys
let rec convert_deep (env : ML.datatype_env) rigid_env
(params : (ML.tyvar * variable) list) (ty : ML.typ) : deep_ty =
let conv ty = convert_deep env rigid_env params ty in
let rec convert_deep (env : ML.datatype_env)
(tyvar_env : (ML.tyvar * variable) list) (ty : ML.typ) : deep_ty =
let conv ty = convert_deep env tyvar_env ty in
match ty with
| ML.TyVar (_, tx) ->
let tx' = List.assoc tx (params @ rigid_env) in
let tx' = List.assoc tx tyvar_env in
DeepVar tx'
| ML.TyArrow (_, ty1, ty2) ->
@ -270,8 +270,8 @@ let rec convert_deep (env : ML.datatype_env) rigid_env
| ML.TyConstr (_, tid, tys) ->
DeepStructure (S.TyConstr(tid, List.map conv tys))
let convert env rigid_env params ty =
let deep_ty = convert_deep env rigid_env params ty in
let convert env tyvar_env ty =
let deep_ty = convert_deep env tyvar_env ty in
deep deep_ty
(* -------------------------------------------------------------------------- *)
@ -313,7 +313,7 @@ type type_env = (ML.tevar * variable) list
let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.nominal_term co
=
let rec hastype rigid_env t w =
let rec hastype tyvar_env t w =
let loc = get_loc t in
correlate loc @@
match t with
@ -337,7 +337,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let+ () = w --- arrow v1 v2
(* Under the assumption that [x] has type [domain], the term [u] must
have type [codomain]. *)
and+ u' = def (X.Var x) v1 (hastype rigid_env u v2)
and+ u' = def (X.Var x) v1 (hastype tyvar_env u v2)
and+ ty1 = decode v1
in
(* Once these constraints are solved, we obtain the translated function
@ -350,24 +350,24 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(* Introduce a type variable to stand for the unknown argument type. *)
let@ v = exist in
let+ t1' = lift (hastype rigid_env) t1 (arrow v w)
and+ t2' = hastype rigid_env t2 v
let+ t1' = lift (hastype tyvar_env) t1 (arrow v w)
and+ t2' = hastype tyvar_env t2 v
in F.App (loc, t1', t2')
(* Generalization. *)
| ML.Let (loc, rec_, x, t, u) ->
let hastype_def x t v =
match rec_ with
| ML.Non_recursive -> hastype rigid_env t v
| ML.Non_recursive -> hastype tyvar_env t v
| ML.Recursive ->
(* For recursive definitions [let rec x = t], we bind the
variable [x] to the monomorphic expected type of [t] when
inferring the type of [t] itself. *)
def (X.Var x) v (hastype rigid_env t v)
def (X.Var x) v (hastype tyvar_env t v)
in
(* Construct a ``let'' constraint. *)
let+ (a, (b, ty), t', u') =
let1 (X.Var x) (hastype_def x t) (hastype rigid_env u w) in
let1 (X.Var x) (hastype_def x t) (hastype tyvar_env u w) in
(* [a] are the type variables that we must bind (via Lambda abstractions)
while type-checking [t]. [(b, _)] is the type scheme that [x] must
receive while type-checking [u]. Its quantifiers [b] are guaranteed to
@ -418,9 +418,9 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
u'))
| ML.Annot (loc, t, ty) ->
let@ v = convert typedecl_env rigid_env [] ty in
let@ v = convert typedecl_env tyvar_env ty in
let+ () = v -- w
and+ t' = hastype rigid_env t v
and+ t' = hastype tyvar_env t v
and+ ty' = decode v
in F.Annot (loc, t', ty')
@ -441,8 +441,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let+ (alphas, (betas, _), t', tys) =
letr1 (List.length tyvars) x
(fun vs z ->
let rigid_env' = List.combine tyvars vs @ rigid_env in
let+ t' = hastype rigid_env' t z
let tyvar_env' = List.combine tyvars vs @ tyvar_env in
let+ t' = hastype tyvar_env' t z
in t'
) (instance x w)
in
@ -453,14 +453,14 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let@ v = exist in k (alpha, v)
in
let@ new_bindings = mapM_now on_tyvar tyvars in
let rigid_env' = new_bindings @ rigid_env in
hastype rigid_env' t w
let tyvar_env' = new_bindings @ tyvar_env in
hastype tyvar_env' t w
| ML.Tuple (loc, ts) ->
let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
fun (k : ('b * 'c co) -> 'r co) : 'r co ->
let@ v : 'b = exist in
let t = hastype rigid_env t v in
let t = hastype tyvar_env t v in
k (v, t)
in
@ -477,12 +477,12 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
in
let@ vs = mapM_now on_var xs in
let+ t' = lift (hastype rigid_env) t (product vs)
and+ u' = hastype rigid_env u w
let+ t' = lift (hastype tyvar_env) t (product vs)
and+ u' = hastype tyvar_env u w
in F.LetProd(loc, xs, t', u')
| ML.Variant (loc, c, t) ->
let@ (dty, v) = hastype_variant typedecl_env rigid_env ~loc c w in
let@ (dty, v) = hastype_variant typedecl_env tyvar_env ~loc c w in
let+ dty = dty
and+ t' =
@ -490,7 +490,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
| None ->
pure (F.Tuple (loc, []))
| Some t ->
hastype rigid_env t v
hastype tyvar_env t v
in F.Variant (loc, c, dty, t')
| ML.Match (loc, t, branches) ->
@ -498,9 +498,9 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(and of the patterns) *)
let@ v = exist in
let@ branches' = hastype_branches rigid_env typedecl_env branches w v in
let@ branches' = hastype_branches tyvar_env typedecl_env branches w v in
let+ t = hastype rigid_env t v
let+ t = hastype tyvar_env t v
and+ branches' = branches'
and+ ty = decode w
in F.Match (loc, ty, t, branches')
@ -512,13 +512,13 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
variable. *)
let on_subterm t k =
let@ v = exist in
k (hastype rigid_env t v) in
k (hastype tyvar_env t v) in
let@ ts' = mapM_later on_subterm ts in
let+ ts' = ts'
and+ ty = decode w
in F.Hole (loc, ty, ts')
and hastype_variant typedecl_env rigid_env ~loc c w
and hastype_variant typedecl_env tyvar_env ~loc c w
: (F.nominal_datatype co * variable, 'r) binder
= fun k ->
let Datatype.{ type_name ; arg_type ; _ } =
@ -554,13 +554,14 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let sum_type = constr type_name type_param_vars in
let@ argument_v = convert typedecl_env rigid_env type_param_dict arg_type in
let@ argument_v =
convert typedecl_env (type_param_dict @ tyvar_env) arg_type in
let+ () = w --- sum_type
and+ r = k (dty, argument_v)
in r
and hastype_branches rigid_env typedecl_env branches v_return v_scrutinee
and hastype_branches tyvar_env typedecl_env branches v_return v_scrutinee
: (F.nominal_branch list co, 'r) binder
=
@ -572,7 +573,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
| [] ->
(* Here we use [v_return] because [t] should have the same type
as the whole match statement *)
hastype rigid_env u v_return
hastype tyvar_env u v_return
| (x, v1) :: pat_env ->
def (X.Var x) v1 @@ bind_pattern_vars pat_env u
in
@ -580,7 +581,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let on_branch ((pat,u) : ML.branch)
: (F.nominal_branch co, 'r) binder
= fun k ->
let@ (pat_env, pat) = hastype_pat typedecl_env rigid_env pat v_scrutinee in
let@ (pat_env, pat) = hastype_pat typedecl_env tyvar_env pat v_scrutinee in
let u = bind_pattern_vars pat_env u in
@ -594,7 +595,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(* [hastype_pat pat v] returns a type environment, containing term variables
associated with solver variables, and a System F pattern *)
and hastype_pat typedecl_env rigid_env pat w
and hastype_pat typedecl_env tyvar_env pat w
: (type_env * F.nominal_pattern co, 'r) binder
= fun k ->
match pat with
@ -606,8 +607,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
k ([], pure (F.PWildcard loc))
| ML.PAnnot (loc, pat, ty) ->
let@ v = convert typedecl_env rigid_env [] ty in
let@ (pat_env, pat) = hastype_pat typedecl_env rigid_env pat v in
let@ v = convert typedecl_env tyvar_env ty in
let@ (pat_env, pat) = hastype_pat typedecl_env tyvar_env pat v in
let+ () = v -- w
and+ res = k (pat_env,
let+ pat = pat
@ -637,7 +638,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
* F.nominal_pattern co, 'r) binder
= fun k ->
let@ v = exist in
let@ (pat_env, pat) = hastype_pat typedecl_env rigid_env pat v in
let@ (pat_env, pat) = hastype_pat typedecl_env tyvar_env pat v in
k ((v,pat_env), pat)
in
@ -651,7 +652,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
in F.PTuple (loc, pats))
| ML.PVariant (loc, c, pat) ->
let@ (dty, v) = hastype_variant typedecl_env rigid_env ~loc c w in
let@ (dty, v) = hastype_variant typedecl_env tyvar_env ~loc c w in
let@ (pat_env, pat') =
match pat with
@ -659,7 +660,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(fun k ->
k ([], pure (F.PTuple (loc, []))))
| Some pat ->
hastype_pat typedecl_env rigid_env pat v
hastype_pat typedecl_env tyvar_env pat v
in
k(pat_env,
let+ dty = dty

Loading…
Cancel
Save