type types = {synthesized : Cic.term ; expected : Cic.term option};;
+(* does_not_occur n te *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+let rec does_not_occur n =
+ let module C = Cic in
+ function
+ C.Rel m when m = n -> false
+ | C.Rel _
+ | C.Meta _
+ | C.Sort _
+ | C.Implicit -> true
+ | C.Cast (te,ty) ->
+ does_not_occur n te && does_not_occur n ty
+ | C.Prod (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.Lambda (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.LetIn (name,so,dest) ->
+ does_not_occur n so &&
+ does_not_occur (n + 1) dest
+ | C.Appl l ->
+ List.fold_right (fun x i -> i && does_not_occur n x) l true
+ | C.Var (_,exp_named_subst)
+ | C.Const (_,exp_named_subst)
+ | C.MutInd (_,_,exp_named_subst)
+ | C.MutConstruct (_,_,_,exp_named_subst) ->
+ List.fold_right (fun (_,x) i -> i && does_not_occur n x)
+ exp_named_subst true
+ | C.MutCase (_,_,out,te,pl) ->
+ does_not_occur n out && does_not_occur n te &&
+ List.fold_right (fun x i -> i && does_not_occur n x) pl true
+ | C.Fix (_,fl) ->
+ let len = List.length fl in
+ let n_plus_len = n + len in
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ in
+ List.fold_right
+ (fun (_,_,ty,bo) i ->
+ i && does_not_occur n ty &&
+ does_not_occur n_plus_len bo
+ ) fl true
+ | C.CoFix (_,fl) ->
+ let len = List.length fl in
+ let n_plus_len = n + len in
+ let tys =
+ List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+ in
+ List.fold_right
+ (fun (_,ty,bo) i ->
+ i && does_not_occur n ty &&
+ does_not_occur n_plus_len bo
+ ) fl true
+;;
+
(*CSC: potrebbe creare applicazioni di applicazioni *)
(*CSC: ora non e' piu' head, ma completa!!! *)
let rec head_beta_reduce =
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 _ =
- List.iter
- (function
- None -> ()
- | Some t -> ignore (type_of_aux context t None)
- ) l
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> n = m) metasenv
in
- let (_,canonical_context,ty) =
- List.find (function (m,_,_) -> n = m) metasenv
+ let lifted_canonical_context =
+ let rec aux i =
+ function
+ [] -> []
+ | (Some (n,C.Decl t))::tl ->
+ (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def t))::tl ->
+ (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | None::tl -> None::(aux (i+1) tl)
+ in
+ aux 1 canonical_context
in
- (* Checks suppressed *)
- CicSubstitution.lift_meta l ty
+ let _ =
+ List.iter2
+ (fun t ct ->
+ match t,ct with
+ _,None -> ()
+ | Some t,Some (_,C.Def ct) ->
+ let expected_type =
+ R.whd context
+ (CicTypeChecker.type_of_aux' metasenv context ct)
+ in
+ (* Maybe I am a bit too paranoid, because *)
+ (* if the term is well-typed than t and ct *)
+ (* are convertible. Nevertheless, I compute *)
+ (* the expected type. *)
+ ignore (type_of_aux context t (Some expected_type))
+ | Some t,Some (_,C.Decl ct) ->
+ ignore (type_of_aux context t (Some ct))
+ | _,_ -> assert false (* the term is not well typed!!! *)
+ ) l lifted_canonical_context
+ in
+ let (_,canonical_context,ty) =
+ List.find (function (m,_,_) -> n = m) metasenv
+ in
+ (* Checks suppressed *)
+ CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
(*CSC: target of a LetIn? None used. *)
(* Let's visit all the subterms that will not be visited later *)
let _ = type_of_aux context s None in
- (* Checks suppressed *)
- C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
- | C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he None in
- let tlbody_and_type =
- let rec aux =
- function
- _,[] -> []
- | C.Prod (n,s,t),he::tl ->
- (he, type_of_aux context he (Some (head_beta_reduce s)))::
- (aux (R.whd context (S.subst he t), tl))
- | _ -> assert false
+ let t_typ =
+ (* Checks suppressed *)
+ type_of_aux ((Some (n,(C.Def s)))::context) t None
in
- aux (R.whd context hetype, tl)
+ if does_not_occur 1 t_typ then
+ (* since [Rel 1] does not occur in typ, substituting any term *)
+ (* in place of [Rel 1] is equivalent to delifting once *)
+ CicSubstitution.subst C.Implicit t_typ
+ else
+ C.LetIn (n,s,t_typ)
+ | C.Appl (he::tl) when List.length tl > 0 ->
+ let expected_hetype =
+ (* Inefficient, the head is computed twice. But I know *)
+ (* of no other solution. *)
+ R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
in
- eat_prods context hetype tlbody_and_type
+ let hetype = type_of_aux context he (Some expected_hetype) in
+ let tlbody_and_type =
+ let rec aux =
+ function
+ _,[] -> []
+ | C.Prod (n,s,t),he::tl ->
+ (he, type_of_aux context he (Some (head_beta_reduce s)))::
+ (aux (R.whd context (S.subst he t), tl))
+ | _ -> assert false
+ in
+ aux (expected_hetype, tl)
+ 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
(* the synthesized type. Let's forget it. *)
{synthesized = synthesized' ; expected = None}, synthesized
| Some expectedty' ->
-prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
-prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
{synthesized = synthesized' ; expected = Some expectedty'},
expectedty'
in
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