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