(i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
in
NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
- | [] -> NCicUntrusted.apply_subst subst ctx
+ | [] ->
+ (* STRONG ASSUMPTION:
+ since metas occurring in t have an empty context,
+ the substitution i build makes sense (i.e, the Rel
+ I pun in the subst will not be lifted by subst_meta *)
+ NCicUntrusted.apply_subst subst ctx
(NCicSubstitution.lift (List.length ctx) t)
| _ -> assert false
in
in
let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
+(*
prerr_endline (
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
" cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity);
+*)
Some (bo,src,tgt,arity,pos)
with
| NCicTypeChecker.TypeCheckerFailure _
| _ -> obj_kind
in
let obj = uri,height,[],[],obj_kind in
- let status = NCicLibrary.add_obj status obj in
- prerr_endline (NCicPp.ppobj obj);
- let boxml = NCicElim.mk_elims obj in
+ let old_status = status in
+ let status = NCicLibrary.add_obj status obj in
+ HLog.message ("New object: " ^ NUri.string_of_uri uri);
+ (try
+ (*prerr_endline (NCicPp.ppobj obj);*)
+ let boxml = NCicElim.mk_elims obj in
+ let boxml = boxml @ NCicElim.mk_projections obj in
(*
- let objs = [] in
- let timestamp,uris_rev =
- List.fold_left
- (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
- let status = NCicLibrary.add_obj status obj in
- status,uri::uris_rev
- ) (status,[]) objs in
- let uris = uri::List.rev uris_rev in
+ let objs = [] in
+ let timestamp,uris_rev =
+ List.fold_left
+ (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
+ let status = NCicLibrary.add_obj status obj in
+ status,uri::uris_rev
+ ) (status,[]) objs in
+ let uris = uri::List.rev uris_rev in
*)
- let status = status#set_ng_mode `CommandMode in
-let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
- List.fold_left
- (fun (status,uris) boxml ->
- let status,nuris =
- eval_ncommand opts status
- ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
- in
- match uris,nuris with
- `New uris, `New nuris -> status,`New (nuris@uris)
- | _ -> assert false
- ) (status,`New [] (* uris *)) boxml
+ let status = status#set_ng_mode `CommandMode in
+ let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+ let status,uris =
+ List.fold_left
+ (fun (status,uris) boxml ->
+ try
+ let status,nuris =
+ eval_ncommand opts status
+ ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+ in
+ match uris,nuris with
+ `New uris, `New nuris -> status,`New (nuris@uris)
+ | _ -> assert false
+ with
+ NCicTypeChecker.TypeCheckerFailure msg
+ when Lazy.force msg =
+ "Sort elimination not allowed" ->
+ status,uris
+ ) (status,`New [] (* uris *)) boxml in
+ let coercions =
+ match obj with
+ _,_,_,_,NCic.Inductive
+ (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
+ ->
+ HExtlib.filter_map
+ (fun (name,is_coercion,arity) ->
+ if is_coercion then Some(name,leftno,arity) else None) fields
+ | _ -> [] in
+ let status =
+ List.fold_left
+ (fun status (name,cpos,arity) ->
+ (*CSC: COME DICHIARO LA COERCION??? *)
+ status
+ ) status coercions
+ in
+ status,uris
+ with
+ exn ->
+ NCicLibrary.time_travel old_status;
+ raise exn)
| GrafiteAst.NCopy (log,tgt,src_uri, map) ->
if status#ng_mode <> `CommandMode then
raise (GrafiteTypes.Command_error "Not in command mode")
in
let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
let status = status#set_obj (tgt_uri,0,[],[],ok) in
- prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));
+ (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
let status = status#set_ng_mode `ProofMode in