added syntax IRI to theories

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17252 cec4b9c1-7d33-0410-9eda-942365e851bb

ATC/Grothendieck.der.hs

@@ -365,23 +365,26 @@ instance (ShATermLG a) => ShATermLG (IntMap.IntMap a) where
 
 
 instance ShATermLG G_theory where
-  toShATermLG att0 (G_theory lid sign si sens ti) = do
-         (att1, i1) <- toShATermLG' att0 (language_name lid)
+  toShATermLG att0 (G_theory lid syn sign si sens ti) = do
+         (att1a, i1) <- toShATermLG' att0 (language_name lid)
+         (att1, i1a) <- toShATermLG' att1a syn
          (att2, i2) <- toShATermLG' att1 sign
          (att3, i3) <- toShATermLG' att2 si
          (att4, i4) <- toShATermLG' att3 sens
          (att5, i5) <- toShATermLG' att4 ti
-         return $ addATerm (ShAAppl "G_theory" [i1, i2, i3, i4, i5] []) att5
+         return $ addATerm (ShAAppl "G_theory" [i1, i1a, i2, i3, i4, i5] [])
+                att5
   fromShATermLG lg ix att =
          case getShATerm ix att of
-            ShAAppl "G_theory" [i1, i2, i3, i4, i5] _ ->
-                case fromShATermLG' lg i1 att of { (att1, i1') ->
+            ShAAppl "G_theory" [i1, i1a, i2, i3, i4, i5] _ ->
+                case fromShATermLG' lg i1 att of { (att1a, i1') ->
                 case atcLogicLookup lg "G_theory" i1' of { Logic lid ->
+                case fromShATermLG' lg i1a att1a of { (att1, i1a') ->
                 case fromShATermLG' lg i2 att1 of { (att2, i2') ->
                 case fromShATermLG' lg i3 att2 of { (att3, i3') ->
                 case fromShATermLG' lg i4 att3 of { (att4, i4') ->
                 case fromShATermLG' lg i5 att4 of { (att5, i5') ->
-                (att5, G_theory lid i2' i3' i4' i5') }}}}}}
+                (att5, G_theory lid i1a' i2' i3' i4' i5') }}}}}}}
             u -> fromShATermError "G_theory" u
 
 instance Typeable a => ShATermConvertible (MVar a) where

CMDL/InfoCommands.hs

@@ -91,8 +91,8 @@ getGoalThS useTrans x state
     Nothing -> []
     Just th ->
       let nwth = case th of
-                  G_theory x1 x2 x3 thSens x4 ->
-                    G_theory x1 x2 x3
+                  G_theory x1 syn x2 x3 thSens x4 ->
+                    G_theory x1 syn x2 x3
                        (OMap.filter (\ s -> not (isAxiom s) &&
                                           not (isProvenSenStatus s))
                        thSens) x4
@@ -127,7 +127,7 @@ cShowFromNode f input state =
                 case getTh Dont_translate n state of
                   Nothing -> []
                   Just th -> case th of
-                                 G_theory _ _ _ sens _ -> OMap.keys $
+                                 G_theory _ _ _ _ sens _ -> OMap.keys $
                                    OMap.filter f sens)) state
 
 cShowNodeProvenGoals :: String -> CmdlState -> IO CmdlState

CMDL/Utils.hs

@@ -194,7 +194,7 @@ obtainNodeList lN allNodes = mapAndSplit
 nodeContainsGoals :: LNode DGNodeLab -> G_theory -> Bool
 nodeContainsGoals (_, l) th =
    (case th of
-       G_theory _ _ _ sens _ ->
+       G_theory _ _ _ _ sens _ ->
          not $ Map.null $ OMap.filter
            (\ s -> not (isAxiom s) && not (isProvenSenStatus s)) sens) ||
            hasOpenNodeConsStatus False l

Driver/WriteFn.hs

@@ -147,7 +147,7 @@ writeSoftFOL opts f gTh i c n msg = do
               writeVerbFile opts f str) mDoc
 
 writeFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> IO ()
-writeFreeCADFile opts filePrefix (G_theory lid (ExtSign sign _) _ _ _) = do
+writeFreeCADFile opts filePrefix (G_theory lid _ (ExtSign sign _) _ _ _) = do
   fcSign <- coercePlainSign lid FreeCAD
             "Expecting a FreeCAD signature for writing FreeCAD xml" sign
   writeVerbFile opts (filePrefix ++ ".xml") $ exportXMLFC fcSign
@@ -184,7 +184,7 @@ writeIsaFile opts filePrefix raw_gTh ln i = do
 writeTheory :: [String] -> String -> HetcatsOpts -> FilePath -> GlobalAnnos
   -> G_theory -> LibName -> IRI -> OutType -> IO ()
 writeTheory ins nam opts filePrefix ga
-  raw_gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) ln i ot =
+  raw_gTh@(G_theory lid _ (ExtSign sign0 _) _ sens0 _) ln i ot =
     let fp = filePrefix ++ "_" ++ iriToStringShortUnsecure i
         f = fp ++ "." ++ show ot
         th = (sign0, toNamedList sens0)
@@ -262,7 +262,7 @@ writeTheory ins nam opts filePrefix ga
     _ -> return () -- ignore other file types
 
 modelSparQCheck :: HetcatsOpts -> G_theory -> IO ()
-modelSparQCheck opts gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) =
+modelSparQCheck opts gTh@(G_theory lid _ (ExtSign sign0 _) _ sens0 _) =
     case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of
     Just th2 -> do
       table <- parseSparQTableFromFile $ modelSparQ opts

GUI/GraphLogic.hs

@@ -458,7 +458,7 @@ translateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
     Just ist -> do
       let libEnv = i_libEnv ist
       case computeTheory libEnv ln node of
-        Just th@(G_theory lid sign _ sens _) -> do
+        Just th@(G_theory lid _ sign _ sens _) -> do
           -- find all comorphism paths starting from lid
           let paths = findComorphismPaths logicGraph (sublogicOfTh th)
           -- let the user choose one
@@ -480,8 +480,8 @@ translateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
                 Just (sign'', sens1) -> displayTheoryWithWarning
                   "Translated Theory" (getNameOfNode node dgraph)
                   (addHasInHidingWarning dgraph node)
-                  $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)
-                             startThId
+                  $ G_theory lidT Nothing (mkExtSign sign'') startSigId
+                      (toThSens sens1) startThId
         Nothing ->
           errorDialog "Error" $ "no global theory for node " ++ show node
 
@@ -495,7 +495,7 @@ showProofStatusOfNode _ descr dgraph =
 
 showStatusAux :: DGNodeLab -> String
 showStatusAux dgnode = case dgn_theory dgnode of
-  G_theory _ _ _ sens _ ->
+  G_theory _ _ _ _ sens _ ->
      let goals = OMap.filter (not . isAxiom) sens
          (proven, open) = OMap.partition isProvenSenStatus goals
          consGoal = "\nconservativity of this node"

GUI/GtkConsistencyChecker.hs

@@ -111,7 +111,7 @@ showConsistencyChecker mn gi@(GInfo { libName = ln }) le =
       dg = lookupDGraph ln le
       lbl = labDG dg n
       in if case globalTheory lbl of
-        Just (G_theory _ _ _ sens _) -> Map.null sens
+        Just (G_theory _ _ _ _ sens _) -> Map.null sens
         Nothing -> True
         then do
           infoDialogExt "No sentences" $ "Node " ++
@@ -180,7 +180,7 @@ showConsistencyCheckerAux res mn ln le = postGUIAsync $ do
   let dg = lookupDGraph ln le
       nodes = labNodesDG dg
       selNodes = partition (\ (FNode { node = (_, l)}) -> case globalTheory l of
-        Just (G_theory _ _ _ sens _) -> Map.null sens
+        Just (G_theory _ _ _ _ sens _) -> Map.null sens
         Nothing -> True)
       sls = map sublogicOfTh $ mapMaybe (globalTheory . snd) nodes
 

GUI/GtkDisprove.hs

@@ -59,7 +59,7 @@ theory. -}
 showDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
 showDisproveGUI gi le dg (i, lbl) = case globalTheory lbl of
   Nothing -> error "GtkDisprove.showDisproveGUI(no global theory found)"
-  Just gt@(G_theory _ _ _ sens _) -> let
+  Just gt@(G_theory _ _ _ _ sens _) -> let
     fg g th = let
       l = lbl { dgn_theory = th }
       l' = l { globalTheory = computeLabelTheory le dg (i, l) }
@@ -89,7 +89,7 @@ showDisproveGUI gi le dg (i, lbl) = case globalTheory lbl of
 containing all axioms in addition to the one negated sentence. -}
 negate_th :: G_theory -> String -> Maybe G_theory
 negate_th g_th goal = case g_th of
-  G_theory lid1 (ExtSign sign symb) i1 sens i2 ->
+  G_theory lid1 syn (ExtSign sign symb) i1 sens _ ->
     case OMap.lookup goal sens of
       Nothing -> Nothing
       Just sen ->
@@ -98,7 +98,7 @@ negate_th g_th goal = case g_th of
           Just sen' -> let
             negSen = sen { sentence = sen', isAxiom = True }
             sens' = OMap.insert goal negSen $ OMap.filter isAxiom sens
-            in Just $ G_theory lid1 (ExtSign sign symb) i1 sens' i2
+            in Just $ G_theory lid1 syn (ExtSign sign symb) i1 sens' startThId
 
 {- | this function is being called from outside and manages the locking-
 mechanism of the node being called upon. -}
@@ -279,7 +279,7 @@ showDisproveWindow res ln le dg g_th fgoals = postGUIAsync $ do
     maybe_F <- getSelectedSingle trvFinder listFinder
     case maybe_F of
       Just (_, f) -> case g_th of
-        G_theory lid _s _i1 sens _i2 -> let
+        G_theory lid syn sig i1 sens _ -> let
           sens' = foldr (\ fg t -> if (sType . cStatus) fg == CSInconsistent
             then let
               n' = name fg
@@ -292,7 +292,7 @@ showDisproveWindow res ln le dg g_th fgoals = postGUIAsync $ do
               s' = s { senAttr = ThmStatus $ (c, bp) : thmStatus s } in
               Map.insert n' es { OMap.ele = s' } t
             else t ) sens fnodes'
-          in putMVar res $ return (G_theory lid _s _i1 sens' _i2)
+          in putMVar res $ return (G_theory lid syn sig i1 sens' startThId)
       _ -> putMVar res $ return g_th
 
   selectWith (== ConsistencyStatus CSUnchecked "") upd

GUI/GtkProverGUI.hs

@@ -229,7 +229,7 @@ showProverGUI prGuiAcs thName warn th knownProvers comorphList = do
 -- | Called whenever the button "Display" is clicked.
 displayGoals :: ProofState -> IO ()
 displayGoals s = case currentTheory s of
-  G_theory lid1 (ExtSign sig1 _) _ sens1 _ -> do
+  G_theory lid1 _ (ExtSign sig1 _) _ sens1 _ -> do
     let thName = theoryName s
         goalsText = show . Pretty.vsep
           . map (print_named lid1 . AS_Anno.mapNamed (simplify_sen lid1 sig1))
@@ -348,7 +348,7 @@ setSelectedProver trvProvers listProvers cbComorphism shC s = do
 
 wasATheorem :: ProofState -> String -> Bool
 wasATheorem st i = case currentTheory st of
-   G_theory _ _ _ sens _ -> maybe False wasTheorem $ OMap.lookup i sens
+   G_theory _ _ _ _ sens _ -> maybe False wasTheorem $ OMap.lookup i sens
 
 toGoals :: ProofState -> [Goal]
 toGoals = sort . map toGtkGoal . getGoals

GUI/HTkProofDetails.hs

@@ -226,7 +226,7 @@ doShowProofDetails prGUISt =
     pack ptBut [PadX 5, PadY 5]
     pack sBut  [PadX 5, PadY 5]
     pack qBut  [PadX 8, PadY 5]
-    G_theory _ _ _ sSens _ <- return $ selectedTheory prGUISt
+    G_theory _ _ _ _ sSens _ <- return $ selectedTheory prGUISt
     let sttDesc = "Tactic script"
         sptDesc = "Proof tree"
         sens = OMap.filter (not . isAxiom) sSens

GUI/Taxonomy.hs

@@ -1,4 +1,3 @@
-
 {- |
 Module      :  $Header$
 Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2004
@@ -35,7 +34,7 @@ displaySubsortGraph :: String -> G_theory -> IO ()
 displaySubsortGraph = displayGraph KSubsort
 
 displayGraph :: TaxoGraphKind -> String -> G_theory -> IO ()
-displayGraph kind thyName (G_theory lid (ExtSign sign _) _ sens _) =
+displayGraph kind thyName (G_theory lid _ (ExtSign sign _) _ sens _) =
     case theory_to_taxonomy lid kind
                        (emptyMMiSSOntology thyName AutoInsert)
                        sign $ toNamedList sens of

Haskell/CreateModules.hs

@@ -32,7 +32,7 @@ import Comorphisms.CASL2HasCASL
 import Comorphisms.HasCASL2HasCASL
 
 printModule :: G_theory -> Maybe Doc
-printModule (G_theory lid (ExtSign sign0 _) _ sens0 _) =
+printModule (G_theory lid _ (ExtSign sign0 _) _ sens0 _) =
                 let th = (sign0, toNamedList sens0)
                     r1 = do
                       th0 <- coerceBasicTheory lid CASL "" th

Haskell/Haskell2DG.hs

@@ -54,7 +54,8 @@ anaHaskellFile opts file = do
               mName = simpleIdToIRI $ mkSimpleId bas
               name = makeName $ mName
               node_contents = newNodeLab name DGBasic
-                $ G_theory Haskell sig startSigId (toThSens sens) startThId
+                $ G_theory Haskell Nothing sig startSigId (toThSens sens)
+                  startThId
               dg = emptyDG
               node = getNewNodeDG dg
               dg1 = insNodeDG (node, node_contents) dg

HolLight/HolLight2DG.hs

@@ -359,7 +359,7 @@ _insNodeDG :: Sign -> [Named Sentence] -> String
               -> (DGraph, Map.Map String
                (String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
 _insNodeDG sig sens n (dg, m) =
- let gt = G_theory HolLight (makeExtSign HolLight sig) startSigId
+ let gt = G_theory HolLight Nothing (makeExtSign HolLight sig) startSigId
            (toThSens sens) startThId
      n' = snd (System.FilePath.Posix.splitFileName n)
      labelK = newInfoNodeLab

Interfaces/Utils.hs

@@ -258,7 +258,7 @@ checkConservativityEdge :: Bool -> LEdge DGLinkLab -> LibEnv -> LibName
 checkConservativityEdge useGUI link@(source, target, linklab) libEnv ln
  = do
 
-    Just (G_theory lidT _ _ sensT _) <-
+    Just (G_theory lidT _ _ _ sensT _) <-
       return $ computeTheory libEnv ln target
     GMorphism cid _ _ morphism _ <- return $ dgl_morphism linklab
     morphism' <- coerceMorphism (targetLogic cid) lidT
@@ -271,7 +271,7 @@ checkConservativityEdge useGUI link@(source, target, linklab) libEnv ln
                >>= comp morphism' of
                  Result _ (Just phi) -> phi
                  _ -> error "checkconservativityOfEdge: comp"
-    Just (G_theory lidS signS _ sensS _) <-
+    Just (G_theory lidS _ signS _ sensS _) <-
       return $ computeTheory libEnv ln source
     case coerceSign lidS lidT "checkconservativityOfEdge.coerceSign" signS of
      Nothing -> return ( "no implementation for heterogeneous links"
@@ -319,7 +319,7 @@ checkConservativityEdge useGUI link@(source, target, linklab) libEnv ln
                         _ -> []
                    namedNewSens = toThSens [(makeNamed "" o) {isAxiom = False} |
                                              o <- obligations]
-               G_theory glid gsign gsigid gsens gid <- return $ dgn_theory
+               G_theory glid gsyn gsign gsigid gsens gid <- return $ dgn_theory
                                                                   nodelab
                namedNewSens' <- coerceThSens lidT glid "" namedNewSens
                let oldSens = OMap.toList gsens
@@ -329,7 +329,8 @@ checkConservativityEdge useGUI link@(source, target, linklab) libEnv ln
                      (\ (_, a) (_, b) -> sentence a == sentence b)
                      $ oldSens ++ OMap.toList namedNewSens'
                    (newTheory, nodeChange) =
-                     (G_theory glid gsign gsigid (OMap.fromList mergedSens) gid,
+                     (G_theory glid gsyn gsign gsigid
+                      (OMap.fromList mergedSens) gid,
                       length oldSens /= length mergedSens)
                    newTargetNode = (target
                                    , nodelab { dgn_theory = newTheory })

Isabelle/CreateTheories.hs

@@ -41,7 +41,7 @@ import Haskell.Logic_Haskell
 #endif
 
 createIsaTheory :: G_theory -> Result (Sign, [Named Sentence])
-createIsaTheory (G_theory lid (ExtSign sign0 _) _ sens0 _) = do
+createIsaTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
     let th = (sign0, toNamedList sens0)
         r1 = coerceBasicTheory lid CASL "" th
         r1' = do

Isabelle/Isa2DG.hs

@@ -51,7 +51,7 @@ makeNamedSentence (n, t) = makeNamed n $ mkSen t
 _insNodeDG :: Sign -> [Named Sentence] -> String
               -> DGraph -> DGraph
 _insNodeDG sig sens n dg =
- let gt = G_theory Isabelle (makeExtSign Isabelle sig) startSigId
+ let gt = G_theory Isabelle Nothing (makeExtSign Isabelle sig) startSigId
            (toThSens sens) startThId
      labelK = newInfoNodeLab
       (makeName (simpleIdToIRI (mkSimpleId n)))
@@ -107,7 +107,7 @@ anaIsaFile _ path = do
  (name,imps,consts,axioms,theorems,types,classes,locales')
    <- importIsaDataIO path
  let sens = map makeNamedSentence (axioms ++ theorems
-             ++ (foldl (\ l c -> case c of 
+             ++ (foldl (\ l c -> case c of
                           (_,_,Nothing) -> l
                           (n,_,Just tm) -> (n,tm):l) [] consts))
  let sgn = emptySign { constTab = foldl (\ m (n,t,_) -> Map.insert (mkVName n) t m) Map.empty consts, domainTab = types, imports = imps,