Add Refl / Use in System F.

The term Refl is a proof of a type equality TyEq(ty1,ty2) and Use is a construct that introduce a type equality in the typing context.
This commit is contained in:
Olivier 2022-09-12 09:56:57 +02:00
parent bc9ebf36a9
commit 76a12e18b4
7 changed files with 93 additions and 22 deletions

View File

@ -71,6 +71,8 @@ type ('a, 'b) term =
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of range * ('a,'b) typ
| Refl of range * ('a,'b) typ
| Use of range * ('a,'b) term * ('a,'b) term
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
@ -227,6 +229,13 @@ module TypeInTerm : DeBruijn.TRAVERSE
| Absurd (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
Absurd (pos, ty')
| Refl (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
Refl (pos, ty')
| Use (pos, t, u) ->
let t' = trav env t in
let u' = trav env u in
Use (pos, t', u')
and traverse_datatype lookup extend env (tid, tyargs) =
(tid, List.map (TypeInType.traverse lookup extend env) tyargs)

View File

@ -74,6 +74,8 @@ type ('a, 'b) term =
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of range * ('a,'b) typ
| Refl of range * ('a,'b) typ
| Use of range * ('a,'b) term * ('a,'b) term
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term

View File

@ -88,6 +88,12 @@ let rec translate_term env (t : F.nominal_term) : P.term =
)
| F.Absurd (_, ty) ->
P.Absurd (translate_type env ty)
| F.Refl (_, ty) ->
P.Refl (translate_type env ty)
| F.Use (_, t, u) ->
let t' = self env t in
let u' = self env u in
P.Use (t', u')
and translate_branch env (pat, t) =
(translate_pattern env pat, translate_term env t)
@ -196,9 +202,16 @@ let print_type_error e =
str "Type error." ++
str "This type should be a universal type:" ++
print_db_type ty
| NotAnEqual ty ->
str "Type error." ++
str "This type should be an equality type:" ++
print_db_type ty
| UnboundTermVariable x ->
str "Scope error." ++
str "The variable %s is unbound." x
| TwoOccurencesOfSameVariable x ->
str "Scope error." ++
str "The variable %s is bound twice in a pattern." x
| ContextNotAbsurd ->
str "Type error." ++
str "The context is not absurd"

View File

@ -6,8 +6,10 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
and arity_requirement = Index of int | Total of int
@ -61,10 +63,13 @@ type env = {
types: debruijn_type TermVarMap.t;
(* A translation environment of TERM variables to TYPE indices. *)
names: N2DB.env;
(* the global store of the union-find *)
(* The global store of the union-find. *)
store: structure option UF.store;
(* a mapping from rigid variables to union-find vertices *)
(* A mapping from rigid variables to union-find vertices. *)
tyvars: structure option UF.elem list;
(* Is set to true hen an inconsistent equation is introduced in the
* environment. It is useful while typechecking pattern-matching. *)
consistent: bool;
}
let empty = {
@ -72,6 +77,7 @@ let empty = {
names = N2DB.empty;
store = UF.new_store();
tyvars = [];
consistent = true;
}
let lookup { types; names; _ } x =
@ -87,22 +93,23 @@ let lookup { types; names; _ } x =
(* must have been raised by [TermVarMap.find] *)
raise (TypeError (UnboundTermVariable x))
let extend_with_tevar { types; names; store; tyvars } x ty =
let extend_with_tevar { types; names; store; tyvars; consistent } x ty =
(* Map the name [x] to [ty], and record when it was bound, without
incrementing the time. *)
{ types = TermVarMap.add x ty types;
names = N2DB.slide names x;
store;
tyvars }
tyvars;
consistent; }
let extend_with_tyvar { types; names; store; tyvars } =
let extend_with_tyvar { types; names; store; tyvars; consistent } =
(* Create a fresh vertex for the new type variable *)
let v = UF.make store (Some (SForallLevel (List.length tyvars))) in
let v = UF.make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
let names = N2DB.bump names in
{ types; names ; store; tyvars }
{ types; names ; store; tyvars; consistent }
let singleton x ty =
extend_with_tevar empty x ty
@ -112,9 +119,9 @@ let concat env1 env2 =
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars
in
{ types; names; store; tyvars }
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
{ types; names; store; tyvars; consistent }
let concat_disjoint env1 env2 =
let exception Conflict of TermVarMap.key in
@ -124,9 +131,9 @@ let concat_disjoint env1 env2 =
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars
in
Ok { types; names; store; tyvars }
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
Ok { types; names; store; tyvars; consistent }
with Conflict x -> Error x
(* -------------------------------------------------------------------------- *)
@ -318,15 +325,17 @@ let unify_struct q s1 s2 =
| SForall _, _ ->
raise Clash
type mode = Check
type mode = Input | Check
let merge_struct mode q so1 so2 : structure option =
match so1, so2 with
| Some s1, Some s2 ->
unify_struct q s1 s2;
so1
| None, _so | _so, None ->
| None, so | so, None ->
match mode with
| Input ->
so
| Check ->
raise Clash
@ -345,13 +354,17 @@ let unify mode store v1 v2 =
let q = Stack.create() in
unify mode store q v1 v2
let equal env ty1 ty2 =
(* The [mode] argument tells us if one should unify rigid variables with
* structure (Input mode) or if is not allowed (Check mode). *)
let equal mode env ty1 ty2 =
not env.consistent ||
try
let v1 = translate ~inside_mu:false env.store env.tyvars ty1
and v2 = translate ~inside_mu:false env.store env.tyvars ty2 in
unify Check env.store v1 v2;
unify mode env.store v1 v2;
true
with Clash ->
Printexc.print_raw_backtrace stdout (Printexc.get_raw_backtrace ());
false
(* -------------------------------------------------------------------------- *)
@ -359,7 +372,7 @@ let equal env ty1 ty2 =
(* Re-package the type equality test as a type equality check. *)
let (--) ty1 ty2 env : unit =
if not (equal env ty1 ty2) then
if not (equal Check env ty1 ty2) then
raise (TypeError (TypeMismatch (ty1, ty2)))
(* -------------------------------------------------------------------------- *)
@ -423,8 +436,28 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
let tys = List.map (typeof_branch datatype_env env scrutinee_ty) brs in
List.iter (fun ty2 -> (--) ty ty2 env) tys;
ty
| Absurd (_, _ty) ->
failwith "todo"
| Absurd (_, ty) ->
if env.consistent then
raise (TypeError (ContextNotAbsurd))
else
ty
| Refl (_, ty) ->
TyEq (ty, ty)
| Use (_, t, u) ->
let store_copy = UF.copy env.store in
let env = { env with store = store_copy } in
begin
match typeof env t with
| TyEq (ty1, ty2) ->
if equal Input env ty1 ty2 then
(* typecheck [u] in a context containing equalities introduced by
* the equality ty1 = ty2 *)
typeof env u
else
typeof { env with consistent = false } u
| ty ->
raise (TypeError (NotAnEqual ty))
end
and typeof_variant datatype_env lbl (tid, tyargs) =
let Datatype.{ data_kind ; type_params ; labels_descr; _ } =

View File

@ -8,8 +8,10 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
(* An arity-related requirement on a certain (sum or product) type
arising during type-checking:

View File

@ -35,6 +35,8 @@ type term =
| Variant of Datatype.label_id * datatype option * term option
| Match of typ option * term * branch list
| Absurd of typ
| Refl of typ
| Use of term * term
and branch = pattern * term

View File

@ -151,6 +151,11 @@ and print_term_abs t =
^^ print_pattern p ^^ space
^^ string "->"
^//^ print_term_abs t
| Use (t, u) ->
string "use" ^^ space
^^ print_term t
^^ space ^^ string "in" ^^ hardline
^^ print_term u
| t ->
print_term_app t
@ -167,6 +172,11 @@ and print_term_app t =
^^ space ^^ print_term_atom t
| Variant (lbl, dty, t) ->
print_variant lbl dty print_term_atom t
| Refl ty ->
group (
string "Refl"
^^ print_angle_type ty
)
| t ->
print_term_atom t
@ -186,8 +196,8 @@ and print_term_atom t =
print_annot (print_term t) tyannot
| Absurd _ ->
dot
| TyAbs _ | Let _ | Abs _
| TyApp _ | App _ | Proj _ | Inj _ | Variant _ as t ->
| TyAbs _ | Let _ | Abs _ | Use _
| TyApp _ | App _ | Proj _ | Inj _ | Variant _ | Refl _ as t ->
parens (print_term t)
and print_match ty scrutinee brs =