{"action":"opened","issue":{"url":"https://api.github.com/repos/HIPERFIT/futhark/issues/24","labels_url":"https://api.github.com/repos/HIPERFIT/futhark/issues/24/labels{/name}","comments_url":"https://api.github.com/repos/HIPERFIT/futhark/issues/24/comments","events_url":"https://api.github.com/repos/HIPERFIT/futhark/issues/24/events","html_url":"https://github.com/HIPERFIT/futhark/issues/24","id":59953909,"number":24,"title":"Function-Level Shape/Invariant Annotatations","user":{"login":"coancea","id":1225483,"avatar_url":"https://avatars.githubusercontent.com/u/1225483?v=3","gravatar_id":"","url":"https://api.github.com/users/coancea","html_url":"https://github.com/coancea","followers_url":"https://api.github.com/users/coancea/followers","following_url":"https://api.github.com/users/coancea/following{/other_user}","gists_url":"https://api.github.com/users/coancea/gists{/gist_id}","starred_url":"https://api.github.com/users/coancea/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/coancea/subscriptions","organizations_url":"https://api.github.com/users/coancea/orgs","repos_url":"https://api.github.com/users/coancea/repos","events_url":"https://api.github.com/users/coancea/events{/privacy}","received_events_url":"https://api.github.com/users/coancea/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-03-05T13:51:46Z","updated_at":"2015-03-05T13:51:46Z","closed_at":null,"body":"Internal Futhark:\r\n\r\nfun [([int,k1], char, [bool,k2]), k3]\r\n    myFun(int M, int N, [[real, k4],M] arr)\r\n            where { k1 < k2, \r\n                         k3 in k2 + N ... M,\r\n                         k2 = k4*k4 + M + N\r\n                         k4 < M + N,\r\n                         M >= MAX(2*N,0),\r\n                         arr in N ... M-1 } = \r\n    body of function\r\n\r\nSuch annotations allow the user to specify invariants related to\r\nsimple algebraic relations between integers. (Perhaps MIN and \r\nMAX should become part of the language as well.)\r\n\r\nOnly symbols can appear in shapes: either an int parameter of the function\r\n(i.e., not existential) or an (existential) symbol that need to be qualified in \r\nexactly one of the where clauses.  \r\n\r\n`where' clause specifies relations between scalars\r\n      I.  -- there is exactly one symbol on the left-hand side, followed by\r\n          -- a relation, which can be >, >=, <, <=, =, in \r\n                 `in' requires a lower-bound and an upper-bound expression\r\n         -- followed by a (simple) algebraic scalar expression\r\n     II. a symbol may appear in the left-hand side of at most one qualification!\r\n    III. a symbol use in a where clause CANNOT be followed by a qualification\r\n         of that symbol, i.e., regular chain: first define the contraint, then use \r\n         the symbol.\r\n    IV. Note that arrays can be qualified as well: the last qualification\r\n         `arr in N ... M-1' means that all elements of `arr' have lower\r\n         bound N and upper bound M-1.  \r\n\r\n1. Most Relaxed (Liberal) Semantics:\r\n    -- everything is optional, whatever is specified will be checked, i.e.,\r\n        translated to assertions (if function is inlined) and will\r\n        be used for range propagation, allocation, etc.\r\n    -- whatever is not specified will be computed (as currently done)\r\n\r\n2. Restricted Semantics:\r\n        -- all array-parameter shapes should be exactly specified \r\n            (with equality) in terms of former declared scalars (can \r\n            even be required that all such scalars come first)\r\n        -- all result-array shapes have to be specified at least with an\r\n            upper bound.\r\n\r\n3. Combined: compiler flag that determines which 1. or 2.\r\n    and reduces to transforming 1 into 2, which ``should'' not\r\n    be too difficult\r\n\r\n"}}