move refine and linear integer stuff in docs (#533)

typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl

@@ -44,3 +44,93 @@ you want, so you shouldn't use @racket[make-predicate] with these types.
     (radians 0)
     (f (radians 0))]
 }
+
+
+
+@section{Refinements and Linear Integer Reasoning}
+
+Refinement types have been added to Typed Racket's core, but
+Typed Racket does not yet have function types which allow
+dependencies between argument types, limiting how useful
+refinements are for now. Allowing argument dependencies
+is on our `to do' list.
+
+@defform[#:literals (Refine : Top Bot ! and or when
+                            unless if < <= = > >= car cdr
+                            vector-length + *)
+         (Refine [id : type] proposition)
+         #:grammar
+         ([proposition Top
+           Bot
+           (: symbolic-object type)
+           (! symbolic-object type)
+           (and proposition ...)
+           (or proposition ...)
+           (when proposition proposition)
+           (unless proposition proposition)
+           (if proposition proposition proposition)
+           (linear-comp symbolic-object symbolic-object)]
+          [linear-comp < <= = >= >]
+          [symbolic-object exact-integer
+           linear-term
+           (+ linear-term linear-term ...)]
+          [linear-term symbolic-path
+           (* exact-integer symbolic-path)]
+          [symbolic-path id
+           (path-elem symbolic-path)]
+          [path-elem car
+           cdr
+           vector-length])]{@racket[(Refine [v : t] p)] is a
+ refinement of type @racket[t] with logical proposition
+ @racket[p], or in other words it describes any value
+ @racket[v] of type @racket[t] for which the logical
+ proposition @racket[p] holds.
+
+ @ex[(ann 42 (Refine [n : Integer] (= n 42)))]
+
+ Note: The identifier in a refinement type is in scope
+ inside the proposition, but not the type.
+
+}
+
+
+@racket[(: o t)] used as a proposition holds when symbolic object @racket[o]
+is of type @racket[t.]
+
+@defform[(! sym-obj type)]{This is the dual of @racket[(: o t)], holding
+when @racket[o] is not of type @racket[t].}
+
+Propositions can also describe linear inequalities (e.g. @racket[(<= x 42)]
+holds when @racket[x] is less than or equal to @racket[42]), using any
+of the following relations: @racket[<=], @racket[<], @racket[=],
+@racket[>=], @racket[>].
+
+The following logical combinators hold as one would expect
+depending on which of their subcomponents hold hold:
+@racket[and], @racket[or], @racket[if], @racket[not].
+
+@racket[(when p q)] is equivalent to @racket[(or (not p) (and p q))].
+
+@racket[(unless p q)] is equivalent to @racket[(or p q)].
+
+Typed Racket's linear integer reasoning is turned off by
+default. If you want to activate it, you must add the
+@racket[#:with-linear-integer-arithmetic] keyword when
+specifying the language of your program:
+
+
+@racketmod[typed/racket #:with-linear-integer-arithmetic]
+
+
+With this language option on, code such as the following
+will type check:
+
+@racketblock[(if (< 5 4)
+                 (+ "Luke," "I am your father")
+                 "that's impossible!")]
+
+i.e. with linear integer reasoning enabled, Typed Racket
+detects that the comparison is guaranteed to produce
+@racket[#f], and thus the clearly ill-typed `then'-branch is
+ignored by the type checker since it is guaranteed to be
+dead code.

typed-racket-doc/typed-racket/scribblings/reference/types.scrbl

@@ -717,6 +717,13 @@ functions and continuation mark functions.
   contract combinator, but with types instead of contracts.
   }
 
+@deftogether[(
+@defidform[Top]
+@defidform[Bot])]{ These are propositions that can be used with @racket[->].
+  @racket[Top] is the propositions with no information.
+  @racket[Bot] is the propositions which means the result cannot happen.
+}
+
 
 @defidform[Procedure]{is the supertype of all function types. The @racket[Procedure]
   type corresponds to values that satisfy the @racket[procedure?] predicate.
@@ -816,89 +823,16 @@ this top type.
         #s((salad food 1) "quinoa" "EVOO" salad))]
 }
 
-
 @defalias[Union U]
 @defalias[Intersection ∩]
 @defalias[→ ->]
 @defalias[case→ case->]
 @defalias[∀ All]
 
-
-@section{Logical Refinements and Propositions}
-
-
-@defform[#:literals (Refine : Top Bot ! and or when
-                            unless if < <= = > >= car cdr
-                            vector-length + *)
-         (Refine [id : type] proposition)
-         #:grammar
-         ([proposition Top
-           Bot
-           (: symbolic-object type)
-           (! symbolic-object type)
-           (and proposition ...)
-           (or proposition ...)
-           (when proposition proposition)
-           (unless proposition proposition)
-           (if proposition proposition proposition)
-           (linear-comp symbolic-object symbolic-object)]
-          [linear-comp < <= = >= >]
-          [symbolic-object exact-integer
-           linear-term
-           (+ linear-term linear-term ...)]
-          [linear-term symbolic-path
-           (* exact-integer symbolic-path)]
-          [symbolic-path id
-           (path-elem symbolic-path)]
-          [path-elem car
-           cdr
-           vector-length])]{@racket[(Refine [v : t] p)] is a
- refinement of type @racket[t] with logical proposition
- @racket[p], or in other words it describes any value
- @racket[v] of type @racket[t] for which the logical
- proposition @racket[p] holds.
-
- @ex[(ann 42 (Refine [n : Integer] (= n 42)))]
-
- Note: The identifier in a refinement type is in scope
- inside the proposition, but not the type.
-
-}
-
-@deftogether[(
-@defidform[Top]
-@defidform[Bot])]{ These are propositions that can be used with
- @racket[->] and @racket[Refine].
-  @racket[Top] is the proposition with no information (i.e. the trivially true
- proposition).
-  @racket[Bot] is the propositions which means the result cannot happen
- (i.e. the impossible proposition).
-}
-
-@racket[(: o t)] used as a proposition holds when symbolic object @racket[o]
-is of type @racket[t.]
-
-@defform[(! sym-obj type)]{This is the dual of @racket[(: o t)], holding
-when @racket[o] is not of type @racket[t].}
-
-Propositions can also describe linear inequalities (e.g. @racket[(<= x 42)]
-holds when @racket[x] is less than or equal to @racket[42]), using any
-of the following relations: @racket[<=], @racket[<], @racket[=],
-@racket[>=], @racket[>].
-
-The following logical combinators hold as one would expect
-depending on which of their subcomponents hold hold:
-@racket[and], @racket[or], @racket[if], @racket[not].
-
-@racket[(when p q)] is equivalent to @racket[(or (not p) (and p q))].
-
-@racket[(unless p q)] is equivalent to @racket[(or p q)].
-
-
 @section{Other Types}
 
 @defform[(Option t)]{Either @racket[t] or @racket[#f]}
 @defform[(Opaque t)]{A type constructed using the @racket[#:opaque]
 clause of @racket[require/typed].}
 
-@(close-eval the-eval)
+@(close-eval the-eval)