Add type equality in F.
This commit is contained in:
parent
36bad208b0
commit
36980073f3
|
@ -27,6 +27,7 @@ type ('a, 'b) typ =
|
|||
| TyForall of 'b * ('a, 'b) typ
|
||||
| TyMu of 'b * ('a, 'b) typ
|
||||
| TyConstr of ('a, 'b) datatype
|
||||
| TyEq of ('a, 'b) typ * ('a, 'b) typ
|
||||
|
||||
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
|
||||
|
||||
|
@ -149,7 +150,10 @@ module TypeInType : DeBruijn.TRAVERSE
|
|||
let env, x = extend env x in
|
||||
let ty1' = trav env ty1 in
|
||||
TyMu (x, ty1')
|
||||
|
||||
| TyEq (ty1, ty2) ->
|
||||
let ty1' = trav env ty1 in
|
||||
let ty2' = trav env ty2 in
|
||||
TyEq (ty1', ty2')
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -26,6 +26,7 @@ type ('a, 'b) typ =
|
|||
| TyForall of 'b * ('a, 'b) typ
|
||||
| TyMu of 'b * ('a, 'b) typ
|
||||
| TyConstr of ('a, 'b) datatype
|
||||
| TyEq of ('a, 'b) typ * ('a, 'b) typ
|
||||
|
||||
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
|
||||
|
||||
|
|
|
@ -40,6 +40,8 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
|
|||
P.TyMu (alpha, self ((x, alpha) :: env) ty)
|
||||
| F.TyConstr (constr, tys) ->
|
||||
P.TyConstr (constr, List.map (self env) tys)
|
||||
| F.TyEq (ty1, ty2) ->
|
||||
P.TyEq (self env ty1, self env ty2)
|
||||
|
||||
let print_type ty =
|
||||
Printer.print_type (translate_type [] ty)
|
||||
|
@ -155,6 +157,8 @@ let rec translate_db_type (env : P.tyvar list) (ty : F.debruijn_type) : P.typ =
|
|||
P.TyMu (alpha, self (alpha :: env) ty)
|
||||
| F.TyConstr (constr, tys) ->
|
||||
P.TyConstr (constr, List.map (self env) tys)
|
||||
| F.TyEq (ty1, ty2) ->
|
||||
P.TyEq (self env ty1, self env ty2)
|
||||
|
||||
let print_db_type ty =
|
||||
Printer.print_type (translate_db_type [] ty)
|
||||
|
|
|
@ -148,7 +148,8 @@ let equal1 equal ty1 ty2 =
|
|||
assert false
|
||||
| TyVar x1, TyVar x2 ->
|
||||
Int.equal x1 x2
|
||||
| TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b) ->
|
||||
| TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b)
|
||||
| TyEq (ty1a, ty1b), TyEq (ty2a, ty2b) ->
|
||||
equal ty1a ty2a && equal ty1b ty2b
|
||||
| TyForall ((), ty1), TyForall ((), ty2) ->
|
||||
equal ty1 ty2
|
||||
|
@ -158,7 +159,7 @@ let equal1 equal ty1 ty2 =
|
|||
TyConstr (Datatype.Type tyconstr2, tys2) ->
|
||||
String.equal tyconstr1 tyconstr2 &&
|
||||
pointwise equal tys1 tys2
|
||||
| (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _),
|
||||
| (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _ | TyEq _),
|
||||
_ ->
|
||||
false
|
||||
|
||||
|
@ -265,6 +266,9 @@ let rec translate (env : vertex list) (ty : F.debruijn_type) : vertex =
|
|||
let vs = translate_list env tys in
|
||||
UnionFind.make (SStruct (S.TyConstr (id, vs)))
|
||||
|
||||
| TyEq (_ty1, _ty2) ->
|
||||
failwith "todo"
|
||||
|
||||
and translate_list env tys =
|
||||
List.map (translate env) tys
|
||||
|
||||
|
|
|
@ -9,6 +9,7 @@ type typ =
|
|||
| TyForall of tyvar * typ
|
||||
| TyMu of tyvar * typ
|
||||
| TyConstr of datatype
|
||||
| TyEq of typ * typ
|
||||
|
||||
and datatype = Datatype.tyconstr_id * typ list
|
||||
|
||||
|
|
|
@ -38,6 +38,10 @@ and print_type_arrow ty =
|
|||
print_type_tyconstr ty1
|
||||
^^ space ^^ string "->"
|
||||
^//^ print_type_arrow ty2
|
||||
| TyEq (ty1, ty2) ->
|
||||
print_type_tyconstr ty1
|
||||
^^ space ^^ string "="
|
||||
^//^ print_type_arrow ty2
|
||||
| ty ->
|
||||
print_type_tyconstr ty
|
||||
|
||||
|
@ -55,7 +59,7 @@ and print_type_atom ty =
|
|||
| TyProduct tys ->
|
||||
surround_separate_map 2 0 (lbrace ^^ rbrace)
|
||||
lbrace star rbrace print_type tys
|
||||
| TyMu _ | TyForall _ | TyArrow _ | TyConstr _ as ty ->
|
||||
| TyMu _ | TyForall _ | TyArrow _ | TyConstr _ | TyEq _ as ty ->
|
||||
parens (print_type ty)
|
||||
|
||||
and print_datatype (Datatype.Type tyconstr, tyargs) =
|
||||
|
|
Loading…
Reference in New Issue