* http://cs.unibo.it/helm/.
*)
-exception NotImplemented;;
exception Impossible of int;;
exception NotWellTyped of string;;
exception WrongUriToConstant of string;;
exception NotWellFormedTypeOfInductiveConstructor of string;;
exception WrongRequiredArgument of string;;
-let log =
- let module U = UriManager in
- let indent = ref 0 in
- function
- `Start_type_checking uri ->
- print_string (
- (String.make !indent ' ') ^
- "<div style=\"margin-left: " ^
- string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
- "Type-Checking of " ^ (U.string_of_uri uri) ^ " started</div>\n"
- ) ;
- flush stdout ;
- incr indent
- | `Type_checking_completed uri ->
- decr indent ;
- print_string (
- (String.make !indent ' ') ^
- "<div style=\"color: green ; margin-left: " ^
- string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
- "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.</div>\n"
- ) ;
- flush stdout
-;;
-
let fdebug = ref 0;;
-let debug t env =
+let debug t context =
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
in
if !fdebug = 0 then
- raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) ""))
- (*print_endline ("\n" ^ List.fold_right debug_aux (t::env) "") ; flush stdout*)
+ raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))
+ (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
;;
let rec split l n =
match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- log (`Start_type_checking uri) ;
+ Logger.log (`Start_type_checking uri) ;
(* let's typecheck the uncooked obj *)
(match uobj with
C.Definition (_,te,ty,_) ->
| 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))
) ;
CicEnvironment.set_type_checking_info uri ;
- log (`Type_checking_completed uri) ;
+ Logger.log (`Type_checking_completed uri) ;
match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
match CicEnvironment.is_type_checked uri 0 with
CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
| CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
- log (`Start_type_checking uri) ;
+ Logger.log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
let _ = type_of ty in
(match bo with
raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
) ;
CicEnvironment.set_type_checking_info uri ;
- log (`Type_checking_completed uri) ;
+ Logger.log (`Type_checking_completed uri) ;
ty
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
i &&
weakly_positive (n+1) (nn+1) uri x
) cl' true
- | C.MutInd (uri,_,i) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (tl,_,_) ->
- List.length tl = 1
- | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
- )
| t -> does_not_occur n nn t
(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- log (`Start_type_checking uri) ;
+ Logger.log (`Start_type_checking uri) ;
cooked_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
- log (`Type_checking_completed uri) ;
+ Logger.log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- log (`Start_type_checking uri) ;
+ Logger.log (`Start_type_checking uri) ;
cooked_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
- log (`Type_checking_completed uri) ;
+ Logger.log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked uri cookingsno with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
| C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
- | C.Lambda _ -> raise (Impossible 4) (* due to type-checking *)
- | C.LetIn _ -> raise NotImplemented
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
| C.Appl _ -> []
| C.Const _
| C.Abst _ -> raise (Impossible 5)
if b then 1::safes' else safes'
in
get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
- | (C.MutInd _, e, []) -> (e,safes,n,nn,x)
+ | (C.Prod _, (C.MutConstruct _ as e), _)
+ | (C.Prod _, (C.Rel _ as e), _)
+ | (C.MutInd _, e, [])
| (C.Appl _, e, []) -> (e,safes,n,nn,x)
- | (_,_,_) -> raise (Impossible 7)
+ | (_,_,_) ->
+ (* CSC: If the next exception is raised, it just means that *)
+ (* CSC: the proof-assistant allows to use very strange things *)
+ (* CSC: as a branch of a case whose type is a Prod. In *)
+ (* CSC: particular, this means that a new (C.Prod, x,_) case *)
+ (* CSC: must be considered in this match. (e.g. x = MutCase) *)
+ raise (Impossible 7)
-and eat_prods n te =
+and split_prods n te =
let module C = Cic in
let module R = CicReduction in
match (n, R.whd te) with
- (0, _) -> te
- | (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta
+ (0, _) -> [],te
+ | (n, C.Prod (_,so,ta)) when n > 0 ->
+ let (l1,l2) = split_prods (n - 1) ta in
+ (so::l1,l2)
| (_, _) -> raise (Impossible 8)
and eat_lambdas n te =
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
- List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+ List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
in
(isinductive,paramsno,cl')
| _ ->
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
- List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+ List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
in
(isinductive,paramsno,cl')
| _ ->
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
- List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+ List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
in
(isinductive,paramsno,cl')
| _ ->
C.InductiveDefinition (tl,_,paramsno) ->
let (_,isinductive,_,cl) = List.nth tl i in
let cl' =
- List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+ List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
in
(isinductive,paramsno,cl')
| _ ->
bo
) fl true
-(*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h =
+(* 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
- function
- C.Rel m when m > n && m <= nn -> h = 1
+ (*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
| C.Rel _
- | C.Var _
+ | C.Var _ -> true
| C.Meta _
| C.Sort _
- | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
- | C.Cast (te,ty) ->
- guarded_by_constructors n nn h te &&
- guarded_by_constructors n nn h ty
- | C.Prod (_,so,de) ->
+ | C.Implicit
+ | C.Cast _
+ | C.Prod _
+ | C.LetIn _ ->
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
- | C.LetIn (_,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) ->
- let (is_coinductive, 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 -> (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
- is_coinductive &&
- List.fold_right
- (fun (x,r) i ->
- i &&
- if r then
- guarded_by_constructors n nn 1 x
- 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
+ let n_plus_len = n + len
+ and nn_plus_len = nn + len 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 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 args coInductiveTypeURI
+ ) pl true
| C.Appl l ->
List.fold_right (fun x i -> i && does_not_occur n nn x) l true
- | C.Const _
+ | C.Const _ -> true
| C.Abst _
- | C.MutInd _
- | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
+ | C.MutInd _ -> assert false
+ | C.MutConstruct _ -> true
| C.MutCase (_,_,_,out,te,pl) ->
- let rec returns_a_coinductive =
- function
- (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *)
- (*CSC: effettata solo una volta, per mangiarsi l'astrazione *)
- (*CSC: non dummy *)
- C.Lambda (_,_,de) -> returns_a_coinductive de
- | C.MutInd (uri,_,i) ->
- (*CSC: definire una funzioncina per questo codice sempre replicato *)
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
- | _ ->
- raise (WrongUriToMutualInductiveDefinitions
- (UriManager.string_of_uri uri))
- )
- (*CSC: bug nella prossima riga (manca la whd) *)
- | C.Appl ((C.MutInd (uri,_,i))::_) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- not is_inductive
- | _ ->
- raise (WrongUriToMutualInductiveDefinitions
- (UriManager.string_of_uri uri))
- )
- | _ -> false
- in
does_not_occur n nn out &&
does_not_occur n nn te &&
- if returns_a_coinductive out then
List.fold_right
- (fun x i -> i && guarded_by_constructors n nn h x) pl true
- else
- List.fold_right (fun x i -> i && does_not_occur n nn 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 &&
- does_not_occur n_plus_len nn_plus_len 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 =
| (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
| (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
(match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,paramsno) ->
let (_,_,_,cl) = List.nth itl i in
- List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+ List.fold_right (fun (_,x,_) i -> i && is_small paramsno x) cl true
| _ ->
raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
)
| C.Sort C.Set -> true
| C.Sort C.Type ->
(match CicEnvironment.get_obj uri with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,paramsno) ->
let (_,_,_,cl) = List.nth itl i in
- List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+ List.fold_right
+ (fun (_,x,_) i -> i && is_small paramsno x) cl true
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(U.string_of_uri uri))
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' env t =
- let rec type_of_aux env =
+and type_of_aux' metasenv context t =
+ let rec type_of_aux context =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
C.Rel n ->
let t =
try
- List.nth env (n - 1)
+ List.nth context (n - 1)
with
_ -> raise (NotWellTyped "Not a close term")
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) ->
- let _ = type_of ty in
- if R.are_convertible (type_of_aux env te) ty then ty
+ let _ = type_of_aux context ty in
+ if R.are_convertible (type_of_aux context te) ty then ty
else raise (NotWellTyped "Cast")
| C.Prod (_,s,t) ->
- let sort1 = type_of_aux env s
- and sort2 = type_of_aux (s::env) t in
+ let sort1 = type_of_aux context s
+ and sort2 = type_of_aux (s::context) t in
sort_of_prod (sort1,sort2)
| C.Lambda (n,s,t) ->
- let sort1 = type_of_aux env s
- and type2 = type_of_aux (s::env) t in
- let sort2 = type_of_aux (s::env) type2 in
+ let sort1 = type_of_aux context s
+ and type2 = type_of_aux (s::context) t in
+ let sort2 = type_of_aux (s::context) type2 in
(* only to check if the product is well-typed *)
let _ = sort_of_prod (sort1,sort2) in
C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
- let type1 = type_of_aux env s in
- let type2 = type_of_aux (type1::env) t in
- type2
+ let t' = CicSubstitution.subst s t in
+ type_of_aux context t'
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux env he
- and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
- (try
- eat_prods hetype tlbody_and_type
- with _ -> debug (C.Appl (he::tl)) env ; C.Implicit)
+ let hetype = type_of_aux context he
+ and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+ eat_prods hetype tlbody_and_type
| C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
| C.Const (uri,cookingsno) ->
incr fdebug ;
in
cty
| C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
- let outsort = type_of_aux env outtype in
+ let outsort = type_of_aux context outtype in
let (need_dummy, k) =
let rec guess_args t =
- match decast t with
+ match CicReduction.whd t with
C.Sort _ -> (true, 0)
| C.Prod (_, s, t) ->
let (b, n) = guess_args t in
if not b then (b, k - 1) else (b, k)
in
let (parameters, arguments) =
- match R.whd (type_of_aux env term) with
+ match R.whd (type_of_aux context term) with
(*CSC manca il caso dei CAST *)
C.MutInd (uri',_,i') ->
(*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
in
if not (check_allowed_sort_elimination uri i need_dummy
- sort_of_ind_type (type_of_aux env sort_of_ind_type) outsort)
+ sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
then
raise (NotWellTyped "MutCase: not allowed sort elimination") ;
(C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
in
(j + 1, b &&
- R.are_convertible (type_of_aux env p)
+ R.are_convertible (type_of_aux context p)
(type_of_branch parsno need_dummy outtype cons
- (type_of_aux env cons))
+ (type_of_aux context cons))
)
) (1,true) (List.combine pl cl)
in
| C.Fix (i,fl) ->
let types_times_kl =
List.rev
- (List.map (fun (_,k,ty,_) -> let _ = type_of_aux env ty in (ty,k)) fl)
+ (List.map
+ (fun (_,k,ty,_) -> let _ = type_of_aux context ty in (ty,k)) fl)
in
let (types,kl) = List.split types_times_kl in
let len = List.length types in
List.iter
(fun (name,x,ty,bo) ->
- if (R.are_convertible (type_of_aux (types @ env) bo)
+ if (R.are_convertible (type_of_aux (types @ context) bo)
(CicSubstitution.lift len ty))
then
begin
ty
| C.CoFix (i,fl) ->
let types =
- List.rev (List.map (fun (_,ty,_) -> let _ = type_of_aux env ty in ty) fl)
+ List.rev
+ (List.map (fun (_,ty,_) -> let _ = type_of_aux context ty in ty) fl)
in
let len = List.length types in
List.iter
(fun (_,ty,bo) ->
- if (R.are_convertible (type_of_aux (types @ env) bo)
+ if (R.are_convertible (type_of_aux (types @ context) bo)
(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")
+ (* 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")
let (_,ty,_) = List.nth fl i in
ty
- (* CSC: wrong name and position: decast really does Cast-LetIn reduction *)
- and decast =
- let module C = Cic in
- function
- C.Cast (t,_) -> decast t
- | C.LetIn (_,s,t) -> decast (CicSubstitution.subst s t)
- | t -> t
-
and sort_of_prod (t1, t2) =
let module C = Cic in
- match (decast t1, decast t2) with
+ let t1' = CicReduction.whd t1 in
+ let t2' = CicReduction.whd t2 in
+ match (t1', t2') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
C.Sort s2
| (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| (_,_) ->
raise
- (NotWellTyped ("Prod: sort1= " ^ CicPp.ppterm t1 ^ " ;
- sort2= " ^ CicPp.ppterm t2))
+ (NotWellTyped
+ ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
and eat_prods hetype =
(*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
Cic.Prod (n,s,t) ->
if CicReduction.are_convertible s hety then
(CicReduction.fdebug := -1 ;
- eat_prods (CicSubstitution.subst hete t) tl
+ eat_prods (CicSubstitution.subst hete t) tl
)
else
- (
- CicReduction.fdebug := 0 ;
- let _ = CicReduction.are_convertible s hety in
- debug hete [hety ; s] ;
- raise (NotWellTyped "Appl: wrong parameter-type")
-)
+ begin
+ CicReduction.fdebug := 0 ;
+ ignore (CicReduction.are_convertible s hety) ;
+ fdebug := 0 ;
+ debug s [hety] ;
+ raise (NotWellTyped "Appl: wrong parameter-type")
+ end
| _ -> raise (NotWellTyped "Appl: wrong Prod-type")
)
+
+ and returns_a_coinductive ty =
+ let module C = Cic in
+ match CicReduction.whd ty with
+ C.MutInd (uri,cookingsno,i) ->
+ (*CSC: definire una funzioncina per questo codice sempre replicato *)
+ (match CicEnvironment.get_cooked_obj uri cookingsno with
+ C.InductiveDefinition (itl,_,_) ->
+ let (_,is_inductive,_,cl) = List.nth itl i in
+ if is_inductive then None else (Some uri)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions
+ (UriManager.string_of_uri uri))
+ )
+ | C.Appl ((C.MutInd (uri,_,i))::_) ->
+ (match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (itl,_,_) ->
+ let (_,is_inductive,_,_) = List.nth itl i in
+ if is_inductive then None else (Some uri)
+ | _ ->
+ raise (WrongUriToMutualInductiveDefinitions
+ (UriManager.string_of_uri uri))
+ )
+ | C.Prod (_,_,de) -> returns_a_coinductive de
+ | _ -> None
+
in
- type_of_aux env t
+ type_of_aux context t
(* is a small constructor? *)
(*CSC: ottimizzare calcolando staticamente *)
-and is_small c =
- let rec is_small_aux env c =
+and is_small paramsno c =
+ let rec is_small_aux context c =
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' [] context so in
(s = C.Sort C.Prop || s = C.Sort C.Set) &&
- is_small_aux (so::env) de
+ is_small_aux (so::context) de
| _ -> true (*CSC: we trust the type-checker *)
in
- is_small_aux [] c
+ let (sx,dx) = split_prods paramsno c in
+ is_small_aux (List.rev sx) dx
and type_of t =
- type_of_aux' [] t
+ type_of_aux' [] [] t
;;
let typecheck uri =
CicEnvironment.CheckedObj _ -> ()
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
- log (`Start_type_checking uri) ;
+ Logger.log (`Start_type_checking uri) ;
(match uobj with
C.Definition (_,te,ty,_) ->
let _ = type_of ty in
| 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
cooked_mutual_inductive_defs uri uobj
) ;
CicEnvironment.set_type_checking_info uri ;
- log (`Type_checking_completed uri)
+ Logger.log (`Type_checking_completed uri)
+;;
+
+(*******************************************************)
+(*CSC: Da qua in avanti deve sparire tutto *)
+exception NotImplemented
+let wrong_context_of_context context =
+ let module C = Cic in
+ List.map
+ (function
+ C.Decl bt -> bt
+ | C.Def bt -> raise NotImplemented
+ ) context
+;;
+
+let type_of_aux' metasenv context t =
+ let context' = wrong_context_of_context context in
+ type_of_aux' metasenv context' t
;;
projects / helm.git / blobdiff