X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicTypeChecker.ml;h=b57ad4e78876b1192d31a33ec195bd2cf4411b75;hb=78f2fb8fcf0bbd2521b67e4366b734ad88ebdc68;hp=7e2715d0a8b592d9367652688817a3c651567c44;hpb=c8b4fe261c80f5cb8b9bf998495996c469783ba6;p=helm.git diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml index 7e2715d0a..b57ad4e78 100644 --- a/components/cic_proof_checking/cicTypeChecker.ml +++ b/components/cic_proof_checking/cicTypeChecker.ml @@ -292,8 +292,12 @@ and does_not_occur ?(subst=[]) context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -304,8 +308,12 @@ and does_not_occur ?(subst=[]) context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -886,7 +894,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -899,7 +912,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1091,7 +1109,12 @@ and guarded_by_destructors ~subst context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -1104,7 +1127,12 @@ and guarded_by_destructors ~subst context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1257,7 +1285,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1298,7 +1332,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1309,7 +1349,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1543,11 +1589,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt t' t ugraph in - (C.Sort (C.Type t')),ugraph1 - (* TASSI: CONSTRAINTS *) + (try + let ugraph1 = CicUniv.add_gt t' t ugraph in + (C.Sort (C.Type t')),ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Cast (te,ty) as t -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in @@ -1832,16 +1880,14 @@ end; in outtype,ugraph5 | C.Fix (i,fl) -> - let types_times_kl,ugraph1 = - (* WAS: list rev list map *) + let types,kl,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,k,ty,_) -> + (fun (types,kl,ugraph,len) (n,k,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + k::kl,ugraph1,len+1) + ) ([],[],ugraph,0) fl in - let (types,kl) = List.split types_times_kl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (name,x,ty,bo) -> @@ -1875,15 +1921,15 @@ end; let (_,_,ty,_) = List.nth fl i in ty,ugraph2 | C.CoFix (i,fl) -> - let types,ugraph1 = + let types,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,ty,_) -> + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl ty))::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + ugraph1,len+1) + ) ([],ugraph,0) fl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (_,ty,bo) -> @@ -1963,9 +2009,12 @@ end; | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),ugraph2 + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)