exception ListTooShort;;
exception RelToHiddenHypothesis;;
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+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 _ 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
+ (function None -> None | Some t -> Some (head_beta_reduce t)) l
+ )
+ | C.Sort _ as t -> t
+ | C.Implicit -> assert false
+ | C.Cast (te,ty) ->
+ C.Cast (head_beta_reduce te, head_beta_reduce ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+ | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
+ let he' = S.subst he t in
+ if tl = [] then
+ head_beta_reduce he'
+ else
+ head_beta_reduce (C.Appl (he'::tl))
+ | C.Appl l ->
+ C.Appl (List.map head_beta_reduce l)
+ | 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' =
+ List.map
+ (function (name,i,ty,bo) ->
+ name,i,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.Fix (i,fl')
+ | C.CoFix (i,fl) ->
+ let fl' =
+ List.map
+ (function (name,ty,bo) ->
+ name,head_beta_reduce ty,head_beta_reduce bo
+ ) fl
+ in
+ C.CoFix (i,fl')
+;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant), *)
+(* distinction between fake dependent products *)
+(* and non-dependent products, alfa-conversion *)
+(*CSC: must alfa-conversion be considered or not? *)
+let syntactic_equality t t' =
+ let module C = Cic in
+ let rec syntactic_equality t t' =
+ if t = t' then true
+ else
+ match t, t' with
+ 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'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ syntactic_equality s s' &&
+ syntactic_equality t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ syntactic_equality s s' &&
+ 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,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' &&
+ List.fold_left2
+ (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
+ | C.Fix (i,fl), C.Fix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+ b && i = i' &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | C.CoFix (i,fl), C.CoFix (i',fl') ->
+ i = i' &&
+ List.fold_left2
+ (fun b (_,ty,bo) (_,ty',bo') ->
+ b &&
+ syntactic_equality ty ty' &&
+ syntactic_equality bo bo') true fl fl'
+ | _, _ -> 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'
+ with
+ _ -> false
+;;
let rec split l n =
match (l,n) with
| (_,_) -> 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))
;;
;;
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-let rec type_of_aux' subterms_to_types metasenv context t =
+let rec type_of_aux' subterms_to_types metasenv context t expectedty =
(* Coscoy's double type-inference algorithm *)
(* It computes the inner-types of every subterm of [t], *)
(* even when they are not needed to compute the types *)
(* of other terms. *)
- let rec type_of_aux context t =
+ let rec type_of_aux context t expectedty =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t
- | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
+ | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
| None -> raise RelToHiddenHypothesis
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)) 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) ->
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context te in
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
+ let _ = type_of_aux context ty None in
(* Checks suppressed *)
ty
| C.Prod (name,s,t) ->
- let sort1 = type_of_aux context s
- and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+ let sort1 = type_of_aux context s None
+ and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
sort_of_prod context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
(* Let's visit all the subterms that will not be visited later *)
- let _ = type_of_aux context s in
- let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
- (* Checks suppressed *)
- C.Prod (n,s,type2)
+ let _ = type_of_aux context s None in
+ let expected_target_type =
+ match expectedty with
+ None -> None
+ | Some expectedty' ->
+ let ty =
+ match R.whd context expectedty' with
+ C.Prod (_,_,expected_target_type) ->
+ head_beta_reduce expected_target_type
+ | _ -> assert false
+ in
+ Some ty
+ in
+ let type2 =
+ type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
+ in
+ (* Checks suppressed *)
+ C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
+(*CSC: What are the right expected types for the source and *)
+(*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 in
- (* Checks suppressed *)
- C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+ let _ = type_of_aux context s None in
+ let t_typ =
+ (* Checks suppressed *)
+ type_of_aux ((Some (n,(C.Def s)))::context) t None
+ in
+ 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 hetype = type_of_aux context he
- and tlbody_and_type =
- List.map (fun x -> (x, type_of_aux context x)) tl
+ 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
- | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
- | C.Const (uri,cookingsno) ->
- cooked_type_of_constant uri cookingsno
- | C.Abst _ -> raise (Impossible 22)
- | 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) ->
- (* Let's visit all the subterms that will not be visited later *)
- let _ = List.map (type_of_aux context) pl in
- let outsort = type_of_aux context outtype in
- let (need_dummy, k) =
- let rec guess_args context t =
- match CicReduction.whd context t with
- C.Sort _ -> (true, 0)
- | C.Prod (name, s, t) ->
- let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
- 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 ->
- (false, 1)
- | C.Appl ((C.MutInd (uri',_,i')) :: _)
- when U.eq uri' uri && i' = i -> (false, 1)
- | _ -> (true, 1)
- else
- (b, n + 1)
- | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
+ 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
- (*CSC whd non serve dopo type_of_aux ? *)
- let (b, k) = guess_args context outsort in
- if not b then (b, k - 1) else (b, k)
+ aux (expected_hetype, tl)
+ in
+ eat_prods context hetype tlbody_and_type
+ | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
+ | 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 =
+ match CicReduction.whd context t with
+ C.Sort _ -> (true, 0)
+ | C.Prod (name, s, t) ->
+ let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
+ if n = 0 then
+ (* last prod before sort *)
+ match CicReduction.whd context s with
+ C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
+ (false, 1)
+ | C.Appl ((C.MutInd (uri',i',_)) :: _)
+ when U.eq uri' uri && i' = i -> (false, 1)
+ | _ -> (true, 1)
+ else
+ (b, n + 1)
+ | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
in
- let (_, arguments) =
- match R.whd context (type_of_aux context term) with
- (*CSC manca il caso dei CAST *)
- C.MutInd (uri',_,i') ->
- (* Checks suppressed *)
- [],[]
- | C.Appl (C.MutInd (uri',_,i') :: tl) ->
- split tl (List.length tl - k)
- | _ ->
- raise (NotWellTyped "MutCase: the term is not an inductive one")
+ let (b, k) = guess_args context outsort in
+ if not b then (b, k - 1) else (b, k)
+ in
+ let (parameters, arguments,exp_named_subst) =
+ let type_of_term =
+ CicTypeChecker.type_of_aux' metasenv context term
in
- (* Checks suppressed *)
- if not need_dummy then
- C.Appl ((outtype::arguments)@[term])
- else if arguments = [] then
- outtype
- else
- C.Appl (outtype::arguments)
+ match
+ R.whd context (type_of_aux context term
+ (Some (head_beta_reduce type_of_term)))
+ with
+ (*CSC manca il caso dei CAST *)
+ C.MutInd (uri',i',exp_named_subst) ->
+ (* Checks suppressed *)
+ [],[],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 with
+ C.InductiveDefinition (tl,_,parsno) ->
+ let (_,_,_,cl) = List.nth tl i in (cl,parsno)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ in
+ let _ =
+ List.fold_left
+ (fun j (p,(_,c)) ->
+ let cons =
+ if parameters = [] then
+ (C.MutConstruct (uri,i,j,exp_named_subst))
+ else
+ (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
+ in
+ let expectedtype =
+ type_of_branch context parsno need_dummy outtype cons
+ (CicTypeChecker.type_of_aux' metasenv context cons)
+ in
+ ignore (type_of_aux context p
+ (Some (head_beta_reduce expectedtype))) ;
+ j+1
+ ) 1 (List.combine pl cl)
+ in
+ if not need_dummy then
+ C.Appl ((outtype::arguments)@[term])
+ else if arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments)
| C.Fix (i,fl) ->
(* Let's visit all the subterms that will not be visited later *)
let context' =
List.rev
(List.map
(fun (n,_,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
in
(* Checks suppressed *)
let (_,_,ty,_) = List.nth fl i in
List.rev
(List.map
(fun (n,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux context ty None in
(Some (C.Name n,(C.Decl ty)))
) fl
) @
in
let _ =
List.iter
- (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+ (fun (_,ty,bo) ->
+ let expectedty =
+ head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+ in
+ ignore (type_of_aux context' bo (Some expectedty))
+ ) fl
in
(* Checks suppressed *)
let (_,ty,_) = List.nth fl i in
ty
in
- (*CSC: Is whd the right thing to do? Or should full beta *)
- (*CSC: reduction be more appropriate? *)
-(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
-(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
- let synthesized' = CicReduction.whd context synthesized in
- CicHash.add subterms_to_types t
- {synthesized = synthesized' ; expected = Cic.Implicit} ;
- synthesized'
+ let synthesized' = head_beta_reduce synthesized in
+ let types,res =
+ match expectedty with
+ None ->
+ (* No expected type *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some ty when syntactic_equality synthesized' ty ->
+ (* The expected type is synthactically equal to *)
+ (* the synthesized type. Let's forget it. *)
+ {synthesized = synthesized' ; expected = None}, synthesized
+ | Some expectedty' ->
+ {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
| _ -> raise (NotWellTyped "Appl: wrong Prod-type")
)
+and type_of_branch context argsno need_dummy outtype term constype =
+ let module C = Cic in
+ let module R = CicReduction in
+ match R.whd context constype with
+ C.MutInd (_,_,_) ->
+ if need_dummy then
+ outtype
+ else
+ C.Appl [outtype ; term]
+ | C.Appl (C.MutInd (_,_,_)::tl) ->
+ let (_,arguments) = split tl argsno
+ in
+ if need_dummy && arguments = [] then
+ outtype
+ else
+ C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
+ | C.Prod (name,so,de) ->
+ let term' =
+ match CicSubstitution.lift 1 term with
+ C.Appl l -> C.Appl (l@[C.Rel 1])
+ | t -> C.Appl [t ; C.Rel 1]
+ in
+ 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)
+
in
- type_of_aux context t
+ type_of_aux context t expectedty
;;
-let double_type_of metasenv context t =
+let double_type_of metasenv context t expectedty =
let subterms_to_types = CicHash.create 503 in
- ignore (type_of_aux' subterms_to_types metasenv context t) ;
+ ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
subterms_to_types
;;
projects / helm.git / blobdiff