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.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)
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
| C.Prod (n,s,t) ->
C.Prod
in
C.Meta(i,l')
| C.Sort _ as t -> t
- | C.Implicit as t -> t
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
| C.Prod (n,s,t) ->
C.Prod (n, substaux k s, substaux (k + 1) t)
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) -> reduceaux context l (S.lift n bo)
+ | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_,_) ->
+ | C.Variable (_,None,_,_,_) ->
let t' = C.Var (uri,exp_named_subst') in
if l = [] then t' else C.Appl (t'::l)
- | C.Variable (_,Some body,_,_) ->
+ | C.Variable (_,Some body,_,_,_) ->
(reduceaux context l
(CicSubstitution.subst_vars exp_named_subst' 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.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (match CicEnvironment.get_obj uri with
- C.Constant (_,Some body,_,_) ->
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ C.Constant (_,Some body,_,_,_) ->
(reduceaux context l
(CicSubstitution.subst_vars exp_named_subst' body))
- | C.Constant (_,None,_,_) ->
+ | C.Constant (_,None,_,_,_) ->
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,_,_) ->
+ | C.CurrentProof (_,_,body,_,_,_) ->
(reduceaux context l
(CicSubstitution.subst_vars exp_named_subst' body))
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- match CicEnvironment.get_obj mutind with
- C.InductiveDefinition (tl,_,r) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
- | _ -> raise WrongUriToInductiveDefinition
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ match o with
+ C.InductiveDefinition (tl,_,r,_) ->
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
+ | _ -> raise WrongUriToInductiveDefinition
in
let ts =
let rec eat_first =
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
(* 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 *)
+(* w.r.t. zero or more variables and if the Fix can be reductaed, 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 *)
(* 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 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
in
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_,_) ->
+ | C.Variable (_,None,_,_,_) ->
let t' = C.Var (uri,exp_named_subst') in
if l = [] then t' else C.Appl (t'::l)
- | C.Variable (_,Some body,_,_) ->
+ | C.Variable (_,Some body,_,_,_) ->
reduceaux context l
(CicSubstitution.subst_vars exp_named_subst' 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.Implicit _ as t -> t
| C.Cast (te,ty) ->
C.Cast (reduceaux context l te, reduceaux context l ty)
| C.Prod (name,s,t) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (match CicEnvironment.get_obj uri with
- C.Constant (_,Some body,_,_) ->
- try_delta_expansion l
+ (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.Constant (_,None,_,_,_) ->
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.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
| C.MutInd (uri,i,exp_named_subst) ->
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- match CicEnvironment.get_obj mutind with
- C.InductiveDefinition (tl,ingredients,r) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
- | _ -> raise WrongUriToInductiveDefinition
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ match o with
+ C.InductiveDefinition (tl,ingredients,r,_) ->
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
+ | _ -> raise WrongUriToInductiveDefinition
in
let ts =
let rec eat_first =
eat_first (r,tl)
in
reduceaux context (ts@l) (List.nth pl (j-1))
- | C.Cast _ | C.Implicit ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let outtype' = reduceaux context [] outtype in
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