exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception WrongUriToInductiveDefinition;;
+exception WrongUriToConstant;;
exception RelToHiddenHypothesis;;
let alpha_equivalence =
in
if l = [] then t' else C.Appl (t'::l)
and reduceaux_exp_named_subst context l =
- List.map (function uri,t -> uri,reduceaux context l t)
+ List.map (function uri,t -> uri,reduceaux context [] t)
in
reduceaux context []
;;
(*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
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 body' = CicSubstitution.subst_vars exp_named_subst' body in
+ match constant_args with
+ [] -> body'
+ | _ -> 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 [] 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 *)
if l = [] then t' else C.Appl (t'::l)
end
| C.Constant (_,None,_,_) ->
- let exp_named_subst' =
- reduceaux_exp_named_subst context l exp_named_subst
- in
- let t' = C.Const (uri,exp_named_subst') in
- if l = [] then t' else C.Appl (t'::l)
+ let t' = C.Const (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
in
if l = [] then t' else C.Appl (t'::l)
and reduceaux_exp_named_subst context l =
- List.map (function uri,t -> uri,reduceaux context l t)
+ List.map (function uri,t -> uri,reduceaux context [] t)
in
reduceaux context []
;;