287 | is_unit _ = false; |
287 | is_unit _ = false; |
288 |
288 |
289 |
289 |
290 (* prod *) |
290 (* prod *) |
291 |
291 |
292 fun mk_prodT (T1, T2) = Type ("*", [T1, T2]); |
292 fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]); |
293 |
293 |
294 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) |
294 fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2) |
295 | dest_prodT T = raise TYPE ("dest_prodT", [T], []); |
295 | dest_prodT T = raise TYPE ("dest_prodT", [T], []); |
296 |
296 |
297 fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2)); |
297 fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2)); |
298 |
298 |
299 fun mk_prod (t1, t2) = |
299 fun mk_prod (t1, t2) = |
300 let val T1 = fastype_of t1 and T2 = fastype_of t2 in |
300 let val T1 = fastype_of t1 and T2 = fastype_of t2 in |
301 pair_const T1 T2 $ t1 $ t2 |
301 pair_const T1 T2 $ t1 $ t2 |
302 end; |
302 end; |
303 |
303 |
304 fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2) |
304 fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2) |
305 | dest_prod t = raise TERM ("dest_prod", [t]); |
305 | dest_prod t = raise TERM ("dest_prod", [t]); |
306 |
306 |
307 fun mk_fst p = |
307 fun mk_fst p = |
308 let val pT = fastype_of p in |
308 let val pT = fastype_of p in |
309 Const ("fst", pT --> fst (dest_prodT pT)) $ p |
309 Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p |
310 end; |
310 end; |
311 |
311 |
312 fun mk_snd p = |
312 fun mk_snd p = |
313 let val pT = fastype_of p in |
313 let val pT = fastype_of p in |
314 Const ("snd", pT --> snd (dest_prodT pT)) $ p |
314 Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p |
315 end; |
315 end; |
316 |
316 |
317 fun split_const (A, B, C) = |
317 fun split_const (A, B, C) = |
318 Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C); |
318 Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C); |
319 |
319 |
320 fun mk_split t = |
320 fun mk_split t = |
321 (case Term.fastype_of t of |
321 (case Term.fastype_of t of |
322 T as (Type ("fun", [A, Type ("fun", [B, C])])) => |
322 T as (Type ("fun", [A, Type ("fun", [B, C])])) => |
323 Const ("split", T --> mk_prodT (A, B) --> C) $ t |
323 Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t |
324 | _ => raise TERM ("mk_split: bad body type", [t])); |
324 | _ => raise TERM ("mk_split: bad body type", [t])); |
325 |
325 |
326 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) |
326 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) |
327 fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 |
327 fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 |
328 | flatten_tupleT T = [T]; |
328 | flatten_tupleT T = [T]; |
329 |
329 |
330 |
330 |
331 (* tuples with right-fold structure *) |
331 (* tuples with right-fold structure *) |
332 |
332 |
333 fun mk_tupleT [] = unitT |
333 fun mk_tupleT [] = unitT |
334 | mk_tupleT Ts = foldr1 mk_prodT Ts; |
334 | mk_tupleT Ts = foldr1 mk_prodT Ts; |
335 |
335 |
336 fun strip_tupleT (Type ("Product_Type.unit", [])) = [] |
336 fun strip_tupleT (Type ("Product_Type.unit", [])) = [] |
337 | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2 |
337 | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2 |
338 | strip_tupleT T = [T]; |
338 | strip_tupleT T = [T]; |
339 |
339 |
340 fun mk_tuple [] = unit |
340 fun mk_tuple [] = unit |
341 | mk_tuple ts = foldr1 mk_prod ts; |
341 | mk_tuple ts = foldr1 mk_prod ts; |
342 |
342 |
343 fun strip_tuple (Const ("Product_Type.Unity", _)) = [] |
343 fun strip_tuple (Const ("Product_Type.Unity", _)) = [] |
344 | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2 |
344 | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2 |
345 | strip_tuple t = [t]; |
345 | strip_tuple t = [t]; |
346 |
346 |
347 |
347 |
348 (* tuples with specific arities |
348 (* tuples with specific arities |
349 |
349 |
365 in fst o mk [] end; |
365 in fst o mk [] end; |
366 |
366 |
367 fun strip_ptupleT ps = |
367 fun strip_ptupleT ps = |
368 let |
368 let |
369 fun factors p T = if member (op =) ps p then (case T of |
369 fun factors p T = if member (op =) ps p then (case T of |
370 Type ("*", [T1, T2]) => |
370 Type ("Product_Type.*", [T1, T2]) => |
371 factors (1::p) T1 @ factors (2::p) T2 |
371 factors (1::p) T1 @ factors (2::p) T2 |
372 | _ => ptuple_err "strip_ptupleT") else [T] |
372 | _ => ptuple_err "strip_ptupleT") else [T] |
373 in factors [] end; |
373 in factors [] end; |
374 |
374 |
375 val flat_tupleT_paths = |
375 val flat_tupleT_paths = |
376 let |
376 let |
377 fun factors p (Type ("*", [T1, T2])) = |
377 fun factors p (Type ("Product_Type.*", [T1, T2])) = |
378 p :: factors (1::p) T1 @ factors (2::p) T2 |
378 p :: factors (1::p) T1 @ factors (2::p) T2 |
379 | factors p _ = [] |
379 | factors p _ = [] |
380 in factors [] end; |
380 in factors [] end; |
381 |
381 |
382 fun mk_ptuple ps = |
382 fun mk_ptuple ps = |
383 let |
383 let |
384 fun mk p T ts = |
384 fun mk p T ts = |
385 if member (op =) ps p then (case T of |
385 if member (op =) ps p then (case T of |
386 Type ("*", [T1, T2]) => |
386 Type ("Product_Type.*", [T1, T2]) => |
387 let |
387 let |
388 val (t, ts') = mk (1::p) T1 ts; |
388 val (t, ts') = mk (1::p) T1 ts; |
389 val (u, ts'') = mk (2::p) T2 ts' |
389 val (u, ts'') = mk (2::p) T2 ts' |
390 in (pair_const T1 T2 $ t $ u, ts'') end |
390 in (pair_const T1 T2 $ t $ u, ts'') end |
391 | _ => ptuple_err "mk_ptuple") |
391 | _ => ptuple_err "mk_ptuple") |
393 in fst oo mk [] end; |
393 in fst oo mk [] end; |
394 |
394 |
395 fun strip_ptuple ps = |
395 fun strip_ptuple ps = |
396 let |
396 let |
397 fun dest p t = if member (op =) ps p then (case t of |
397 fun dest p t = if member (op =) ps p then (case t of |
398 Const ("Pair", _) $ t $ u => |
398 Const ("Product_Type.Pair", _) $ t $ u => |
399 dest (1::p) t @ dest (2::p) u |
399 dest (1::p) t @ dest (2::p) u |
400 | _ => ptuple_err "strip_ptuple") else [t] |
400 | _ => ptuple_err "strip_ptuple") else [t] |
401 in dest [] end; |
401 in dest [] end; |
402 |
402 |
403 val flat_tuple_paths = |
403 val flat_tuple_paths = |
404 let |
404 let |
405 fun factors p (Const ("Pair", _) $ t $ u) = |
405 fun factors p (Const ("Product_Type.Pair", _) $ t $ u) = |
406 p :: factors (1::p) t @ factors (2::p) u |
406 p :: factors (1::p) t @ factors (2::p) u |
407 | factors p _ = [] |
407 | factors p _ = [] |
408 in factors [] end; |
408 in factors [] end; |
409 |
409 |
410 (*In mk_psplits ps S T u, term u expects separate arguments for the factors of S, |
410 (*In mk_psplits ps S T u, term u expects separate arguments for the factors of S, |
412 of type S.*) |
412 of type S.*) |
413 fun mk_psplits ps T T3 u = |
413 fun mk_psplits ps T T3 u = |
414 let |
414 let |
415 fun ap ((p, T) :: pTs) = |
415 fun ap ((p, T) :: pTs) = |
416 if member (op =) ps p then (case T of |
416 if member (op =) ps p then (case T of |
417 Type ("*", [T1, T2]) => |
417 Type ("Product_Type.*", [T1, T2]) => |
418 split_const (T1, T2, map snd pTs ---> T3) $ |
418 split_const (T1, T2, map snd pTs ---> T3) $ |
419 ap ((1::p, T1) :: (2::p, T2) :: pTs) |
419 ap ((1::p, T1) :: (2::p, T2) :: pTs) |
420 | _ => ptuple_err "mk_psplits") |
420 | _ => ptuple_err "mk_psplits") |
421 else Abs ("x", T, ap pTs) |
421 else Abs ("x", T, ap pTs) |
422 | ap [] = |
422 | ap [] = |