-and get_relevance ~subst context te args =
- match te with
- | C.Const r when List.length (E.get_relevance r) >= List.length args ->
- let relevance = E.get_relevance r in
- (match r with
- | Ref.Ref (_,Ref.Con (_,_,lno)) ->
- let _,relevance = HExtlib.split_nth lno relevance in
- HExtlib.mk_list false lno @ relevance
- | _ -> relevance)
- | t ->
- let ty = typeof ~subst ~metasenv:[] context t in
- let rec aux context ty = function
- | [] -> []
- | arg::tl -> match R.whd ~subst context ty with
- | C.Prod (name,so,de) ->
- let sort = typeof ~subst ~metasenv:[] context so in
- let new_ty = S.subst ~avoid_beta_redexes:true arg de in
- (match R.whd ~subst context sort with
- | C.Sort C.Prop ->
- false::(aux ((name,(C.Decl so))::context) new_ty tl)
- | C.Sort _
- | C.Meta _ -> true::(aux ((name,(C.Decl so))::context) de tl)
- | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
- "Prod: the type %s of the source of %s is not a sort"
- (PP.ppterm ~subst ~metasenv:[] ~context sort)
- (PP.ppterm ~subst ~metasenv:[] ~context so)))))
- | _ ->
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- "Appl: %s is not a function, it cannot be applied"
- (PP.ppterm ~subst ~metasenv:[] ~context
- (let res = List.length tl in
- let eaten = List.length args - res in
- (C.Appl
- (t::fst
- (HExtlib.split_nth eaten args))))))))
- in aux context ty args
+and get_relevance ~subst context t args =
+ let ty = typeof ~subst ~metasenv:[] context t in
+ let rec aux context ty = function
+ | [] -> []
+ | arg::tl -> match R.whd ~subst context ty with
+ | C.Prod (name,so,de) ->
+ let sort = typeof ~subst ~metasenv:[] context so in
+ let new_ty = S.subst ~avoid_beta_redexes:true arg de in
+ (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[]
+ ~context so);
+ prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[]
+ ~context sort);*)
+ (match R.whd ~subst context sort with
+ | C.Sort C.Prop ->
+ false::(aux context new_ty tl)
+ | C.Sort _
+ | C.Meta _ -> true::(aux context new_ty tl)
+ | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
+ "Prod: the type %s of the source of %s is not a sort"
+ (PP.ppterm ~subst ~metasenv:[] ~context sort)
+ (PP.ppterm ~subst ~metasenv:[] ~context so)))))
+ | _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ "Appl: %s is not a function, it cannot be applied"
+ (PP.ppterm ~subst ~metasenv:[] ~context
+ (let res = List.length tl in
+ let eaten = List.length args - res in
+ (C.Appl
+ (t::fst
+ (HExtlib.split_nth eaten args))))))))
+ in aux context ty args