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 =
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
+ guarded_by_destructors context m nn kl x safes
+ (CicSubstitution.lift m bo)
| None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
)
| C.Meta _
| (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
C.Sort C.Prop
| C.Sort C.Set -> true
| C.Sort C.CProp -> true
- | C.Sort C.Type ->
+ | 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
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
and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
sort_of_prod context (name,s) (sort1,sort2)
| 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
| 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
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
)