Permalink
Browse files

[feature] Typer: Height of type abbreviation to balance unwinding dur…

…ing unification.
  • Loading branch information...
fpessaux committed Aug 8, 2011
1 parent d166dbf commit b12589bd70afa75742fca8e6c63ff6a273c5e75b
View
@@ -485,7 +485,7 @@ let of_ty ~gamma ty =
is really bound to a Q.TypeAbstract. *)
QmlTypes.Env.TypeIdent.findi_opt
~visibility_applies: false typeident gamma with
- | Some (typeident, typ) -> (
+ | Some (typeident, (typ, _)) -> (
let ident = Q.TypeIdent.to_string typeident in
(* Standard extended types in LibBSL : bool, option *)
match ident with
@@ -99,7 +99,7 @@ let mapi f = StringListMap.mapi
let get_type_from_name ~context gamma tylst tid =
match
QmlTypes.Env.TypeIdent.findi_opt ~visibility_applies: false tid gamma with
- | Some (tid, ts) ->
+ | Some (tid, (ts, _)) ->
QmlTypes.Scheme.specialize ~typeident:tid ~ty:tylst ts
| None ->
QmlError.error context
@@ -299,7 +299,8 @@ let rec add_subgraph ~context ?(boundnames = []) gamma t parent edge ty =
must know they are not "visible" type structures to forbid partial
writes in paths with these types in databases. *)
let is_abstract_or_private_ty =
- (match snd (QmlTypes.Env.TypeIdent.raw_find ty_name gamma) with
+ let (_, _, vis) = QmlTypes.Env.TypeIdent.raw_find ty_name gamma in
+ (match vis with
| QmlAst.TDV_public -> false
| QmlAst.TDV_abstract _ | QmlAst.TDV_private _ ->
(* A priori, we make so that partial writes on abstract and
@@ -704,9 +705,7 @@ let register_new_db_value ~name_default_values t gamma (label, value) =
match value with
| Db.Db_TypeDecl (p,ty) ->
let ty =
- try
- QmlTypes.type_of_type gamma ty
- with
+ try fst (QmlTypes.type_of_type gamma ty) with
| (QmlTyperException.Exception _) as exn ->
QmlError.error context
"@[<2>Type error in DB definition:@\n%a@]"
@@ -741,10 +740,9 @@ let register_db_declaration t gamma (label, ident, p, opts) =
let error msg =
QmlError.i_error None context msg
in
- let database_type = QmlTypes.type_of_type gamma C.tydb in
+ let (database_type, _) = QmlTypes.type_of_type gamma C.tydb in
let gamma =
- QmlTypes.Env.Ident.add
- ident (QmlTypes.Scheme.quantify database_type) gamma
+ QmlTypes.Env.Ident.add ident (QmlTypes.Scheme.quantify database_type) gamma
in
begin match p with
| [] ->
@@ -574,7 +574,7 @@ struct
| Q.TypeName (targs, tn) ->
if List.mem tn acc then failwith "loop in a type definition"
else
- let tsc =
+ let (tsc, _) =
QmlTypes.Env.TypeIdent.find ~visibility_applies:false tn gamma in
let ty = QmlTypes.Scheme.specialize ~typeident: tn ~ty: targs tsc in
aux (tn :: acc) ty
@@ -1095,7 +1095,11 @@ object (self)
method patlist pl = self#wrap (TypedPat.list annotmap pl)
method match_ e pel = self#wrap (TypedExpr.match_ annotmap e pel)
- method tyname name tyl = QmlTypes.type_of_type gamma (Q.TypeName (tyl,TypeIdent.of_string name))
+ method tyname name tyl =
+ let (ty, _) =
+ QmlTypes.type_of_type
+ gamma (Q.TypeName (tyl,TypeIdent.of_string name)) in
+ ty
method tylist ty = self#tyname "list" [ty]
method tyoption ty = self#tyname Opacapi.Types.option [ty]
@@ -85,3 +85,7 @@ let full_arity t =
let map_body_unsafe f t =
{t with body = f t.body}
+
+let map_body_unsafe2 f t =
+ let (t', v) = f t.body in
+ ({t with body = t'}, v)
@@ -46,5 +46,6 @@ val full_arity : ('t, 'c) tsc -> int * int * int
val is_empty : ('t, 'c) tsc -> bool
val map_body_unsafe : ('t -> 'u) -> ('t, 'c) tsc -> ('u, 'c) tsc
+val map_body_unsafe2 : ('t -> ('u * 'a)) -> ('t, 'c) tsc -> (('u, 'c) tsc) * 'a
(* TODO: add refresh, etc. here, when they are made generic *)
@@ -215,7 +215,8 @@ struct
List.fold_left_map
(fun (more_gamma, gamma) (ti, (vars, te), visibility) ->
(* /!\ may raise TypeidentNotFound *)
- let te = QT.type_of_type ~typedef: true ~tirec gamma te in
+ let (te, abb_height) =
+ QT.type_of_type ~typedef: true ~tirec gamma te in
let te = QmlAstWalk.Type.map
(fun t ->
match t with
@@ -230,16 +231,81 @@ struct
| _ -> t)
te in
let def_scheme = QT.Scheme.definition ~typevar: vars ti te in
+ (* Check if the definition is a trivial abbreviation, i.e. is of
+ the shape: type t('a, 'b...) = 'b. If so, then the abbreviation
+ height of this named type is set to the negated position
+ (numbered from 1) of the parameter used in the body of the
+ trivial abbreviation definition (in our example, -2).
+ Otherwise, it is set to 1 + the abbreviation height of the
+ body. *)
+ let abb_height' =
+ (match (vars, te) with
+ | ((_ :: _), (Q.TypeVar var_body)) -> (
+ let opt_found =
+ List.findi
+ (fun v -> (QmlTypeVars.TypeVar.compare v var_body) = 0)
+ vars in
+ match opt_found with
+ | None -> assert false
+ | Some index ->
+ (* Avoid 0 since it's a regular height. So, start
+ counting position from 1 instead of 0. *)
+ - (index + 1)
+ )
+ | (_, _) ->
+ (* Attention, here check if the height is negative. *)
+ if abb_height < 0 then (
+ (* The type expression of the body must be a type name
+ otherwise there is something broken. We must hence
+ recover it and get the height of the argument applied
+ at the - (abb_height + 1) position. Thsi will then
+ be the height of the defined type constructor. *)
+ match te with
+ | Q.TypeName (args, _) ->
+ let interest_index = - (abb_height + 1) in
+ (* Get the effective type expression at this
+ position. *)
+ let interest_arg = List.nth args interest_index in
+ let (interest_arg, interest_arg_height) =
+ QmlTypes.type_of_type gamma interest_arg in
+ (* Again special case if we get -1 which means that's
+ a type variable. *)
+ if interest_arg_height = -1 then (
+ match interest_arg with
+ | Q.TypeVar interest_var -> (
+ let opt_found =
+ List.findi
+ (fun v ->
+ (QmlTypeVars.TypeVar.compare
+ v interest_var) = 0)
+ vars in
+ match opt_found with
+ | None -> assert false
+ | Some index ->
+ (* Avoid 0 since it's a regular height. So,
+ start counting position from 1 instead of
+ 0. *)
+ - (index + 1)
+ )
+ | _ -> assert false
+ )
+ else 1 + interest_arg_height
+ | _ -> assert false
+ )
+ else 1 + abb_height (* Regular case. *)
+ ) in
(* Here we must the @private and @abstract directives by
exploiting the visibility information of the type definition. *)
let gamma =
- QT.Env.TypeIdent.add ti (def_scheme, visibility) gamma in
+ QT.Env.TypeIdent.add
+ ti (def_scheme, abb_height', visibility) gamma in
let more_gamma =
- QT.Env.TypeIdent.add ti (def_scheme, visibility) more_gamma in
+ QT.Env.TypeIdent.add
+ ti (def_scheme, abb_height', visibility) more_gamma in
if env.QT.display then (
- (* Reset the type vars to avoid variables names to be continuously
- incremented and not restarted at "'v0" for this new type
- definition. *)
+ (* Reset the type vars to avoid variables names to be
+ continuously incremented and not restarted at "'v0" for this
+ new type definition. *)
QmlPrint.pp#reset_typevars ;
let ((vars, _, _), ty) = QT.Scheme.export def_scheme in
let def_for_print = {
@@ -36,8 +36,9 @@ let compare_field (s1,_) (s2,_) = String.compare s1 s2
let compare_rec l1 l2 = List.make_compare compare_field l1 l2
let is_private_or_external gamma n =
- let tsc = QmlTypes.Env.TypeIdent.find ~visibility_applies:false n gamma in
- let _, body, () = QmlGenericScheme.export_unsafe tsc in
+ let (tsc, _) =
+ QmlTypes.Env.TypeIdent.find ~visibility_applies:false n gamma in
+ let (_, body, ()) = QmlGenericScheme.export_unsafe tsc in
match body with
| Q.TypeAbstract -> true
| _ -> false
@@ -97,15 +98,17 @@ let show_instantiation ~allow_partial_application gamma quant vars rows cols spe
begin match need_expansion eh spec gen with
| None -> ()
| Some eh ->
- let tsc = QmlTypes.Env.TypeIdent.find ~visibility_applies:false n1 gamma in
+ let (tsc, _) =
+ QmlTypes.Env.TypeIdent.find ~visibility_applies:false n1 gamma in
let t1 = QmlTypes.Scheme.specialize ~typeident:n1 ~ty:tyl1 tsc in
aux_eh eh t1 t2
end
| t1, Q.TypeName (tyl2, n2) when not (is_private_or_external gamma n2) ->
begin match need_expansion eh spec gen with
| None -> ()
| Some eh ->
- let tsc = QmlTypes.Env.TypeIdent.find ~visibility_applies:false n2 gamma in
+ let (tsc, _) =
+ QmlTypes.Env.TypeIdent.find ~visibility_applies:false n2 gamma in
let t2 = QmlTypes.Scheme.specialize ~typeident:n2 ~ty:tyl2 tsc in
aux_eh eh t1 t2
end
@@ -170,7 +170,8 @@ let refresh_gamma package gamma =
let refresh_tsc = refresh_typevars_from_tsc package in
let gamma = QmlTypes.Env.Ident.map refresh_tsc gamma in
QmlTypes.Env.TypeIdent.map
- (fun (tsc, visibility) -> ((refresh_tsc tsc), visibility)) gamma
+ (fun (tsc, height, visibility) -> ((refresh_tsc tsc), height, visibility))
+ gamma
let refresh_typevars_from_code package code =
List.map
Oops, something went wrong.

0 comments on commit b12589b

Please sign in to comment.