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 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 (1,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, context, Cic.Sort Cic.Type ;
32 newmeta + 1, context, Cic.Meta (newmeta, irl);
33 newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
36 let mk_implicit' metasenv context =
37 let (metasenv, index) = mk_implicit metasenv context in
38 (metasenv, index - 1, index)
40 let mk_implicit_type metasenv context =
41 let newmeta = new_meta metasenv in
42 let irl = identity_relocation_list_for_metavariable context in
43 ([ newmeta, context, Cic.Sort Cic.Type ;
44 newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
47 let expand_implicits metasenv context term =
48 let rec aux metasenv context = function
49 | (Cic.Rel _) as t -> metasenv, t
50 | (Cic.Sort _) as t -> metasenv, t
51 | Cic.Const (uri, subst) ->
52 let metasenv', subst' = do_subst metasenv context subst in
53 metasenv', Cic.Const (uri, subst')
54 | Cic.Var (uri, subst) ->
55 let metasenv', subst' = do_subst metasenv context subst in
56 metasenv', Cic.Var (uri, subst')
57 | Cic.MutInd (uri, i, subst) ->
58 let metasenv', subst' = do_subst metasenv context subst in
59 metasenv', Cic.MutInd (uri, i, subst')
60 | Cic.MutConstruct (uri, i, j, subst) ->
61 let metasenv', subst' = do_subst metasenv context subst in
62 metasenv', Cic.MutConstruct (uri, i, j, subst')
64 let metasenv', l' = do_local_context metasenv context l in
65 metasenv', Cic.Meta (n, l')
67 let (metasenv', type_index, _) = mk_implicit' metasenv context in
68 let irl = identity_relocation_list_for_metavariable context in
69 metasenv', Cic.Meta (type_index, irl)
70 | Cic.Cast (te, ty) ->
71 let metasenv', ty' = aux metasenv context ty in
72 let metasenv'', te' = aux metasenv' context te in
73 metasenv'', Cic.Cast (te', ty')
74 | Cic.Prod (name, s, t) ->
75 let metasenv', s' = aux metasenv context s in
77 aux metasenv' (Some (name, Cic.Decl s') :: context) t
79 metasenv'', Cic.Prod (name, s', t')
80 | Cic.Lambda (name, s, t) ->
81 let metasenv', s' = aux metasenv context s in
83 aux metasenv' (Some (name, Cic.Decl s') :: context) t
85 metasenv'', Cic.Lambda (name, s', t')
86 | Cic.LetIn (name, s, t) ->
87 let metasenv', s' = aux metasenv context s in
89 aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
91 metasenv'', Cic.LetIn (name, s', t')
92 | Cic.Appl l when List.length l > 1 ->
95 (fun term (metasenv, terms) ->
96 let new_metasenv, term = aux metasenv context term in
97 new_metasenv, term :: terms)
100 metasenv', Cic.Appl l'
101 | Cic.Appl _ -> assert false
102 | Cic.MutCase (uri, i, outtype, term, patterns) ->
105 (fun term (metasenv, terms) ->
106 let new_metasenv, term = aux metasenv context term in
107 new_metasenv, term :: terms)
108 (outtype :: term :: patterns) (metasenv, [])
110 let outtype', term', patterns' =
112 | outtype' :: term' :: patterns' -> outtype', term', patterns'
115 metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
116 | Cic.Fix (i, funs) ->
117 let metasenv', types =
119 (fun (name, _, typ, _) (metasenv, types) ->
120 let new_metasenv, new_type = aux metasenv context typ in
121 (new_metasenv, (name, new_type) :: types))
126 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
130 let metasenv'', bodies =
132 (fun (_, _, _, body) (metasenv, bodies) ->
133 let new_metasenv, new_body = aux metasenv context' body in
134 (new_metasenv, new_body :: bodies))
137 let rec combine = function
138 | ((name, index, _, _) :: funs_tl),
139 ((_, typ) :: typ_tl),
141 (name, index, typ, term) :: combine (funs_tl, typ_tl, body_tl)
145 let funs' = combine (funs, types, bodies) in
146 metasenv'', Cic.Fix (i, funs')
147 | Cic.CoFix (i, funs) ->
148 let metasenv', types =
150 (fun (name, typ, _) (metasenv, types) ->
151 let new_metasenv, new_type = aux metasenv context typ in
152 (new_metasenv, (name, new_type) :: types))
157 (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
161 let metasenv'', bodies =
163 (fun (_, _, body) (metasenv, bodies) ->
164 let new_metasenv, new_body = aux metasenv context' body in
165 (new_metasenv, new_body :: bodies))
168 let rec combine = function
169 | ((name, _, _) :: funs_tl),
170 ((_, typ) :: typ_tl),
172 (name, typ, term) :: combine (funs_tl, typ_tl, body_tl)
176 let funs' = combine (funs, types, bodies) in
177 metasenv'', Cic.CoFix (i, funs')
178 and do_subst metasenv context subst =
180 (fun (uri, term) (metasenv, substs) ->
181 let metasenv', term' = aux metasenv context term in
182 (metasenv', (uri, term') :: substs))
184 and do_local_context metasenv context local_context =
186 (fun term (metasenv, local_context) ->
187 let metasenv', term' =
189 | None -> metasenv, None
191 let metasenv', term' = aux metasenv context term in
192 metasenv', Some term'
194 metasenv', term' :: local_context)
195 local_context (metasenv, [])
197 aux metasenv context term