Commit 1e3305ab authored by charguer's avatar charguer

polylet

parent aa0bace8
......@@ -9,63 +9,109 @@ open Pervasives
(********************************************************************)
(* ** Value restriction *)
(* ** Polymorphic let bindings and value restriction *)
(* -- rejected program: the internal type-checking involves a
['_a ref] type, even though the result type is ['a list].
let let_poly_p0 () =
let x = (None = None) in ()
let value_restriction_0 () =
let let_poly_p1 () =
let f x = x in
let _r = f None in
()
let let_poly_p2 () =
let f x = x in
let _r =
let _s = f None in ()
in
()
let let_poly_p3 () =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (Some 3, None)) in
let _r4 = (true = false) in
()
let let_poly_f0 () =
let r = ref [] in
!r
*)
(* TODO: how to make this program accepted?
=> it is not currently because ocaml typechecker does not
propagate the information downwards in the term.
let value_restriction_1 () : 'a list =
let let_poly_f1 () : 'a list =
let r = ref ([] : 'a list) in
!r
*)
(* -- rejected program: use of ['_a ref] type annotation is not supported.
let value_restriction_2 () =
let r : '_a ref = ref [] in
let let_poly_f2 () =
let r : ('a ref) = ref [] in
!r
*)
(* -- accepted program: monomorphic annotation on the let-bindings *)
(*
let value_restriction_3 () =
let let_poly_f3 () =
let r : (int list) ref = ref [] in
!r
*)
(* -- accepted program: monomorphic annotation on the empty list *)
(*
let value_restriction_4 () =
let let_poly_f4 () =
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]. *)
let value_restriction_5 () =
let let_poly_g1 () : 'a list =
let r = ref [] in
r := [5];
!r
let let_poly_g2 () =
let r : ('a list) ref = ref [] in
r := [4];
!r
(* -- accepted program: likewise, the list [[5]] is accepted at type
['a list], but it comes out at type [int list] from the type-checker. *)
let value_restriction_6 () : 'a list =
let let_poly_h0 () =
let r = ref [] in
r := [5];
!r
r
let let_poly_h1 () =
let g =
let f () = ref [] in
f in
g
let let_poly_h2 () =
let f () : 'a list ref = ref [] in
f
let let_poly_h3 () =
let f () = ref [] in
f()
let let_poly_k1 () =
[]
let let_poly_k2 () =
ref []
let let_poly_r1 () =
let _x = ref [] in
()
let let_poly_r2 () =
let _x = ref [] in
let y = [] in
y
let let_poly_r3 () =
let r =
let x = ref [] in
[] in
r
(* ---Code 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
*)
......
......@@ -5,6 +5,282 @@ Require Import Demo_ml.
Require Import Stdlib.
Open Scope tag_scope.
Notation "'LetPoly' '{' A1 '}' x ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[@P1 A1 r] \* H1))
/\ forall x, (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, A1 ident, x ident, right associativity) : charac.
(*--------------------------------------------------------*)
(* ** [xlet_poly] *)
(** [xlet_poly] is used to reason on a let node, i.e. on a goal
of the form [(LetPoly {A1} x := F1 in F2) H Q].
Variants:
- [xlet_poly P H] to describe the pure postcondition and
the final state.
- [xlet_poly_keep P] to provide a pure postcondition and
use the current pre-condition as final state.
- [xlet_poly P] to provide a pure postcondition and introduce
a unification variable for the imperative state.
- [xlet_poly as y] to rename [x] into [y].
- [xlet_poly P H as y].
*)
Ltac xlet_poly_core cont0 cont1 cont2 :=
apply local_erase;
cont0 tt;
split; [ intros | cont1 tt; cont2 tt ];
xtag_goal.
Ltac xlet_poly_def cont0 cont1 cont2 :=
xextract_check_not_needed tt;
xuntag tag_let_poly;
xlet_poly_core cont0 cont1 cont2.
Tactic Notation "xlet_poly" constr(P) constr(H) "as" simple_intropattern(x) simple_intropattern(Hx) :=
xlet_poly_def
ltac:(fun _ => exists P; exists H)
ltac:(fun _ => intros x Hx)
ltac:(fun _ => try xextract).
Tactic Notation "xlet_poly" constr(P) constr(H) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly P H as x Hx.
Tactic Notation "xlet_poly" constr(P) constr(H) :=
xlet_poly_def
ltac:(fun _ => exists P; exists H)
ltac:(fun _ => intro)
ltac:(fun _ => try xextract).
Tactic Notation "xlet_poly" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
xlet_poly_def
ltac:(fun _ => exists P; esplit)
ltac:(fun _ => intros x Hx)
ltac:(fun _ => idtac).
Tactic Notation "xlet_poly" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly P as x Hx.
Tactic Notation "xlet_poly" constr(P) :=
xlet_poly_def
ltac:(fun _ => exists P; esplit)
ltac:(fun _ => intro)
ltac:(fun _ => idtac).
Tactic Notation "xlet_poly_keep" constr(P) "as" simple_intropattern(x) simple_intropattern(Hx) :=
let H := cfml_get_precondition tt in
xlet_poly P H as x.
Tactic Notation "xlet_poly_keep" constr(P) "as" simple_intropattern(x) :=
let Hx := fresh "H" x in
xlet_poly_keep P as x Hx.
Tactic Notation "xlet_poly_keep" constr(P) :=
let H := cfml_get_precondition tt in
xlet_poly P H.
(* LATER
Tactic Notation "xlet_poly" "~" := xlet; xauto~.
Tactic Notation "xlet" "~" "as" simple_intropattern(x) := xlet as x; xauto~.
Tactic Notation "xlet" "~" constr(Q) := xlet Q; xauto~.
Tactic Notation "xlet" "~" constr(Q) "as" simple_intropattern(x) := xlet Q as x; xauto~.
Tactic Notation "xlet" "*" := xlet; xauto*.
Tactic Notation "xlet" "*" "as" simple_intropattern(x) := xlet as x; xauto*.
Tactic Notation "xlet" "*" constr(Q) := xlet Q; xauto*.
Tactic Notation "xlet" "*" constr(Q) "as" simple_intropattern(x) := xlet Q as x; xauto*.
*)
(*-------*)
Ltac xapps_skip_core tt :=
let cont2 tt := instantiate; try xextract; try intro_subst in
let cont1 tt :=
match cfml_get_tag tt with
| tag_apply => xuntag tag_apply; xapp_skip_core
| tag_none_app => xapp_skip_core
| tag_record_new => xapp_skip_core
end
in
match cfml_get_tag tt with
| tag_let => xlet; [ cont1 tt | cont2 tt ]
| tag_seq => xseq; [ cont1 tt | cont2 tt ]
| _ => cont1 tt
end.
Tactic Notation "xapps_skip" :=
xapps_skip_core tt.
(********************************************************************)
(********************************************************************)
(********************************************************************)
Notation "'LetPoly' '{' A1 '}' x ':' T ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[P1 r] \* H1))
/\ forall (x:T), (P1 x) -> F2 H1 Q))
(at level 69, A1 ident, x ident, T at level 0, right associativity) : charac.
Notation "'LetPoly' '{' A1 '}' x ':' T ':=' F1 'in' F2" :=
(!LetPoly (fun H Q => exists P1 H1,
(forall A1, F1 H (fun r => \[@P1 A1 r] \* H1))
/\ forall (x:T), (forall A1, @P1 A1 (@x A1)) -> F2 H1 Q))
(at level 69, A1 ident, x ident, T at level 0, right associativity) : charac.
Lemma let_poly_p0_spec :
app let_poly_p0 [tt] \[] \[= tt].
Proof using.
xcf. xlet_poly_keep (= true). xapp_skip. intro_subst. xrets~.
Qed.
Lemma let_poly_p1_spec :
app let_poly_p1 [tt] \[] \[= tt].
Proof using.
xcf. xfun. xlet_poly_keep (fun B (r:option B) => r = None).
{ xapps. xrets. }
{ intros Hr. xrets~. }
Qed.
Lemma let_poly_p2_spec :
app let_poly_p2 [tt] \[] \[= tt].
Proof using.
xcf. xfun. xlet.
{ xlet_poly_keep (fun B (r:option B) => r = None).
{ xapps. xrets. }
{ intros Hr. xrets~. } }
{ xrets~. }
Qed.
Lemma let_poly_p3_spec :
app let_poly_p3 [tt] \[] \[= tt].
Proof using.
xcf.
xlet_poly_keep (= true). { xapp_skip. } intro_subst.
xapp_skip.
xlet_poly_keep (= false). { xapp_skip. } intro_subst.
xapp_skip.
xrets~.
Qed.
Lemma let_poly_f0_spec : forall A,
app let_poly_f0 [tt] \[] \[= @nil A].
Proof using.
xcf. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_f1_spec : forall A,
app let_poly_f1 [tt] \[] \[= @nil A].
Proof using.
xcf. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_f2_spec : forall A,
app let_poly_f2 [tt] \[] \[= @nil A].
Proof using.
xcf. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_f3_spec :
app let_poly_f3 [tt] \[] \[= @nil int].
Proof using.
xcf. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_f4_spec :
app let_poly_f4 [tt] \[] \[= @nil int].
Proof using.
xcf. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_g1_spec :
app let_poly_g1 [tt] \[] \[= 5::nil].
Proof using.
xcf. xapps. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_g2_spec :
app let_poly_g2 [tt] \[] \[= 4::nil].
Proof using.
xcf. xapps. xapps. xapps. xsimpl~.
Qed.
Lemma let_poly_h0_spec :
app let_poly_h0 [tt] \[] \[= 4::nil].
Proof using.
xcf. xapps. xapps. xapps. xsimpl~.
Qed.
(*
let let_poly_h0 () =
let r = ref [] in
r
let let_poly_h1 () =
let g =
let f () = ref [] in
f in
g
let let_poly_h2 () =
let f () : 'a list ref = ref [] in
f
let let_poly_h3 () =
let f () = ref [] in
f()
let let_poly_k1 () =
[]
let let_poly_k2 () =
ref []
let let_poly_r1 () =
let _x = ref [] in
()
let let_poly_r2 () =
let _x = ref [] in
let y = [] in
y
let let_poly_r3 () =
let r =
let x = ref [] in
[] in
r
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(*
let compare_options =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
......@@ -20,14 +296,15 @@ let match_term_when () =
| n when n > 0 -> 2
| _ -> 3
let match_or_clauses p =
(* captures (Some x, _) or (_, Some x) with x > 0 *)
let match_or_clauses p =
match p with
| (None, None) -> false
| ((Some x, _) | (_, Some x)) when x > 0 -> true
| (Some x, _) | (_, Some x) -> false
*)
(********************************************************************)
......
......@@ -2,9 +2,10 @@
# 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
#CFDEBUG := 1
ML := Demo.ml
include ../Makefile.example
(* ---CFML not supported : requires value restriction *)
let p0 () =
let x = (None = None) in ()
let p1 () =
let f x = x in
let _r = f None in
()
let p2 () =
let f x = x in
let _r =
let _s = f None in ()
in
()
(*
let compare_poly () =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
let _r3 = ((Some 3, None) = (Some 3, None)) in
let _r4 = (true = false) in
()
*)
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
(* ---Code 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
*)
(* ---CFML does not yet support: relaxed value restriction
let r3 () =
let r =
let x = ref [] in
[] in
r
*)
type 'a sitems = {
mutable nb : int;
mutable items : 'a list; }
let sitems_build n =
{ nb = n; items = [7] }
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
(*----------------------
--------------------*)
\ No newline at end of file
let x = 3
\ No newline at end of file
......@@ -97,8 +97,8 @@ cf: $(ML)
# Make sure TLC and CFML itself are up-to-date.
# Needed only when developing TLC and CFML. Ideally, should be removed.
@$(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) --no-print-directory tools coqlib_quick_cf
@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick
@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
@$(MAKE) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
......
......@@ -635,12 +635,12 @@ let show_fvs title fvs =
let get_fvs_typ loc fvs typ =
let typ = lift_typ_exp loc typ in
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
(fvs, [], typ)
(* DEPRECATED
let fvs_typ, typ = lift_typ_sch loc typ in
let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
if Settings.debug_generic then begin
show_fvs "fvs_typ" fvs_typ;
show_fvs "fvs" fvs;
......@@ -728,16 +728,6 @@ let rec cfg_exp env e =
let (pat,bod) = List.hd pat_expr_list in
let x = pattern_name_protect_infix pat in
(* deprecated: pure-mode let-binding
if !pure_mode then begin
let cf1 = cfg_exp env bod in
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf2 = cfg_exp env' body in
add_used_label x;
Cf_let_poly (x, fvs_strict, fvs_others, typ, cf1, cf2)