add more documentation

Author: pkoerner

src/lisb/translation/definition.clj

@@ -50,9 +50,6 @@
 
 ; Missing:
 ;;    Predicates
-;;    Set Operators
-;;    Relations
-;;    Functions
 ;;    Sequences
 ;;    Records
 ;;    Substitutions
@@ -325,10 +322,315 @@
    Then, map the expression over all those values and return the set intersection of the results.
    See also: union-pe, intersection, intersect-sets, sigma.")
 
+;; ----
+
+(op "cartesian-product" (cartesian-product #{1 2} #{3 4}) [& sets]
+  "Set operator. Calculates the cartesian product of all given sets.")
+
+(op "cart-or-mult" (cart-or-mult #{1 2} #{3 4}) [& all-sets-or-all-nums]
+  "DEPRECATED! Do not use this.
+   This is an internal node which only exists because the parser does not include
+   type checking information. It does not contain information whether it is 
+   a cartesian product or a multiplication. Please use instead:
+   *, cartesian-product.")
+;; -----
+
+(literal [1 -> 2]
+  "Tuple literal. Can be chained, for example, as [1 -> 2 -> 3 -> etc].
+   Must be a vector, must contain a left element, the arrow symbol `->` and a right element.
+   Does not directly create an intermediate representation but a tuple object instead.
+   Corresponding IR can be seen when the print is wrapped in
+      `(binding [lisb.translation.types/*as-ir* true] ...)`.
+   See also: maplet, |->.")
+
+(op "maplet" (maplet 1 2 3) [& elements]
+  "Tuple constructor. Creates the (nested) tuple from the passed elements.
+   See also: Tuple literal, |->")
+
+(op "|->" (|-> 1 2 3) [& elements]
+  "Tuple constructor. Creates the (nested) tuple from the passed elements.
+   Same as maplet.
+   See also: Tuple literal, maplet")
+
+
+;; --
+(op "<->" (<-> #{1 2} #{2 3}) [& sets]
+  "Returns the set of all relations between the given sets.
+   See also: relation, <<->, <->>, <<->>")
+
+(op "relation" (relation #{1 2} #{2 3}) [& sets]
+  "Returns the set of all relations between the given sets.
+   Same as <->.
+   See also: <->, total-relation, surjective-relation, total-surjective-relation.")
+
+(op "<<->" (<<-> #{1 2} #{2 3}) [& sets]
+  "Returns the set of all total relations between the given sets.
+   See also: total-relation, <->, <->>, <<->>")
+
+(op "total-relation" (total-relation #{1 2} #{2 3}) [& sets]
+  "Returns the set of all total relations between the given sets.
+   Same as <<->.
+   See also: <<->, relation, surjective-relation, total-surjective-relation.")
+
+(op "<->>" (<->> #{1 2} #{2 3}) [& sets]
+  "Returns the set of all surjective relations between the given sets.
+   See also: surjective-relation, <->, <<->, <<->>")
+
+(op "surjective-relation" (surjective-relation #{1 2} #{2 3}) [& sets]
+  "Returns the set of all total relations between the given sets.
+   Same as <->>.
+   See also: <->>, relation, total-relation, total-surjective-relation.")
+
+(op "<<->>" (<<->> #{1 2} #{2 3}) [& sets]
+  "Returns the set of all total and surjective relations between the given sets.
+   See also: total-surjective-relation, <->, <<->, <->>")
+
+(op "total-surjective-relation" (total-surjective-relation #{1 2} #{2 3}) [& sets]
+  "Returns the set of all total and surjective relations between the given sets.
+   Same as <<->>.
+   See also: <<->>, relation, total-relation, surjective-relation.")
+
+;; ---
+
+(op "dom" (dom #{[1 -> 2], [2 -> 3]}) [relation]
+  "Returns the domain of a given relation.
+   Note that the operation returns the left sides of the tuples actually contained 
+   in the relation, not the domain of the type of the relation.
+   See also: ran")
+
+(op "ran" (ran #{[1 -> 2], [2 -> 3]}) [relation]
+  "Returns the range of a given relation.
+   Note that the operation returns the right sides of the tuples actually contained 
+   in the relation, not the domain of the type of the relation.
+   See also: dom")
+
+;; --
+(op "id" (id #{1 2 3}) [set]
+  "Returns the identity relation over a given set, mapping each element to itself.")
+
+
+;; --
+(op "<|" (<| #{1 2 3} #{[0 -> 1] [1 -> 2]}) [set relation]
+  "Restricts the domain of a relation to the specified set, i.e., it removes all tuples
+   whose left-hand side is not contained in the set.
+   See also: domain-restriction, <||, |>, |>>")
+
+(op "domain-restriction" (domain-restriction #{1 2 3} #{[0 -> 1] [1 -> 2]}) [set relation]
+  "Restricts the domain of a relation to the specified set, i.e., it removes all tuples
+   whose left-hand side is not contained in the set.
+   Same as <|.
+   See also: <|, domain-subtraction, range-restriction")
+
+(op "<||" (<| #{1 2 3} #{[0 -> 1] [1 -> 2]}) [set relation]
+  "Subtracts the specified set from the domain of the relation, i.e., it removes all tuples
+   whose left-hand side is contained in the set.
+   See also: domain-subtraction, <|, |>, |>>")
+
+(op "domain-subtraction" (domain-subtraction #{1 2 3} #{[0 -> 1] [1 -> 2]}) [set relation]
+  "Subtracts the specified set from the domain of the relation, i.e., it removes all tuples
+   whose left-hand side is contained in the set.
+   Same as <||.
+   See also: <|, domain-restriction, range-subtraction")
+
+(op "|>" (|> #{[0 -> 1] [1 -> 2]} #{1 2 3}) [relation set]
+  "Restricts the range of a relation to the specified set, i.e., it removes all tuples
+   whose right-hand side is not contained in the set.
+   See also: range-restriction, <|, <||, <<|, |>>")
+
+(op "range-restriction" (range-restriction #{[0 -> 1] [1 -> 2]} #{1 2 3} ) [relation set]
+  "Restricts the domain of a relation to the specified set, i.e., it removes all tuples
+   whose left-hand side is not contained in the set.
+   Same as |>.
+   See also: |>, domain-restriction, range-subtraction")
+
+(op "|>>" (|>> #{[0 -> 1] [1 -> 2]} #{1 2 3}) [relation set]
+  "Subtracts the specified set from the range of the relation, i.e., it removes all tuples
+   whose right-hand side is contained in the set.
+   See also: range-restriction, <|, <||, <<|, |>>")
+
+(op "range-subtraction" (range-restriction #{[0 -> 1] [1 -> 2]} #{1 2 3} ) [relation set]
+  "Subtracts the specified set from the range of the relation, i.e., it removes all tuples
+   whose right-hand side is contained in the set.
+   Same as |>>.
+   See also: |>>, domain-subtraction, range-restriction")
+
+;; ---
+(op "inverse" (inverse #{[1 -> 2]}) [relation]
+  "Returns the inverse relation that swaps the left- and right-hand side of all contained tuples.")
+
+(op "image" (image #{[1 -> 2] [2 -> 3] [3 -> 4]} #{1 2}) [relation set]
+  "Returns the relational image, i.e., the set of all right-hand sides contained in the relation,
+   whose left-hand side is contained in the passed set.")
+
+(op "<+" (<+ #{[1 -> 2] [1 -> 3] [3 -> 4]} #{[1 -> 1] [2 -> 0]}) [& relations]
+  "Relational override. Can be seen as a combination of domain subtraction of the domain of relation2
+   from relation1, followed by a union with relation2.")
+
+(op "override" (override #{[1 -> 2] [1 -> 3] [3 -> 4]} #{[1 -> 1] [2 -> 0]}) [& relations]
+  "Relational override. Can be seen as a combination of domain subtraction of the domain of relation2
+   from relation1, followed by a union with relation2.
+   Same as <+.")
+
+(op "><" (>< #{[3 -> 4] [1 -> 2] [2 -> 3]} #{[4 -> 0] [1 -> 0]}) [& relations]
+  "Direct product of the relations. If relation1 and relation2 have tuples with the same left-hand side,
+   the resulting relation will contain a tuple with this value as its left-hand side and
+   both right-hand sides of relation1 and relation2 as its right-hand side.
+   Could be written as: {x,y,z | (x,y) : relation1 & (x,z) : relation2} 
+   See also: direct-product.")
+
+(op "direct-product" (direct-product #{[3 -> 4] [1 -> 2] [2 -> 3]} #{[4 -> 0] [1 -> 0]}) [& relations]
+  "Direct product of the relations. If relation1 and relation2 have tuples with the same left-hand side,
+   the resulting relation will contain a tuple with this value as its left-hand side and
+   both right-hand sides of relation1 and relation2 as its right-hand side.
+   Could be written as: {x,y,z | (x,y) : relation1 & (x,z) : relation2}.
+   Same as ><.
+   See also: ><.")
+
+(op "composition" (composition #{[1 -> 2] [3 -> 4]} #{[2 -> 6] [4 -> 4]}) [& relations]
+  "The composition of two relations. If a right-hand side of relation1 is contained as a left-hand side
+   in relation2, replace its with the corresponding right-hand side of relation2.
+   Could be written as: {x,z | exists y . (x,y) : relation1 & (y,z) : relation2}.") 
+
+(op "parallel-product" (parallel-product #{[3 -> 4] [1 -> 2]} #{[5 -> 6] [7 -> 8]}) [& relations]
+  "Parallel product of two relations. Returns a set of nested tuples [lhs1 -> lhs2 -> [rhs1 -> rhs2]].
+   Could be written as: {((x,v), (y,w)) | (x,y) : relation1 & (v,w) : relation2}.")
+
+;; --
+(op "prj1" (prj1 nat-set nat-set) [set-domain set-range]
+  "Transformation function.
+   Returns a projection function, properly typed according to the passed sets.
+   If a tuple is passed to this function, will return the left-hand side.")
+
+(op "prj2" (prj2 nat-set nat-set) [set-domain set-range]
+  "Transformation function.
+   Returns a projection function, properly typed according to the passed sets.
+   If a tuple is passed to this function, will return the right-hand side.")
+
+;; --
+(op "closure" (closure #{[1 -> 2] [2 -> 3]}) [relation]
+  "Transitive and reflexive closure.
+   Transitive: If [elem1 -> elem2] and [elem2 -> elem3] is contained in the relation, [elem1 -> elem3]
+               will be contained as well. Same with any element that is further 'reachable' from elem3.
+   Reflexive: If elem is contained as a left-hand side, [elem -> elem] will be contained in the result.
+   See also: closure1, iterate.")
+
+(op "closure1" (closure1 #{[1 -> 2] [2 -> 3]}) [relation]
+  "Transitive closure.
+   Transitive: If [elem1 -> elem2] and [elem2 -> elem3] is contained in the relation, [elem1 -> elem3]
+               will be contained as well. Same with any element that is further 'reachable' from elem3.
+   Will only contain [elem -> elem] if elem is reachable from the same node via a non-empty 'path'.
+   See also: closure, iterate.")
+
+(op "iterate" (iterate #{[1 -> 2] [2 -> 3]} 2) [relation n]
+  "Iteration of the relation.
+   Will contain tuples [elem1 -> elem2] with elem2 'reachable' from elem1 within n steps.
+   See also: closure, closure1.")
+
+;; --
+(op "fnc" (fnc #{[1 -> 2] [1 -> 3]}) [relation]
+  "Transformation function. Will transform the relation to a function by collecting all right-hand sides
+   of the same left-hand side as a set and create the corresponding mapping #{[lhs1 -> #{rhs1, rhs2}] etc}.
+   Inverse function of rel.
+   See also: rel.")
+
+(op "rel" (rel #{(maplet 1 #{1 2})}) [function]
+  "Transformation function. Will transform a function of the form elem -> set(elems) by 'splicing'
+   the set into (multiple) relational mappings [elem -> elem1], [elem -> elem2], etc.
+   Inverse function of fnc.
+   See also: fnc.")
+
+;; ---
+
+(op "+->" (+-> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial functions from set1 to set2.
+   See also: partial-function, -->, +->>, >+>, >+>>.")
+
+(op "partial-function" (partial-function #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial functions from set1 to set2.
+   Same as +->.
+   See also: +->, total-function, partial-surjection, partial-injection, partial-bijection.")
+
+(op "-->" (--> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total functions from set1 to set2.
+   See also: total-function, +->, -->>, >->, >->>.")
+
+(op "total-function" (total-function #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total functions from set1 to set2.
+   Same as -->.
+   See also: -->, partial-function, total-surjection, total-injection, total-bijection.")
+
+(op "+->>" (+->> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial surjective functions from set1 to set2.
+   See also: partial-surjection, -->, +->>, >+>, >+>>.")
+
+(op "partial-surjection" (partial-surjection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial surjective functions from set1 to set2.
+   Same as +->>.
+   See also: +->>, total-surjection, partial-function, partial-injection, partial-bijection.")
+
+(op "-->>" (-->> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total surjective functions from set1 to set2.
+   See also: total-surjection, -->, +->>, >->, >->>.")
+
+(op "total-surjection" (total-surjection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total surjective functions from set1 to set2.
+   Same as -->>.
+   See also: +->>, total-function, partial-surjection, total-injection, total-bijection.")
+
+
+(op ">+>" (>+> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial injective functions from set1 to set2.
+   See also: partial-injection, >->, +->, +->>, >+>>.")
+
+(op "partial-injection" (partial-injection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial injective functions from set1 to set2.
+   Same as >+>.
+   See also: +->>, total-injection, partial-function, partial-surjection, partial-bijection.")
+
+(op ">->" (>-> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total injective functions from set1 to set2.
+   See also: total-injection, -->, +->>, >->, >->>.")
+
+(op "total-injection" (total-surjection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total injective functions from set1 to set2.
+   Same as >->.
+   See also: >->, total-function, partial-injection, total-surjection, total-bijection.")
+
+
+(op ">+>>" (>+>> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial bijective functions from set1 to set2.
+   See also: partial-bijection, >->>, +->, +->>, >+>.")
+
+(op "partial-bijection" (partial-bijection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all partial bijective functions from set1 to set2.
+   Same as >+>>.
+   See also: +->>, total-bijection, partial-function, partial-surjection, partial-injection.")
+
+(op ">->>" (>->> #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total bijective functions from set1 to set2.
+   See also: total-bijection, -->, >+>>, >->, -->>.")
+
+(op "total-bijection" (total-bijection #{1 2 3} #{4 5 6}) [set1 set2]
+  "Set of all total bijective functions from set1 to set2.
+   Same as >->>.
+   See also: >->, total-function, partial-bijection, total-surjection, total-injection.")
+
+;; ---
+
+(op "lambda" (lambda [:x] (member? :x #{1 2}) (inc :x)) [ids pred expr]
+  "Lambda expression. Creates a function mapping all identifer values constrained by the predicate
+   to the given expression (likely depending on the identifier values).")
+
+(op "fn-call" (fn-call #{[1 -> 2]} 1) [fn & elems]
+  "Function call. Will apply the function to the specified element.
+   Has a well-definedness condition. The element must be in the domain of the function.")
+ 
+
 ])
 
 
 
+
 (defn bpropos [search & {:as opts :keys [short]}]
   (let [search (clojure.string/lower-case search)]
     (doseq [res (filter (fn [x] (some #(clojure.string/includes?
@@ -342,3 +644,4 @@
 
 (comment (bpropos "add" :short false)
 (bpropos "greater"))
+(bpropos "NAT")