(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
(* where n = List.length [canonical_context] *)
(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
+let identity_relocation_list_for_metavariable ?(start = 1) canonical_context =
let canonical_context_length = List.length canonical_context in
let rec aux =
function
| (n,None::tl) -> None::(aux ((n+1),tl))
| (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
in
- aux (1,canonical_context)
+ aux (start,canonical_context)
(* Returns the first meta whose number is above the *)
(* number of the higher meta. *)
(uri,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris
-let mk_implicit' metasenv context =
- let (metasenv, index) = mk_implicit metasenv context in
- (metasenv, index - 1, index)
-
let mk_implicit_type metasenv context =
let newmeta = new_meta metasenv in
let irl = identity_relocation_list_for_metavariable context in
let metasenv', l' = do_local_context metasenv context l in
metasenv', Cic.Meta (n, l')
| Cic.Implicit ->
- let (metasenv', type_index, _) = mk_implicit' metasenv context in
+ let (metasenv', idx) = mk_implicit metasenv context in
let irl = identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (type_index, irl)
+ metasenv', Cic.Meta (idx, irl)
| Cic.Cast (te, ty) ->
let metasenv', ty' = aux metasenv context ty in
let metasenv'', te' = aux metasenv' context te in
| ((name, index, _, _) :: funs_tl),
((_, typ) :: typ_tl),
(body :: body_tl) ->
- (name, index, typ, term) :: combine (funs_tl, typ_tl, body_tl)
+ (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl)
| [], [], [] -> []
| _ -> assert false
in
| ((name, _, _) :: funs_tl),
((_, typ) :: typ_tl),
(body :: body_tl) ->
- (name, typ, term) :: combine (funs_tl, typ_tl, body_tl)
+ (name, typ, body) :: combine (funs_tl, typ_tl, body_tl)
| [], [], [] -> []
| _ -> assert false
in