| C.Axiom (_,ty,_) ->
(* only to check that ty is well-typed *)
let _ = type_of ty in ()
- | C.CurrentProof (_,_,te,ty) ->
- let _ = type_of ty in
- if not (R.are_convertible (type_of te) ty) then
+ | C.CurrentProof (_,conjs,te,ty) ->
+ let _ = type_of_aux' conjs [] ty in
+ if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
| _ -> raise (WrongUriToConstant (U.string_of_uri uri))
) ;
bo
) fl true
-(*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h te =
+(* the boolean h means already protected *)
+(* args is the list of arguments the type of the constructor that may be *)
+(* found in head position must be applied to. *)
+(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
+and guarded_by_constructors n nn h te args coInductiveTypeURI =
let module C = Cic in
(*CSC: There is a lot of code replication between the cases X and *)
(*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
(*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
match CicReduction.whd te with
- C.Rel m when m > n && m <= nn -> h = 1
+ C.Rel m when m > n && m <= nn -> h
| C.Rel _
| C.Var _ -> true
| C.Meta _
raise (Impossible 17) (* the term has just been type-checked *)
| C.Lambda (_,so,de) ->
does_not_occur n nn so &&
- guarded_by_constructors (n + 1) (nn + 1) h de
+ guarded_by_constructors (n + 1) (nn + 1) h de args coInductiveTypeURI
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
- h = 1 &&
+ h &&
List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
| C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
- (* Invariant: we are sure that the constructor is a constructor *)
- (* of the output inductive type of the whole co-fixpoint. *)
- let rl =
+ let consty =
match CicEnvironment.get_cooked_obj uri cookingsno with
C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,cl) = List.nth itl i in
- let (_,cons,rrec_args) = List.nth cl (j - 1) in
- (match !rrec_args with
- None -> raise (Impossible 18)
- | Some rec_args -> assert (not is_inductive) ; rec_args
- )
+ let (_,_,_,cl) = List.nth itl i in
+ let (_,cons,_) = List.nth cl (j - 1) in cons
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(UriManager.string_of_uri uri))
in
- List.fold_right
- (fun (x,r) i ->
- i &&
- if r then
-begin
-let res =
- guarded_by_constructors n nn 1 x
-in
- if not res then
- begin
- prerr_endline ("BECCATO: " ^ CicPp.ppterm x) ; flush stderr ; assert false
- end ;
- res
-end
- else
- does_not_occur n nn x
- ) (List.combine tl rl) true
+ let rec analyse_branch ty te =
+ match CicReduction.whd ty with
+ C.Meta _ -> raise (Impossible 34)
+ | C.Rel _
+ | C.Var _
+ | C.Sort _ ->
+ does_not_occur n nn te
+ | C.Implicit
+ | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
+ | C.Prod (_,_,de) ->
+ analyse_branch de te
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
+ | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
+ when uri == coInductiveTypeURI ->
+ guarded_by_constructors n nn true te [] coInductiveTypeURI
+ | C.Appl ((C.MutInd (uri,_,_))::tl) as ty ->
+ guarded_by_constructors n nn true te tl coInductiveTypeURI
+ | C.Appl _ ->
+ does_not_occur n nn te
+ | C.Const _
+ | C.Abst _ -> raise (Impossible 26)
+ | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
+ guarded_by_constructors n nn true te [] coInductiveTypeURI
+ | C.MutInd _ ->
+ does_not_occur n nn te
+ | C.MutConstruct _ -> raise (Impossible 27)
+ (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+ (*CSC: in head position. *)
+ | C.MutCase _
+ | C.Fix _
+ | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
+ in
+ let rec analyse_instantiated_type ty l =
+ match CicReduction.whd ty with
+ C.Rel _
+ | C.Var _
+ | C.Meta _
+ | C.Sort _
+ | C.Implicit
+ | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
+ | C.Prod (_,so,de) ->
+ begin
+ match l with
+ [] -> true
+ | he::tl ->
+ analyse_branch so he &&
+ analyse_instantiated_type de tl
+ end
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
+ | C.Appl _ ->
+ List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+ | C.Const _
+ | C.Abst _ -> raise (Impossible 31)
+ | C.MutInd _ ->
+ List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+ | C.MutConstruct _ -> raise (Impossible 32)
+ (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+ (*CSC: in head position. *)
+ | C.MutCase _
+ | C.Fix _
+ | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
+ in
+ let rec instantiate_type args consty =
+ function
+ [] -> true
+ | tlhe::tltl as l ->
+ let consty' = CicReduction.whd consty in
+ match args with
+ he::tl ->
+ begin
+ match consty' with
+ C.Prod (_,_,de) ->
+ let instantiated_de = CicSubstitution.subst he de in
+ (*CSC: siamo sicuri che non sia troppo forte? *)
+ does_not_occur n nn tlhe &
+ instantiate_type tl instantiated_de tltl
+ | _ ->
+ (*CSC:We do not consider backbones with a MutCase, a *)
+ (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
+ raise (Impossible 23)
+ end
+ | [] -> analyse_instantiated_type consty' l
+ (* These are all the other cases *)
+ in
+ instantiate_type args consty tl
| C.Appl ((C.CoFix (_,fl))::tl) ->
List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
let len = List.length fl in
List.fold_right
(fun (_,ty,bo) i ->
i && does_not_occur n_plus_len nn_plus_len ty &&
- guarded_by_constructors n_plus_len nn_plus_len h bo
+ guarded_by_constructors n_plus_len nn_plus_len h bo args
+ coInductiveTypeURI
) fl true
| C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
does_not_occur n nn out &&
does_not_occur n nn te &&
List.fold_right
- (fun x i -> i && guarded_by_constructors n nn h x) pl true
+ (fun x i ->
+ i &&
+ guarded_by_constructors n nn h x args coInductiveTypeURI
+ ) pl true
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n nn x) l true
| C.Const _ -> true
does_not_occur n nn out &&
does_not_occur n nn te &&
List.fold_right
- (fun x i -> i && guarded_by_constructors n nn h x) pl true
+ (fun x i ->
+ i &&
+ guarded_by_constructors n nn h x args coInductiveTypeURI
+ ) pl true
| C.Fix (_,fl) ->
let len = List.length fl in
let n_plus_len = n + len
List.fold_right
(fun (_,ty,bo) i ->
i && does_not_occur n_plus_len nn_plus_len ty &&
- guarded_by_constructors n_plus_len nn_plus_len h bo
+ guarded_by_constructors n_plus_len nn_plus_len h bo args
+ coInductiveTypeURI
) fl true
and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' env t =
+and type_of_aux' metasenv env t =
let rec type_of_aux env =
let module C = Cic in
let module R = CicReduction in
let ty = type_of_variable uri in
decr fdebug ;
ty
- | C.Meta n -> raise NotImplemented
+ | C.Meta n -> List.assoc n metasenv
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
(CicSubstitution.lift len ty))
then
begin
- (* let's control the guarded by constructors conditions C{f,M} *)
- if not (guarded_by_constructors 0 len 0 bo) then
- raise (NotWellTyped "CoFix: not guarded by constructors") ;
- if not (returns_a_coinductive ty) then
- raise (NotWellTyped "CoFix: does not return a coinductive type")
+ (* let's control that the returned type is coinductive *)
+ match returns_a_coinductive ty with
+ None ->
+ raise(NotWellTyped "CoFix: does not return a coinductive type")
+ | Some uri ->
+ (*let's control the guarded by constructors conditions C{f,M}*)
+ if not (guarded_by_constructors 0 len false bo [] uri) then
+ raise (NotWellTyped "CoFix: not guarded by constructors")
end
else
raise (NotWellTyped "CoFix: ill-typed bodies")
and returns_a_coinductive ty =
let module C = Cic in
match CicReduction.whd ty with
- C.MutInd (uri,_,i) ->
+ C.MutInd (uri,cookingsno,i) ->
(*CSC: definire una funzioncina per questo codice sempre replicato *)
- (match CicEnvironment.get_obj uri with
+ (match CicEnvironment.get_cooked_obj uri cookingsno with
C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
+ let (_,is_inductive,_,cl) = List.nth itl i in
+ if is_inductive then None else (Some uri)
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(UriManager.string_of_uri uri))
(match CicEnvironment.get_obj uri with
C.InductiveDefinition (itl,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
+ if is_inductive then None else (Some uri)
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(UriManager.string_of_uri uri))
)
| C.Prod (_,_,de) -> returns_a_coinductive de
- | _ -> assert false
+ | _ -> None
in
type_of_aux env t
let module C = Cic in
match CicReduction.whd c with
C.Prod (_,so,de) ->
- let s = type_of_aux' env so in
+ (*CSC: [] is an empty metasenv. Is it correct? *)
+ let s = type_of_aux' [] env so in
(s = C.Sort C.Prop || s = C.Sort C.Set) &&
is_small_aux (so::env) de
| _ -> true (*CSC: we trust the type-checker *)
is_small_aux (List.rev sx) dx
and type_of t =
- type_of_aux' [] t
+ type_of_aux' [] [] t
;;
let typecheck uri =
| C.Axiom (_,ty,_) ->
(* only to check that ty is well-typed *)
let _ = type_of ty in ()
- | C.CurrentProof (_,_,te,ty) ->
- (*CSC [] wrong *)
- let _ = type_of ty in
- debug (type_of te) [] ;
- if not (R.are_convertible (type_of te) ty) then
- raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+ | C.CurrentProof (_,conjs,te,ty) ->
+ (*CSC [] wrong *)
+ let _ = type_of_aux' conjs [] ty in
+ debug (type_of_aux' conjs [] te) [] ;
+ if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+ raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
| C.Variable (_,bo,ty) ->
(* only to check that ty is well-typed *)
let _ = type_of ty in
CicEnvironment.set_type_checking_info uri ;
log (`Type_checking_completed uri)
;;
+
projects / helm.git / blobdiff