1   module Build_Tm where
    2 
    3   import Unparse
    4 
    5   import Kernel
    6 
    7   import Sub_Core1
    8 
    9   import Sub_Core2
   10 
   11   import Sub_Core3
   12 
   13   import Sub_Core4
   14 
   15   import Type_defs
   16 
   17   import Core_datatype
   18 
   19   import Vtslib
   20 
   21   build_trm :: Sgn -> Flagged_ITrm -> Trm
   22 
   23   build_trm sg ( Opnd ( Itrm itm ))
   24         = build_trm' sg itm
   25 
   26   build_trm ( SG sg ) oth
   27         = error ("Error: " ++ unparse sg oth ++ "|\n")
   28 
   29 
   30 
   31   build_trm' sg ( Sym i j tyL attL )
   32         = add_l ( symbol sg i j ) tyL attL
   33 
   34   build_trm' sg ( App itm1 itm2 tyL attL )
   35         = add_l ( appl tm1 tm2 ) tyL attL
   36           where
   37           tm1 = build_trm' sg itm1 
   38           tm2 = build_trm' sg itm2
   39 
   40 
   41 
   42   build_trm' sg ( Pair itm1 itm2 itm3 tyL attL )
   43         = add_l ( pair tm1 tm2 tm3 ) tyL attL
   44           where
   45           tm1 = build_trm' sg itm1
   46           tm2 = build_trm' sg itm2
   47           tm3 = case itm3 of
   48                         Constant ( Univ (-1)) _ _ 
   49                                 -> sigma btm2 
   50                                    where
   51                                    btm2 = shift_Trm 1 sg2 ( typ_of_Trm tm2 )
   52                                    sg2  = extend bdc1 sg
   53                                    bdc1 = symbol_dec ( typ_of_Trm tm1 )
   54                         _       -> build_trm' sg itm3
   55 
   56   build_trm' sg ( Binder bdr idc itm tyL attL )
   57         = add_l ( bdr_fn tm ) tyL attL
   58           where
   59           tm = build_trm' ( extend dc sg ) itm
   60           dc = gen_dc sg idc
   61           bdr_fn = case bdr of
   62                         Lambda  -> lambda
   63                         Forall  -> universal
   64                         Imp     -> implication
   65                         Exists  -> existential
   66                         Pi      -> pi'
   67                         Sigma   -> sigma
   68                         Subtype -> subtype
   69                         Delta   -> \ _ -> TM_Err "Invalid occurance of \196"
   70                         Choose  -> \ _ -> TM_Err "Invalid occurance of \229"    
   71 
   72   build_trm' sg ( Constant cst tyL attL )
   73         = add_l ( cst_fn sg ) tyL attL
   74           where
   75           cst_fn = case cst of
   76                         Bool'  -> bool_sm
   77                         T      -> true_sm
   78                         F      -> false_sm
   79                         Univ i -> \sg -> universe sg i
   80 
   81   build_trm' sg ( Binary' b_op itm1 itm2 tyL attL )
   82         = add_l ( bin_fn tm1 tm2 ) tyL attL
   83           where
   84           tm1 = build_trm' sg itm1
   85           tm2 = build_trm' sg itm2
   86           bin_fn = case b_op of
   87                         And       -> conjunction
   88                         Or        -> disjunction
   89                         Eq'       -> equal
   90                         Issubtype -> issubtype
   91 
   92   build_trm' sg ( Unary Not itm tyL attL )
   93         = add_l ( negation tm ) tyL attL 
   94           where
   95           tm = build_trm' sg itm
   96 
   97   build_trm' sg ( Cond idc itm1 itm2 tyL attL )
   98         = add_l ( conditional tm1 tm2 ) tyL attL
   99           where
  100           tm1 = build_trm' sg2 itm1
  101           tm2 = build_trm' sg3 itm2
  102           sg2 = extend dc1 sg
  103           sg3 = extend dc2 sg 
  104           dc2 = symbol_dec ( negation ( typ_of_Dec dc1 ))
  105           dc1 = gen_dc sg idc
  106 
  107   build_trm' sg ( Const i j k tyL attL )
  108         = add_l ( constructor sg i j k ) tyL attL
  109 
  110   build_trm' sg ( Recurse itmL itm tyL attL )
  111         = add_l ( recurse tmL tm ) tyL attL
  112           where
  113           tmL = map ( build_trm' sg ) itmL
  114           tm  = build_trm' sg itm
  115 
  116   build_trm' sg ( Tagid ( str , _ , cnv_fnL ) argL )
  117         = case fetch_fn cnv_fnL of
  118                 Ok cnv_fn -> cnv_fn argL
  119                 Bad mesg  -> TM_Err mesg
  120           where
  121  --       fetch_fn :: [Cnv_Fn] -> MayBe ( [Tag_Arg] -> Trm )
  122           fetch_fn ( Trm_Fn fn : _ ) = Ok fn
  123           fetch_fn ( _ : oth )       = fetch_fn oth
  124           fetch_fn []                = Bad ( "cannot convert tag " ++ str ++ " to term" )
  125 
  126   build_trm' ( SG isg ) oth
  127         = error ("Unimplemented construction: " ++ unparse' isg oth ++ "|\n")
  128 
  129 
  130 
  131 
  132   build_dc = gen_dc
  133 
  134 
  135 
  136   gen_dc sg ( Symbol_dec itm attL )
  137         = case typ_of_trm isg itm of
  138                 Constant Bool' _ _ 
  139                        -> set_Dec_att ( axiom_dec ( build_trm' sg itm )) attL
  140                 otherwise 
  141                        -> set_Dec_att ( symbol_dec ( build_trm' sg itm )) attL
  142           where
  143           isg = internal_Sgn sg
  144 
  145   gen_dc sg ( Axiom_dec itm attL )
  146         = set_Dec_att ( axiom_dec ( build_trm' sg itm )) attL
  147 
  148   gen_dc sg ( Decpair idc1 idc2 attL )
  149         = set_Dec_att dc_pair attL
  150           where
  151           dc_pair = decpair dc2
  152           dc2     = gen_dc sg2 idc2 
  153           sg2     = extend dc1 sg 
  154           dc1     = gen_dc sg idc1
  155 
  156   gen_dc _ _ = error "Only symbol_dec so far implemented"
  157 
  158 
  159 
  160 
  161 
  162 
  163   add_l ( TM_Err mesg ) _ _ = TM_Err mesg
  164 
  165 
  166 
  167   add_l tm tyL@( srt : _ ) attL
  168         = if eq_trm srt_tm srt 
  169                 then set_Trm_att tm [] attL     
  170                 else TM_Err "Invalid type specification"
  171           where
  172           ( _ , srt_tm , _ ) = internal_Trm tm
  173 
  174   add_l tm [] attL 
  175         = set_Trm_att tm [] attL
  176 
  177 
  178 
  179 
  180 
  181 
  182   build_sg :: ISgn -> Sgn
  183 
  184   build_sg ( Empty _ ) = empty
  185 
  186   build_sg ( Extend idc isg _ ) 
  187         = extend ( build_dc sg idc ) sg
  188           where
  189           sg = build_sg isg
  190 
  191   build_sg _ = error "unimplemented signature constructor"
  192