Commit da76f9a2 authored by Dan Frumin's avatar Dan Frumin

Write a section about typechecking user programs

parent 11948e6e
iris-logrel reference manual
============================
writing programs
================
Typechecking your programs automatically
----------------------------------------
`iris-logrel` supports (semi)-automatic typechecking of programs in F_mu_ref_conc
1. Make sure that you import modules `F_mu_ref_conc.typing` and `F_mu_ref_conc.reflection`
which contain tactics for solving typeability and closendess.
2. Define your program, usually as a closed value.
```coq
Definition prog : val := λ: "x", if: !"x" then (λ: <>, 1) else (λ: <>, 0).
```
3. Typecheck it, in an arbitrary context, using the `solve_typed` tactic.
```coq
Lemma prog_typed Γ : Γ ⊢ₜ prog : TArrow (Tref TBool) (TArrow TUnit TNat).
Proof.
solve_typed.
Qed.
```
4. Add the typeability lemma to the common database.
```coq
Hint Resolve prog_typed : typeable.
```
It is important that in step 3 your lemma is general enough. Once you
add the lemma to the hint database (step 4), it can be used in
typechecking compound expressions containing values already
typechecked before, for example:
```coq
Definition prog2 : val := λ: <>,
let: "x" := ref false in
prog "x" ().
Lemma prog2_typed Γ : Γ ⊢ₜ prog2 : TArrow TUnit TNat.
Proof. solve_typed. Qed.
Hint Resolve prog2_typed : typeable.
```
tactics/proofmode reference manual
==================================
Threadpool tactics
------------------
......
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