module C = NCic
module Ref = NReference
-let map_term_fold_a g k f a = function
+let map_term_fold_a status g k f a = function
| C.Meta _ -> assert false
| C.Implicit _
| C.Sort _
| C.Appl l :: tl -> C.Appl (l@tl)
| _ -> C.Appl l1
in
- if fire_beta then NCicReduction.head_beta_reduce ~upto t
+ if fire_beta then NCicReduction.head_beta_reduce status ~upto t
else t
| C.Prod (n,s,t) as orig ->
let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
else C.Match(r,oty1,t1,pl1)
;;
-let metas_of_term subst context term =
+let metas_of_term status subst context term =
let rec aux ctx acc = function
| NCic.Rel i ->
(match HExtlib.list_skip (i-1) ctx with
| NCic.Meta(i,l) ->
(try
let _,_,bo,_ = NCicUtils.lookup_subst i subst in
- let bo = NCicSubstitution.subst_meta l bo in
+ let bo = NCicSubstitution.subst_meta status l bo in
aux ctx acc bo
with NCicUtils.Subst_not_found _ ->
let shift, lc = l in
let lc = NCicUtils.expand_local_context lc in
- let l = List.map (NCicSubstitution.lift shift) lc in
+ let l = List.map (NCicSubstitution.lift status shift) lc in
List.fold_left (aux ctx) (i::acc) l)
| t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
in
- HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
+ HExtlib.list_uniq (List.sort Stdlib.compare (aux context [] term))
;;
module NCicHash =
exception Occurr;;
-let clean_or_fix_dependent_abstrations ctx t =
+let clean_or_fix_dependent_abstrations status ctx t =
let occurrs_1 t =
let rec aux n _ = function
| NCic.Meta _ -> ()
| NCic.Lambda (name,s,t) when List.mem name ctx ->
let name = fresh ctx name in
NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
- | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t
+ | t -> NCicUtils.map status (fun (e,_) ctx -> e::ctx) ctx aux t
in
aux (List.map fst ctx) t
;;
-let rec fire_projection_redex on_args = function
+let rec fire_projection_redex status () = function
| C.Meta _ as t -> t
- | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
- let l= if on_args then List.map (fire_projection_redex true) ol else ol in
- let t = if l == ol then ot else C.Appl l in
- let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
- let conclude () =
- if on_args then
- let l' = HExtlib.sharing_map (fire_projection_redex true) l in
- if l == l' then t else C.Appl l'
- else
- t (* ot is the same *)
- in
- if pragma <> `Projection || List.length args <= rno then conclude ()
+ | C.Appl((C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r) as hd)::args) as ot->
+ let args'= HExtlib.sharing_map (fire_projection_redex status ()) args in
+ let t = if args == args' then ot else C.Appl (hd::args') in
+ let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
+ if pragma <> `Projection || List.length args <= rno then t
else
- (match List.nth l (rno+1) with
+ (match List.nth args' rno with
| C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
- let t = C.Appl (fbody::List.tl l) in
- (match NCicReduction.head_beta_reduce ~delta:max_int t with
+ let t = C.Appl (fbody::args') in
+ (match NCicReduction.head_beta_reduce status ~delta:max_int t with
| 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)))
+ NCicReduction.head_beta_reduce status
+ ~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
+ fire_projection_redex status ()
+ (NCicReduction.head_beta_reduce status
~delta:max_int (C.Appl (pat :: kargs @ args)))
- | _ -> conclude ())
- | _ -> conclude ())
- | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
- | t -> t
+ | _ -> assert false)
+ | _ -> t)
+ | t ->
+ NCicUtils.map status (fun _ x -> x) () (fire_projection_redex status) t
;;
-let apply_subst ?(fix_projections=false) subst context t =
+let apply_subst status ?(fix_projections=false) subst context t =
let rec apply_subst subst () =
function
NCic.Meta (i,lc) ->
(try
let _,_,t,_ = NCicUtils.lookup_subst i subst in
- let t = NCicSubstitution.subst_meta lc t in
+ let t = NCicSubstitution.subst_meta status lc t in
apply_subst subst () t
with
NCicUtils.Subst_not_found j when j = i ->
NCic.Meta
(i,(0,NCic.Ctx
(List.map (fun t ->
- apply_subst subst () (NCicSubstitution.lift n t)) l))))
- | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
+ apply_subst subst () (NCicSubstitution.lift status n t)) l))))
+ | t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
in
- (if fix_projections then fire_projection_redex true else fun x -> x)
- (clean_or_fix_dependent_abstrations context (apply_subst subst () t))
+ let t = apply_subst subst () t in
+ let t = clean_or_fix_dependent_abstrations status context t in
+ if fix_projections then
+ fire_projection_redex status () t
+ else
+ t
;;
-let apply_subst_context ~fix_projections subst context =
- let apply_subst = apply_subst ~fix_projections in
+let apply_subst_context status ~fix_projections subst context =
+ let apply_subst = apply_subst status ~fix_projections in
let rec aux c = function
| [] -> []
| (name,NCic.Decl t as e) :: tl ->
List.rev (aux [] (List.rev context))
;;
-let rec apply_subst_metasenv subst = function
+let rec apply_subst_metasenv status subst = function
| [] -> []
| (i,_) :: _ when List.mem_assoc i subst -> assert false
| (i,(name,ctx,ty)) :: tl ->
- (i,(name,apply_subst_context ~fix_projections:true subst ctx,
- apply_subst ~fix_projections:true subst ctx ty)) ::
- apply_subst_metasenv subst tl
+ (i,(name,apply_subst_context status ~fix_projections:true subst ctx,
+ apply_subst status ~fix_projections:true subst ctx ty)) ::
+ apply_subst_metasenv status subst tl
;;
(* hide optional arg *)
-let apply_subst s c t = apply_subst s c t;;
+let apply_subst status s c t = apply_subst status s c t;;
type meta_kind = [ `IsSort | `IsType | `IsTerm ]
;;
let set_kind newkind attrs =
- newkind :: List.filter (fun x -> not (is_kind x)) attrs
+ (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs
;;
let max_kind k1 k2 =
module OT =
struct
type t = int * NCic.conjecture
- let compare (i,_) (j,_) = Pervasives.compare i j
+ let compare (i,_) (j,_) = Stdlib.compare i j
end
module MS = HTopoSort.Make(OT)
-let relations_of_menv subst m c =
+let relations_of_menv status 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_ty = metas_of_term status 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.Decl ty -> metas_of_term status subst ctx ty
| _,NCic.Def (t,ty) ->
- metas_of_term subst ctx ty @ metas_of_term subst ctx t) @ res)
+ metas_of_term status subst ctx ty @ metas_of_term status 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 sort_metasenv status subst (m : NCic.metasenv) =
+ (MS.topological_sort m (relations_of_menv status subst m) : NCic.metasenv)
;;
-let count_occurrences ~subst n t =
+let count_occurrences status ~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.Rel _m -> ()
| C.Implicit _ -> ()
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
| C.Meta (mno,(s,l)) ->
(* 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)
+ aux (k-s) () (NCicSubstitution.subst_meta status (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*))
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
+;;
projects / helm.git / blobdiff