exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception WrongUriToInductiveDefinition;;
+exception WrongUriToConstant;;
exception RelToHiddenHypothesis;;
let alpha_equivalence =
(*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. *)
+ (* reduce, but for the const case. *)
(**** Step 1 ****)
let rec reduceaux context l =
let module C = Cic in
aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
in
(**** Step 3 ****)
- let term_to_fold =
- match constant_args with
- [] -> C.Const (uri,exp_named_subst')
- | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
+ let term_to_fold, delta_expanded_term_to_fold =
+ let body' = CicSubstitution.subst_vars exp_named_subst' body in
+ match constant_args with
+ [] -> C.Const (uri,exp_named_subst'), body'
+ | _ ->
+ C.Appl ((C.Const (uri,exp_named_subst'))::constant_args),
+ C.Appl (body'::constant_args)
in
- let reduced_term_to_fold = reduce context term_to_fold in
- replace (=) reduced_term_to_fold term_to_fold res
+ let simplified_term_to_fold =
+ reduceaux context [] delta_expanded_term_to_fold
+ in
+ replace (=) simplified_term_to_fold term_to_fold res
with
WrongShape ->
(* The constant does not unfold to a Fix lambda-abstracted *)