let module S = CicSubstitution in
let module C = Cic in
function
- C.Rel _
- | C.Var _ as t -> t
+ C.Rel _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst)
| C.Meta (n,l) ->
C.Meta (n,
List.map
head_beta_reduce (C.Appl (he'::tl))
| C.Appl l ->
C.Appl (List.map head_beta_reduce l)
- | C.Const _ as t -> t
- | C.MutInd _
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cno,i,outt,t,pl) ->
- C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
List.map head_beta_reduce pl)
| C.Fix (i,fl) ->
let fl' =
if t = t' then true
else
match t, t' with
- C.Rel _, C.Rel _
- | C.Var _, C.Var _
- | C.Meta _, C.Meta _
- | C.Sort _, C.Sort _
- | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
+ UriManager.eq uri uri' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
| C.Cast (te,ty), C.Cast (te',ty') ->
syntactic_equality te te' &&
syntactic_equality ty ty'
syntactic_equality t t'
| C.Appl l, C.Appl l' ->
List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
- | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
- | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
- UriManager.eq uri uri' && i = i'
- | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
- UriManager.eq uri uri' && i = i' && j = j'
- | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
+ UriManager.eq uri uri' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
+ UriManager.eq uri uri' && i = i' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutConstruct (uri,i,j,exp_named_subst),
+ C.MutConstruct (uri',i',j',exp_named_subst') ->
+ UriManager.eq uri uri' && i = i' && j = j' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
UriManager.eq sp sp' && i = i' &&
syntactic_equality outt outt' &&
syntactic_equality t t' &&
b &&
syntactic_equality ty ty' &&
syntactic_equality bo bo') true fl fl'
- | _,_ -> false
+ | _, _ -> false (* we already know that t != t' *)
+ and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
+ List.fold_left2
+ (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
+ exp_named_subst1 exp_named_subst2
in
try
syntactic_equality t t'
| (_,_) -> raise ListTooShort
;;
-let cooked_type_of_constant uri cookingsno =
+let type_of_constant uri =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri cookingsno with
+ match CicEnvironment.is_type_checked uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked constant")
in
match cobj with
- C.Definition (_,_,ty,_) -> ty
- | C.Axiom (_,ty,_) -> ty
- | C.CurrentProof (_,_,_,ty) -> ty
+ C.Constant (_,_,ty,_) -> ty
+ | C.CurrentProof (_,_,_,ty,_) -> ty
| _ -> raise (WrongUriToConstant (U.string_of_uri uri))
;;
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (* 0 because a variable is never cooked => no partial cooking at one level *)
- match CicEnvironment.is_type_checked uri 0 with
- CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
+ match CicEnvironment.is_type_checked uri with
+ CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
| CicEnvironment.UncheckedObj (C.Variable _) ->
raise (NotWellTyped "Reference to an unchecked variable")
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
;;
-let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+let type_of_mutual_inductive_defs uri i =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri cookingsno with
+ match CicEnvironment.is_type_checked uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked inductive type")
| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;
-let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+let type_of_mutual_inductive_constr uri i j =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked uri cookingsno with
+ match CicEnvironment.is_type_checked uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
raise (NotWellTyped "Reference to an unchecked constructor")
match cobj with
C.InductiveDefinition (dl,_,_) ->
let (_,_,_,cl) = List.nth dl i in
- let (_,ty,_) = List.nth cl (j-1) in
+ let (_,ty) = List.nth cl (j-1) in
ty
| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;
with
_ -> raise (NotWellTyped "Not a close term")
)
- | C.Var uri -> type_of_variable uri
+ | C.Var (uri,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
| C.Meta (n,l) ->
(* Let's visit all the subterms that will not be visited later *)
let (_,canonical_context,_) =
in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
- | C.Const (uri,cookingsno) ->
- cooked_type_of_constant uri cookingsno
- | C.MutInd (uri,cookingsno,i) ->
- cooked_type_of_mutual_inductive_defs uri cookingsno i
- | C.MutConstruct (uri,cookingsno,i,j) ->
- let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
- cty
- | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
+ | C.Const (uri,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+ | C.MutInd (uri,i,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_defs uri i)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_constr uri i j)
+ | C.MutCase (uri,i,outtype,term,pl) ->
let outsort = type_of_aux context outtype None in
let (need_dummy, k) =
let rec guess_args context t =
if n = 0 then
(* last prod before sort *)
match CicReduction.whd context s with
- (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
- C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
+ C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
(false, 1)
- | C.Appl ((C.MutInd (uri',_,i')) :: _)
+ | C.Appl ((C.MutInd (uri',i',_)) :: _)
when U.eq uri' uri && i' = i -> (false, 1)
| _ -> (true, 1)
else
let (b, k) = guess_args context outsort in
if not b then (b, k - 1) else (b, k)
in
- let (parameters, arguments) =
+ let (parameters, arguments,exp_named_subst) =
let type_of_term =
CicTypeChecker.type_of_aux' metasenv context term
in
(Some (head_beta_reduce type_of_term)))
with
(*CSC manca il caso dei CAST *)
- C.MutInd (uri',_,i') ->
+ C.MutInd (uri',i',exp_named_subst) ->
(* Checks suppressed *)
- [],[]
- | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+ [],[],exp_named_subst
+ | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
+ let params,args =
split tl (List.length tl - k)
+ in params,args,exp_named_subst
| _ ->
raise (NotWellTyped "MutCase: the term is not an inductive one")
in
(* Checks suppressed *)
(* Let's visit all the subterms that will not be visited later *)
let (cl,parsno) =
- match CicEnvironment.get_cooked_obj uri cookingsno with
+ match CicEnvironment.get_cooked_obj uri with
C.InductiveDefinition (tl,_,parsno) ->
let (_,_,_,cl) = List.nth tl i in (cl,parsno)
| _ ->
in
let _ =
List.fold_left
- (fun j (p,(_,c,_)) ->
+ (fun j (p,(_,c)) ->
let cons =
if parameters = [] then
- (C.MutConstruct (uri,cookingsno,i,j))
+ (C.MutConstruct (uri,i,j,exp_named_subst))
else
- (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
+ (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
in
let expectedtype =
type_of_branch context parsno need_dummy outtype cons
CicHash.add subterms_to_types t types ;
res
+ and visit_exp_named_subst context uri exp_named_subst =
+ let uris_and_types =
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,_,_,params)
+ | Cic.CurrentProof (_,_,_,_,params)
+ | Cic.Variable (_,_,_,params)
+ | Cic.InductiveDefinition (_,params,_) ->
+ List.map
+ (function uri ->
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Variable (_,None,ty,_) -> uri,ty
+ | _ -> assert false (* the theorem is well-typed *)
+ ) params
+ in
+ let rec check uris_and_types subst =
+ match uris_and_types,subst with
+ _,[] -> []
+ | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
+ ignore (type_of_aux context t (Some ty)) ;
+ let tytl' =
+ List.map
+ (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
+ in
+ check tytl' substtl
+ | _,_ -> assert false (* the theorem is well-typed *)
+ in
+ check uris_and_types exp_named_subst
+
and sort_of_prod context (name,s) (t1, t2) =
let module C = Cic in
let t1' = CicReduction.whd context t1 in
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonimous,so,type_of_branch
+ C.Prod (C.Anonymous,so,type_of_branch
((Some (name,(C.Decl so)))::context) argsno need_dummy
(CicSubstitution.lift 1 outtype) term' de)
| _ -> raise (Impossible 20)
projects / helm.git / blobdiff