in
if pragma <> `Projection || List.length args <= rno then conclude ()
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
+ let t = C.Appl (fbody::args) 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
;;
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 =
| _ -> `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
-;;