From 8ced93b24ec20302294b3f627a6d06fc36bcc41a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jul 2009 14:06:20 +0000 Subject: [PATCH] Generation of principles is now atomic. --- .../grafite_engine/grafiteEngine.ml | 56 +++++++++++-------- 1 file changed, 32 insertions(+), 24 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ceaa75962..b5f503497 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -637,12 +637,14 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = 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 _ @@ -960,31 +962,37 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = | _ -> 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 + (try + (*prerr_endline (NCicPp.ppobj obj);*) + let boxml = NCicElim.mk_elims 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 + 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 + 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") @@ -1011,7 +1019,7 @@ let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in 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 -- 2.39.2