X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5d1b81d7442605411098412ab3f332ab332e3966;hb=b0325c1fa8f59f8aaff2b6df59f3852338e82523;hp=c75e1aa3fa2ebe3549290262fb764349bc6244f2;hpb=72cd94b68037956a70b98cfa54f316fd54e52bae;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c75e1aa3f..5d1b81d74 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -495,8 +495,166 @@ let eval_unification_hint status t n = 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 = - NCicCoercion.index_coercion status t s d a p + 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 = @@ -506,6 +664,44 @@ let inject_ncoercion = 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 = @@ -517,32 +713,8 @@ let eval_ncoercion status name t ty (id,src) tgt = assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in - let 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 - let metasenv,subst,status,src = - GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,src) in - let src = NCicUntrusted.apply_subst subst [] src in - let _ = NCicUnification.unify status metasenv subst ctx ty src in - src, cpos - | _ -> assert false - in - aux 0 [] ty - in - let tgt, arity = - let metasenv,subst,status,tgt = - GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,tgt) in - let tgt = NCicUntrusted.apply_subst subst [] tgt in - (* CHECK *) - let rec count_prod = function - | NCic.Prod (_,_,x) -> 1 + count_prod x - | _ -> 0 - in - tgt, count_prod tgt + 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 @@ -790,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")