Skip to content
Snippets Groups Projects
Commit d5ab6f51 authored by Ralf Jung's avatar Ralf Jung
Browse files

use new function type notation for examples

parent 052d9f00
No related branches found
No related tags found
No related merge requests found
......@@ -12,7 +12,10 @@ Section get_x.
Lemma get_x_type :
typed_instruction_ty [] [] [] get_x
(fn (λ α, [α])%EL (λ α, [# &uniq{α}Π[int; int]]%T) (λ α, &shr{α} int)%T).
fn( α, [α]; &uniq{α} Π[int; int] &shr{α} int).
(* FIXME: The above is pretty-printed with some explicit scope annotations,
and without using 'typed_instruction_ty'. I think that's related to
the list notation that we added to %TC. *)
Proof.
apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|].
......
......@@ -13,7 +13,7 @@ Section init_prod.
Lemma init_prod_type :
typed_instruction_ty [] [] [] init_prod
(fn (λ _, []) (λ _, [# int; int]) (λ (_ : ()), Π[int;int])).
fn([]; int, int Π[int;int]).
Proof.
apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
......
......@@ -18,7 +18,7 @@ Section lazy_lft.
Lemma lazy_lft_type :
typed_instruction_ty [] [] [] lazy_lft
(fn (λ _, [])%EL (λ _, [#]) (λ _:(), unit)).
fn([]; unit).
Proof.
apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
eapply (type_newlft []); [solve_typing|]=>α.
......
......@@ -16,7 +16,7 @@ Section option_as_mut.
Lemma option_as_mut_type τ :
typed_instruction_ty [] [] [] option_as_mut
(fn (λ α, [α])%EL (λ α, [# &uniq{α}Σ[unit; τ]]%T) (λ α, Σ[unit; &uniq{α}τ])%T).
fn( α, [α]; &uniq{α} Σ[unit; τ] Σ[unit; &uniq{α}τ]).
Proof.
apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
eapply (type_cont [_] [] (λ r, [o _; r!!!0 _])%TC) ; [solve_typing..| |].
......
......@@ -17,7 +17,7 @@ Section rebor.
Lemma rebor_type :
typed_instruction_ty [] [] [] rebor
(fn (λ _, []) (λ _, [# Π[int; int]; Π[int; int]]) (λ (_ : ()), int)).
fn([]; Π[int; int], Π[int; int] int).
Proof.
apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
eapply (type_newlft []). apply _. move=> α.
......
......@@ -12,7 +12,7 @@ Section unbox.
Lemma ubox_type :
typed_instruction_ty [] [] [] unbox
(fn (λ α, [α])%EL (λ α, [# &uniq{α}box (Π[int; int])]%T) (λ α, &uniq{α} int)%T).
fn( α, [α]; &uniq{α}box (Π[int; int]) &uniq{α} int).
Proof.
apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|].
......
......@@ -13,7 +13,7 @@ Section unwrap_or.
Lemma unwrap_or_type τ :
typed_instruction_ty [] [] [] (unwrap_or τ)
(fn (λ _, [])%EL (λ _, [# Σ[unit; τ]; τ])%T (λ _:(), τ)).
fn([]; Σ[unit; τ], τ τ).
Proof.
apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
......
......@@ -65,14 +65,22 @@ Section fn.
Qed.
End fn.
(* TODO: Once we depend on 8.6pl1, extend this to recursive binders so that
patterns like '(a, b) can be used. *)
Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN '→' R ')'" :=
(fn (λ x, E%EL) (λ x, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ x, R%T))
(at level 0, E, T1, TN, R at level 50) : lrust_type_scope.
Notation "'fn(∀' x ',' E ';' '→' R ')'" :=
(fn (λ x, E%EL) (λ x, Vector.nil) (λ x, R%T))
(at level 0, E, R at level 50) : lrust_type_scope.
Notation "'fn(' E ';' T1 ',' .. ',' TN '→' R ')'" :=
(fn (λ _:(), E%EL) (λ _, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ _, R%T))
(at level 0, E, T1, TN, R at level 50,
format "'fn(' E ';' T1 ',' .. ',' TN '→' R ')'") : lrust_type_scope.
Notation "'fn(' E ';' '→' R ')'" :=
(fn (λ _:(), E%EL) (λ _, Vector.nil) (λ _, R%T))
(at level 0, E, R at level 50,
format "'fn(' E ';' '→' R ')'") : lrust_type_scope.
Section typing.
Context `{typeG Σ}.
......
......@@ -80,7 +80,7 @@ Section typing.
End typing.
Notation typed_instruction_ty E L T1 e ty :=
(typed_instruction E L T1 e (λ v : val, [v ty]%TC)).
(typed_instruction E L T1 e (λ v : val, [v ty%list%T]%TC)).
Section typing_rules.
Context `{typeG Σ}.
......
......@@ -17,7 +17,7 @@ Notation tctx := (list tctx_elt).
Delimit Scope lrust_tctx_scope with TC.
Bind Scope lrust_tctx_scope with tctx_elt.
Infix "◁" := TCtx_hasty (at level 70) : lrust_tctx_scope.
Notation "p ◁ ty" := (TCtx_hasty p ty%list%T) (at level 70) : lrust_tctx_scope.
Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
(at level 70, format "p ◁{ κ } ty") : lrust_tctx_scope.
Notation "a :: b" := (@cons tctx_elt a%TC b%TC)
......
......@@ -122,7 +122,7 @@ Section refmut_functions.
Lemma refmut_drop_type ty :
typed_instruction_ty [] [] [] refmut_drop
(fn (fun α => [α])%EL (fun α => [# refmut α ty]) (fun α => unit)).
fn( α, [α]; refmut α ty unit).
Proof.
apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
iIntros "!# * #LFT Hna Hα HL Hk Hx".
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment