blob: 9df751b46fe9ffd446f125adde275b1f48d75fc8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
(* $Id$ *)
open Util
open Names
open Generic
open Term
type abstraction_body = {
abs_kind : path_kind;
abs_arity : int array;
abs_rhs : constr }
let rec count_dlam = function
| DLAM (_,c) -> 1 + (count_dlam c)
| _ -> 0
let sAPP c n =
match c with
| DLAM(na,m) -> subst1 n m
| _ -> invalid_arg "SAPP"
let contract_abstraction ab args =
if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args)
else
failwith "contract_abstraction"
|
