X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=36bfb28b19cd22c77c7471ec5343dab140f20861;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=b034e3928800e139e80e94e7d2396618f8e66255;hpb=b621ad609dab703c4a8055e2554fe39b1bcfb07c;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b034e3928..36bfb28b1 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -66,7 +66,7 @@ let debrujin_constructor uri number_of_types = C.Var (uri,exp_named_subst') | C.Meta _ -> assert false | C.Sort _ - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) @@ -203,9 +203,9 @@ and does_not_occur context n nn te = match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> false | C.Rel _ - | C.Meta _ + | C.Meta _ (* CSC: Are we sure? No recursion?*) | C.Sort _ - | C.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> does_not_occur context n nn te && does_not_occur context n nn ty | C.Prod (name,so,dest) -> @@ -265,7 +265,7 @@ and weakly_positive context n nn uri te = 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 = @@ -567,7 +567,7 @@ and recursive_args context n nn te = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ (*CSC ??? *) -> raise (AssertFailure "3") (* due to type-checking *) | C.Prod (name,so,de) -> @@ -604,13 +604,16 @@ and get_new_safes context p c rl safes n nn x = | (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 @@ -631,7 +634,8 @@ and eat_lambdas context n te = eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta in (te, k + 1, context') - | (_, _) -> raise (AssertFailure "9") + | (n, te) -> + raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te))) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and check_is_really_smaller_arg context n nn kl x safes te = @@ -645,7 +649,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ (* | C.Cast (te,ty) -> check_is_really_smaller_arg n nn kl x safes te && @@ -789,16 +793,17 @@ and guarded_by_destructors context n nn kl x safes = 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.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> guarded_by_destructors context n nn kl x safes te && guarded_by_destructors context n nn kl x safes ty @@ -840,17 +845,21 @@ and guarded_by_destructors context n nn kl x safes = 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:" ^ @@ -868,11 +877,8 @@ and guarded_by_destructors context n nn kl x safes = 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 @@ -976,7 +982,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Rel _ -> true | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ | C.Prod _ | C.LetIn _ -> @@ -1007,7 +1013,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Var _ | C.Sort _ -> does_not_occur context n nn te - | C.Implicit + | C.Implicit _ | C.Cast _ -> raise (AssertFailure "24")(* due to type-checking *) | C.Prod (name,so,de) -> @@ -1041,7 +1047,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *) | C.Prod (name,so,de) -> begin @@ -1168,7 +1174,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = | (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,_,_) -> @@ -1185,7 +1192,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = | (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) -> @@ -1199,7 +1207,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = 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 @@ -1228,7 +1237,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = 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 @@ -1245,7 +1255,8 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = ) | _ -> 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 @@ -1293,7 +1304,8 @@ and check_metasenv_consistency metasenv context canonical_context l = | (Some (n,C.Def (t,None)))::tl -> (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (_,Some _)))::_ -> assert false + | (Some (n,C.Def (t,Some ty)))::tl -> + (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1336,8 +1348,7 @@ and type_of_aux' metasenv context t = | 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 ; @@ -1351,8 +1362,16 @@ and type_of_aux' metasenv context t = 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!!! *) - | C.Implicit -> raise (AssertFailure "21") + (* 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 if R.are_convertible context (type_of_aux context te) ty then @@ -1365,12 +1384,19 @@ and type_of_aux' metasenv context t = 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 @@ -1610,7 +1636,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ | 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 @@ -1633,11 +1659,23 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ 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!!! *) - | (_,_) -> - raise (TypeCheckerFailure (sprintf + | (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 -> + t2' + | (_,_) -> raise (TypeCheckerFailure (sprintf "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) @@ -1649,7 +1687,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ | (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 )