does_not_occur context n nn te && does_not_occur context n nn ty
| C.Prod (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ dest
| C.Lambda (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ dest
| C.LetIn (name,so,dest) ->
does_not_occur context n nn so &&
- does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
+ does_not_occur ((Some (name,(C.Def (so,None))))::context)
+ (n + 1) (nn + 1) dest
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
| C.Var (_,exp_named_subst)
(fun x i ->
i &&
weakly_positive
- ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
+ ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+ x
) cl' true
| t -> does_not_occur context n nn t
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.LetIn (name,so,ta) ->
check_is_really_smaller_arg context n nn kl x safes so &&
- check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
+ check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl (he::_) ->
(*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
match CicEnvironment.get_obj uri with
C.InductiveDefinition (tl,_,paramsno) ->
let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
+ List.map
+ (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
in
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map (fun (n,_,ty,_) ->
+ Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
| C.Rel n ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
- | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
+ | Some (_,C.Def (bo,_)) ->
+ guarded_by_destructors context n nn kl x safes bo
| None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
)
| C.Meta _
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.LetIn (name,so,ta) ->
guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Def so)))::context)
+ guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map (fun (n,_,ty,_) ->
+ Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
- List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+ List.map
+ (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
in
let cl' =
List.map
[] -> true
| he::tl ->
analyse_branch context so he &&
- analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
- de tl
+ analyse_instantiated_type
+ ((Some (name,(C.Decl so)))::context) de tl
end
| C.Lambda _
| C.LetIn _ ->
let n_plus_len = n + len
and nn_plus_len = nn + len
(*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
- and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+ and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,_,ty,bo) i ->
i && does_not_occur context n nn ty &&
[] -> []
| (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)
+ | (Some (n,C.Def (t,None)))::tl ->
+ (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
+ | (Some (n,C.Def (_,Some _)))::_ -> assert false
in
aux 1 canonical_context
in
let res =
match (t,ct) with
_,None -> true
- | Some t,Some (_,C.Def ct) ->
+ | Some t,Some (_,C.Def (ct,_)) ->
R.are_convertible context t ct
| Some t,Some (_,C.Decl ct) ->
R.are_convertible context (type_of_aux' metasenv context t) ct
(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)
- | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty
+ | Some (_,C.Def (bo,None)) ->
+ prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ;
+ type_of_aux context (S.lift n bo)
+ | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
with
_ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term"))
)
C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let _ = type_of_aux context s in
+ let ty = type_of_aux context s in
(* The type of a LetIn is a LetIn. Extremely slow since the computed
LetIn is later reduced and maybe also re-checked.
(C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
(CicSubstitution.subst s
- (type_of_aux ((Some (n,(C.Def s)))::context) t))
+ (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
| 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 in
projects / helm.git / blobdiff