X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=04b769b5c2b68366d2c1f765a39d21f7b7f43f62;hb=8c058315b08e90f975895c2354941e3cef69051e;hp=3959795055c0d8b9a2be4a9009c0f588b4419de5;hpb=fbe2b073c8a78abd5e8c65eff92158357997e370;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 395979505..04b769b5c 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 @@ -646,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 && @@ -790,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 @@ -841,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:" ^ @@ -869,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 @@ -977,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 _ -> @@ -1008,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) -> @@ -1042,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 @@ -1294,7 +1299,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 @@ -1337,8 +1343,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 ; @@ -1353,7 +1358,7 @@ and type_of_aux' metasenv context t = 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") + | 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 @@ -1366,12 +1371,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 @@ -1611,7 +1623,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 @@ -1638,8 +1650,9 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) | (C.Meta _, C.Sort _) -> t2' - | (C.Meta _, C.Meta (_,[])) - | (C.Sort _, C.Meta (_,[])) -> 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'))) @@ -1652,7 +1665,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 )