- | (k, e, (C.Meta _ as t), s) -> if s = [] then t
- else C.Appl (t::s)
- | (k, e, (C.Sort _ as t), s) -> t (* s should be empty *)
- | (k, e, (C.Implicit as t), s) -> t (* s should be empty *)
- | (k, e, (C.Cast (te,ty) as t), s) -> reduce (k, e,te,s) (* s should be empty *)
- | (k, e, (C.Prod _ as t), s) -> unwind k e t (* s should be empty *)
- | (k, e, (C.Lambda (_,_,t) as t'), []) -> unwind k e t'
- | (k, e, C.Lambda (_,_,t), p::s) ->
-(* prerr_string ("Lambda body: " ^ CicPp.ppterm t) ; flush stderr ; *)
- reduce (k+1, p::e,t,s)
- | (k, e, (C.LetIn (_,m,t) as t'), s) -> let m' = reduce (k,e,m,[]) in
- reduce (k+1, m'::e,t,s)
- | (k, e, C.Appl [], s) -> raise (Impossible 1)
- (* this is lazy
- | (k, e, C.Appl (he::tl), s) -> let tl' = List.map (unwind k e) tl
- in reduce (k, e, he, (List.append tl' s)) *)
- (* this is strict *)
- | (k, e, C.Appl (he::tl), s) ->
- (* constants are NOT unfolded *)
- let red = function
- C.Const _ as t -> t
- | t -> reduce (k, e,t,[]) in
- let tl' = List.map red tl in
- reduce (k, e, he , List.append tl' s)
-(*
- | (k, e, C.Appl ((C.Lambda _ as he)::tl), s)
- | (k, e, C.Appl ((C.Const _ as he)::tl), s)
- | (k, e, C.Appl ((C.MutCase _ as he)::tl), s)
- | (k, e, C.Appl ((C.Fix _ as he)::tl), s) ->
-(* strict evaluation, but constants are NOT
- unfolded *)
- let red = function
- C.Const _ as t -> t
- | t -> reduce (k, e,t,[]) in
- let tl' = List.map red tl in
- reduce (k, e, he , List.append tl' s)
- | (k, e, C.Appl l, s) -> C.Appl (List.append (List.map (unwind k e) l) s) *)
- | (k, e, (C.Const (uri,cookingsno) as t), s) ->
- (match CicEnvironment.get_cooked_obj uri cookingsno with
- C.Definition (_,body,_,_) -> reduce (0, [], body, s)
- (* constants are closed *)
- | C.Axiom _ -> if s = [] then t else C.Appl (t::s)
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s)
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- | (k, e, (C.Abst _ as t), s) -> t (* s should be empty ????? *)
- | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in
- if s = [] then t' else C.Appl (t'::s)
- | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) ->
- let t' = unwind k e t in
- if s = [] then t' else C.Appl (t'::s)
- | (k, e, (C.MutCase (mutind,cookingsno,i,_,term,pl) as t),s) ->
+ | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
+ if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
+ reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
+ else
+ (match CicEnvironment.get_obj uri with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_,_) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else
+ C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | C.Variable (_,Some body,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ reduce (0, [], ens', body, s)
+ )
+ | (k, e, ens, (C.Meta _ as t), s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
+ | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
+ | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+ reduce (k, e, ens, te, s) (* s should be empty *)
+ | (k, e, ens, (C.Prod _ as t), s) ->
+ unwind k e ens t (* s should be empty *)
+ | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
+ | (k, e, ens, C.Lambda (_,_,t), p::s) ->
+ reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
+ | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+ let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
+ reduce (k+1, m'::e, ens, t, s)
+ | (_, _, _, C.Appl [], _) -> assert false
+ | (k, e, ens, C.Appl (he::tl), s) ->
+ let tl' =
+ List.map
+ (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
+ in
+ reduce (k, e, ens, he, (List.append tl') s)
+ (* CSC: Old Dead Code
+ | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
+ | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
+ (* strict evaluation, but constants are NOT unfolded *)
+ let red =
+ function
+ C.Const _ as t -> unwind k e ens t
+ | t -> reduce (k,e,ens,t,[])
+ in
+ let tl' = List.map red tl in
+ reduce (k, e, ens, he , List.append tl' s)
+ | (k, e, ens, C.Appl l, s) ->
+ C.Appl (List.append (List.map (unwind k e ens) l) s)
+ *)
+ | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ (* constants are closed *)
+ reduce (0, [], ens', body, s)
+ | C.Constant (_,None,_,_) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,body,_,_) ->
+ let ens' = push_exp_named_subst k e ens exp_named_subst in
+ (* constants are closed *)
+ reduce (0, [], ens', body, s)
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | (k, e, ens, (C.MutInd _ as t),s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, ens, (C.MutConstruct _ as t),s) ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->