102 lines
2.6 KiB
Text
102 lines
2.6 KiB
Text
|
// https://www.fstar-lang.org/tutorial/book/part2/part2_stlc.html
|
||
|
|
|
||
|
|
module Hello
|
||
|
|
|
||
|
|
open FStar.Exn
|
||
|
|
|
||
|
|
type monotype =
|
||
|
|
| MTVar of string
|
||
|
|
| MTArrow of monotype * monotype
|
||
|
|
| MTEmpty
|
||
|
|
| MTUnit
|
||
|
|
| MTSum of monotype * monotype
|
||
|
|
| MTProd of monotype * monotype
|
||
|
|
| MTInductive of string * monotype
|
||
|
|
|
||
|
|
type polytype =
|
||
|
|
| Mono of monotype
|
||
|
|
| Forall of string * polytype
|
||
|
|
|
||
|
|
type expr =
|
||
|
|
| EVar of string
|
||
|
|
| EPoly of string * expr
|
||
|
|
| ETypeSub
|
||
|
|
| ELam of string * monotype * expr
|
||
|
|
| EApp of expr * expr
|
||
|
|
| EAbort of expr
|
||
|
|
| EInl of expr
|
||
|
|
| EInr of expr
|
||
|
|
| ECase of expr * (string * expr) * (string * expr)
|
||
|
|
| EUnit
|
||
|
|
| EPair of expr * expr
|
||
|
|
| EFst of expr
|
||
|
|
| ESnd of expr
|
||
|
|
| ERoll of string * monotype * expr
|
||
|
|
| EFold of (string * monotype) * monotype * (expr * string * expr)
|
||
|
|
|
||
|
|
let rec appearsIn
|
||
|
|
(a : string)
|
||
|
|
(mono : monotype)
|
||
|
|
: prop
|
||
|
|
=
|
||
|
|
match mono with
|
||
|
|
| MTEmpty -> False
|
||
|
|
| MTUnit -> False
|
||
|
|
| MTVar b -> if a = b then True else False
|
||
|
|
| MTProd (left, right) -> appearsIn a left \/ appearsIn a right
|
||
|
|
| MTSum (left, right) -> appearsIn a left \/ appearsIn a right
|
||
|
|
| MTArrow (left, right) -> appearsIn a left \/ appearsIn a right
|
||
|
|
| MTInductive (b, t) -> if a = b then False else appearsIn a t
|
||
|
|
|
||
|
|
let rec strictlyPositive
|
||
|
|
(a : string)
|
||
|
|
(mono : monotype)
|
||
|
|
: prop
|
||
|
|
=
|
||
|
|
match mono with
|
||
|
|
| MTEmpty -> True
|
||
|
|
| MTUnit -> True
|
||
|
|
| MTVar b -> True
|
||
|
|
| MTProd (left, right) -> strictlyPositive a left /\ strictlyPositive a right
|
||
|
|
| MTSum (left, right) -> strictlyPositive a left /\ strictlyPositive a right
|
||
|
|
| MTArrow (t1, t2) -> ~(appearsIn a t1) /\ strictlyPositive a t2
|
||
|
|
| MTInductive (_, t) -> strictlyPositive a t
|
||
|
|
|
||
|
|
exception InductiveCase
|
||
|
|
|
||
|
|
let rec logNoInductive
|
||
|
|
(mono : monotype)
|
||
|
|
(a : string)
|
||
|
|
: Exn monotype (requires True) (ensures (fun _ -> True))
|
||
|
|
=
|
||
|
|
match mono with
|
||
|
|
| MTEmpty -> MTEmpty
|
||
|
|
| MTUnit -> MTEmpty
|
||
|
|
| MTVar a' -> if a' = a then MTUnit else MTEmpty
|
||
|
|
| MTArrow (t1, t2) -> MTProd (t1, logNoInductive t2 a)
|
||
|
|
| MTProd (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
|
||
|
|
| MTSum (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
|
||
|
|
| MTInductive (_, _) -> raise InductiveCase
|
||
|
|
|
||
|
|
let rec isVal
|
||
|
|
(e : expr)
|
||
|
|
: prop
|
||
|
|
=
|
||
|
|
match e with
|
||
|
|
| EPoly (_, _) -> True
|
||
|
|
| ELam (_, _, _) -> True
|
||
|
|
| EInl e' -> isVal e'
|
||
|
|
| EInr e' -> isVal e'
|
||
|
|
| EUnit -> True
|
||
|
|
| EPair (e1, e2) -> isVal e1 /\ isVal e2
|
||
|
|
| ERoll (_, _, e') -> isVal e'
|
||
|
|
| _ -> False
|
||
|
|
|
||
|
|
// | EVar _ -> True
|
||
|
|
// | ETypeSub -> True
|
||
|
|
// | EApp (_, _) -> True
|
||
|
|
// | EAbort _ -> True
|
||
|
|
// | ECase (_, _, _) -> True
|
||
|
|
// | EFst _ -> True
|
||
|
|
// | ESnd _ -> True
|
||
|
|
// | EFold (_, _, _) -> True
|