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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
(******************************************************************************)
(* *)
(* PROJECT HELM *)
(* *)
(* A tactic to print Coq objects in XML *)
(* *)
(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
(* 02/12/1999 *)
(* *)
(* This module compute the list of variables occurring in a term from the *)
(* term and the list of variables possibly occuring in it *)
(* *)
(******************************************************************************)
let get_depth_of_var vl v =
let rec aux n =
function
[] -> None
| (he::tl) -> if List.mem v he then Some n else aux (n + 1) tl
in
aux 0 vl
;;
exception CookingInternalError;;
let string_of_vars_list =
let add_prefix n s = string_of_int n ^ ": " ^ s in
let rec aux =
function
[n,v] -> (n,v)
| (n,v)::tl ->
let (k,s) = aux tl in
if k = n then (k, v ^ " " ^ s) else (n, v ^ " " ^ add_prefix k s)
| [] -> raise CookingInternalError
in
function
[] -> ""
| vl -> let (k,s) = aux vl in add_prefix k s
;;
(*CSC commento sbagliato ed obsoleto *)
(* If t is \v1. ... \vn.t' where v1, ..., vn are in the variable list vl then *)
(* get_params_from_type vl t returns [v1; ...; vn] *)
let get_params_from_type vl t =
let rec rget t l =
let module T = Term in
let module N = Names in
match T.kind_of_term t with
T.IsProd (N.Name id, _, target) ->
let id' = N.string_of_id id in
(match get_depth_of_var vl id' with
None -> l
| Some n -> rget target ((n,id')::l)
)
| T.IsCast (term, _) -> rget term l
| _ -> l
in
let pl = List.rev (rget t []) in
string_of_vars_list pl
;;
(* add_cooking_information csp vl *)
(* when csp is the section path of the most cooked object co *)
(* and vl is the list of variables possibly occuring in co *)
(* returns the list of variables actually occurring in co *)
let add_cooking_information sp vl =
let module D = Declarations in
let module G = Global in
let module N = Names in
let module T = Term in
let module X = Xml in
try
let {D.const_body=val0 ; D.const_type = typ} = G.lookup_constant sp in
let typ = T.body_of_type typ in
get_params_from_type vl typ
with
Not_found ->
try
let {D.mind_packets=packs ; D.mind_nparams=nparams} =
G.lookup_mind sp
in
let {D.mind_nf_arity=arity} = packs.(0) in
let arity = T.body_of_type arity in
get_params_from_type vl arity
with
Not_found -> Util.anomaly "Cooking of an uncoockable term required"
;;
|
