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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
(* $:Id$ *)
open Util;;
open Names;;
open Term;;
(*
open Generic;;
open Mach;;
open Command;;
open More_util;;
open Pp;;
open Constrtypes;;
open Termenv;;
open Trad;;
open Ast;;
open CoqAst;;
open Machops;;
open Classops;;
open Recordops;;
*)
(********** definition d'un record (structure) **************)
let make_constructor fields appc =
let rec aux fields =
match fields with
[] -> appc
| (id,ty)::l -> ope("PROD",[ty; slam(Some (string_of_id id), aux l)])
in aux fields;;
(* free_vars existe de'ja` dans ast.ml *)
let rec drop = function
[] -> []
| (None::t) -> drop t
| ((Some id)::t) -> id::(drop t)
;;
let fold curriedf l base =
List.fold_right (fun a -> fun b -> curriedf(a,b)) l base
;;
let free_vars t =
let rec aux = function
(Nvar(_,s),accum) -> add_set (id_of_string s) accum
| (Node(_,_,tl),accum) -> fold aux tl accum
| (Slam(_,None,body),accum) ->
(aux(body,[]))@accum
| (Slam(_,Some id,body),accum) ->
(subtract (aux(body,[])) [(id_of_string id)])@accum
| (_,accum) -> accum
in aux(t,[])
;;
let free_in_asts id l =
let rec aux =
function [] -> true
| a::l -> (not (List.mem id (free_vars a))) & (aux l) in
aux l;;
let all_vars t =
let rec aux = function
(Nvar(_,id),accum) -> add_set (id_of_string id) accum
| (Node(_,_,tl),accum) -> fold aux tl accum
| (Slam(_,None,body),accum) -> aux (body,accum)
| (Slam(_,Some id,body),accum) ->
aux (body,(union accum [(id_of_string id)]))
| (_,accum) -> accum
in aux(t,[])
;;
let print_id_list l =
[< 'sTR "[" ; prlist (fun id -> [< 'sTR (string_of_id id) >]) l; 'sTR "]" >]
;;
let typecheck_params_and_field ps fs =
let sign0 = initial_sign() in
let sign1,newps =
List.fold_left
(fun (sign,newps) (id,t) ->
let tj = type_of_com sign t in
(add_sign (id,tj) sign,(id,tj.body)::newps))
(sign0,[]) ps in
let sign2,newfs =
List.fold_left
(fun (sign,newfs) (id,t) ->
let tj = type_of_com sign t in
(add_sign (id,tj) sign,(id,tj.body)::newfs)) (sign1,[]) fs
in List.rev(newps),List.rev(newfs)
;;
let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b);;
let definition_structure (coe_constr,struc,ps,cfs,const,s) =
let (sign,fsign) = initial_assumptions() in
let fs = List.map snd cfs in
let coers = List.map fst cfs in
let idps = List.map fst ps in
let typs = List.map snd ps in
let idfs = List.map fst fs in
let tyfs = List.map snd fs in
let _ = if not (free_in_asts struc tyfs)
then message "Error: A record cannot be recursive" in
let newps,newfs = typecheck_params_and_field ps fs in
let app_constructor = ope("APPLIST",
(ope("XTRA",[str "!";(nvar (string_of_id struc))]))::
List.map (fun id -> nvar(string_of_id id)) idps) in
let type_constructor = make_constructor fs app_constructor in
let _ = build_mutual ps [(struc,s,[(const,type_constructor)])] true in
let x = next_ident_away (id_of_string "x")
(List.fold_left (fun l ty -> union (all_vars ty) l)
(union idps (fst sign)) tyfs) in
let r = Machops.global (gLOB sign) struc in
let (rsp,_,_) = destMutInd r in
let rid = basename rsp in
let lp = length idps in
let rp1 = applist (r,(rel_list 0 lp)) in
let rp2 = applist (r,(rel_list 1 lp)) in
let warning_or_error coe st = if coe then (errorlabstrm "structure" st)
else pPNL [< 'sTR"Warning: "; st >] in
let (sp_projs,_,_,_,_) =
List.fold_left
(fun (sp_projs,ids_ok,ids_not_ok,sigma,coes) (fi,ti) ->
let fv_ti = global_vars ti in
let bad_projs = (intersect ids_not_ok fv_ti) in
if bad_projs <> []
then begin (warning_or_error (hd coes)
[< 'sTR(string_of_id fi);
'sTR" cannot be defined. The projections ";
print_id_list bad_projs; 'sTR " were not defined" >]);
(None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
end
else
let p = mkNamedLambda x rp2 (replace_vars sigma ti) in
let branch = mk_LambdaCit newfs (VAR fi) in
let proj = mk_LambdaCit newps
(mkNamedLambda x rp1 (mkMutCaseA (ci_of_mind r) p (Rel 1) [|branch|])) in
let ok = try (Declare.machine_constant (sign,fsign)
((fi,false,NeverDischarge),proj); true)
with UserError(s,pps) ->
((warning_or_error (hd coes)
[<'sTR (string_of_id fi);
'sTR" cannot be defined. "; pps >]);false) in
if not ok
then (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
else begin
if List.hd coes then
Class.try_add_new_coercion_record fi NeverDischarge rsp;
let constr_fi = Machops.global (gLOB sign) fi in
let constr_fip =
applist (constr_fi,(List.map (fun id -> VAR id) idps)@[VAR x])
in (Some(path_of_const constr_fi)::sp_projs,fi::ids_ok,ids_not_ok,
(fi,{sinfo=Closed;sit=constr_fip})::sigma,(tl coes))
end)
([],[],[],[],coers) newfs
in (if coe_constr="COERCION"
then Class.try_add_new_coercion const NeverDischarge);
add_new_struc (rsp,const,lp,rev sp_projs)
;;
(* $Id$ *)
|
