examples/problems/graph-types.shape

   1 /** This file is part of Shapes.
   2  **
   3  ** Shapes is free software: you can redistribute it and/or modify
   4  ** it under the terms of the GNU General Public License as published by
   5  ** the Free Software Foundation, either version 3 of the License, or
   6  ** any later version.
   7  **
   8  ** Shapes is distributed in the hope that it will be useful,
   9  ** but WITHOUT ANY WARRANTY; without even the implied warranty of
  10  ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  11  ** GNU General Public License for more details.
  12  **
  13  ** You should have received a copy of the GNU General Public License
  14  ** along with Shapes.  If not, see <http://www.gnu.org/licenses/>.
  15  **
  16  ** Copyright 2013 Henrik Tidefelt
  17  **/
  18
  19 /** In the type system, all nodes of a graph have one value type, and all edges have one value type. **/
  20 gv:: [§Graph §String §Real]
  21 /**
  22 Nodes and edges have nominal types, since they have hidden member data that enable efficient use.
  23 §Node: \ §n §e → nominal (> key:§Symbol degree:§Integer edges:[§List [§Edge §e]] value:§n ... <)
  24 §Edge: \ §e → nominal (> value:§e <)
  25 **/
  26 node_gva:: [§Node §String §Real]
  27 node_gva: [gv.find_node 'a]
  28 •stdout << `Type of a node: ´ << (typestring typeof node_gva) << "{n}
  29
  30 /** Graph domain type **/
  31 [§USimpleGraph §N §E]: [§Graph §N §E] ∩ (> directed::§(false) loops::§(false) parallel::§(false) <)
  32
  33 {
  34   /** First some notes on fields of singleton types in general. **/
  35
  36   /** A value of singleton type. **/
  37   bar::§(8)
  38   bar: 8     /** The right hand side must be possible to evaluate at compile time **/
  39
  40   /** A function that returns a subtype of a structure where a field has a particular value **/
  41   §AB: (> a::§Real b::§Boolean <)                  /** Generic type. **/
  42   f:: \ x::§Real y::§Boolean → §AB ∩ (> b::§(y) <) /** Return type is the subtype of §AB where b has the singleton type given by the argument y.
  43                                                     ** The argument passed as y to f must be possible to evaluate at compile time.
  44                                                     **/
  45   f: \ x y → (> a:x b:y <)                         /** The type system can think of the type of y as "§(y)" which is known to be a subtype of §Boolean. **/
  46
  47   foo:: §AB ∩ (> b::§(true) <) /** That is, foo has type (> a::§Real b::§(true) <). **/
  48   foo: [f 1.5 true]            /** "true" can be evaluated at compile time. **/
  49
  50   [f 1.5 (•time) > 1] /** Since (•time) > 1 cannot be evaluated at compile time, the result type is simply §AB. **/
  51 }
  52
  53 graph:: ∀§N ∀§E \ nodes::[§List [§NodeData §N]] edges::[§List [§EdgeData §E]] undirected::§Boolean:false directed::§Boolean:false loops::§Boolean:false parallel::§Boolean:false → [§Graph §N §E] ∩ (> undirected?::§(not directed) directed?::§(not undirected) mixed?::§(directed and undirected) loops?::§(loops) parallel?::§(parallel) <)