X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;fp=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=0000000000000000000000000000000000000000;hp=441d7c9a938425a573c15f7236308f189e2be165;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml deleted file mode 100644 index 441d7c9a9..000000000 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ /dev/null @@ -1,747 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -exception Impossible of int;; -exception NotWellTyped of string;; -exception WrongUriToConstant of string;; -exception WrongUriToVariable of string;; -exception WrongUriToMutualInductiveDefinitions of string;; -exception ListTooShort;; -exception RelToHiddenHypothesis;; - -let syntactic_equality_add_time = ref 0.0;; -let type_of_aux'_add_time = ref 0.0;; -let number_new_type_of_aux'_double_work = ref 0;; -let number_new_type_of_aux' = ref 0;; -let number_new_type_of_aux'_prop = ref 0;; - -let double_work = ref 0;; - -let xxx_type_of_aux' m c t = - let t1 = Sys.time () in - let res = CicTypeChecker.type_of_aux' m c t in - let t2 = Sys.time () in - type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; - res -;; - -type types = {synthesized : Cic.term ; expected : Cic.term option};; - -(* does_not_occur n te *) -(* returns [true] if [Rel n] does not occur in [te] *) -let rec does_not_occur n = - let module C = Cic in - function - C.Rel m when m = n -> false - | C.Rel _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ -> true - | C.Cast (te,ty) -> - does_not_occur n te && does_not_occur n ty - | C.Prod (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.Lambda (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.LetIn (name,so,dest) -> - does_not_occur n so && - does_not_occur (n + 1) dest - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur n x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) - | C.MutInd (_,_,exp_named_subst) - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur n x) - exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> - does_not_occur n out && does_not_occur n te && - List.fold_right (fun x i -> i && does_not_occur n x) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur n ty && - does_not_occur n_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur n ty && - does_not_occur n_plus_len bo - ) fl true -;; - -(*CSC: potrebbe creare applicazioni di applicazioni *) -(*CSC: ora non e' piu' head, ma completa!!! *) -let rec head_beta_reduce = - let module S = CicSubstitution in - let module C = Cic in - function - C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.Var (uri,exp_named_subst) - | C.Meta (n,l) -> - C.Meta (n, - List.map - (function None -> None | Some t -> Some (head_beta_reduce t)) l - ) - | C.Sort _ as t -> t - | C.Implicit _ -> assert false - | C.Cast (te,ty) -> - C.Cast (head_beta_reduce te, head_beta_reduce ty) - | C.Prod (n,s,t) -> - C.Prod (n, head_beta_reduce s, head_beta_reduce t) - | C.Lambda (n,s,t) -> - C.Lambda (n, head_beta_reduce s, head_beta_reduce t) - | C.LetIn (n,s,t) -> - C.LetIn (n, head_beta_reduce s, head_beta_reduce t) - | C.Appl ((C.Lambda (name,s,t))::he::tl) -> - let he' = S.subst he t in - if tl = [] then - head_beta_reduce he' - else - head_beta_reduce (C.Appl (he'::tl)) - | C.Appl l -> - C.Appl (List.map head_beta_reduce l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t, - List.map head_beta_reduce pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (function (name,i,ty,bo) -> - name,i,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.Fix (i,fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (function (name,ty,bo) -> - name,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.CoFix (i,fl') -;; - -(* syntactic_equality up to the *) -(* distinction between fake dependent products *) -(* and non-dependent products, alfa-conversion *) -(*CSC: must alfa-conversion be considered or not? *) -let syntactic_equality t t' = - let module C = Cic in - let rec syntactic_equality t t' = - if t = t' then true - else - match t, t' with - C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.Cast (te,ty), C.Cast (te',ty') -> - syntactic_equality te te' && - syntactic_equality ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutConstruct (uri,i,j,exp_named_subst), - C.MutConstruct (uri',i',j',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && j = j' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - syntactic_equality outt outt' && - syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | _, _ -> false (* we already know that t != t' *) - and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = - List.fold_left2 - (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true - exp_named_subst1 exp_named_subst2 - in - try - syntactic_equality t t' - with - _ -> false -;; - -let xxx_syntactic_equality t t' = - let t1 = Sys.time () in - let res = syntactic_equality t t' in - let t2 = Sys.time () in - syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ; - res -;; - - -let rec split l n = - match (l,n) with - (l,0) -> ([], l) - | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) - | (_,_) -> raise ListTooShort -;; - -let type_of_constant uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked constant") - in - match cobj with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) -;; - -let type_of_variable uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty - | CicEnvironment.UncheckedObj (C.Variable _) -> - raise (NotWellTyped "Reference to an unchecked variable") - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) -;; - -let type_of_mutual_inductive_defs uri i = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked inductive type") - in - match cobj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -;; - -let type_of_mutual_inductive_constr uri i j = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj - | CicEnvironment.UncheckedObj uobj -> - raise (NotWellTyped "Reference to an unchecked constructor") - in - match cobj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -;; - -module CicHash = - Hashtbl.Make - (struct - type t = Cic.term - let equal = (==) - let hash = Hashtbl.hash - end) -;; - -(* type_of_aux' is just another name (with a different scope) for type_of_aux *) -let rec type_of_aux' subterms_to_types metasenv context t expectedty = - (* Coscoy's double type-inference algorithm *) - (* It computes the inner-types of every subterm of [t], *) - (* even when they are not needed to compute the types *) - (* of other terms. *) - let rec type_of_aux context t expectedty = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let module U = UriManager in - let synthesized = - match t with - C.Rel n -> - (try - match List.nth context (n - 1) with - Some (_,C.Decl t) -> S.lift n t - | Some (_,C.Def (_,Some ty)) -> S.lift n ty - | Some (_,C.Def (bo,None)) -> - type_of_aux context (S.lift n bo) expectedty - | None -> raise RelToHiddenHypothesis - with - _ -> raise (NotWellTyped "Not a close term") - ) - | C.Var (uri,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) - | C.Meta (n,l) -> - (* Let's visit all the subterms that will not be visited later *) - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let lifted_canonical_context = - let rec aux i = - function - [] -> [] - | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (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 (_,C.Def (_,Some _)))::_ -> assert false - in - aux 1 canonical_context - in - let _ = - List.iter2 - (fun t ct -> - match t,ct with - _,None -> () - | Some t,Some (_,C.Def (ct,_)) -> - let expected_type = - R.whd context - (xxx_type_of_aux' metasenv context ct) - in - (* Maybe I am a bit too paranoid, because *) - (* if the term is well-typed than t and ct *) - (* are convertible. Nevertheless, I compute *) - (* the expected type. *) - ignore (type_of_aux context t (Some expected_type)) - | Some t,Some (_,C.Decl ct) -> - ignore (type_of_aux context t (Some ct)) - | _,_ -> assert false (* the term is not well typed!!! *) - ) l lifted_canonical_context - in - let (_,canonical_context,ty) = - List.find (function (m,_,_) -> n = m) metasenv - in - (* Checks suppressed *) - CicSubstitution.lift_meta l ty - | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *) - 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') - | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *) - | C.Implicit _ -> raise (Impossible 21) - | C.Cast (te,ty) -> - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context te (Some (head_beta_reduce ty)) in - let _ = type_of_aux context ty None in - (* Checks suppressed *) - ty - | C.Prod (name,s,t) -> - let sort1 = type_of_aux context s None - and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in - sort_of_prod context (name,s) (sort1,sort2) - | C.Lambda (n,s,t) -> - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s None in - let expected_target_type = - match expectedty with - None -> None - | Some expectedty' -> - let ty = - match R.whd context expectedty' with - C.Prod (_,_,expected_target_type) -> - head_beta_reduce expected_target_type - | _ -> assert false - in - Some ty - in - let type2 = - type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type - in - (* Checks suppressed *) - C.Prod (n,s,type2) - | C.LetIn (n,s,t) -> -(*CSC: What are the right expected types for the source and *) -(*CSC: target of a LetIn? None used. *) - (* Let's visit all the subterms that will not be visited later *) - let ty = type_of_aux context s None in - let t_typ = - (* Checks suppressed *) - type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None - in (* CicSubstitution.subst s t_typ *) - if does_not_occur 1 t_typ then - (* since [Rel 1] does not occur in typ, substituting any term *) - (* in place of [Rel 1] is equivalent to delifting once *) - CicSubstitution.subst (C.Implicit None) t_typ - else - C.LetIn (n,s,t_typ) - | C.Appl (he::tl) when List.length tl > 0 -> - (* - let expected_hetype = - (* Inefficient, the head is computed twice. But I know *) - (* of no other solution. *) - (head_beta_reduce - (R.whd context (xxx_type_of_aux' metasenv context he))) - in - let hetype = type_of_aux context he (Some expected_hetype) in - let tlbody_and_type = - let rec aux = - function - _,[] -> [] - | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: - (aux (R.whd context (S.subst he t), tl)) - | _ -> assert false - in - aux (expected_hetype, tl) *) - let hetype = R.whd context (type_of_aux context he None) in - let tlbody_and_type = - let rec aux = - function - _,[] -> [] - | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: - (aux (R.whd context (S.subst he t), tl)) - | _ -> assert false - in - aux (hetype, tl) - in - eat_prods context hetype tlbody_and_type - | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") - | C.Const (uri,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) - | C.MutInd (uri,i,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_defs uri i) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - visit_exp_named_subst context uri exp_named_subst ; - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_constr uri i j) - | C.MutCase (uri,i,outtype,term,pl) -> - let outsort = type_of_aux context outtype None in - let (need_dummy, k) = - let rec guess_args context t = - match CicReduction.whd context t with - C.Sort _ -> (true, 0) - | C.Prod (name, s, t) -> - let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd context s with - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) - | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") - in - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) - in - let (parameters, arguments,exp_named_subst) = - let type_of_term = - xxx_type_of_aux' metasenv context term - in - match - R.whd context (type_of_aux context term - (Some (head_beta_reduce type_of_term))) - with - (*CSC manca il caso dei CAST *) - C.MutInd (uri',i',exp_named_subst) -> - (* Checks suppressed *) - [],[],exp_named_subst - | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) -> - let params,args = - split tl (List.length tl - k) - in params,args,exp_named_subst - | _ -> - raise (NotWellTyped "MutCase: the term is not an inductive one") - in - (* Checks suppressed *) - (* Let's visit all the subterms that will not be visited later *) - let (cl,parsno) = - match CicEnvironment.get_cooked_obj uri with - C.InductiveDefinition (tl,_,parsno) -> - let (_,_,_,cl) = List.nth tl i in (cl,parsno) - | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) - in - let _ = - List.fold_left - (fun j (p,(_,c)) -> - let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) - in - let expectedtype = - type_of_branch context parsno need_dummy outtype cons - (xxx_type_of_aux' metasenv context cons) - in - ignore (type_of_aux context p - (Some (head_beta_reduce expectedtype))) ; - j+1 - ) 1 (List.combine pl cl) - in - if not need_dummy then - C.Appl ((outtype::arguments)@[term]) - else if arguments = [] then - outtype - else - C.Appl (outtype::arguments) - | C.Fix (i,fl) -> - (* Let's visit all the subterms that will not be visited later *) - let context' = - List.rev - (List.map - (fun (n,_,ty,_) -> - let _ = type_of_aux context ty None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - in - (* Checks suppressed *) - let (_,_,ty,_) = List.nth fl i in - ty - | C.CoFix (i,fl) -> - (* Let's visit all the subterms that will not be visited later *) - let context' = - List.rev - (List.map - (fun (n,ty,_) -> - let _ = type_of_aux context ty None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - in - (* Checks suppressed *) - let (_,ty,_) = List.nth fl i in - ty - in - let synthesized' = head_beta_reduce synthesized in - let types,res = - match expectedty with - None -> - (* No expected type *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when xxx_syntactic_equality synthesized' ty -> - (* The expected type is synthactically equal to *) - (* the synthesized type. Let's forget it. *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some expectedty' -> - {synthesized = synthesized' ; expected = Some expectedty'}, - expectedty' - in - CicHash.add subterms_to_types t types ; - res - - and visit_exp_named_subst context uri exp_named_subst = - let uris_and_types = - match CicEnvironment.get_cooked_obj uri with - Cic.Constant (_,_,_,params) - | Cic.CurrentProof (_,_,_,_,params) - | Cic.Variable (_,_,_,params) - | Cic.InductiveDefinition (_,params,_) -> - List.map - (function uri -> - match CicEnvironment.get_cooked_obj uri with - Cic.Variable (_,None,ty,_) -> uri,ty - | _ -> assert false (* the theorem is well-typed *) - ) params - in - let rec check uris_and_types subst = - match uris_and_types,subst with - _,[] -> [] - | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' -> - ignore (type_of_aux context t (Some ty)) ; - let tytl' = - List.map - (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl - in - check tytl' substtl - | _,_ -> assert false (* the theorem is well-typed *) - in - check uris_and_types exp_named_subst - - and sort_of_prod context (name,s) (t1, t2) = - let module C = Cic in - let t1' = CicReduction.whd context t1 in - let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in - match (t1', t2') with - (C.Sort _, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> - (* different from Coq manual!!! *) - C.Sort s2 - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker,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 cictypechecker,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 - (NotWellTyped - ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) - - and eat_prods context hetype = - (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) - (*CSC: cucinati *) - function - [] -> hetype - | (hete, hety)::tl -> - (match (CicReduction.whd context hetype) with - Cic.Prod (n,s,t) -> - (* Checks suppressed *) - eat_prods context (CicSubstitution.subst hete t) tl - | _ -> raise (NotWellTyped "Appl: wrong Prod-type") - ) - -and type_of_branch context argsno need_dummy outtype term constype = - let module C = Cic in - let module R = CicReduction in - match R.whd context constype with - C.MutInd (_,_,_) -> - if need_dummy then - outtype - else - C.Appl [outtype ; term] - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl argsno - in - if need_dummy && arguments = [] then - outtype - else - C.Appl (outtype::arguments@(if need_dummy then [] else [term])) - | C.Prod (name,so,de) -> - let term' = - match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1] - in - C.Prod (C.Anonymous,so,type_of_branch - ((Some (name,(C.Decl so)))::context) argsno need_dummy - (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (Impossible 20) - - in - type_of_aux context t expectedty -;; - -let double_type_of metasenv context t expectedty = - let subterms_to_types = CicHash.create 503 in - ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ; - subterms_to_types -;;