aux
;;
-(* "textual" replacement of a subterm with another one *)
+exception WhatAndWithWhatDoNotHaveTheSameLength;;
+
+(* "textual" replacement of several subterms with other ones *)
let replace ~equality ~what ~with_what ~where =
let module C = Cic in
- let rec aux =
- function
- t when (equality t what) -> with_what
- | C.Rel _ as t -> t
- | C.Var (uri,exp_named_subst) ->
- C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
- | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
- | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l ->
- (* Invariant enforced: no application of an application *)
- (match List.map aux l with
- (C.Appl l')::tl -> C.Appl (l'@tl)
- | l' -> C.Appl l')
- | C.Const (uri,exp_named_subst) ->
- C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
- | C.MutInd (uri,i,exp_named_subst) ->
- C.MutInd
- (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- C.MutConstruct
- (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
- | C.MutCase (sp,i,outt,t,pl) ->
- C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
- | C.Fix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, aux ty, aux bo))
- fl
- in
- C.CoFix (i, substitutedfl)
+ let find_image t =
+ let rec find_image_aux =
+ function
+ [],[] -> raise Not_found
+ | what::tl1,with_what::tl2 ->
+ if equality t what then with_what else find_image_aux (tl1,tl2)
+ | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+ in
+ find_image_aux (what,with_what)
in
- aux where
+ let rec aux t =
+ try
+ find_image t
+ with Not_found ->
+ match t with
+ C.Rel _ -> t
+ | C.Var (uri,exp_named_subst) ->
+ C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.Meta _ -> t
+ | C.Sort _ -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.Appl l ->
+ (* Invariant enforced: no application of an application *)
+ (match List.map aux l with
+ (C.Appl l')::tl -> C.Appl (l'@tl)
+ | l' -> C.Appl l')
+ | C.Const (uri,exp_named_subst) ->
+ C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutInd (uri,i,exp_named_subst) ->
+ C.MutInd
+ (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ C.MutConstruct
+ (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
+ | C.Fix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+ aux where
;;
(* replaces in a term a term with another one. *)
let simplified_term_to_fold =
reduceaux context [] delta_expanded_term_to_fold
in
- replace (=) simplified_term_to_fold term_to_fold res
+ replace (=) [simplified_term_to_fold] [term_to_fold] res
with
WrongShape ->
(* The constant does not unfold to a Fix lambda-abstracted *)
*)
(* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let term =
- match term with None -> ty | Some t -> t
+ let terms =
+ match terms with None -> [ty] | Some l -> l
in
(* We don't know if [term] is a subterm of [ty] or a subterm of *)
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
try
- let term' = reduction context term in
- ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+ let terms' = List.map (reduction context) terms in
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
~where:where
with
_ -> where
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
(*CSC: che si guadagni nulla in fatto di efficienza. *)
let replace =
- ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term
+ ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
in
let ty' = replace ty in
let metasenv' =
projects / helm.git / commitdiff