Commit be23eaf9 authored by charguer's avatar charguer

typecheck

parent 7fcc8cc6
......@@ -59,6 +59,9 @@ MAJOR POSTPONED
should be systematically let-bound; this would allow binding these names.
- mutual recursive definitions, polymophic type variables should be more precise
##################################################################
# FUTURE WORK
......
......@@ -2,9 +2,9 @@
# Possible to define "ML" to be the list of source files to consider
# Uncomment next line to compile only Test.ml
# ML := Test.ml
ML := Test.ml
# Demo.ml
CFDEBUG := 1
include ../Makefile.example
include ../Makefile.example
let f0 () =
let r = ref [] in
!r
let f1 () : 'a list =
let r = ref ([] : 'a list) in
!r
let f2 () =
let r : ('a ref) = ref [] in
!r
let f3 () =
let r : (int list) ref = ref [] in
!r
let f4 () =
let r = ref ([] : int list) in
!r
let g1 () : 'a list =
let r = ref [] in
r := [5];
!r
let g2 () =
let r : ('a list) ref = ref [] in
r := [4];
!r
let m0 () =
let r = ref [] in
r
let h0 () =
let g =
let f () = ref [] in
f in
g
(* not allowed because produces a ['_a list ref] at top level;
i.e. rejected when using OCaml "-strict_value_restriction" flag
let h1 =
let f () : 'a list ref = ref [] in
f
*)
let h2 () =
let f () : 'a list ref = ref [] in
f
let h3 () =
let f () = ref [] in
f()
let k1 () =
[]
let k2 () =
ref []
(* CF does not typecheck because the type cannot be resolved
let r1 () =
let _x = ref [] in
()
*)
(* CF does not typecheck because the type cannot be resolved
let r2 () =
let _x = ref [] in
let y = [] in
y
*)
type 'a sitems = {
mutable nb : int;
mutable items : 'a list; }
let sitems_build n =
{ nb = n; items = [] }
let sitems_incr_nb_let r =
let x = r.nb in
r.nb <- x + 1
let sitems_length_items_let r =
let x = r.items in
List.length x
......@@ -106,12 +106,15 @@ else
#----------------FOR DIRECT TEST----------------------
#-strict_value_restriction
EXTRA= -only_normalize -debug
cf: $(ML)
@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf
# @$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick
@$(MAKE) -C $(CFML)/lib/stdlib CFDEBUG=$(CFDEBUG) --no-print-directory cmj
@$(MAKE) CFML=$(CFML) EXTRA="-debug" OCAML_FLAGS="$(OCAML_FLAGS)" COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
@$(MAKE) CFML=$(CFML) EXTRA="$(EXTRA)" OCAML_FLAGS="$(OCAML_FLAGS)" COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
endif
......
......@@ -106,7 +106,7 @@ let rec fv_btyp ?(through_arrow = true) t =
| Btyp_arrow (t1,t2) -> if through_arrow then aux t1 @ aux t2 else []
| Btyp_constr (id,ts) -> list_concat_map aux ts
| Btyp_tuple ts -> list_concat_map aux ts
| Btyp_var (b,s,ty) -> typvar_mark_used ty; [s]
| Btyp_var (s,ty) -> typvar_mark_used ty; [s]
| Btyp_poly (ss,t) -> unsupported_noloc "poly-types"
| Btyp_alias (t,s) -> s :: aux t
......@@ -126,12 +126,12 @@ let rec lift_btyp loc t =
coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
| Btyp_tuple ts ->
coq_prod (List.map aux ts)
| Btyp_var (b,s,ty) ->
| Btyp_var (s,ty) ->
typvar_mark_used ty;
(*if b then unsupported loc ("non-generalizable free type variables (of the form '_a); please add a type annotation if the type is not polymorphic; if it is, then ask to get the typechecker patched for propagating the annotation. var=" ^ s);
TODO: check if this is needed *)
let s = if b then "__" ^ s else s in
Coq_var s
(* DEPRECATED
if b then unsupported loc ("non-generalizable free type variables (of the form '_a); please add a type annotation if the type is not polymorphic; if it is, then ask to get the typechecker patched for propagating the annotation. var=" ^ s);
let s = if b then "__" ^ s else s in *)
| Btyp_poly (ss,t) ->
unsupported_noloc "poly-types"
| Btyp_alias (t1,s) ->
......
......@@ -38,6 +38,7 @@ let spec =
("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name");
("-only_cmj", Arg.Set only_cmj, " only generate the .cmj file, not the .v file");
("-only_normalize", Arg.Set only_normalize, " only generate the .cmj file, and attempt normalization, not the .v file");
("-strict_value_restriction", Arg.Set Clflags.strict_value_restriction, " enforce the strict value restriction (relaxed value restriction is the default)");
("-debug", Arg.Set is_tracing, " trace the various steps");
("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
]
......
......@@ -11,6 +11,10 @@ open Print_type
(** Printing facility for typed abstract syntax trees produced by the
type-checker*)
let _ =
Print_type.type_rename := (fun s -> s)
(*#########################################################################*)
(* ** Printing of items *)
......@@ -20,6 +24,12 @@ let string_of_typed_var s t =
let string_of_path p =
Path.name p
let string_of_fvs fvs =
if fvs = []
then ""
else sprintf "[%s]" (show_list show_str " " (List.map string_of_type_exp fvs))
(*#########################################################################*)
(* ** Printing of patterns *)
......@@ -58,9 +68,10 @@ let string_of_pattern par p =
aux false p
let string_of_let_pattern par fvs p =
let typ = p.pat_type in
string_of_pattern par p
(* let typ = p.pat_type in
let styp = string_of_type_sch fvs typ in
sprintf "%s : %s" (string_of_pattern par p) styp
sprintf "%s : %s" (string_of_pattern par p) styp *)
(*
match p.pat_desc with
| Tpat_var id ->
......@@ -69,6 +80,7 @@ let string_of_let_pattern par fvs p =
| _ -> unsupported_noloc "let-pattern not reduced to a variable"
*)
(*#########################################################################*)
(* ** Printing of expression *)
......@@ -83,14 +95,14 @@ let rec string_of_expression par e =
match e.exp_desc with
| Texp_ident (p,vd) -> string_of_path p (* string_of_typed_var (string_of_path p) vd.val_type*)
| Texp_constant c -> string_of_constant c
| Texp_let (rf, fvs, l, e) -> (* TODO FVS *)
| Texp_let (rf, fvs, l, e) ->
let show_pe (p,e) =
let sp = (string_of_let_pattern false fvs p) in
let se = aux e in
Format.sprintf "%s =@ @[%s@]" sp se in
let sl = show_list show_pe " and " l in
let se = aux e in
Format.sprintf "@[let%s %s in@ @[%s@]@]" (string_of_recflag rf) sl se
Format.sprintf "@[let%s%s %s in@ @[%s@]@]" (string_of_recflag rf) (string_of_fvs fvs) sl se
| Texp_function (_,(p1,e1)::[], pa) ->
let rec explore pats e =
match e.exp_desc with
......@@ -275,7 +287,7 @@ and string_of_structure_item (si:structure_item) =
let se = string_of_expression false e in
Format.sprintf "%s =@ @[%s@]" sp se in
let sl = show_list show_pe " and " l in
Format.sprintf "@[let%s %s@]" (string_of_recflag r) sl
Format.sprintf "@[let%s%s %s@]" (string_of_recflag r) (string_of_fvs fvs) sl
(* Format.sprintf "@[let%s %s =@ @[<2>%s@]@]" *)
| Tstr_primitive (id,v) -> sprintf "val %s : 'external" (string_of_ident id)
| Tstr_type l -> sprintf "type _ = _"
......
......@@ -19,6 +19,7 @@ open Renaming
from the representation used by OCaml's compiler. *)
let type_rename = ref type_variable_name
(*#########################################################################*)
......@@ -29,7 +30,7 @@ type btyp =
| Btyp_arrow of btyp * btyp
| Btyp_constr of Path.t * btyp list
| Btyp_tuple of btyp list
| Btyp_var of bool * string * type_expr
| Btyp_var of string * type_expr
| Btyp_poly of string list * btyp
| Btyp_val
......@@ -47,25 +48,33 @@ type btyp =
(*#########################################################################*)
(* ** Used variables *)
let eliminate_unused_variables = false
(** Special level used to mark used variables *)
let used_level = 11111111111
(** Mark a variable as used at least once. *)
let typvar_mark_used ty =
let ty = repr ty in
(* ()*) ty.level <- used_level
if eliminate_unused_variables then ty.level <- used_level
(** Test if a variable has been used at least once. *)
let typvar_is_used ty = (*true *)
let ty = repr ty in
ty.level = used_level
let typvar_is_used ty =
if not eliminate_unused_variables then true else begin
let ty = repr ty in
ty.level = used_level
end
(*#########################################################################*)
(* ** Helper functions *)
(** Gathering of free type variables of a btyp *)
(** Gathering of free type variables of a btyp
DEPRECATED
*)
type occ = Occ_gen of type_expr | Occ_alias of type_expr
let occured : (occ list) ref = ref []
......@@ -84,7 +93,7 @@ let mark_loops = mark_loops
let name_of_type ty =
let ty = proxy ty in
let x = Printtyp.name_of_type ty in
type_variable_name x
!type_rename x
let reset_names = reset_names
......@@ -94,25 +103,23 @@ let reset_names = reset_names
(** Algorithm translating an OCaml's typechecker type into a btyp *)
(* new def here for is_non_gen *)
let is_non_gen sch ty =
sch && ty.desc = Tvar && ty.level <> generic_level
&& ty.level <> used_level (* HACK *)
(* ty.level <> used_level *)
let rec btree_of_typexp sch ty =
let ty = repr ty in
let px = proxy ty in
if List.mem_assq px !names && not (List.memq px !delayed) then
let mark = is_non_gen sch ty in
if List.mem_assq px !names (* && not (List.memq px !delayed) *) then
(* let mark = is_non_gen sch ty in *)
if is_aliased px && aliasable ty
then Btyp_val (* todo: hack ok ? *)
else Btyp_var (mark, name_of_type px, ty) else
else Btyp_var (name_of_type px, ty) else
let pr_typ () =
match ty.desc with
| Tvar ->
add_occured (Occ_gen ty);
Btyp_var (is_non_gen sch ty, name_of_type ty, ty)
Btyp_var (name_of_type ty, ty)
(* add_occured (Occ_gen ty); *)
(* is_non_gen sch ty, *)
| Tarrow(l, ty1, ty2, _) ->
(* with labels
let pr_arrow l ty1 ty2 =
......@@ -147,6 +154,8 @@ let rec btree_of_typexp sch ty =
| Tpoly (ty, []) ->
btree_of_typexp sch ty
| Tpoly (ty, tyl) ->
fatal_error "Printtyp.btree_of_typexp poly unsupported"
(*
let tyl = List.map repr tyl in
(* let tyl = List.filter is_aliased tyl in *)
if tyl = [] then btree_of_typexp sch ty else begin
......@@ -156,16 +165,17 @@ let rec btree_of_typexp sch ty =
let tr = Btyp_poly (tl, btree_of_typexp sch ty) in
delayed := old_delayed; tr
end
*)
| Tunivar ->
fatal_error "Printtyp.btree_of_typexp univar unsupported"
(* Btyp_var (false, name_of_type ty, ty) *)
| Tpackage _ ->
unsupported_noloc "packaged types"
fatal_error "Printtyp.btree_of_typexp Tpackage unsupported"
in
if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed;
(* if List.memq px !delayed then delayed := List.filter ((!=) px) !delayed; *)
if is_aliased px && aliasable ty then begin
check_name_of_type px;
add_occured (Occ_alias ty); (* todo: devrait pas compter ? *)
(* add_occured (Occ_alias ty); *)
Btyp_alias (pr_typ (), name_of_type px) end
else pr_typ ()
......@@ -186,7 +196,8 @@ let btyp_of_typ_exp t =
btree_of_typexp false t
(** Translates of a type scheme [t] into a [btyp], including the call
to [mark_loops]. CURRENTLY NOT USED *)
to [mark_loops].
DEPRECATED *)
let btyp_of_typ_sch t =
mark_loops t;
......@@ -260,7 +271,7 @@ and print_simple_out_type =
function
| Btyp_constr (id, tyl) ->
sprintf "@[%a%a@]" (ign print_typargs) tyl (ign print_path) id
| Btyp_var (ng, s, ty) -> sprintf "'%s%s" (if ng then "_" else "") s
| Btyp_var (s, ty) -> sprintf "'%s" s (* %s (if ng then "_" else "") *)
| Btyp_val | Btyp_alias _ | Btyp_poly _ | Btyp_arrow _ | Btyp_tuple _ as ty ->
sprintf "@[<1>(%a)@]" (ign print_out_type) ty
(*| Btyp_abstract -> ""
......
......@@ -6,9 +6,8 @@ type btyp =
| Btyp_arrow of btyp * btyp
| Btyp_constr of Path.t * btyp list
| Btyp_tuple of btyp list
| Btyp_var of bool * string * Types.type_expr
(* - bool: indicates whether generalizable (ie ['a] vs ['_a] type)
- string: name of variable
| Btyp_var of string * Types.type_expr
(* - string: name of variable
- type_expr: for internal use to track which variables are used *)
| Btyp_poly of string list * btyp
| Btyp_val
......@@ -48,3 +47,7 @@ val string_of_type_exp : Types.type_expr -> string
(** Convert a type scheme into a string *)
val string_of_type_sch : Types.type_expr list -> Types.type_expr -> string
(** Customization of the type renaming function *)
val type_rename : (string -> string) ref
let configure () =
Config.interface_suffix := "____mli_files_are_ignored____";
Clflags.strict_value_restriction := true;
(* Clflags.strict_value_restriction := true; *)
Clflags.no_std_include := true
......@@ -172,37 +172,6 @@ let hook_fresh_var t =
| _ -> () (* not added because t certainly won't generalize *)
(* DEPRECATED
let max_depth = 100 in (* TODO: how to prevent traversing cycles? *)
let rec aux n t =
Format.fprintf Format.err_formatter "call to aux\n";
if n = 0 then Printf.printf "warning:hook_fresh_var traversing cyclic type; approximating the result.\n" else begin
let aux = aux (n-1) in
let t = repr t in (* TODO: might want to use proxy if objects are supported *)
match t.desc with
| Tvar | Tunivar ->
if debug_generic then Format.printf "add generic var\n" ;
if not (List.memq t !tys)
then tys := t :: !tys
| Tarrow (_,t1,t2,_) -> aux t1; aux t2
| Ttuple ts ->
Format.printf "traverse tuple of length %d\n" (List.length ts);
List.iter aux ts
| Tconstr (_,ts,_) ->
Format.printf "traverse constr of length %d\n" (List.length ts);
List.iter aux ts
| Tobject _ -> failwith "unsupported Tobject type"
| Tfield _ -> failwith "unsupported Tfield type"
| Tnil -> failwith "unsupported Tnil type"
| Tvariant _ -> failwith "unsupported Tvariant type"
| Tunivar -> failwith "unsupported Tunivar type"
| Tpoly _ -> failwith "unsupported Tpoly type"
| Tpackage _ -> failwith "unsupported Tpackage type"
| Tlink _ -> failwith "unsupported Tlink type"
| Tsubst _ -> failwith "unsupported Tsubst type"
end in
aux max_depth t
*)
(* END CFML *)
(**********************************)
(* End CFML hooks *)
......@@ -812,12 +781,20 @@ let limited_generalize ty0 ty =
(* CFML *)
let close_hook ?(showtyp=(fun t -> ())) () =
let close_hook ?(showtyp=(fun t -> ())) ~gen_nonexpansive () =
if debug_generic
then Format.fprintf Format.err_formatter "=== close hook at level %d\n" !current_level;
match !hook_generic with
| [] -> failwith "close_hook called while hook list is empty"
| h::hs ->
let push_into_outer_hook t =
match hs with
| [] -> () (* TODO: might want to do something with outermost vars *)
| hnext::_ ->
if not (List.memq t !hnext)
then hnext := t :: !hnext
in
hook_generic := hs;
let r = ref [] in
let select_generic t =
......@@ -831,12 +808,21 @@ let close_hook ?(showtyp=(fun t -> ())) () =
if debug_generic then begin
Format.fprintf Format.err_formatter "-->was at level %d\n" t.level;
end;
generalize t;
generalize_structure t;
if gen_nonexpansive && t.level = !nongen_level then begin
Format.fprintf Format.err_formatter "-->>> generalized non-expansive\n";
set_level t generic_level;
end;
if debug_generic then begin
Format.fprintf Format.err_formatter "-->now at level %d\n" t.level;
end;
if (t.level = generic_level || t.level = !nongen_level) && not (List.memq t !r)
then r := t::!r
if (t.level = generic_level) then begin
if not (List.memq t !r) (* TODO: auxiliary function for this pattern *)
then r := t::!r
end else begin
push_into_outer_hook t
end
| Tunivar -> failwith "unsupported Tunivar type"
| _ -> ()
in
......
......@@ -249,4 +249,4 @@ val collapse_conj_params: Env.t -> type_expr list -> unit
(* CFML *)
val open_hook : unit -> unit
val close_hook : ?showtyp:(type_expr->unit) -> unit -> type_expr list
val close_hook : ?showtyp:(type_expr->unit) -> gen_nonexpansive:bool -> unit -> type_expr list
......@@ -22,6 +22,14 @@ open Typedtree
open Btype
open Ctype
(* CFML *)
let cfml_showtyp t =
let err = Format.err_formatter in
Printtyp.type_expr err t;
Format.fprintf err "\n"
type error =
Polymorphic_label of Longident.t
| Constructor_arity_mismatch of Longident.t * int * int
......@@ -1155,7 +1163,7 @@ let rec type_exp env sexp =
open_hook(); (* CFML *)
let (pat_exp_list, new_env, unpacks) =
type_let env rec_flag spat_sexp_list scp true in
let fvs = close_hook() in (* CFML *)
let fvs = close_hook ~showtyp:cfml_showtyp ~gen_nonexpansive:false () in (* CFML *)
let body = type_exp new_env (wrap_unpacks sbody unpacks) in
re {
exp_desc = Texp_let(rec_flag, fvs, pat_exp_list, body); (* CFML *)
......@@ -2108,7 +2116,7 @@ and type_expect ?in_function env sexp ty_expected' =
open_hook(); (* CFML *)
let (pat_exp_list, new_env, unpacks) =
type_let env rec_flag spat_sexp_list None true in
let fvs = close_hook() in (* CFML *)
let fvs = close_hook ~showtyp:cfml_showtyp ~gen_nonexpansive:false() in (* CFML *)
let body =
type_expect new_env (wrap_unpacks sbody unpacks) ty_expected in
re {
......@@ -2628,3 +2636,5 @@ let report_error ppf = function
fprintf ppf
"This expression is packed module, but the expected type is@ %a"
type_expr ty
......@@ -119,3 +119,7 @@ val type_package:
val create_package_type: Location.t -> Env.t -> Parsetree.package_type ->
Path.t * (string * Typedtree.core_type) list * Types.type_expr
(* CFML *)
val cfml_showtyp : Types.type_expr -> unit
\ No newline at end of file
......@@ -885,12 +885,7 @@ and type_structure funct_body anchor env sstr scope =
let (defs, newenv) =
Typecore.type_binding env rec_flag sdefs scope in
let showtyp t =
let err = Format.err_formatter in
Printtyp.type_expr err t;
Format.fprintf err "\n"
in
let fvs = Ctype.close_hook ~showtyp:showtyp () in (* CFML *)
let fvs = Ctype.close_hook ~showtyp:Typecore.cfml_showtyp ~gen_nonexpansive:false () in (* CFML *)
let (str_rem, sig_rem, final_env) = type_struct newenv srem in
let bound_idents = let_bound_idents defs in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment