X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5d1b81d7442605411098412ab3f332ab332e3966;hb=b0325c1fa8f59f8aaff2b6df59f3852338e82523;hp=b6a8786f22e2dc933ac1bdf2756cb286238ccf38;hpb=bd1e80fb01cfb419e256d5899ac5bf8818f11e64;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index b6a8786f2..5d1b81d74 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -475,7 +475,10 @@ let basic_eval_unification_hint (t,n) status = ;; let inject_unification_hint = - let basic_eval_unification_hint (t,n) ~refresh_uri_in_term = + let basic_eval_unification_hint (t,n) + ~refresh_uri_in_universe + ~refresh_uri_in_term + = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint @@ -488,6 +491,257 @@ let eval_unification_hint status t n = let t = NCicUntrusted.apply_subst subst [] t in let status = basic_eval_unification_hint (t,n) status in let dump = inject_unification_hint (t,n)::status#dump in + let status = status#set_dump dump in + status,`New [] +;; + +let product f l1 l2 = + List.fold_left + (fun acc x -> + List.fold_left + (fun acc y -> + f x y :: acc) + acc l2) + [] l1 +;; + +let pos_in_list x l = + match + HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l + with + | Some i -> i + | None -> assert false +;; + +let pos_of x t = + match t with + | NCic.Appl l -> pos_in_list x l + | _ -> assert false +;; + +let rec count_prod = function + | NCic.Prod (_,_,x) -> 1 + count_prod x + | _ -> 0 +;; + +let term_at i t = + match t with + | NCic.Appl l -> + (match + HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l + with + | Some i -> i + | None -> assert false) + | _ -> assert false +;; + +let src_tgt_of_ty_cpos_arity ty cpos arity = + let pis = count_prod ty in + let tpos = pis - arity in + let rec aux i j = function + | NCic.Prod (_,s,_) when i = j -> s + | NCic.Prod (_,_,t) -> aux (i+1) j t + | t -> assert (i = j); t + in + let mask t = + let rec aux () = function + | NCic.Meta _ + | NCic.Implicit _ as x -> x + | NCic.Rel _ -> NCic.Implicit `Type + | t -> NCicUtils.map (fun _ () -> ()) () aux t + in + aux () t + in + mask (aux 0 cpos ty), mask (aux 0 tpos ty) +;; + +let close_in_context t metasenv = + let rec aux m_subst subst ctx = function + | (i,(tag,[],ty)) :: tl -> + let name = "x" ^ string_of_int (List.length ctx) in + let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in + let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in + let m_subst m = + (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) + | [] -> + (* 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 + aux (fun _ -> []) [] [] metasenv +;; + +let toposort metasenv = + let module T = HTopoSort.Make( + struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end) + in + let deps (_,(_,_,t)) = + List.filter (fun (j,_) -> + List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv + in + T.topological_sort metasenv deps +;; + +let basic_eval_ncoercion (name,t,s,d,p,a) status = + let to_s = + NCicCoercion.look_for_coercion status [] [] [] (NCic.Implicit `Type) s + in + let from_d = + NCicCoercion.look_for_coercion status [] [] [] d (NCic.Implicit `Type) + in + let status = NCicCoercion.index_coercion status t s d a p in + let c = + List.find + (function (_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) + (NCicCoercion.look_for_coercion status [] [] [] s d) + in + let composites = + let to_s_o_c = + product (fun (m1,t1,_,j) (mc,c,_,i) -> m1@mc,c,[i,t1],j,a) + to_s [c] + in + let c_o_from_d = + product (fun (mc,c,_,j) (m1,t1,ty,i) -> m1@mc,t1,[i,c],j,count_prod ty) + [c] from_d + in + let to_s_o_c_o_from_d = + product (fun (m1,t1,_,j) (m,t,upl,i,a)-> + m@m1,t,(i,t1)::upl,j,a) + to_s c_o_from_d + in + to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d + in + let composites = + HExtlib.filter_map + (fun (metasenv, bo, upl, p, arity) -> + try + let metasenv, subst = + List.fold_left + (fun (metasenv,subst) (a,b) -> + NCicUnification.unify status metasenv subst [] a b) + (metasenv,[]) upl + in + let bo = NCicUntrusted.apply_subst subst [] bo in + let metasenv = toposort metasenv in + let bo = close_in_context bo metasenv in + let pos = + match p with + | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) + | _ -> assert false + 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 _ + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ -> None + ) composites + in + List.fold_left + (fun st (t,s,d,a,p) -> NCicCoercion.index_coercion st t s d a p) + status composites +;; + +let inject_ncoercion = + let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term = + basic_eval_ncoercion x + in + NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion +;; + +let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = + let status, src, cpos = + let rec aux cpos ctx = function + | NCic.Prod (name,ty,bo) -> + if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo + else + (try + let metasenv,subst,status,src = + GrafiteDisambiguate.disambiguate_nterm + None status ctx [] [] ("",0,src) in + let src = NCicUntrusted.apply_subst subst [] src in + (* CHECK that the declared pattern matches the abstraction *) + let _ = NCicUnification.unify status metasenv subst ctx ty src in + status, src, cpos + with + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ + | MultiPassDisambiguator.DisambiguationError _ -> + raise (GrafiteTypes.Command_error "bad source pattern")) + | _ -> assert false + in + aux 0 [] ty + in + let status, tgt, arity = + let metasenv,subst,status,tgt = + GrafiteDisambiguate.disambiguate_nterm + None status [] [] [] ("",0,tgt) in + let tgt = NCicUntrusted.apply_subst subst [] tgt in + (* CHECK che sia unificabile mancante *) + let rec count_prod = function + | NCic.Prod (_,_,x) -> 1 + count_prod x + | _ -> 0 + in + status, tgt, count_prod tgt + in + status, src, tgt, cpos, arity +;; + +let eval_ncoercion status name t ty (id,src) tgt = + + let metasenv,subst,status,ty = + GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in + assert (metasenv=[]); + let ty = NCicUntrusted.apply_subst subst [] ty in + let metasenv,subst,status,t = + GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in + assert (metasenv=[]); + let t = NCicUntrusted.apply_subst subst [] t in + + let status, src, tgt, cpos, arity = + src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt + in + + let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in + let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in + let status = status#set_dump dump in + status,`New [] +;; + +let basic_eval_add_constraint (s,u1,u2) status = + NCicLibrary.add_constraint status s u1 u2 +;; + +let inject_constraint = + let basic_eval_add_constraint (s,u1,u2) + ~refresh_uri_in_universe + ~refresh_uri_in_term + = + let u1 = refresh_uri_in_universe u1 in + let u2 = refresh_uri_in_universe u2 in + basic_eval_add_constraint (s,u1,u2) + in + NRstatus.Serializer.register "constraints" basic_eval_add_constraint +;; + +let eval_add_constraint status s u1 u2 = + let status = basic_eval_add_constraint (s,u1,u2) status in + let dump = inject_constraint (s,u1,u2)::status#dump in let status = status#set_dump dump in status,`Old [] ;; @@ -599,7 +853,8 @@ let eval_ng_punct (_text, _prefix_len, punct) = | GrafiteAst.Merge _ -> NTactics.merge_tac ;; -let rec eval_ng_tac (text, prefix_len, tac) = +let eval_ng_tac tac = + let rec aux f (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) | GrafiteAst.NAssert (_loc, seqs) -> @@ -651,8 +906,14 @@ let rec eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac | GrafiteAst.NTry (_,tac) -> NTactics.try_tac - (eval_ng_tac (text, prefix_len, tac)) + (aux f (text, prefix_len, tac)) | GrafiteAst.NAssumption _ -> NTactics.assumption_tac + | GrafiteAst.NBlock (_,l) -> + NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) + |GrafiteAst.NRepeat (_,tac) -> + NTactics.repeat_tac (f f (text, prefix_len, tac)) + in + aux aux tac (* trick for non uniform recursion call *) ;; let subst_metasenv_and_fix_names status = @@ -667,6 +928,8 @@ let subst_metasenv_and_fix_names status = let rec eval_ncommand opts status (text,prefix_len,cmd) = match cmd with | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n + | GrafiteAst.NCoercion (loc, name, t, ty, source, target) -> + eval_ncoercion status name t ty source target | GrafiteAst.NQed loc -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") @@ -679,7 +942,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let obj_kind = NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst []) obj_kind in - let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in + let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in (* fix the height inside the object *) let rec fix () = function | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> @@ -699,16 +962,94 @@ 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 - let objs = NCicElim.mk_elims obj 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 - status#set_ng_mode `CommandMode,`New uris + 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 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") + else + let tgt_uri_ext, old_ok = + match NCicEnvironment.get_checked_obj src_uri with + | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok + | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok + | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok + | _ -> assert false + in + let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in + let map = (src_uri, tgt_uri) :: map in + let ok = + let rec subst () = function + | NCic.Meta _ -> assert false + | NCic.Const (NReference.Ref (u,spec)) as t -> + (try NCic.Const + (NReference.reference_of_spec (List.assoc u map)spec) + with Not_found -> t) + | t -> NCicUtils.map (fun _ _ -> ()) () subst t + in + NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok + 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));*) + 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 + eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | GrafiteAst.NObj (loc,obj) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -727,8 +1068,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status,`New []) | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> - NCicEnvironment.add_constraint strict [false,u1] [false,u2]; - status, `New [u1;u2] + eval_add_constraint status strict [false,u1] [false,u2] ;; let rec eval_command = {ec_go = fun ~disambiguate_command opts status @@ -795,24 +1135,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,`Old [] | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Include (loc, _, baseuri) -> - let moopath_rw, moopath_r = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false - in - let moopath = - if Sys.file_exists moopath_r then moopath_r else - if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled (moopath_rw,baseuri)) - in - let status = eval_from_moo.efm_go status moopath in + | GrafiteAst.Include (loc, mode, new_or_old, baseuri) -> + (* Old Include command is not recursive; new one is *) let status = - NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status + if new_or_old = `OldAndNew then + let moopath_rw, moopath_r = + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true, + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:false in + let moopath = + if Sys.file_exists moopath_r then moopath_r else + if Sys.file_exists moopath_rw then moopath_rw else + raise (IncludedFileNotCompiled (moopath_rw,baseuri)) + in + eval_from_moo.efm_go status moopath + else + status in - status,`Old [] + let status = + NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = + GrafiteTypes.add_moo_content + [GrafiteAst.Include (loc,mode,`New,baseuri)] status + in + status,`Old [] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in prerr_endline (Auto.pp_proofterm (Lazy.force p));