--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 12/04/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+
+(* The code of this module is derived from the code of CicReduction *)
+
+exception Impossible of int;;
+exception ReferenceToDefinition;;
+exception ReferenceToAxiom;;
+exception ReferenceToVariable;;
+exception ReferenceToCurrentProof;;
+exception ReferenceToInductiveDefinition;;
+exception WrongUriToInductiveDefinition;;
+
+(* "textual" replacement of a subterm with another one *)
+let replace ~what ~with_what ~where =
+ let module C = Cic in
+ let rec aux =
+ function
+ t when t = what -> with_what
+ | C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | 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 -> C.Appl (List.map aux l)
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,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
+;;
+
+(* Takes a well-typed term and fully reduces it. *)
+(*CSC: It does not perform reduction in a Case *)
+let reduce =
+ let rec reduceaux l =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Var uri as t ->
+ (match CicEnvironment.get_cooked_obj uri 0 with
+ C.Definition _ -> raise ReferenceToDefinition
+ | C.Axiom _ -> raise ReferenceToAxiom
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
+ | C.Variable (_,Some body,_) -> reduceaux l body
+ )
+ | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Sort _ as t -> t (* l should be empty *)
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
+ | C.Prod (name,s,t) ->
+ assert (l = []) ;
+ C.Prod (name, reduceaux [] s, reduceaux [] t)
+ | C.Lambda (name,s,t) ->
+ (match l with
+ [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
+ | he::tl -> reduceaux tl (S.subst he t)
+ (* when name is Anonimous the substitution should be superfluous *)
+ )
+ | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (reduceaux []) tl in
+ reduceaux (tl'@l) he
+ | C.Appl [] -> raise (Impossible 1)
+ | C.Const (uri,cookingsno) as t ->
+ (match CicEnvironment.get_cooked_obj uri cookingsno with
+ C.Definition (_,body,_,_) -> reduceaux l body
+ | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,body,_) -> reduceaux l body
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | C.Abst _ as t -> t (*CSC l should be empty ????? *)
+ | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
+ | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
+ | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
+ let decofix =
+ function
+ C.CoFix (i,fl) as t ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ reduceaux [] body'
+ | C.Appl (C.CoFix (i,fl) :: tl) ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ let tl' = List.map (reduceaux []) tl in
+ reduceaux tl body'
+ | t -> t
+ in
+ (match decofix (reduceaux [] term) with
+ C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+ | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
+ let (arity, r, num_ingredients) =
+ match CicEnvironment.get_obj mutind with
+ C.InductiveDefinition (tl,ingredients,r) ->
+ let (_,_,arity,_) = List.nth tl i
+ and num_ingredients =
+ List.fold_right
+ (fun (k,l) i ->
+ if k < cookingsno then i + List.length l else i
+ ) ingredients 0
+ in
+ (arity,r,num_ingredients)
+ | _ -> raise WrongUriToInductiveDefinition
+ in
+ let ts =
+ let num_to_eat = r + num_ingredients in
+ let rec eat_first =
+ function
+ (0,l) -> l
+ | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+ | _ -> raise (Impossible 5)
+ in
+ eat_first (num_to_eat,tl)
+ in
+ reduceaux (ts@l) (List.nth pl (j-1))
+ | C.Abst _ | C.Cast _ | C.Implicit ->
+ raise (Impossible 2) (* we don't trust our whd ;-) *)
+ | _ ->
+ let outtype' = reduceaux [] outtype in
+ let term' = reduceaux [] term in
+ let pl' = List.map (reduceaux []) pl in
+ let res =
+ C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ in
+ if l = [] then res else C.Appl (res::l)
+ )
+ | C.Fix (i,fl) ->
+ let t' () =
+ let fl' =
+ List.map
+ (function (n,recindex,ty,bo) ->
+ (n,recindex,reduceaux [] ty, reduceaux [] bo)
+ ) fl
+ in
+ C.Fix (i, fl')
+ in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (List.nth l recindex)
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduceaux [] recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ (* Possible optimization: substituting whd recparam in l *)
+ reduceaux l body'
+ | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | C.CoFix (i,fl) ->
+ let t' =
+ let fl' =
+ List.map
+ (function (n,ty,bo) ->
+ (n,reduceaux [] ty, reduceaux [] bo)
+ ) fl
+ in
+ C.CoFix (i, fl')
+ in
+ if l = [] then t' else C.Appl (t'::l)
+ in
+function t -> let res =
+prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
+ reduceaux []
+t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
+;;
+
+exception WrongShape;;
+exception AlreadySimplified;;
+exception WhatShouldIDo;;
+
+(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
+(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
+(*CSC: Fix foo *)
+(*CSC: {foo [n,m:nat]:nat := *)
+(*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
+(*CSC: } *)
+(* Takes a well-typed term and *)
+(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
+(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
+(* w.r.t. zero or more variables and if the Fix can be reduced, than it *)
+(* is reduced, the delta-reduction is succesfull and the whole algorithm *)
+(* is applied again to the new redex; Step 3) is applied to the result *)
+(* of the recursive simplification. Otherwise, if the Fix can not be *)
+(* reduced, than the delta-reductions fails and the delta-redex is *)
+(* not reduced. Otherwise, if the delta-residual is not the *)
+(* lambda-abstraction of a Fix, then it is reduced and the result is *)
+(* directly returned, without performing step 3). *)
+(* 3) Folds the application of the constant to the arguments that did not *)
+(* 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 =
+ (* reduceaux is equal to the reduceaux locally defined inside *)
+ (*reduce, but for the const case. *)
+ (**** Step 1 ****)
+ let rec reduceaux l =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Var uri as t ->
+ (match CicEnvironment.get_cooked_obj uri 0 with
+ C.Definition _ -> raise ReferenceToDefinition
+ | C.Axiom _ -> raise ReferenceToAxiom
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
+ | C.Variable (_,Some body,_) -> reduceaux l body
+ )
+ | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Sort _ as t -> t (* l should be empty *)
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> reduceaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *)
+ | C.Prod (name,s,t) ->
+ assert (l = []) ;
+ C.Prod (name, reduceaux [] s, reduceaux [] t)
+ | C.Lambda (name,s,t) ->
+ (match l with
+ [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
+ | he::tl -> reduceaux tl (S.subst he t)
+ (* when name is Anonimous the substitution should be superfluous *)
+ )
+ | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+ | C.Appl (he::tl) ->
+ let tl' = List.map (reduceaux []) tl in
+ reduceaux (tl'@l) he
+ | C.Appl [] -> raise (Impossible 1)
+ | C.Const (uri,cookingsno) as t ->
+ (match CicEnvironment.get_cooked_obj uri cookingsno with
+ C.Definition (_,body,_,_) ->
+ begin
+ try
+ (**** Step 2 ****)
+ let res,constant_args =
+ let rec aux rev_constant_args l =
+ function
+ C.Lambda (name,s,t) as t' ->
+ begin
+ match l with
+ [] -> raise WrongShape
+ | he::tl ->
+ (* when name is Anonimous the substitution should be *)
+ (* superfluous *)
+ aux (he::rev_constant_args) tl (S.subst he t)
+ end
+ | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
+ | C.Fix (i,fl) as t ->
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ List.nth l recindex
+ with
+ _ -> raise AlreadySimplified
+ in
+ (match CicReduction.whd recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (function _ ->
+ decr counter ; S.subst (C.Fix (!counter,fl))
+ ) fl body
+ in
+ (* Possible optimization: substituting whd *)
+ (* recparam in l *)
+ reduceaux l body', List.rev rev_constant_args
+ | _ -> raise AlreadySimplified
+ )
+ | _ -> raise WrongShape
+ in
+ aux [] l body
+ in
+ (**** Step 3 ****)
+ let term_to_fold =
+ match constant_args with
+ [] -> C.Const (uri,cookingsno)
+ | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
+ in
+ let reduced_term_to_fold = reduce term_to_fold in
+prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
+prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
+ replace reduced_term_to_fold term_to_fold res
+ with
+ WrongShape ->
+ (* The constant does not unfold to a Fix lambda-abstracted *)
+ (* w.r.t. zero or more variables. We just perform reduction. *)
+ reduceaux l body
+ | AlreadySimplified ->
+ (* If we performed delta-reduction, we would find a Fix *)
+ (* not applied to a constructor. So, we refuse to perform *)
+ (* delta-reduction. *)
+ if l = [] then
+ t
+ else
+ C.Appl (t::l)
+ end
+ | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,body,_) -> reduceaux l body
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | C.Abst _ as t -> t (*CSC l should be empty ????? *)
+ | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
+ | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
+ | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
+ let decofix =
+ function
+ C.CoFix (i,fl) as t ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ reduceaux [] body'
+ | C.Appl (C.CoFix (i,fl) :: tl) ->
+ let (_,_,body) = List.nth fl i in
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+ fl
+ body
+ in
+ let tl' = List.map (reduceaux []) tl in
+ reduceaux tl body'
+ | t -> t
+ in
+ (match decofix (reduceaux [] term) with
+ C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+ | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
+ let (arity, r, num_ingredients) =
+ match CicEnvironment.get_obj mutind with
+ C.InductiveDefinition (tl,ingredients,r) ->
+ let (_,_,arity,_) = List.nth tl i
+ and num_ingredients =
+ List.fold_right
+ (fun (k,l) i ->
+ if k < cookingsno then i + List.length l else i
+ ) ingredients 0
+ in
+ (arity,r,num_ingredients)
+ | _ -> raise WrongUriToInductiveDefinition
+ in
+ let ts =
+ let num_to_eat = r + num_ingredients in
+ let rec eat_first =
+ function
+ (0,l) -> l
+ | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+ | _ -> raise (Impossible 5)
+ in
+ eat_first (num_to_eat,tl)
+ in
+ reduceaux (ts@l) (List.nth pl (j-1))
+ | C.Abst _ | C.Cast _ | C.Implicit ->
+ raise (Impossible 2) (* we don't trust our whd ;-) *)
+ | _ ->
+ let outtype' = reduceaux [] outtype in
+ let term' = reduceaux [] term in
+ let pl' = List.map (reduceaux []) pl in
+ let res =
+ C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ in
+ if l = [] then res else C.Appl (res::l)
+ )
+ | C.Fix (i,fl) ->
+ let t' () =
+ let fl' =
+ List.map
+ (function (n,recindex,ty,bo) ->
+ (n,recindex,reduceaux [] ty, reduceaux [] bo)
+ ) fl
+ in
+ C.Fix (i, fl')
+ in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ Some (List.nth l recindex)
+ with
+ _ -> None
+ in
+ (match recparam with
+ Some recparam ->
+ (match reduceaux [] recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+ fl
+ body
+ in
+ (* Possible optimization: substituting whd recparam in l *)
+ reduceaux l body'
+ | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+ )
+ | C.CoFix (i,fl) ->
+ let t' =
+ let fl' =
+ List.map
+ (function (n,ty,bo) ->
+ (n,reduceaux [] ty, reduceaux [] bo)
+ ) fl
+ in
+ C.CoFix (i, fl')
+ in
+ if l = [] then t' else C.Appl (t'::l)
+ in
+ reduceaux []
+;;
projects / helm.git / commitdiff