(*CSC: It does not perform simplification in a Case *)
let simpl context =
+ let mk_appl t l =
+ if l = [] then
+ t
+ else
+ match t with
+ | Cic.Appl l' -> Cic.Appl (l'@l)
+ | _ -> Cic.Appl (t::l)
+ in
(* reduceaux is equal to the reduceaux locally defined inside *)
(* reduce, but for the const case. *)
(**** Step 1 ****)
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
| Some (_,C.Def (bo,_)) ->
let lifted_bo = S.lift n bo in
- let applied_lifted_bo =
- if l = [] then lifted_bo else C.Appl (lifted_bo::l) in
+ let applied_lifted_bo = mk_appl lifted_bo l in
let simplified = try_delta_expansion context l t lifted_bo in
if simplified = applied_lifted_bo then
if l = [] then t else C.Appl (t::l)
;;
let unfold ?what context where =
- let first_is_the_expandable_head_of_second t1 t2 =
+ let contextlen = List.length context in
+ let first_is_the_expandable_head_of_second context' t1 t2 =
match t1,t2 with
Cic.Const (uri,_), Cic.Const (uri',_)
| Cic.Var (uri,_), Cic.Var (uri',_)
| Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
| Cic.Const _, _
| Cic.Var _, _ -> false
+ | Cic.Rel n, Cic.Rel m
+ | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
+ n + (List.length context' - contextlen) = m
+ | Cic.Rel _, _ -> false
| _,_ ->
raise
(ProofEngineTypes.Fail
- "The term to unfold is neither a constant nor a variable")
+ "The term to unfold is not a constant, a variable or a bound variable ")
in
let appl he tl =
if tl = [] then he else Cic.Appl (he::tl) in