2 (* identity_relocation_list_for_metavariable i canonical_context *)
3 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
4 (* where n = List.length [canonical_context] *)
5 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
6 let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
7 let canonical_context_length = List.length canonical_context in
11 | (n,None::tl) -> None::(aux ((n+1),tl))
12 | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
14 aux (start,canonical_context)
16 (* Returns the first meta whose number is above the *)
17 (* number of the higher meta. *)
18 let new_meta metasenv =
23 | None,(n,_,_)::tl -> aux (Some n,tl)
24 | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
26 1 + aux (None,metasenv)
28 let mk_implicit metasenv context =
29 let newmeta = new_meta metasenv in
30 let irl = identity_relocation_list_for_metavariable context in
31 ([ newmeta, [], Cic.Sort Cic.Type ;
32 newmeta + 1, context, Cic.Meta (newmeta, []);
33 newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
36 let mk_implicit_type metasenv context =
37 let newmeta = new_meta metasenv in
38 ([ newmeta, [], Cic.Sort Cic.Type ;
39 newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
42 let mk_implicit_sort metasenv =
43 let newmeta = new_meta metasenv in
44 ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta)
46 let n_fresh_metas metasenv context n =
47 if n = 0 then metasenv, []
49 let irl = identity_relocation_list_for_metavariable context in
50 let newmeta = new_meta metasenv in
51 let rec aux newmeta n =
52 if n = 0 then metasenv, []
54 let metasenv', l = aux (newmeta + 3) (n-1) in
55 (newmeta, context, Cic.Sort Cic.Type)::
56 (newmeta + 1, context, Cic.Meta (newmeta, irl))::
57 (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
58 Cic.Meta(newmeta+2,irl)::l in
61 let fresh_subst metasenv context uris =
62 let irl = identity_relocation_list_for_metavariable context in
63 let newmeta = new_meta metasenv in
64 let rec aux newmeta = function
67 let metasenv', l = aux (newmeta + 3) tl in
68 (newmeta, context, Cic.Sort Cic.Type)::
69 (newmeta + 1, context, Cic.Meta (newmeta, irl))::
70 (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
71 (uri,Cic.Meta(newmeta+2,irl))::l in
74 let expand_implicits metasenv context term =
75 let rec aux metasenv context = function
76 | (Cic.Rel _) as t -> metasenv, t
77 | (Cic.Sort _) as t -> metasenv, t
78 | Cic.Const (uri, subst) ->
79 let metasenv', subst' = do_subst metasenv context subst in
80 metasenv', Cic.Const (uri, subst')
81 | Cic.Var (uri, subst) ->
82 let metasenv', subst' = do_subst metasenv context subst in
83 metasenv', Cic.Var (uri, subst')
84 | Cic.MutInd (uri, i, subst) ->
85 let metasenv', subst' = do_subst metasenv context subst in
86 metasenv', Cic.MutInd (uri, i, subst')
87 | Cic.MutConstruct (uri, i, j, subst) ->
88 let metasenv', subst' = do_subst metasenv context subst in
89 metasenv', Cic.MutConstruct (uri, i, j, subst')
91 let metasenv', l' = do_local_context metasenv context l in
92 metasenv', Cic.Meta (n, l')
93 | Cic.Implicit (Some `Type) ->
94 let (metasenv', idx) = mk_implicit_type metasenv context in
95 let irl = identity_relocation_list_for_metavariable context in
96 metasenv', Cic.Meta (idx, irl)
97 | Cic.Implicit (Some `Closed) ->
98 let (metasenv', idx) = mk_implicit metasenv [] in
99 metasenv', Cic.Meta (idx, [])
100 | Cic.Implicit None ->
101 let (metasenv', idx) = mk_implicit metasenv context in
102 let irl = identity_relocation_list_for_metavariable context in
103 metasenv', Cic.Meta (idx, irl)
104 | Cic.Cast (te, ty) ->
105 let metasenv', ty' = aux metasenv context ty in
106 let metasenv'', te' = aux metasenv' context te in
107 metasenv'', Cic.Cast (te', ty')
108 | Cic.Prod (name, s, t) ->
109 let metasenv', s' = aux metasenv context s in
111 aux metasenv' (Some (name, Cic.Decl s') :: context) t
113 metasenv'', Cic.Prod (name, s', t')
114 | Cic.Lambda (name, s, t) ->
115 let metasenv', s' = aux metasenv context s in
117 aux metasenv' (Some (name, Cic.Decl s') :: context) t
119 metasenv'', Cic.Lambda (name, s', t')
120 | Cic.LetIn (name, s, t) ->
121 let metasenv', s' = aux metasenv context s in
123 aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
125 metasenv'', Cic.LetIn (name, s', t')
126 | Cic.Appl l when List.length l > 1 ->
129 (fun term (metasenv, terms) ->
130 let new_metasenv, term = aux metasenv context term in
131 new_metasenv, term :: terms)
134 metasenv', Cic.Appl l'
135 | Cic.Appl _ -> assert false
136 | Cic.MutCase (uri, i, outtype, term, patterns) ->
139 (fun term (metasenv, terms) ->
140 let new_metasenv, term = aux metasenv context term in
141 new_metasenv, term :: terms)
142 (outtype :: term :: patterns) (metasenv, [])
144 let outtype', term', patterns' =
146 | outtype' :: term' :: patterns' -> outtype', term', patterns'
149 metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
150 | Cic.Fix (i, funs) ->
151 let metasenv', types =
153 (fun (name, _, typ, _) (metasenv, types) ->
154 let new_metasenv, new_type = aux metasenv context typ in
155 (new_metasenv, (name, new_type) :: types))
160 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
164 let metasenv'', bodies =
166 (fun (_, _, _, body) (metasenv, bodies) ->
167 let new_metasenv, new_body = aux metasenv context' body in
168 (new_metasenv, new_body :: bodies))
171 let rec combine = function
172 | ((name, index, _, _) :: funs_tl),
173 ((_, typ) :: typ_tl),
175 (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
179 let funs' = combine (funs, types, bodies) in
180 metasenv'', Cic.Fix (i, funs')
181 | Cic.CoFix (i, funs) ->
182 let metasenv', types =
184 (fun (name, typ, _) (metasenv, types) ->
185 let new_metasenv, new_type = aux metasenv context typ in
186 (new_metasenv, (name, new_type) :: types))
191 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
195 let metasenv'', bodies =
197 (fun (_, _, body) (metasenv, bodies) ->
198 let new_metasenv, new_body = aux metasenv context' body in
199 (new_metasenv, new_body :: bodies))
202 let rec combine = function
203 | ((name, _, _) :: funs_tl),
204 ((_, typ) :: typ_tl),
206 (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
210 let funs' = combine (funs, types, bodies) in
211 metasenv'', Cic.CoFix (i, funs')
212 and do_subst metasenv context subst =
214 (fun (uri, term) (metasenv, substs) ->
215 let metasenv', term' = aux metasenv context term in
216 (metasenv', (uri, term') :: substs))
218 and do_local_context metasenv context local_context =
220 (fun term (metasenv, local_context) ->
221 let metasenv', term' =
223 | None -> metasenv, None
225 let metasenv', term' = aux metasenv context term in
226 metasenv', Some term'
228 metasenv', term' :: local_context)
229 local_context (metasenv, [])
231 aux metasenv context term