Commit 7fcc8cc6 authored by charguer's avatar charguer

cp

parent 43ee4bb8
MAJOR TODAY
patterns
rename xextract to xpull; and xgen to xpush.
infix_eq_
comparable_type A || comparable_value x || comparable_value y
x = y : A
comparable_value x || comparable_value y
x = y : A
forall x : int, comparable_value x
- patterns
- rename xextract to xpull; and xgen to xpush.
- record with
......
......@@ -37,15 +37,19 @@ let value_restriction_2 () =
(* -- accepted program: monomorphic annotation on the let-bindings *)
(*
let value_restriction_3 () =
let r : (int list) ref = ref [] in
!r
*)
(* -- accepted program: monomorphic annotation on the empty list *)
(*
let value_restriction_4 () =
let r = ref ([] : int list) in
!r
*)
(* -- accepted program: the polymorphic type annotation is accepted,
but it fact it is refined by the type-checker as [(int list) ref]. *)
......@@ -113,9 +117,11 @@ let ret_poly_internal () =
(* --TODO: BUG
The reference A_ was not found in the current environment.*)
(*
let ret_poly_internal () =
let x = ignore (None : 'a option) in
()
*)
(********************************************************************)
......@@ -507,9 +513,17 @@ let sitems_build n =
let sitems_get_nb r =
r.nb
let sitems_incr_nb_let r =
let x = r.nb in
r.nb <- x + 1
let sitems_incr_nb r =
r.nb <- r.nb + 1
let sitems_length_items_let r =
let x = r.items in
List.length x
let sitems_length_items r =
List.length r.items
......
......@@ -2,7 +2,8 @@
# 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
......
......@@ -128,8 +128,9 @@ let rec lift_btyp loc t =
coq_prod (List.map aux ts)
| Btyp_var (b,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, because the relaxed value restriction is not supported.";
TODO: check if this is needed *)
(*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
| Btyp_poly (ss,t) ->
unsupported_noloc "poly-types"
......@@ -169,6 +170,10 @@ let lift_typ_sch loc ty =
let fv = fv_btyp ~through_arrow:false t in
fv, lift_btyp loc t
let lift_typ_sch_as_forall loc ty =
let fv, typ = lift_typ_sch loc ty in
coq_forall_types fv typ
(** Translates the type of a Caml expression into a Coq type *)
let coq_typ loc e =
......@@ -280,7 +285,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
| TPat_alias id ->
if through_aliases then aux p else Coq_var (var_name (Ident.name id))
| TPat_constraint ty ->
let typ = lift_typ_exp loc ty.ctyp_type in
let typ = lift_typ_sch_as_forall loc ty.ctyp_type in
Coq_annot (aux p, typ)
| TPat_type pp -> aux p
end
......@@ -503,7 +508,7 @@ let rec lift_val env e =
| Texp_lazy e ->
aux e
| Texp_constraint (e, Some ty, None) ->
let typ = lift_typ_exp loc ty.ctyp_type in
let typ = lift_typ_sch_as_forall loc ty.ctyp_type in
Coq_annot (aux e, typ)
(* --uncomment for debugging
......@@ -690,7 +695,7 @@ let rec cfg_exp env e =
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
if debug_generic
then Printf.printf "fvs exp_let = %s\n" (show_list show_str " , " fvs);
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_strict = (* list_intersect fvs *) fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(fvs_strict, fvs_others, typ)
in
......@@ -722,7 +727,9 @@ let rec cfg_exp env e =
(* term let-binding *)
end else begin
let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
if fvs_strict <> [] || fvs_others <> [] then begin
if fvs_strict <> [] (* || fvs_others <> []
TODO: if this is not empty, it'd better get bind elsewhere
*) then begin
Printf.printf "fvs_strict = %s\n" (show_list show_str " , " fvs_strict);
Printf.printf "fvs_others = %s\n" (show_list show_str " , " fvs_others);
unsupported loc "relaxed value restriction";
......@@ -862,12 +869,22 @@ and cfg_func env fvs pat bod =
let loc = pat.pat_loc in
let f = pattern_name_protect_infix pat in
let targs, body = get_typed_args [] bod in
let typ = coq_typ loc body in
let fv_body, typ = lift_typ_sch loc body.exp_type in
let cf_body = cfg_exp env body in
let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
(* fvs computation must come after cf_body *)
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
if debug_generic
then Printf.printf "fvs cfg_func = %s\n" (show_list show_str " , " fvs);
if debug_generic then begin
Printf.printf "fvs cfg_func = %s\n" (show_list show_str " , " fvs);
Printf.printf "fvs_body cfg_func = %s\n" (show_list show_str " , " fv_body);
end;
(*
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
let fvs_strict = (*list_intersect fvs*) fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(fvs_strict, fvs_others, typ)
*)
Cf_body (f, fvs, targs, typ, cf_body)
(* --todo: check if the set of type variables quantified is not too
conservative. Indeed, some type variables may no longer occur. *)
......@@ -929,7 +946,7 @@ let rec cfg_structure_item s : cftops =
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
if debug_generic
then Printf.printf "fvs str_value = %s\n" (show_list show_str " , " fvs);
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_strict = (*list_intersect fvs*) fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(fvs_strict, fvs_others, typ)
in
......
......@@ -52,11 +52,13 @@ let used_level = 11111111111
(** Mark a variable as used at least once. *)
let typvar_mark_used ty =
ty.level <- used_level
let ty = repr ty in
(* ()*) ty.level <- used_level
(** Test if a variable has been used at least once. *)
let typvar_is_used ty =
let typvar_is_used ty = (*true *)
let ty = repr ty in
ty.level = used_level
......@@ -92,6 +94,12 @@ 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 *)
let rec btree_of_typexp sch ty =
let ty = repr ty in
let px = proxy ty in
......@@ -100,7 +108,6 @@ let rec btree_of_typexp sch ty =
if is_aliased px && aliasable ty
then Btyp_val (* todo: hack ok ? *)
else Btyp_var (mark, name_of_type px, ty) else
let pr_typ () =
match ty.desc with
| Tvar ->
......
......@@ -846,7 +846,7 @@ let close_hook ?(showtyp=(fun t -> ())) () =
(List.length !hook_generic)
(List.length !h)
(List.length !r);
!r
List.rev !r
(* Circular
let err = Format.error_formatter 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