{"action":"created","comment":{"url":"https://api.github.com/repos/spechub/Hets/pulls/comments/66434485","id":66434485,"diff_hunk":"@@ -0,0 +1,184 @@\n+{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}\n+{- |\n+Module      :  $Header$\n+Description :  prenex normal form for sentences of a CASL theory\n+Copyright   :  (c) Mihai Codescu, 2016\n+License     :  GPLv2 or higher, see LICENSE.txt\n+\n+Maintainer  :  codescu@iws.cs.uni-magdeburg.de\n+Stability   :  provisional\n+Portability :  non-portable (imports Logic.Comorphism)\n+\n+-}\n+\n+module Comorphisms.CASL2Prenex where\n+\n+import Logic.Logic\n+import Logic.Comorphism\n+\n+import CASL.Logic_CASL\n+import CASL.AS_Basic_CASL\n+import CASL.Sign\n+import CASL.Morphism\n+import CASL.Sublogic as SL hiding (bottom)\n+import CASL.Induction\n+import CASL.Quantification\n+\n+import Common.Result\n+import Common.Id\n+import qualified Data.Set as Set\n+\n+import Common.AS_Annotation\n+import Common.ProofTree\n+\n+data CASL2Prenex = CASL2Prenex deriving Show\n+\n+instance Language CASL2Prenex where\n+    language_name CASL2Prenex = \"CASL2Prenex\"\n+\n+instance Comorphism CASL2Prenex\n+               CASL CASL_Sublogics\n+               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS\n+               CASLSign\n+               CASLMor\n+               Symbol RawSymbol ProofTree\n+               CASL CASL_Sublogics\n+               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS\n+               CASLSign\n+               CASLMor\n+               Symbol RawSymbol ProofTree where\n+    sourceLogic CASL2Prenex = CASL\n+    sourceSublogic CASL2Prenex = SL.caslTop\n+    targetLogic CASL2Prenex = CASL\n+    mapSublogic CASL2Prenex sl = Just sl -- TODO\n+    map_theory CASL2Prenex = mapTheory\n+    map_morphism CASL2Prenex = return\n+    map_sentence CASL2Prenex sig = return . (mapSentence sig)\n+    map_symbol CASL2Prenex _ = Set.singleton . id\n+    has_model_expansion CASL2Prenex = True\n+    is_weakly_amalgamable CASL2Prenex = True\n+\n+-- remove equivalences\n+preprocessSen :: CASLFORMULA -> CASLFORMULA\n+preprocessSen sen = case sen of\n+ Quantification q vdecls sen' r ->\n+   Quantification q vdecls (preprocessSen sen') r\n+ Junction j sens r -> \n+   Junction j (map preprocessSen sens) r\n+ Relation sen1 Equivalence sen2 _ -> let\n+    sen1' = Relation sen1 Implication sen2 nullRange\n+    sen2' = Relation sen2 Implication sen1 nullRange\n+   in Junction Con [sen1', sen2'] nullRange\n+ Relation sen1 rel sen2 r -> \n+   Relation (preprocessSen sen1) rel \n+            (preprocessSen sen2) r\n+ Negation sen' r -> \n+   Negation (preprocessSen sen') r\n+ _ -> sen\n+\n+-- make variables distinct: \n+-- if a variable v of sort s already appears in a formula\n+-- substitute it with a fresh variable\n+mkDistVars :: CASLFORMULA -> CASLFORMULA\n+mkDistVars sen = \n+ let (_, _, sen') = mkDistVarsAux 0 [] sen\n+ in sen'\n+\n+mkDistVarsAux :: Int -- first available suffix for vars\n+              -> [(VAR, SORT)] -- vars encountered so far\n+              -> CASLFORMULA\n+              -> (Int, [(VAR, SORT)], CASLFORMULA)\n+mkDistVarsAux n vlist sen = case sen of\n+ Quantification q vdecls form range -> let\n+   -- first make variables distinct for form\n+   dvars = flatVAR_DECLs vdecls\n+   (n', _, form') = mkDistVarsAux n (dvars ++ vlist) form\n+   -- here we are not interested in the variables generated for the quantified form, so we can forget them\n+   replVarDecl vds oN nN s = reverse $ \n+                              foldl (\\usedD vd@(Var_decl names sort r) -> \n+                                       if sort == s then -- found it, replace oN with nN in names\n+                                         let vd' = Var_decl (map (\\x -> if x == oN then nN else x) names) sort r  \n+                                         in vd':usedD\n+                                       else vd:usedD \n+                                 ) [] vds\n+   checkAndReplace (n0, knownV, quantF, quants) (x, s) =\n+      if (x,s) `elem` knownV \n+       then\n+         let  \n+           x' = genNumVar \"x\" n0\n+           quants' = replVarDecl quants x x' s\n+           quantF' = substitute x s (Qual_var x' s nullRange) quantF\n+         in (n0 + 1, (x', s):knownV, quantF', quants')\n+       else (n0    , (x , s):knownV, quantF , quants )  \n+   (n'', vlist', form'', vdecls') = foldl checkAndReplace (n', vlist, form', vdecls) dvars\n+  in (n'', vlist', Quantification q vdecls' form'' range)\n+ Junction j sens r -> let\n+   (n', vlist', sens') = foldl (\\(x, vs, osens) s -> \n+                           let\n+                            (x', vs', s') = mkDistVarsAux x vs s\n+                           in (x', vs', s':osens)) (n, vlist, []) sens\n+  in (n', vlist', Junction j (reverse sens') r)\n+ Relation sen1 rel sen2 r -> let\n+   (n1, vlist1, sen1') = mkDistVarsAux n  vlist  sen1\n+   (n2, vlist2, sen2') = mkDistVarsAux n1 vlist1 sen2\n+  in (n2, vlist2, Relation sen1' rel sen2' r)\n+ Negation sen' r -> let \n+   (n', vlist', sen'') = mkDistVarsAux n vlist sen' \n+  in (n', vlist', Negation sen'' r)\n+ _ -> (n, vlist, sen)\n+       \n+computePNF :: CASLFORMULA -> CASLFORMULA\n+computePNF sen = case sen of \n+ Negation nsen _ -> let \n+   nsen' = computePNF nsen\n+   in case nsen' of \n+       Quantification q vdecls qsen _ -> \n+         Quantification (dualQuant q) vdecls \n+                        (computePNF $ Negation qsen nullRange) nullRange\n+       _ -> Negation nsen' nullRange\n+ Relation sen1 Implication sen2 _ -> let \n+   sen1' = computePNF sen1\n+   sen2' = computePNF sen2\n+   in case sen1' of \n+      Quantification q vdecls qsen _ -> \n+        Quantification (dualQuant q) vdecls (computePNF $ Relation qsen Implication sen2 nullRange) nullRange\n+      _ -> case sen2' of \n+        Quantification q vdecls qsen _ -> \n+          Quantification q vdecls \n+            (computePNF $ Relation sen1' Implication qsen nullRange) nullRange \n+          -- recursive call to catch multiple quantifiers for sen2'\n+        _ -> -- no quantifications\n+          Relation sen1' Implication sen2' nullRange\n+ Relation sen1 RevImpl sen2 _ -> \n+  computePNF $ Relation sen2 Implication sen1 nullRange\n+ Quantification q vdecls qsen _ -> \n+  Quantification q vdecls (computePNF qsen) nullRange\n+ Junction j sens _ -> let\n+   sens' = map computePNF sens\n+   processQuants asen = case asen of\n+     Quantification q vdecls sen' _ -> Quantification q vdecls (processQuants sen') nullRange","path":"Comorphisms/CASL2Prenex.hs","position":159,"original_position":159,"commit_id":"e2fdd28e29f151215a081dd95fcc443a4c8ccf23","original_commit_id":"e2fdd28e29f151215a081dd95fcc443a4c8ccf23","user":{"login":"tillmo","id":642775,"avatar_url":"https://avatars.githubusercontent.com/u/642775?v=3","gravatar_id":"","url":"https://api.github.com/users/tillmo","html_url":"https://github.com/tillmo","followers_url":"https://api.github.com/users/tillmo/followers","following_url":"https://api.github.com/users/tillmo/following{/other_user}","gists_url":"https://api.github.com/users/tillmo/gists{/gist_id}","starred_url":"https://api.github.com/users/tillmo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tillmo/subscriptions","organizations_url":"https://api.github.com/users/tillmo/orgs","repos_url":"https://api.github.com/users/tillmo/repos","events_url":"https://api.github.com/users/tillmo/events{/privacy}","received_events_url":"https://api.github.com/users/tillmo/received_events","type":"User","site_admin":false},"body":"this code will never be entered, because `processQuants` is only called on a `Junction`.","created_at":"2016-06-09T12:54:06Z","updated_at":"2016-06-09T12:54:06Z","html_url":"https://github.com/spechub/Hets/pull/1593#discussion_r66434485","pull_request_url":"https://api.github.com/repos/spechub/Hets/pulls/1593","_links":{"self":{"href":"https://api.github.com/repos/spechub/Hets/pulls/comments/66434485"},"html":{"href":"https://github.com/spechub/Hets/pull/1593#discussion_r66434485"},"pull_request":{"href":"https://api.github.com/repos/spechub/Hets/pulls/1593"}}},"pull_request":{"url":"https://api.github.com/repos/spechub/Hets/pulls/1593","id":62583414,"html_url":"https://github.com/spechub/Hets/pull/1593","diff_url":"https://github.com/spechub/Hets/pull/1593.diff","patch_url":"https://github.com/spechub/Hets/pull/1593.patch","issue_url":"https://api.github.com/repos/spechub/Hets/issues/1593","number":1593,"state":"open","locked":false,"title":"Skolemization and prenex normal form","user":{"login":"mcodescu","id":1632930,"avatar_url":"https://avatars.githubusercontent.com/u/1632930?v=3","gravatar_id":"","url":"https://api.github.com/users/mcodescu","html_url":"https://github.com/mcodescu","followers_url":"https://api.github.com/users/mcodescu/followers","following_url":"https://api.github.com/users/mcodescu/following{/other_user}","gists_url":"https://api.github.com/users/mcodescu/gists{/gist_id}","starred_url":"https://api.github.com/users/mcodescu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mcodescu/subscriptions","organizations_url":"https://api.github.com/users/mcodescu/orgs","repos_url":"https://api.github.com/users/mcodescu/repos","events_url":"https://api.github.com/users/mcodescu/events{/privacy}","received_events_url":"https://api.github.com/users/mcodescu/received_events","type":"User","site_admin":false},"body":"","created_at":"2016-03-11T18:31:50Z","updated_at":"2016-06-09T12:54:06Z","closed_at":null,"merged_at":null,"merge_commit_sha":"573a9bce8c84e8fe7e405be846caac02730f95fb","assignee":null,"milestone":null,"commits_url":"https://api.github.com/repos/spechub/Hets/pulls/1593/commits","review_comments_url":"https://api.github.com/repos/spechub/Hets/pulls/1593/comments","review_comment_url":"https://api.github.com/repos/spechub/Hets/pulls/comments{/number}","comments_url":"https://api.github.com/repos/spechub/Hets/issues/1593/comments","statuses_url":"https://api.github.com/repos/spechub/Hets/statuses/e2fdd28e29f151215a081dd95fcc443a4c8ccf23","head":{"label":"spechub:skolemization_and_prenex_normal_form","ref":"skolemization_and_prenex_normal_form","sha":"e2fdd28e29f151215a081dd95fcc443a4c8ccf23","user":{"login":"spechub","id":6953185,"avatar_url":"https://avatars.githubusercontent.com/u/6953185?v=3","gravatar_id":"","url":"https://api.github.com/users/spechub","html_url":"https://github.com/spechub","followers_url":"https://api.github.com/users/spechub/followers","following_url":"https://api.github.com/users/spechub/following{/other_user}","gists_url":"https://api.github.com/users/spechub/gists{/gist_id}","starred_url":"https://api.github.com/users/spechub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spechub/subscriptions","organizations_url":"https://api.github.com/users/spechub/orgs","repos_url":"https://api.github.com/users/spechub/repos","events_url":"https://api.github.com/users/spechub/events{/privacy}","received_events_url":"https://api.github.com/users/spechub/received_events","type":"Organization","site_admin":false},"repo":{"id":20492711,"name":"Hets","full_name":"spechub/Hets","owner":{"login":"spechub","id":6953185,"avatar_url":"https://avatars.githubusercontent.com/u/6953185?v=3","gravatar_id":"","url":"https://api.github.com/users/spechub","html_url":"https://github.com/spechub","followers_url":"https://api.github.com/users/spechub/followers","following_url":"https://api.github.com/users/spechub/following{/other_user}","gists_url":"https://api.github.com/users/spechub/gists{/gist_id}","starred_url":"https://api.github.com/users/spechub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spechub/subscriptions","organizations_url":"https://api.github.com/users/spechub/orgs","repos_url":"https://api.github.com/users/spechub/repos","events_url":"https://api.github.com/users/spechub/events{/privacy}","received_events_url":"https://api.github.com/users/spechub/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/spechub/Hets","description":"The Heterogeneous Tool Set","fork":false,"url":"https://api.github.com/repos/spechub/Hets","forks_url":"https://api.github.com/repos/spechub/Hets/forks","keys_url":"https://api.github.com/repos/spechub/Hets/keys{/key_id}","collaborators_url":"https://api.github.com/repos/spechub/Hets/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/spechub/Hets/teams","hooks_url":"https://api.github.com/repos/spechub/Hets/hooks","issue_events_url":"https://api.github.com/repos/spechub/Hets/issues/events{/number}","events_url":"https://api.github.com/repos/spechub/Hets/events","assignees_url":"https://api.github.com/repos/spechub/Hets/assignees{/user}","branches_url":"https://api.github.com/repos/spechub/Hets/branches{/branch}","tags_url":"https://api.github.com/repos/spechub/Hets/tags","blobs_url":"https://api.github.com/repos/spechub/Hets/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/spechub/Hets/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/spechub/Hets/git/refs{/sha}","trees_url":"https://api.github.com/repos/spechub/Hets/git/trees{/sha}","statuses_url":"https://api.github.com/repos/spechub/Hets/statuses/{sha}","languages_url":"https://api.github.com/repos/spechub/Hets/languages","stargazers_url":"https://api.github.com/repos/spechub/Hets/stargazers","contributors_url":"https://api.github.com/repos/spechub/Hets/contributors","subscribers_url":"https://api.github.com/repos/spechub/Hets/subscribers","subscription_url":"https://api.github.com/repos/spechub/Hets/subscription","commits_url":"https://api.github.com/repos/spechub/Hets/commits{/sha}","git_commits_url":"https://api.github.com/repos/spechub/Hets/git/commits{/sha}","comments_url":"https://api.github.com/repos/spechub/Hets/comments{/number}","issue_comment_url":"https://api.github.com/repos/spechub/Hets/issues/comments{/number}","contents_url":"https://api.github.com/repos/spechub/Hets/contents/{+path}","compare_url":"https://api.github.com/repos/spechub/Hets/compare/{base}...{head}","merges_url":"https://api.github.com/repos/spechub/Hets/merges","archive_url":"https://api.github.com/repos/spechub/Hets/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/spechub/Hets/downloads","issues_url":"https://api.github.com/repos/spechub/Hets/issues{/number}","pulls_url":"https://api.github.com/repos/spechub/Hets/pulls{/number}","milestones_url":"https://api.github.com/repos/spechub/Hets/milestones{/number}","notifications_url":"https://api.github.com/repos/spechub/Hets/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/spechub/Hets/labels{/name}","releases_url":"https://api.github.com/repos/spechub/Hets/releases{/id}","deployments_url":"https://api.github.com/repos/spechub/Hets/deployments","created_at":"2014-06-04T17:20:48Z","updated_at":"2016-02-11T12:30:52Z","pushed_at":"2016-06-07T12:26:05Z","git_url":"git://github.com/spechub/Hets.git","ssh_url":"git@github.com:spechub/Hets.git","clone_url":"https://github.com/spechub/Hets.git","svn_url":"https://github.com/spechub/Hets","homepage":"http://hets.eu","size":261360,"stargazers_count":7,"watchers_count":7,"language":"Haskell","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":8,"mirror_url":null,"open_issues_count":515,"forks":8,"open_issues":515,"watchers":7,"default_branch":"master"}},"base":{"label":"spechub:master","ref":"master","sha":"c7e636bf6c287e3ddfb68d3be233b1c5f8392f03","user":{"login":"spechub","id":6953185,"avatar_url":"https://avatars.githubusercontent.com/u/6953185?v=3","gravatar_id":"","url":"https://api.github.com/users/spechub","html_url":"https://github.com/spechub","followers_url":"https://api.github.com/users/spechub/followers","following_url":"https://api.github.com/users/spechub/following{/other_user}","gists_url":"https://api.github.com/users/spechub/gists{/gist_id}","starred_url":"https://api.github.com/users/spechub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spechub/subscriptions","organizations_url":"https://api.github.com/users/spechub/orgs","repos_url":"https://api.github.com/users/spechub/repos","events_url":"https://api.github.com/users/spechub/events{/privacy}","received_events_url":"https://api.github.com/users/spechub/received_events","type":"Organization","site_admin":false},"repo":{"id":20492711,"name":"Hets","full_name":"spechub/Hets","owner":{"login":"spechub","id":6953185,"avatar_url":"https://avatars.githubusercontent.com/u/6953185?v=3","gravatar_id":"","url":"https://api.github.com/users/spechub","html_url":"https://github.com/spechub","followers_url":"https://api.github.com/users/spechub/followers","following_url":"https://api.github.com/users/spechub/following{/other_user}","gists_url":"https://api.github.com/users/spechub/gists{/gist_id}","starred_url":"https://api.github.com/users/spechub/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spechub/subscriptions","organizations_url":"https://api.github.com/users/spechub/orgs","repos_url":"https://api.github.com/users/spechub/repos","events_url":"https://api.github.com/users/spechub/events{/privacy}","received_events_url":"https://api.github.com/users/spechub/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/spechub/Hets","description":"The Heterogeneous Tool Set","fork":false,"url":"https://api.github.com/repos/spechub/Hets","forks_url":"https://api.github.com/repos/spechub/Hets/forks","keys_url":"https://api.github.com/repos/spechub/Hets/keys{/key_id}","collaborators_url":"https://api.github.com/repos/spechub/Hets/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/spechub/Hets/teams","hooks_url":"https://api.github.com/repos/spechub/Hets/hooks","issue_events_url":"https://api.github.com/repos/spechub/Hets/issues/events{/number}","events_url":"https://api.github.com/repos/spechub/Hets/events","assignees_url":"https://api.github.com/repos/spechub/Hets/assignees{/user}","branches_url":"https://api.github.com/repos/spechub/Hets/branches{/branch}","tags_url":"https://api.github.com/repos/spechub/Hets/tags","blobs_url":"https://api.github.com/repos/spechub/Hets/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/spechub/Hets/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/spechub/Hets/git/refs{/sha}","trees_url":"https://api.github.com/repos/spechub/Hets/git/trees{/sha}","statuses_url":"https://api.github.com/repos/spechub/Hets/statuses/{sha}","languages_url":"https://api.github.com/repos/spechub/Hets/languages","stargazers_url":"https://api.github.com/repos/spechub/Hets/stargazers","contributors_url":"https://api.github.com/repos/spechub/Hets/contributors","subscribers_url":"https://api.github.com/repos/spechub/Hets/subscribers","subscription_url":"https://api.github.com/repos/spechub/Hets/subscription","commits_url":"https://api.github.com/repos/spechub/Hets/commits{/sha}","git_commits_url":"https://api.github.com/repos/spechub/Hets/git/commits{/sha}","comments_url":"https://api.github.com/repos/spechub/Hets/comments{/number}","issue_comment_url":"https://api.github.com/repos/spechub/Hets/issues/comments{/number}","contents_url":"https://api.github.com/repos/spechub/Hets/contents/{+path}","compare_url":"https://api.github.com/repos/spechub/Hets/compare/{base}...{head}","merges_url":"https://api.github.com/repos/spechub/Hets/merges","archive_url":"https://api.github.com/repos/spechub/Hets/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/spechub/Hets/downloads","issues_url":"https://api.github.com/repos/spechub/Hets/issues{/number}","pulls_url":"https://api.github.com/repos/spechub/Hets/pulls{/number}","milestones_url":"https://api.github.com/repos/spechub/Hets/milestones{/number}","notifications_url":"https://api.github.com/repos/spechub/Hets/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/spechub/Hets/labels{/name}","releases_url":"https://api.github.com/repos/spechub/Hets/releases{/id}","deployments_url":"https://api.github.com/repos/spechub/Hets/deployments","created_at":"2014-06-04T17:20:48Z","updated_at":"2016-02-11T12:30:52Z","pushed_at":"2016-06-07T12:26:05Z","git_url":"git://github.com/spechub/Hets.git","ssh_url":"git@github.com:spechub/Hets.git","clone_url":"https://github.com/spechub/Hets.git","svn_url":"https://github.com/spechub/Hets","homepage":"http://hets.eu","size":261360,"stargazers_count":7,"watchers_count":7,"language":"Haskell","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":8,"mirror_url":null,"open_issues_count":515,"forks":8,"open_issues":515,"watchers":7,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/spechub/Hets/pulls/1593"},"html":{"href":"https://github.com/spechub/Hets/pull/1593"},"issue":{"href":"https://api.github.com/repos/spechub/Hets/issues/1593"},"comments":{"href":"https://api.github.com/repos/spechub/Hets/issues/1593/comments"},"review_comments":{"href":"https://api.github.com/repos/spechub/Hets/pulls/1593/comments"},"review_comment":{"href":"https://api.github.com/repos/spechub/Hets/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/spechub/Hets/pulls/1593/commits"},"statuses":{"href":"https://api.github.com/repos/spechub/Hets/statuses/e2fdd28e29f151215a081dd95fcc443a4c8ccf23"}}}}
{"actor":{"display_login":"tillmo"}}