X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fd2819738af77561725d77067926a694b90b9480;hb=063523ae5f8da7e6458232f4afb6744ec86dc8bd;hp=35015e541202d36fe82a245ddd167e7322fc2c1c;hpb=ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 35015e541..fd2819738 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -557,25 +557,37 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (* constructors using Prods *) let len = List.length itl in let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in + List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in let _,ugraph2 = List.fold_right - (fun (_,_,_,cl) (i,ugraph) -> + (fun (_,_,ty,cl) (i,ugraph) -> + let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debrujinedte = debrujin_constructor uri len [] te in - let augmented_term = - List.fold_right - (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl debrujinedte - in - let _,ugraph' = type_of ~logger augmented_term ugraph in + let te = debrujin_constructor uri len [] te in + let context,te = split_prods ~subst:[] tys indparamsno te in + let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in + let ugraph = + match + CicReduction.whd context con_sort, CicReduction.whd [] ty_sort + with + Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) -> + CicUniv.add_ge u2 u1 ugraph + | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort _, Cic.Sort Cic.Set + | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp + | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph + | a,b -> + raise + (TypeCheckerFailure + (lazy ("Wrong constructor or inductive arity shape: "^ + CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in (* let's check also the positivity conditions *) if not - (are_all_occurrences_positive tys uri indparamsno i 0 len - debrujinedte) + (are_all_occurrences_positive context uri indparamsno + (i+indparamsno) indparamsno (len+indparamsno) te) then begin prerr_endline (UriManager.string_of_uri uri); @@ -584,7 +596,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (TypeCheckerFailure (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else - ugraph' + ugraph ) ugraph cl in (i + 1),ugraph'' ) itl (1,ugrap1) @@ -708,7 +720,8 @@ and split_prods ~subst context n te = let module R = CicReduction in match (n, R.whd ~subst context te) with (0, _) -> context,te - | (n, C.Prod (name,so,ta)) when n > 0 -> + | (n, C.Sort _) when n <= 0 -> context,te + | (n, C.Prod (name,so,ta)) -> split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta | (_, _) -> raise (AssertFailure (lazy "8")) @@ -1328,7 +1341,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Var (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in let ty1 = CicSubstitution.subst_vars exp_named_subst ty in @@ -1441,7 +1454,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in let cty1 = @@ -1452,11 +1465,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: da me c'era anche questa, ma in CVS no *) let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in - (* fine parte dubbia *) let cty = CicSubstitution.subst_vars exp_named_subst mty in @@ -1464,9 +1475,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = cty,ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: idem come sopra *) let mty,ugraph2 = type_of_mutual_inductive_constr ~logger uri i j ugraph1 in @@ -1773,7 +1783,24 @@ end; let (_,ty,_) = List.nth fl i in ty,ugraph2 - and check_exp_named_subst ~logger ~subst context = + and check_exp_named_subst uri ~logger ~subst context ens ugraph = + let params = + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match obj with + Cic.Constant (_,_,_,params,_) -> params + | Cic.Variable (_,_,_,params,_) -> params + | Cic.CurrentProof (_,_,_,_,params,_) -> params + | Cic.InductiveDefinition (_,params,_,_) -> params + ) in + let rec check_same_order params ens = + match params,ens with + | _,[] -> () + | [],_::_ -> + raise (TypeCheckerFailure (lazy "Bad explicit named substitution")) + | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' -> + check_same_order tl tl' + | _::tl,l -> check_same_order tl l + in let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with [] -> ugraph @@ -1799,7 +1826,8 @@ end; raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in - check_exp_named_subst_aux ~logger [] + check_same_order params ens ; + check_exp_named_subst_aux ~logger [] ens ugraph and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in