46 val dest_comb: cterm -> cterm * cterm |
46 val dest_comb: cterm -> cterm * cterm |
47 val dest_fun: cterm -> cterm |
47 val dest_fun: cterm -> cterm |
48 val dest_arg: cterm -> cterm |
48 val dest_arg: cterm -> cterm |
49 val dest_fun2: cterm -> cterm |
49 val dest_fun2: cterm -> cterm |
50 val dest_arg1: cterm -> cterm |
50 val dest_arg1: cterm -> cterm |
51 val dest_abs: string option -> cterm -> cterm * cterm |
51 val dest_abs_name: string -> cterm -> cterm * cterm |
|
52 val dest_abs: cterm -> cterm * cterm |
52 val rename_tvar: indexname -> ctyp -> ctyp |
53 val rename_tvar: indexname -> ctyp -> ctyp |
53 val var: indexname * ctyp -> cterm |
54 val var: indexname * ctyp -> cterm |
54 val apply: cterm -> cterm -> cterm |
55 val apply: cterm -> cterm -> cterm |
55 val lambda_name: string * cterm -> cterm -> cterm |
56 val lambda_name: string * cterm -> cterm -> cterm |
56 val lambda: cterm -> cterm -> cterm |
57 val lambda: cterm -> cterm -> cterm |
302 fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = |
303 fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = |
303 let val A = Term.argument_type_of c 0 |
304 let val A = Term.argument_type_of c 0 |
304 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end |
305 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end |
305 | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); |
306 | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); |
306 |
307 |
307 fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = |
308 fun dest_abs_name x (Cterm {t = Abs (_, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = |
308 let val (y', t') = Term.dest_abs (the_default x a, T, t) in |
309 let val (y', t') = Term.dest_abs (x, T, t) in |
309 (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, |
310 (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, |
310 Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) |
311 Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) |
311 end |
312 end |
312 | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); |
313 | dest_abs_name _ ct = raise CTERM ("dest_abs_name", [ct]); |
|
314 |
|
315 fun dest_abs (ct as Cterm {t = Abs (x, _, _), ...}) = dest_abs_name x ct |
|
316 | dest_abs ct = raise CTERM ("dest_abs", [ct]); |
313 |
317 |
314 |
318 |
315 (* constructors *) |
319 (* constructors *) |
316 |
320 |
317 fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = |
321 fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = |