Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.
(* change in every iteration, i.e. to the actual arguments for the *)
(* lambda-abstractions that precede the Fix. *)
(*CSC: It does not perform simplification in a Case *)
(* change in every iteration, i.e. to the actual arguments for the *)
(* lambda-abstractions that precede the Fix. *)
(*CSC: It does not perform simplification in a Case *)
let simpl context =
(* reduceaux is equal to the reduceaux locally defined inside *)
(* reduce, but for the const case. *)
let simpl context =
(* reduceaux is equal to the reduceaux locally defined inside *)
(* reduce, but for the const case. *)
let module S = CicSubstitution in
function
C.Rel n as t ->
let module S = CicSubstitution in
function
C.Rel n as t ->
- (match List.nth context (n-1) with
- Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def (bo,_)) ->
- try_delta_expansion l t (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
- )
+ (try
+ match List.nth context (n-1) with
+ Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
+ | Some (_,C.Def (bo,_)) ->
+ try_delta_expansion context l t (S.lift n bo)
+ | None -> raise RelToHiddenHypothesis
+ with
+ Failure _ -> assert false)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.Constant (_,Some body,_,_,_) ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
C.Constant (_,Some body,_,_,_) ->
+ try_delta_expansion context l
(C.Const (uri,exp_named_subst'))
(CicSubstitution.subst_vars exp_named_subst' body)
| C.Constant (_,None,_,_,_) ->
(C.Const (uri,exp_named_subst'))
(CicSubstitution.subst_vars exp_named_subst' body)
| C.Constant (_,None,_,_,_) ->
and reduceaux_exp_named_subst context l =
List.map (function uri,t -> uri,reduceaux context [] t)
(**** Step 2 ****)
and reduceaux_exp_named_subst context l =
List.map (function uri,t -> uri,reduceaux context [] t)
(**** Step 2 ****)
- and try_delta_expansion l term body =
+ and try_delta_expansion context l term body =
let module C = Cic in
let module S = CicSubstitution in
try
let module C = Cic in
let module S = CicSubstitution in
try