CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
CicLogger.log (`Start_type_checking uri) ;
+ CicUniv.directly_to_env_begin ();
(* let's typecheck the uncooked obj *)
(match uobj with
C.Constant (_,Some te,ty,_) ->
("Unknown constant:" ^ U.string_of_uri uri))
);
CicEnvironment.set_type_checking_info uri ;
+ CicUniv.directly_to_env_end ();
CicLogger.log (`Type_checking_completed uri) ;
match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
| CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
CicLogger.log (`Start_type_checking uri) ;
+ CicUniv.directly_to_env_begin ();
(* only to check that ty is well-typed *)
let _ = type_of ty in
(match bo with
("Unknown variable:" ^ U.string_of_uri uri))
) ;
CicEnvironment.set_type_checking_info uri ;
+ CicUniv.directly_to_env_end ();
CicLogger.log (`Type_checking_completed uri) ;
ty
| _ ->
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
CicLogger.log (`Start_type_checking uri) ;
+ CicUniv.directly_to_env_begin ();
check_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
+ CicUniv.directly_to_env_end ();
CicLogger.log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
CicLogger.log (`Start_type_checking uri) ;
+ (*CicUniv.directly_to_env_begin ();*)
check_mutual_inductive_defs uri uobj ;
CicEnvironment.set_type_checking_info uri ;
+ (*CicUniv.directly_to_env_end ();*)
CicLogger.log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| Some (_,C.Def (bo,_)) ->
guarded_by_destructors context m nn kl x safes
(CicSubstitution.lift m bo)
- | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+ | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
)
| C.Meta _
| C.Sort _
(match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
C.Sort C.Prop
| C.Sort C.Set -> true
- | C.Sort C.CProp -> true
+ | C.Sort C.CProp -> true
| C.Sort (C.Type _) ->
- (* TASSI: da verificare *)
+ (* TASSI: da verificare *)
(match CicEnvironment.get_obj uri with
C.InductiveDefinition (itl,_,paramsno) ->
let (_,_,_,cl) = List.nth itl i in
| Some (_,C.Def (bo,None)) ->
debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
type_of_aux context (S.lift n bo)
- | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+ | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
with
_ ->
raise (TypeCheckerFailure "unbound variable")
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
if not (CicUniv.add_gt t' t ) then
- assert false (* t' is fresh! an error in CicUniv *)
- else
+ assert false (* t' is fresh! an error in CicUniv *)
+ else
C.Sort (C.Type t')
(* TASSI: CONSTRAINTS *)
| C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
| 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
- sort_of_prod context (name,s) (sort1,sort2)
+ let res = sort_of_prod context (name,s) (sort1,sort2) in
+ res
| C.Lambda (n,s,t) ->
let sort1 = type_of_aux context s in
(match R.whd context sort1 with
(CicSubstitution.subst s
(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
+ let hetype = type_of_aux context he in
+ let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
List.rev
(List.map
(fun (n,ty,_) ->
- let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
+ let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
in
let len = List.length types in
List.iter
| ((uri,t) as subst)::tl ->
let typeofvar =
CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: this test should not exist
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
("Unknown variable definition:" ^
UriManager.string_of_uri uri))
) ;
+*)
let typeoft = type_of_aux context t in
if CicReduction.are_convertible context typeoft typeofvar then
check_exp_named_subst_aux (substs@[subst]) tl
match (t1', t2') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
- (* different from Coq manual!!! *)
+ (* different from Coq manual!!! *)
C.Sort s2
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
C.Sort (C.Type t')
| (C.Sort _,C.Sort (C.Type t1)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
- C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+ C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
| (C.Meta _, C.Sort _) -> t2'
| (C.Meta _, (C.Meta (_,_) as t))
| (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
*)
;;
+(* tassi FIXME: not sure where is this called... no history here... *)
let typecheck uri =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- match CicEnvironment.is_type_checked ~trust:false uri with
- CicEnvironment.CheckedObj _ -> ()
+ (*match CicEnvironment.is_type_checked ~trust:false uri with*)
+ match CicEnvironment.is_type_checked ~trust:true uri with
+ CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
CicLogger.log (`Start_type_checking uri) ;
+ CicUniv.directly_to_env_begin ();
(match uobj with
C.Constant (_,Some te,ty,_) ->
let _ = type_of ty in
check_mutual_inductive_defs uri uobj
) ;
CicEnvironment.set_type_checking_info uri ;
- CicLogger.log (`Type_checking_completed uri)
+ CicUniv.directly_to_env_end ();
+ CicLogger.log (`Type_checking_completed uri);
+ uobj
;;