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
| _ ->
let module C = Cic in
(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
let dummy_mutind =
- C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
+ C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
in
(*CSC mettere in cicSubstitution *)
let rec subst_inductive_type_with_dummy_mutind =
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
| (C.Prod _, (C.Rel _ as e), _)
| (C.MutInd _, e, [])
| (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
- | (_,_,_) ->
+ | (c,p,l) ->
(* 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 (AssertFailure "7")
+ raise
+ (AssertFailure
+ (Printf.sprintf "Get New Safes: c=%s ; p=%s"
+ (CicPp.ppterm c) (CicPp.ppterm p)))
and split_prods context n te =
let module C = Cic in
let module U = UriManager in
function
C.Rel m when m > n && m <= nn -> false
- | C.Rel n ->
+ | C.Rel m ->
(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
- | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+ guarded_by_destructors context m nn kl x safes
+ (CicSubstitution.lift m bo)
+ | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
)
| C.Meta _
| C.Sort _
let (tys,len,isinductive,paramsno,cl) =
match CicEnvironment.get_obj uri with
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
- in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods tys paramsno ty))) cl
+ let len = List.length tl in
+ let (_,isinductive,_,cl) = List.nth tl i in
+ let tys =
+ List.map (fun (n,_,ty,_) ->
+ Some(Cic.Name n,(Cic.Decl ty))) tl
in
- (tys,List.length tl,isinductive,paramsno,cl')
+ let cl' =
+ List.map
+ (fun (id,ty) ->
+ let debrujinedty = debrujin_constructor uri len ty in
+ (id, snd (split_prods tys paramsno ty),
+ snd (split_prods tys paramsno debrujinedty)
+ )) cl
+ in
+ (tys,len,isinductive,paramsno,cl')
| _ ->
raise (TypeCheckerFailure
("Unknown mutual inductive definition:" ^
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args tys 0 len debrujinedte
- in
+ (fun (p,(_,c,brujinedc)) i ->
+ let rl' = recursive_args tys 0 len brujinedc in
let (e,safes',n',nn',x',context') =
get_new_safes context p c rl' safes n nn x
in
| (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
| (C.Sort C.Prop, C.Sort C.Set)
| (C.Sort C.Prop, C.Sort C.CProp)
- | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
+ | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
+ (* TASSI: da verificare *)
(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
(match CicEnvironment.get_obj uri with
C.InductiveDefinition (itl,_,_) ->
| (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
| (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
| (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
- | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
+ | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
+ (* TASSI: da verificare *)
when need_dummy ->
(match CicEnvironment.get_obj uri with
C.InductiveDefinition (itl,_,paramsno) ->
raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri))
)
- | (C.Sort C.Type, C.Sort _) when need_dummy -> true
+ | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true
+ (* TASSI: da verificare *)
| (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
let res = CicReduction.are_convertible context so ind
in
(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.Type ->
+ | C.Sort C.CProp -> true
+ | C.Sort (C.Type _) ->
+ (* TASSI: da verificare *)
(match CicEnvironment.get_obj uri with
C.InductiveDefinition (itl,_,paramsno) ->
let (_,_,_,cl) = List.nth itl i in
)
| _ -> raise (AssertFailure "19")
)
- | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
+ | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
+ (* TASSI: da verificare *)
CicReduction.are_convertible context so ind
| (_,_) -> false
| 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 found in constructor type")
+ raise (TypeCheckerFailure "unbound variable")
)
| C.Var (uri,exp_named_subst) ->
incr fdebug ;
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
check_metasenv_consistency metasenv context canonical_context l;
CicSubstitution.lift_meta l ty
- | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+ (* TASSI: CONSTRAINTS *)
+ | 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
+ C.Sort (C.Type t')
+ (* TASSI: CONSTRAINTS *)
+ | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
| C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) as t ->
let _ = type_of_aux context ty in
| 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
- and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
- let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
- (* only to check if the product is well-typed *)
- let _ = sort_of_prod context (n,s) (sort1,sort2) in
- C.Prod (n,s,type2)
+ let sort1 = type_of_aux context s in
+ (match R.whd context sort1 with
+ C.Meta _
+ | C.Sort _ -> ()
+ | _ ->
+ raise
+ (TypeCheckerFailure (sprintf
+ "Not well-typed lambda-abstraction: the source %s should be a
+ type; instead it is a term of type %s" (CicPp.ppterm s)
+ (CicPp.ppterm sort1)))
+ ) ;
+ let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
+ C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
let ty = type_of_aux context s in
(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
| Cic.Variable (_,None,_,_) -> ()
| _ ->
raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
+ ("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
let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
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!!! *)
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ (* different from Coq manual!!! *)
C.Sort s2
- | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+ assert false ; (* not possible, error in CicUniv *)
+ 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.Meta _, C.Sort _) -> t2'
| (C.Meta _, (C.Meta (_,_) as t))
| (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
| (hete, hety)::tl ->
(match (CicReduction.whd context hetype) with
Cic.Prod (n,s,t) ->
- if CicReduction.are_convertible context s hety then
+ if CicReduction.are_convertible context hety s then
(CicReduction.fdebug := -1 ;
eat_prods context (CicSubstitution.subst hete t) tl
)
*)
;;
+(* 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
;;
projects / helm.git / blobdiff