X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=022482b0a9e60c44e20398d586b74bd9ddaa9e2a;hb=d3a143f3edce2a255c449526e0ecf85435a6bad4;hp=771568018b0d44ca99c61580e27152d2f1befad1;hpb=63b86fce8a75490b957e7301517b9006f58321b6;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 771568018..022482b0a 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -25,12 +25,7 @@ let map_term_fold_a g k f a = function let fire_beta, upto = match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 in - let a,l1 = - (* sharing fold? *) - List.fold_right - (fun t (a,l) -> let a,t = f k a t in a, t :: l) - l (a,[]) - in + let a,l1 = HExtlib.sharing_map_acc (f k) a l in a, if l1 == l then orig else let t = match l1 with @@ -51,10 +46,7 @@ let map_term_fold_a g k f a = function a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1) | C.Match (r,oty,t,pl) as orig -> let a,oty1 = f k a oty in let a,t1 = f k a t in - let a,pl1 = - (* sharing fold? *) - List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[]) - in + let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in a, if oty1 == oty && t1 == t && pl1 == pl then orig else C.Match(r,oty1,t1,pl1) ;; @@ -183,21 +175,23 @@ let rec fire_projection_redex on_args = function in if pragma <> `Projection || List.length args <= rno then conclude () else - (match List.nth args rno with + (match List.nth l (rno+1) with | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) -> let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *) - let t = C.Appl (fbody::args) in + let t = C.Appl (fbody::List.tl l) in (match NCicReduction.head_beta_reduce ~delta:max_int t with - | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])-> + | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno))) + ::kargs),[pat])-> let _,kargs = HExtlib.split_nth leftno kargs in - fire_projection_redex false - (NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs))) - | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) -> + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs))) + | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno))) + ::kargs),[pat]) :: args) -> let _,kargs = HExtlib.split_nth leftno kargs in - fire_projection_redex false - (NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs @ args))) + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs @ args))) | _ -> conclude ()) | _ -> conclude ()) | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t @@ -252,3 +246,105 @@ let rec apply_subst_metasenv subst = function (* hide optional arg *) let apply_subst s c t = apply_subst s c t;; + +type meta_kind = [ `IsSort | `IsType | `IsTerm ] + +let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;; + +let kind_of_meta l = + try + (match List.find is_kind l with + | `IsSort | `IsType | `IsTerm as x -> x + | _ -> assert false) + with + Not_found -> assert false +;; + +let rec replace_in_metasenv i f = function + | [] -> assert false + | (j,e)::tl when j=i -> (i,f e) :: tl + | x::tl -> x :: replace_in_metasenv i f tl +;; + +let rec replace_in_subst i f = function + | [] -> assert false + | (j,e)::tl when j=i -> (i,f e) :: tl + | x::tl -> x :: replace_in_subst i f tl +;; + +let set_kind newkind attrs = + (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs +;; + +let max_kind k1 k2 = + match k1, k2 with + | `IsSort, _ | _, `IsSort -> `IsSort + | `IsType, _ | _, `IsType -> `IsType + | _ -> `IsTerm +;; + +module OT = + struct + type t = int * NCic.conjecture + let compare (i,_) (j,_) = Pervasives.compare i j + end + +module MS = HTopoSort.Make(OT) +let relations_of_menv subst m c = + let i, (_, ctx, ty) = c in + let m = List.filter (fun (j,_) -> j <> i) m in + let m_ty = metas_of_term subst ctx ty in + let m_ctx = + snd + (List.fold_right + (fun i (ctx,res) -> + (i::ctx), + (match i with + | _,NCic.Decl ty -> metas_of_term subst ctx ty + | _,NCic.Def (t,ty) -> + metas_of_term subst ctx ty @ metas_of_term subst ctx t) @ res) + ctx ([],[])) + in + let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in + List.filter (fun (i,_) -> List.exists ((=) i) metas) m +;; + +let sort_metasenv subst (m : NCic.metasenv) = + (MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv) +;; + +let count_occurrences ~subst n t = + let occurrences = ref 0 in + let rec aux k _ = function + | C.Rel m when m = n+k -> incr occurrences + | C.Rel _m -> () + | C.Implicit _ -> () + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () + | C.Meta (mno,(s,l)) -> + (try + (* possible optimization here: try does_not_occur on l and + perform substitution only if DoesOccur is raised *) + let _,_,term,_ = NCicUtils.lookup_subst mno subst in + aux (k-s) () (NCicSubstitution.subst_meta (0,l) term) + with NCicUtils.Subst_not_found _ -> () (*match l with + | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur + | C.Ctx lc -> List.iter (aux (k-s) ()) lc*)) + | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t + in + aux 0 () t; + !occurrences +;; + +exception Found_variable + +let looks_closed t = + let rec aux k _ = function + | C.Rel m when k < m -> raise Found_variable + | C.Rel _m -> () + | C.Implicit _ -> () + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () + | C.Meta _ -> raise Found_variable + | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t + in + try aux 0 () t; true with Found_variable -> false +;;