exception WrongRequiredArgument of string;;
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 =
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' metasenv 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
| 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
+ 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 t' = CicSubstitution.subst s t in
- type_of_aux env t'
+ 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
+ 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) ->
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 CicReduction.whd t with
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
| _ -> None
in
- type_of_aux env t
+ type_of_aux context t
(* is a small constructor? *)
(*CSC: ottimizzare calcolando staticamente *)
and is_small paramsno c =
- let rec is_small_aux env c =
+ let rec is_small_aux context c =
let module C = Cic in
match CicReduction.whd c with
C.Prod (_,so,de) ->
(*CSC: [] is an empty metasenv. Is it correct? *)
- let s = type_of_aux' [] env so in
+ 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
let (sx,dx) = split_prods paramsno c in
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