{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveDataTypeable
  , GeneralizedNewtypeDeriving, TypeSynonymInstances #-}
{- |
Module      :  ./FreeCAD/Logic_FreeCAD.hs
Description :  Instance of class Logic for FreeCAD
Copyright   :  (c) Christian Maeder DFKI, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

instance of class Logic for FreeCAD

-}

module FreeCAD.Logic_FreeCAD where

import Logic.Logic

import Common.DefaultMorphism
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.LibName
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Result

import ATerm.Lib

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Typeable

import FreeCAD.As
import FreeCAD.ATC_FreeCAD ()
import FreeCAD.PrintAs ()
import FreeCAD.Translator (processFile)

import Logic.Grothendieck (G_basic_spec (..))
import Syntax.AS_Library (fromBasicSpec, LIB_DEFN)

data FreeCAD = FreeCAD deriving Int -> FreeCAD -> ShowS
[FreeCAD] -> ShowS
FreeCAD -> String
(Int -> FreeCAD -> ShowS)
-> (FreeCAD -> String) -> ([FreeCAD] -> ShowS) -> Show FreeCAD
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreeCAD] -> ShowS
$cshowList :: [FreeCAD] -> ShowS
show :: FreeCAD -> String
$cshow :: FreeCAD -> String
showsPrec :: Int -> FreeCAD -> ShowS
$cshowsPrec :: Int -> FreeCAD -> ShowS
Show

instance Language FreeCAD where
  description :: FreeCAD -> String
description _ = "FreeCAD object representation language"

instance Pretty Text where
  pretty :: Text -> Doc
pretty (Text s :: String
s) = String -> Doc
text String
s

newtype Text = Text { Text -> String
fromText :: String }
  deriving (Int -> Text -> ShowS
[Text] -> ShowS
Text -> String
(Int -> Text -> ShowS)
-> (Text -> String) -> ([Text] -> ShowS) -> Show Text
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Text] -> ShowS
$cshowList :: [Text] -> ShowS
show :: Text -> String
$cshow :: Text -> String
showsPrec :: Int -> Text -> ShowS
$cshowsPrec :: Int -> Text -> ShowS
Show, Text -> Text -> Bool
(Text -> Text -> Bool) -> (Text -> Text -> Bool) -> Eq Text
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Text -> Text -> Bool
$c/= :: Text -> Text -> Bool
== :: Text -> Text -> Bool
$c== :: Text -> Text -> Bool
Eq, Eq Text
Eq Text =>
(Text -> Text -> Ordering)
-> (Text -> Text -> Bool)
-> (Text -> Text -> Bool)
-> (Text -> Text -> Bool)
-> (Text -> Text -> Bool)
-> (Text -> Text -> Text)
-> (Text -> Text -> Text)
-> Ord Text
Text -> Text -> Bool
Text -> Text -> Ordering
Text -> Text -> Text
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Text -> Text -> Text
$cmin :: Text -> Text -> Text
max :: Text -> Text -> Text
$cmax :: Text -> Text -> Text
>= :: Text -> Text -> Bool
$c>= :: Text -> Text -> Bool
> :: Text -> Text -> Bool
$c> :: Text -> Text -> Bool
<= :: Text -> Text -> Bool
$c<= :: Text -> Text -> Bool
< :: Text -> Text -> Bool
$c< :: Text -> Text -> Bool
compare :: Text -> Text -> Ordering
$ccompare :: Text -> Text -> Ordering
$cp1Ord :: Eq Text
Ord, Text -> [Pos]
Text -> Range
(Text -> Range) -> (Text -> [Pos]) -> GetRange Text
forall a. (a -> Range) -> (a -> [Pos]) -> GetRange a
rangeSpan :: Text -> [Pos]
$crangeSpan :: Text -> [Pos]
getRange :: Text -> Range
$cgetRange :: Text -> Range
GetRange, Typeable, Typeable Text
Typeable Text =>
(ATermTable -> Text -> IO (ATermTable, Int))
-> (ATermTable -> [Text] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, Text))
-> (Int -> ATermTable -> (ATermTable, [Text]))
-> ShATermConvertible Text
Int -> ATermTable -> (ATermTable, [Text])
Int -> ATermTable -> (ATermTable, Text)
ATermTable -> [Text] -> IO (ATermTable, Int)
ATermTable -> Text -> IO (ATermTable, Int)
forall t.
Typeable t =>
(ATermTable -> t -> IO (ATermTable, Int))
-> (ATermTable -> [t] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, t))
-> (Int -> ATermTable -> (ATermTable, [t]))
-> ShATermConvertible t
fromShATermList' :: Int -> ATermTable -> (ATermTable, [Text])
$cfromShATermList' :: Int -> ATermTable -> (ATermTable, [Text])
fromShATermAux :: Int -> ATermTable -> (ATermTable, Text)
$cfromShATermAux :: Int -> ATermTable -> (ATermTable, Text)
toShATermList' :: ATermTable -> [Text] -> IO (ATermTable, Int)
$ctoShATermList' :: ATermTable -> [Text] -> IO (ATermTable, Int)
toShATermAux :: ATermTable -> Text -> IO (ATermTable, Int)
$ctoShATermAux :: ATermTable -> Text -> IO (ATermTable, Int)
$cp1ShATermConvertible :: Typeable Text
ShATermConvertible)

type FCMorphism = DefaultMorphism Sign

-- use generic Category instance from Logic.Logic

instance Syntax FreeCAD Document () () () where
  parse_basic_spec :: FreeCAD -> Maybe (PrefixMap -> AParser st Document)
parse_basic_spec FreeCAD = Maybe (PrefixMap -> AParser st Document)
forall a. Maybe a
Nothing

instance Sentences FreeCAD () Sign FCMorphism () where
  map_sen :: FreeCAD -> FCMorphism -> () -> Result ()
map_sen FreeCAD _ = () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return
  sym_of :: FreeCAD -> Sign -> [Set ()]
sym_of FreeCAD _ = [() -> Set ()
forall a. a -> Set a
Set.singleton ()]
  symmap_of :: FreeCAD -> FCMorphism -> EndoMap ()
symmap_of FreeCAD _ = EndoMap ()
forall k a. Map k a
Map.empty
  sym_name :: FreeCAD -> () -> Id
sym_name FreeCAD _ = String -> Id
genName "FreeCAD"

instance StaticAnalysis FreeCAD Document () () () Sign FCMorphism () ()
  where
  basic_analysis :: FreeCAD
-> Maybe
     ((Document, Sign, GlobalAnnos)
      -> Result (Document, ExtSign Sign (), [Named ()]))
basic_analysis FreeCAD = ((Document, Sign, GlobalAnnos)
 -> Result (Document, ExtSign Sign (), [Named ()]))
-> Maybe
     ((Document, Sign, GlobalAnnos)
      -> Result (Document, ExtSign Sign (), [Named ()]))
forall a. a -> Maybe a
Just (Document, Sign, GlobalAnnos)
-> Result (Document, ExtSign Sign (), [Named ()])
basicFCAnalysis
  empty_signature :: FreeCAD -> Sign
empty_signature FreeCAD = Sign :: Set NamedObject -> Sign
Sign { objects :: Set NamedObject
objects = Set NamedObject
forall a. Set a
Set.empty }
  is_subsig :: FreeCAD -> Sign -> Sign -> Bool
is_subsig FreeCAD s1 :: Sign
s1 s2 :: Sign
s2 = Set NamedObject -> Set NamedObject -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> Set NamedObject
objects Sign
s1) (Set NamedObject -> Bool) -> Set NamedObject -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set NamedObject
objects Sign
s2

instance Logic FreeCAD
    ()                        -- Sublogics
    Document                  -- basic_spec
    ()                        -- no sentences
    ()                        -- no symb_items
    ()                        -- no symb_map_items
    Sign                      -- sign
    (DefaultMorphism Sign)    -- morphism
    ()                        -- no symbol
    ()                        -- no raw_symbol
    ()                        -- no proof_tree
    where
      stability :: FreeCAD -> Stability
stability FreeCAD = Stability
Experimental

readFreeCADLib :: FilePath -> LibName -> IO LIB_DEFN
readFreeCADLib :: String -> LibName -> IO LIB_DEFN
readFreeCADLib fp :: String
fp ln :: LibName
ln = do
  Document
bs <- String -> IO Document
processFile String
fp
  let sn :: IRI
sn = SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "FreeCAD-Design"
  LIB_DEFN -> IO LIB_DEFN
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_DEFN -> IO LIB_DEFN) -> LIB_DEFN -> IO LIB_DEFN
forall a b. (a -> b) -> a -> b
$ LibName -> IRI -> G_basic_spec -> LIB_DEFN
fromBasicSpec LibName
ln IRI
sn (G_basic_spec -> LIB_DEFN) -> G_basic_spec -> LIB_DEFN
forall a b. (a -> b) -> a -> b
$ FreeCAD -> Document -> G_basic_spec
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> basic_spec -> G_basic_spec
G_basic_spec FreeCAD
FreeCAD Document
bs

basicFCAnalysis :: (Document, Sign, GlobalAnnos)
                -> Result (Document, ExtSign Sign (), [Named ()])
basicFCAnalysis :: (Document, Sign, GlobalAnnos)
-> Result (Document, ExtSign Sign (), [Named ()])
basicFCAnalysis (bs :: Document
bs, _, _) = (Document, ExtSign Sign (), [Named ()])
-> Result (Document, ExtSign Sign (), [Named ()])
forall (m :: * -> *) a. Monad m => a -> m a
return (Document
bs, Sign -> ExtSign Sign ()
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign (Sign -> ExtSign Sign ()) -> Sign -> ExtSign Sign ()
forall a b. (a -> b) -> a -> b
$ Document -> Sign
bsToSign Document
bs, [])

bsToSign :: Document -> Sign
bsToSign :: Document -> Sign
bsToSign doc :: Document
doc = Set NamedObject -> Sign
Sign (Set NamedObject -> Sign) -> Set NamedObject -> Sign
forall a b. (a -> b) -> a -> b
$ Document -> Set NamedObject
forall a. Ord a => [a] -> Set a
Set.fromList Document
doc