TFL/tfl.sml
changeset 4062 fa2eb95b1b2d
parent 4027 15768dba480e
child 4149 a6ccec4fd0c3
equal deleted inserted replaced
4061:5a2cc5752cb6 4062:fa2eb95b1b2d
   222      let val pty as Type (ty_name,_) = type_of p
   222      let val pty as Type (ty_name,_) = type_of p
   223      in
   223      in
   224      case (ty_info ty_name)
   224      case (ty_info ty_name)
   225      of None => mk_case_fail("Not a known datatype: "^ty_name)
   225      of None => mk_case_fail("Not a known datatype: "^ty_name)
   226       | Some{case_const,constructors} =>
   226       | Some{case_const,constructors} =>
   227         let val case_const_name = #1(dest_Const case_const)
   227         let open Basis_Library (*restore original List*)
   228             val nrows = List_.concat (map (expand constructors pty) rows)
   228 	    val case_const_name = #1(dest_Const case_const)
       
   229             val nrows = List.concat (map (expand constructors pty) rows)
   229             val subproblems = divide(constructors, pty, range_ty, nrows)
   230             val subproblems = divide(constructors, pty, range_ty, nrows)
   230             val groups      = map #group subproblems
   231             val groups      = map #group subproblems
   231             and new_formals = map #new_formals subproblems
   232             and new_formals = map #new_formals subproblems
   232             and constructors' = map #constructor subproblems
   233             and constructors' = map #constructor subproblems
   233             val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
   234             val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
   237             val case_functions = map S.list_mk_abs
   238             val case_functions = map S.list_mk_abs
   238                                   (ListPair.zip (new_formals, dtrees))
   239                                   (ListPair.zip (new_formals, dtrees))
   239             val types = map type_of (case_functions@[u]) @ [range_ty]
   240             val types = map type_of (case_functions@[u]) @ [range_ty]
   240             val case_const' = Const(case_const_name, list_mk_type types)
   241             val case_const' = Const(case_const_name, list_mk_type types)
   241             val tree = list_comb(case_const', case_functions@[u])
   242             val tree = list_comb(case_const', case_functions@[u])
   242             val pat_rect1 = List_.concat
   243             val pat_rect1 = List.concat
   243                               (ListPair.map mk_pat (constructors', pat_rect))
   244                               (ListPair.map mk_pat (constructors', pat_rect))
   244         in (pat_rect1,tree)
   245         in (pat_rect1,tree)
   245         end 
   246         end 
   246      end end
   247      end end
   247  in mk
   248  in mk