Rigid casl #1845

mcodescu · 2018-04-23T08:01:30Z

Test file at https://ontohub.org/forver/bufferDol.dol

implementation of HybridPartialAlgebraswithRigidsymbols (HPAR) in Hets:

RigidCASL (PAR) extends CASL with rigid symbols
HPAR is the hybridization of PAR
HPAR2CASL is the hybridization of the comorphism CASL2SubCFOL True NoMembershipOrCast
for now, proofs can be done by translating the entire graph to FOL (there is a question about this in Comorphisms/HPAR2CASL.hs)
the branch should not be merged, the implementation is a test towards a generic hybridization method. Therefore, I did not focus so much on the style (e.g. long lines)

…id_casl

tillmo · 2019-07-03T17:24:22Z

could you please resolve the conflicts here?

mcodescu · 2019-07-03T18:26:29Z

Sure. Also have to shorten some lines.

tillmo

Please add more documentation.
Please resolve the todos (I have commented some, but not all).
Please add a general explanation in the style of CASL.hs.
Please merge master into this branch.
Why is RigidCASL/AS.der.hs empty?

tillmo · 2019-07-29T10:50:48Z

CASL/Morphism.hs

+rawToSymbol (ASymbol s) = Just s
+rawToSymbol (AKindedSymb k i) = 
+   case k of
+    Sorts_kind -> Just $ Symbol i SortAsItemType


why is kind sort assumed here?

tillmo · 2019-07-29T10:52:37Z

CASL/Sign.hs

@@ -591,8 +600,16 @@ addSymbToSign sig sy =
        PredAsItemType pt -> return $ addPred' sig' n pt
        OpAsItemType ot -> return $ addOp' sig' n ot

+addNomsToSign :: Sign e f -> Set.Set Id -> Result (Sign e f)


Please add a comment documenting the function (I won' repeat this comment for other functions).

tillmo · 2023-08-23T19:27:41Z

CASL/Sign.hs

+extSymbolKind t = case t of 
+  OpAsItemType (OpType k l _) -> 
+     case (k, l) of 
+      (Total, []) -> "const"


what about partial constants? Should they really lead to "op"?

tillmo · 2023-08-23T19:29:22Z

CASL/Sign.hs


-- The function below belong in a different file. But I put them here for now.
+-- TODO: The function below belong in a different file. But I put them here for now.


the TODO should be resolved

tillmo · 2023-08-23T19:30:37Z

CASL/StaticAna.hs

@@ -908,15 +915,161 @@ basicCASLAnalysis = basicAnalysis (const return) (const return)

 -- | extra
 cASLsen_analysis ::
-        (BASIC_SPEC () () (), Sign () (), FORMULA ()) -> Result (FORMULA ())
+        (BASIC_SPEC () () (), Sign () (), FORMULA ()) ->
+        Result (FORMULA (), FORMULA ())


please document the purpose of returning two formulas

tillmo · 2023-08-23T20:16:12Z

RigidCASL/StaticAna.hs

+type Ana a b s f e = Mix b s f e -> a -> State (Sign f e) a
+
+
+-}


tillmo · 2023-08-23T20:16:24Z

RigidCASL/StaticAna.hs

+                                     map (\(a,b) -> mkVarTerm a b) $ (genToken "w1", st):(map (\(si, ii) -> (genToken $ "x" ++ show ii, si)) $ xs pt))
+                                   (mkPredication (mkQualPred i $ extPt $ toPRED_TYPE pt) $
+                                     map (\(a,b) -> mkVarTerm a b) $ (genToken "w2", st):(map (\(si, ii) -> (genToken $ "x" ++ show ii, si)) $ xs pt)) 
+            ) $ MapSet.toPairList $ predMap sig -}


tillmo · 2023-08-23T20:17:04Z

Syntax/Parse_AS_Library.hs

@@ -42,6 +44,8 @@ import qualified Control.Monad.Fail as Fail

 import Framework.AS

+import Debug.Trace


please remove

tillmo · 2023-08-23T20:17:40Z

Syntax/Parse_AS_Library.hs

+varP :: AParser st (String, Maybe Token)
+varP = {- do
+   (s, _) <- simpleId `separatedBy` skip
+   return (concat $ map show s, Nothing) 


tillmo · 2023-08-23T20:18:13Z

Syntax/Print_AS_Structured.hs

@@ -120,6 +120,7 @@ printSPEC lg spec = case spec of
      sep [keyword "apply" <+> pretty i, prettyLG lg $ Basic_spec bs nullRange]
    Bridge s1 rs s2 _ -> fsep $ [condBraces lg s1, keyword "bridge"]
      ++ map pretty rs ++ [condBraces lg s2]
+    HSpec _ _ _ _ -> empty


mcodescu added 20 commits March 28, 2018 00:31

hpar first version

8d79d48

added more files

b7bf3cf

more files

b2e91a6

hpar first version

36b782c

added more files

a9a3a5a

more files

39961e8

finished comorphism

cd51df4

Merge branch 'rigid_casl' of https://github.com/spechub/Hets into rig…

b5c0683

…id_casl

added brackets, needs more tests

03b904d

dont print keyword when there are no nominals

c75dcab

dont display rigid symbols as non-rigid

ac440ad

printing finally works, cleaning up needed

985eaa6

total, not partial op symbol

56cb8d8

fixed quantification on nominals

2e33122

corrected the parser

286c44e

no tracing, revert change in comorphism

7f7a727

remove generated file

b40bd6e

code cleanup

8165faa

code cleanup

ba8aa45

comment in comorphism

75b0e77

mcodescu requested a review from tillmo April 23, 2018 08:01

mcodescu added 9 commits April 23, 2018 20:12

added forgotten file

50ce830

hint for repeated rigid symbols

fdbaf1e

hint for symbols redeclared as rigid

53009fc

hint to warning

5ad946f

warning for redeclared modalities or nominals

6b05a92

check that modalities and nominals in sentences have been declared

097ee15

properly use diags

e28bd7c

propagate diags for basic items

c02dfe7

allow nominals to be quantified

e679808

mcodescu and others added 2 commits April 10, 2019 16:16

fixed a bug

45da381

Merge branch 'master' into rigid_casl

ca94f27

mcodescu and others added 12 commits July 3, 2019 20:54

Merge branch 'master' into rigid_casl

0afafa0

shortened lines, trailing

51d8256

shortened, trailing spaces

b58b23e

shorter lines, trailing

a582b79

short lines, trailing, no warnings

6167989

delete example file

7db9a2f

started shortening, long file

f9c9ff1

shortened, ready for review

bb06f8c

trailing

f0e5728

removed existing definitions

68851f0

Merge branch 'master' into rigid_casl

b0fdcdd

Merge branch 'master' into rigid_casl

9ac66b6

tillmo mentioned this pull request Sep 21, 2022

merge relevant existing forks #2106

Open

mcodescu added 12 commits September 23, 2022 10:08

Merge branch 'master' into rigid_casl

7fcbb3c

made Hets compile

c6e5ee0

made docs go through

8dd9855

implementation of H in readme

515af0d

changed copyright

493f693

fixed warnings

226e6fb

add prefix map

6211fd2

Merge branch 'master' into rigid_casl

68ecbb6

removed trace message

32c0310

adapt to the changes in Logic.Logic

16ccc5e

documentation

bffde05

Merge branch 'master' into rigid_casl

3776d95

tillmo requested changes Aug 23, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rigid casl #1845

Rigid casl #1845

mcodescu commented Apr 23, 2018

tillmo commented Jul 3, 2019

mcodescu commented Jul 3, 2019

tillmo left a comment

tillmo Jul 29, 2019

tillmo Jul 29, 2019

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023

tillmo Aug 23, 2023


		-- The function below belong in a different file. But I put them here for now.
		-- TODO: The function below belong in a different file. But I put them here for now.

		type Ana a b s f e = Mix b s f e -> a -> State (Sign f e) a


		-}

		@@ -42,6 +44,8 @@ import qualified Control.Monad.Fail as Fail

		import Framework.AS

		import Debug.Trace

Rigid casl #1845

Are you sure you want to change the base?

Rigid casl #1845

Conversation

mcodescu commented Apr 23, 2018

tillmo commented Jul 3, 2019

mcodescu commented Jul 3, 2019

tillmo left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment