1 {-
    2  * Mon Nov  5 09:54:24 GMT 1990
    3  *
    4  * Implementation of untyped terms, signatures and declarations
    5  *
    6  * Each constructors last argument (of the tuple) is a list of
    7  * information attributes that the parser, unparsers, tactics etc use.
    8  *      
    9  * Each terms' next to last argument is a list of alternative types that the
   10  * term can have to its natutal type.
   11  *
   12  -}
   13 
   14 module Core_datatype where
   15 
   16 
   17 
   18 type Share_map = [ Int ]
   19 
   20 data ITrm =  Sym        Int Int                     [ ITrm ] [ Attribute ]
   21            | App        ITrm ITrm                   [ ITrm ] [ Attribute ]
   22            | Pair       ITrm ITrm ITrm              [ ITrm ] [ Attribute ]
   23            | Binder     Binder_conn IDec ITrm       [ ITrm ] [ Attribute ]
   24            | Constant   Constant_conn               [ ITrm ] [ Attribute ]
   25            | Unary      Unary_conn ITrm             [ ITrm ] [ Attribute ]
   26            | Binary'    Binary_conn ITrm ITrm       [ ITrm ] [ Attribute ]
   27            | Cond       IDec ITrm ITrm              [ ITrm ] [ Attribute ]
   28            | Const      Int Int Int                 [ ITrm ] [ Attribute ]
   29            | Recurse    [ ITrm ] ITrm               [ ITrm ] [ Attribute ]
   30            | Tagid      Tag [ Tag_Arg ]
   31            | ITrm_Err   String
   32 --           deriving (Eq)
   33                
   34 data IDec =  Symbol_dec ITrm                         [ Attribute ]
   35            | Axiom_dec  ITrm                         [ Attribute ]
   36            | Def        ITrm ITrm                    [ Attribute ]
   37            | Data       [ IDec ] [[ ITrm ]]          [ Attribute ]
   38            | Decpair    IDec IDec                    [ Attribute ]
   39 --           deriving (Eq)
   40       
   41 data ISgn =   Empty                                  [ Attribute ]
   42             | Extend     IDec ISgn                      [ Attribute ]
   43             | Combine    ISgn ISgn Int [ Int ]          [ Attribute ]  
   44             | Share      ISgn Int Int Int [ Int ]       [ Attribute ]
   45 --            deriving (Eq)
   46 
   47 data Binder_conn = Lambda | Forall | Exists | Pi | Sigma |
   48                   Imp | Subtype | Delta | Choose
   49                   deriving (Eq)
   50 
   51 data Unary_conn = Not deriving (Eq)
   52 
   53 data Binary_conn = Or | And | Eq' | Issubtype deriving (Eq)
   54 
   55 data Constant_conn = T | F | Bool' | Univ Int deriving (Eq)
   56 
   57 
   58 
   59 
   60 
   61 
   62 
   63 
   64 -- types associated with tags
   65 
   66 type Tag = ( String , [Tag_Arg_type] , [Cnv_Fn]  )
   67 
   68 
   69 -- type indicator and resulting types for args
   70 
   71 data Tag_Arg_type = Term_Arg | Deriv_Arg | Int_Arg deriving ( Eq )
   72 
   73 data Tag_Arg = Tg_Trm Trm | Tg_Thm Thm | Tg_Int [Int] -- deriving ( Eq )
   74 
   75 
   76 -- convertion function ( tags to related objects )
   77 
   78 data Cnv_Fn = Trm_Fn ( [Tag_Arg] -> Trm ) |
   79               Thm_Fn ( [Tag_Arg] -> Thm )     
   80 
   81 -- need terms and theorems in tags ( leave here permanently? )
   82 
   83 data Trm = TM ITrm ITrm ISgn | {- the term, its type, and signature     -}
   84            TM_Err String
   85 
   86 data Thm = TH ITrm ISgn | {- the theorem, and its signature             -}
   87            TH_Err String
   88 
   89 
   90 
   91 
   92 
   93 
   94 -- working types for parser
   95 
   96 type Attribute = ( Attribute_Tag , Attribute_Value ) 
   97 
   98 
   99 data Flagged_ITrm = Opr Operator Oprtype Int |
  100                      Opnd Operand       | 
  101                      Prs_Err String
  102 --                       deriving ( Eq )
  103 
  104 data Operand = Itrm ITrm | Idec IDec | Isgn ISgn   -- normal operands
  105                 | PApp Binder_conn IDec Bool        -- special partial apps, bool indicates anonymous declaration 
  106                 | PairApp ITrm 
  107                 | ParIfx Binary_conn ITrm
  108                 | TypApp Flagged_ITrm
  109                 | ParColon ITrm
  110 --              deriving ( Eq )
  111 
  112 data Operator = OpItrm ITrm | OpBdr Binder_conn 
  113                  | OpIfx Binary_conn | Spl String --deriving ( Eq )
  114 
  115 
  116 data Attribute_Tag =   Name_Style
  117                     | Symbol_Style
  118                     | Pair_Style
  119                     | Let_Style
  120                     | Case_Style
  121                     | Opr_Style
  122                     | Fun_Style
  123                     | Binder_Style
  124                     | Constant_Style
  125                     | Unary_Style
  126                     | Binary_Style
  127                     | Cond_Style
  128                     | Recurse_Style
  129                     | Hyp_Style
  130                     | Dec_Style
  131                     | Def_Style
  132                     | Comment
  133                       deriving (Eq)
  134 
  135 
  136 data Attribute_Value =   Symbol_Name Name' 
  137                       | Datatype_Name [ Name' ]  
  138                       | Named | Indexed
  139                       | Typed | Untyped
  140                       | Let
  141                       | Case
  142                       | Prefixed | Linfixed | Rinfixed | Postfixed
  143                       | Functional | Subscripted
  144                       | Prefix_Binder | Infix_Binder
  145                       | Recursive | Fn
  146                       | NonDependent
  147                       | Grouped | Ungrouped 
  148                       | Parameter | NonParameter
  149                       | String' String
  150                       deriving (Eq)
  151 
  152 data Name' = Name String | Operator' String Int Oprtype
  153                deriving ( Eq )
  154 
  155 data Oprtype = Pre | Post | BinL | BinR deriving ( Eq )
  156 
  157 -- att_to_str (Name' s) = s
  158