From 15ed739c91a22e91ae88d54215f6862fc1074a88 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 26 Aug 1999 12:29:28 +0000 Subject: mach -> typing; machops -> typeops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@27 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mach.ml | 600 ----------------------------------- kernel/mach.mli | 48 --- kernel/machops.ml | 909 ----------------------------------------------------- kernel/machops.mli | 58 ---- kernel/typeops.ml | 909 +++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/typeops.mli | 58 ++++ kernel/typing.ml | 600 +++++++++++++++++++++++++++++++++++ kernel/typing.mli | 48 +++ 8 files changed, 1615 insertions(+), 1615 deletions(-) delete mode 100644 kernel/mach.ml delete mode 100644 kernel/mach.mli delete mode 100644 kernel/machops.ml delete mode 100644 kernel/machops.mli create mode 100644 kernel/typeops.ml create mode 100644 kernel/typeops.mli create mode 100644 kernel/typing.ml create mode 100644 kernel/typing.mli (limited to 'kernel') diff --git a/kernel/mach.ml b/kernel/mach.ml deleted file mode 100644 index 2311fb9992..0000000000 --- a/kernel/mach.ml +++ /dev/null @@ -1,600 +0,0 @@ - -(* $Id$ *) - -open Pp -open Util -open Names -open Univ -open Generic -open Term -open Reduction -open Sign -open Environ -open Type_errors -open Machops - -(* Fonctions temporaires pour relier la forme castée de la forme jugement *) - -let tjudge_of_cast env = function - | DOP2 (Cast, b, t) -> - (match whd_betadeltaiota env t with - | DOP0 (Sort s) -> {body=b; typ=s} - | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]" - | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]") - | _ -> anomaly "Not casted (tjudge_of_cast)" - -let tjudge_of_judge env j = - { body = j.uj_val; - typ = match whd_betadeltaiota env j.uj_type with - (* Nécessaire pour ZFC *) - | DOP0 (Sort s) -> s - | DOP0 Implicit -> anomaly "Tiens, un implicit" - | _ -> anomaly "Not a type (tjudge_ofjudge)" } - -let vect_lift = Array.mapi lift -let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) - -(*s The machine flags. - [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$) - like [Acc_rec.fw]. - [nocheck] indicates if we can skip some verifications to accelerate - the type inference. *) - -type 'a mach_flags = { - fix : bool; - nocheck : bool } - -(* The typing machine without information. *) - -let rec execute mf env cstr = - let u0 = universes env in - match kind_of_term cstr with - | IsMeta n -> - let metaty = - try lookup_meta n env - with Not_found -> error "A variable remains non instanciated" - in - (match kind_of_term metaty with - | IsCast (typ,kind) -> - ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0) - | _ -> - let (jty,u1) = execute mf env metaty in - let k = hnf_constr env jty.uj_type in - ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1)) - - | IsRel n -> - (relative env n, u0) - - | IsVar id -> - (make_judge cstr (snd (lookup_var id env)), u0) - - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - - | IsConst _ -> - (make_judge cstr (type_of_constant_or_existential env cstr), u0) - - | IsMutInd _ -> - (make_judge cstr (type_of_inductive env cstr), u0) - - | IsMutConstruct _ -> - let (typ,kind) = destCast (type_of_constructor env cstr) in - ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0) - - | IsMutCase (_,p,c,lf) -> - let (cj,u1) = execute mf env c in - let env1 = set_universes u1 env in - let (pj,u2) = execute mf env1 p in - let env2 = set_universes u2 env1 in - let (lfj,u3) = execute_array mf env2 lf in - let env3 = set_universes u3 env2 in - (type_of_case env3 pj cj lfj, u3) - - | IsFix (vn,i,lar,lfi,vdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in - let fix = mkFix vn i larv lfi vdefv in - check_fix env fix; - (make_judge fix larv.(i), u1) - - | IsCoFix (i,lar,lfi,vdef) -> - let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in - let cofix = mkCoFix i larv lfi vdefv in - check_cofix env cofix; - (make_judge cofix larv.(i), u1) - - | IsSort (Prop c) -> - (type_of_prop_or_set c, u0) - - | IsSort (Type u) -> - type_of_type u u0 - - | IsAppL a -> - let la = Array.length a in - if la = 0 then error_cant_execute CCI env cstr; - let hd = a.(0) - and tl = Array.to_list (Array.sub a 1 (la - 1)) in - let (j,u1) = execute mf env hd in - let env1 = set_universes u1 env in - let (jl,u2) = execute_list mf env1 tl in - let env2 = set_universes u2 env1 in - apply_rel_list env2 mf.nocheck jl j - - | IsLambda (name,c1,c2) -> - let (j,u1) = execute mf env c1 in - let var = assumption_of_judgement env j in - let env1 = push_rel (name,var) (set_universes u1 env) in - let (j',u2) = execute mf env1 c2 in - let env2 = set_universes u2 env1 in - abs_rel env2 name var j' - - | IsProd (name,c1,c2) -> - let (j,u1) = execute mf env c1 in - let var = assumption_of_judgement env j in - let env1 = push_rel (name,var) (set_universes u1 env) in - let (j',u2) = execute mf env1 c2 in - let env2 = set_universes u2 env1 in - gen_rel env2 name var j' - - | IsCast (c,t) -> - let (cj,u1) = execute mf env c in - let env1 = set_universes u1 env in - let (tj,u2) = execute mf env1 t in - let env2 = set_universes u2 env1 in - (cast_rel env2 cj tj, u2) - - | _ -> error_cant_execute CCI env cstr - -and execute_fix mf env lar lfi vdef = - let (larj,u1) = execute_array mf env lar in - let env1 = set_universes u1 env in - let lara = Array.map (assumption_of_judgement env1) larj in - let nlara = - List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in - let env2 = - List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in - let (vdefj,u2) = execute_array mf env2 vdef in - let env3 = set_universes u2 env2 in - let vdefv = Array.map j_val_only vdefj in - let u3 = type_fixpoint env3 lfi lara vdefj in - (lara,vdefv,u3) - -and execute_array mf env v = - let (jl,u1) = execute_list mf env (Array.to_list v) in - (Array.of_list jl, u1) - -and execute_list mf env = function - | [] -> ([], universes env) - | c::r -> - let (j,u') = execute mf env c in - let (jr,u'') = execute_list mf (set_universes u' env) r in - (j::jr, u'') - - -(* The typed type of a judgment. *) - -let execute_type mf env constr = - let (j,_) = execute mf env constr in - typed_type_of_judgment env j - - -(* Exported machines. First safe machines, with no general fixpoint - allowed (the flag [fix] is not set) and all verifications done (the - flag [nocheck] is not set). *) - -let safe_machine env constr = - let mf = { fix = false; nocheck = false } in - execute mf env constr - -let safe_machine_type env constr = - let mf = { fix = false; nocheck = false } in - execute_type mf env constr - -(* Machines with general fixpoint. *) - -let fix_machine env constr = - let mf = { fix = true; nocheck = false } in - execute mf env constr - -let fix_machine_type env constr = - let mf = { fix = true; nocheck = false } in - execute_type mf env constr - -(* Fast machines without any verification. *) - -let unsafe_machine env constr = - let mf = { fix = true; nocheck = true } in - execute mf env constr - -let unsafe_machine_type env constr = - let mf = { fix = true; nocheck = true } in - execute_type mf env constr - - -(* ``Type of'' machines. *) - -let type_of env c = - let (j,_) = safe_machine env c in nf_betaiota env j.uj_type - -let type_of_type env c = - let tt = safe_machine_type env c in DOP0 (Sort tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_machine env c in nf_betaiota env j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) - - -(*s Machines with information. *) - -type information = Logic | Inf of unsafe_judgment - -(*i -let implicit_judgment = {body=mkImplicit;typ=implicit_sort} - -let add_inf_rel (na,inf) env = - match inf with - Logic -> add_rel (na,implicit_judgment) env - | Inf j -> add_rel (na,tjudge_of_judge j) env - - -let fw_mutind sigma fenv k = - let (sp,x,args) = destMutInd k in - let mis = mind_specif_of_mind k in - match mis_singl mis with - Some a -> Some (a,true) - | None -> - if is_info_cast_type sigma (mis_arity mis) then - let infK = - global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x))) - in Some (infK,false) - else None - -let inf_of_mind sigma fenv mind = - try - match fw_mutind sigma fenv mind with - Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK) - | None -> Logic - with - Not_found | Failure _ -> - anomaly "cannot convert an inductive to an finductive" - -let inf_mconstructor (sigma,metamap) fenv k = - let (sp,x,i,cl) = destMutConstruct k in - let mind = mkMutInd sp x cl in - (match fw_mutind sigma fenv mind with - None -> Logic - | Some(infi,singl) -> - (match mind_lamexp mind with - | Some clamexp -> - if singl - then Inf(cast_fmachine (sigma,[]) fenv clamexp) - else - let (infsp, infx, infcl) = destMutInd infi in - let infmconstructor = mkMutConstruct infsp infx i infcl in - let infval = subst1 infmconstructor clamexp in - Inf (cast_fmachine (sigma,fst metamap) fenv infval) - | _ -> assert false)) - - -exception DefinedExtraction - -(* when c is an evaluable constant with an extraction which - contains an implicit, gives the value of the c constant - otherwise raise DefinedExtraction -*) - -let value_implicit_const sigma c cinf = - match c with DOPN(Const(_),_) -> - if evaluable_const sigma c then - let cv = const_value sigma cinf in - if is_implicit cv (* or contains_implicit sigma cv *) - then const_value sigma c - else raise DefinedExtraction - else raise DefinedExtraction - | _ -> raise DefinedExtraction - -let unsafe_infmachine (sigma,metamap) env fenv c = - let rec infexec env fenv cstr = match cstr with - DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic - | DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic - | DOP2(Cast,c,_) -> infexec env fenv c - | DOP0(Meta n) -> - (match List.assoc n (snd metamap) with - Logic -> Logic - | Inf j -> Inf{uj_val=DOP0(Meta n); - uj_type=j.uj_val; - uj_kind = hnf_constr sigma j.uj_type}) - - | Rel n -> - inf_rel fenv - (contents_of_type sigma (snd (lookup_rel n env))) n - - | VAR str -> - inf_var fenv - (contents_of_type sigma (snd(lookup_glob str env))) str - - | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr - - | DOPN(Abst _,_) -> - if evaluable_abst cstr then infexec env fenv (abst_value cstr) - else error "cannot extract from an unevaluable abstraction" - - | DOP0(Sort s) -> inf_sort s - - | DOPN(AppL,tl) -> - let c1 = (hd_vect tl) - and cl = tl_vect tl in - let funinf = infexec env fenv c1 in - (match funinf with Logic -> Logic - | Inf(j) -> let cinf = j.uj_val in - (* try to expand constants corresponding - to non extractable terms *) - (try if is_extraction_expanded() then - let valcte = value_implicit_const sigma c1 cinf - in infexec env fenv (whd_betaiota (appvect(valcte,cl))) - else raise DefinedExtraction - with DefinedExtraction -> - let argsinf = Array.map (infexec env fenv) cl - in it_vect inf_apply funinf argsinf)) - - | DOP2(Lambda,c1,DLAM(name,c2)) -> - let varinf = infexec env fenv c1 in - let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env) - (add_inf_rel (name,varinf) fenv) c2 - in inf_abs_rel name bodyinf varinf - - | DOP2(Prod,c1,DLAM(name,c2)) -> - let c1inf = infexec env fenv c1 in - let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env) - (add_inf_rel (name,c1inf) fenv) c2 - in inf_gen_rel name c2inf c1inf - - | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr - - | DOPN(MutConstruct _,_) -> - inf_mconstructor (sigma,metamap) fenv cstr - - | DOPN(Fix(vn,i),cl) -> - let lar = Array.sub cl 0 ((Array.length cl) - 1) in - let inflar = Array.map (infexec env fenv) lar in - let infAi = inflar.(i) in - (match infAi with - Logic -> Logic - | Inf aij -> - let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in - let (new_env,new_fenv) = - it_vect2 - (fun (ne,nfe) fk ak -> - (add_rel (fk,tjudge_of_cast sigma ak) ne, - let infAk = infexec ne nfe ak - in (add_inf_rel (fk,infAk) nfe))) - (env,fenv) - (Array.of_list (List.rev lfi)) (vect_lift lar) in -(* a special function to localize the recursive index in the extracted term *) - let rec exec_def ne nfe n def = - (match hnf_constr sigma def with - DOP2(Lambda,c1,DLAM(name,c2)) -> - let varinf = infexec ne nfe c1 in - let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) - and nfe' = add_inf_rel (name,varinf) nfe in - if n = 0 then - let infc2 = infexec ne' nfe' c2 - in let infdef = inf_abs_rel name infc2 varinf - and index = - if varinf = Logic then -1 - (* the recursive call was on a non-informative term *) - else 0 in (infdef,index) - else - let bodyinf,countl = - exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) - (add_inf_rel (name,varinf) nfe) (n-1) c2 in - let (infabs,abs) = - inf_abs_rel_count name bodyinf varinf - in (infabs, - if abs = ERASE then countl - else if countl<0 then countl-1 - else countl+1) - | _ -> anomaly "exec_def : should be a lambda") in - let infdefs_ind = - map2_vect (exec_def new_env new_fenv) vn ldefs - in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind) - - | DOPN(CoFix i,cl) -> - let lar = Array.sub cl 0 ((Array.length cl) - 1) in - let inflar = Array.map (infexec env fenv) lar in - let infAi = inflar.(i) in - (match infAi with - Logic -> Logic - | Inf aij -> - let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in - let (new_env,new_fenv) = - it_vect2 (fun (ne,nfe) fk ak -> - (add_rel (fk,tjudge_of_cast sigma ak) ne, - let infAk = infexec ne nfe ak - in (add_inf_rel (fk,infAk) nfe))) - (env,fenv) - (Array.of_list (List.rev lfi)) (vect_lift lar) in - - let infdefs = Array.map (infexec new_env new_fenv) ldefs - in inf_cofix sigma i aij.uj_type lfi inflar infdefs) - - | DOPN(MutCase _,_) -> - let (ci,p,c,lf) = destCase cstr in - let pinf = infexec env fenv p in - (match pinf with - Logic -> Logic - | Inf pj -> - if is_extraction_expanded() then - let (d,l) = whd_betadeltaiota_stack sigma c [] in - (match d with (DOPN(MutConstruct(_,_),_)) -> - let cstr' = - DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf) - in infexec env fenv (whd_betaiota cstr') - | _ -> - let cinf = infexec env fenv c - and lfinf = Array.map (infexec env fenv) lf - in inf_mutcase fenv sigma pj ci cinf lfinf - ) - else let cinf = infexec env fenv c - and lfinf = Array.map (infexec env fenv) lf - in inf_mutcase fenv sigma pj ci cinf lfinf) - - | _ -> error "Cannot extract information" - in infexec env fenv c - - -let core_infmachine meta env fenv c = - try unsafe_infmachine meta env fenv c - with (UserError _ | Failure _) -> Logic - -(* WITH INFORMATION *) -(* does not check anymore that extracted terms are well-formed *) -let judgement_infmachine meta env fenv c ct = - try - match unsafe_infmachine meta env fenv c with - Inf infj -> - let inftyp = - try unsafe_infmachine meta env fenv ct - with (UserError _ | Failure _) -> - (warning "Failed to extract in type"; Logic) - in (match inftyp with - Inf infjt -> - Inf{uj_val=infj.uj_val; - uj_type=infjt.uj_val; - uj_kind=infj.uj_kind} - | Logic -> Inf infj) - | Logic -> Logic - with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic) - -let infmachine_type nocheck (sigma,metamap) env fenv constr = - let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in - let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in - let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in - let inf = - if is_info_type sigma t then (* Case the term is informative *) - let uniarc = get_uniarc () in - let infjt = - judgement_infmachine - (sigma,(constr_metamap,inf_metamap)) env fenv - t.body - (DOP0 (Sort t.typ)) in - let _ = set_uniarc uniarc in - infjt - else Logic - - in hash_jpair_type - ({body = strip_all_casts t.body; typ = t.typ}, - (inf_app (fun j -> {uj_val = nf_beta j.uj_val; - uj_type = nf_beta j.uj_type; - uj_kind = j.uj_kind }) inf)) - -let infmachine nocheck (sigma,metamap) env fenv constr = - let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in - let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in - let j = core_fmachine nocheck (sigma,constr_metamap) env constr in - let inf = - if is_info_judge sigma j then (* Case the term is informative *) - let uniarc = get_uniarc () in - let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in - let infjt = - judgement_infmachine - (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in - let _ = set_uniarc uniarc in - infjt - else Logic - - in hash_jpair - ({uj_val = strip_all_casts j.uj_val; - uj_type = strip_all_casts j.uj_type; - uj_kind = j.uj_kind}, - (inf_app (fun j -> {uj_val = nf_beta j.uj_val; - uj_type = nf_beta j.uj_type; - uj_kind = j.uj_kind }) inf)) - - -let jsign_of_sign sigma sign = - sign_it - (fun id a (sign,fsign) -> - let sign' = add_sign (id,a) sign in - let fsign' = - match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body - with - (_,Logic) -> fsign - | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign - in (sign',fsign')) - sign (([],[]),([],[])) - - -let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign) - -let infexemeta_type sigma metamap (env,fenv) c = - infmachine_type true (sigma,metamap) env fenv c - -let infexecute_rec_type sigma (env,fenv) c = - infmachine_type false (sigma,[]) env fenv c - -let infexecute_type sigma (sign,fsign) c = - infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c - -let infexemeta sigma metamap (env,fenv) c = - infmachine true (sigma,metamap) env fenv c - -let infexecute_rec sigma (env,fenv) c = - infmachine false (sigma,[]) env fenv c - -let infexecute sigma (sign,fsign) c = - infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c - -(* A adapter pour les nouveaux env -let fvar_type sigma (sign,fsign) v = - let na = destVar v in - let varty = (snd(lookup_sign na sign)) - in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with - Inf ft -> ft.uj_val - | Logic -> invalid_arg "Fvar with a non-informative type (1)!" - -*) - -(* MACHINE WITH UNIVERSES *) -(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab, - recuperer le graphe local, et restaurer l'acien graphe global *) - -let whd_instuni = function - DOP0(Sort(Type(u))) -> - let u = (if u = dummy_univ then new_univ() else u) - in DOP0(Sort(Type(u))) - | c -> c - -(* Instantiate universes: replace all dummy_univ by fresh universes. - This is already done by the machine. - Indtypes instantiates the universes itself, because in the case of - large constructor, additionnal constraints must be considered. *) -let instantiate_universes c = strong whd_instuni c - - -(* sp est le nom de la constante pour laquelle il faut que c soit bien type. - Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles - independamment. - Au lieu de sp, Lib.cwd() serait peut-etre suffisant. - Cela eviterai de donner un section-path quand on veut typer. *) -let fexecute_type_with_univ sigma sign sp c = - with_universes (fexecute_type sigma sign) (sp,initial_universes,c) - - -let fexecute_with_univ sigma sign sp c = - with_universes (fexecute sigma sign) (sp,initial_universes,c) - - -let infexecute_type_with_univ sigma psign sp c = - with_universes (infexecute_type sigma psign) (sp,initial_universes,c) - - -let infexecute_with_univ sigma psign sp c = - with_universes (infexecute sigma psign) (sp,initial_universes,c) -i*) diff --git a/kernel/mach.mli b/kernel/mach.mli deleted file mode 100644 index 9e37c4c798..0000000000 --- a/kernel/mach.mli +++ /dev/null @@ -1,48 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Pp -open Names -open Term -open Univ -open Environ -open Machops -(*i*) - -(*s Machines without information. *) - -val safe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes -val safe_machine_type : 'a unsafe_env -> constr -> typed_type - -val fix_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes -val fix_machine_type : 'a unsafe_env -> constr -> typed_type - -val unsafe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes -val unsafe_machine_type : 'a unsafe_env -> constr -> typed_type - -val type_of : 'a unsafe_env -> constr -> constr - -val type_of_type : 'a unsafe_env -> constr -> constr - -val unsafe_type_of : 'a unsafe_env -> constr -> constr - - -(*s Machine with information. *) - -type information = Logic | Inf of unsafe_judgment - -(*i -val infexemeta : - 'a unsafe_env -> constr -> unsafe_judgment * information * universes - -val infexecute_type : - 'a unsafe_env -> constr -> typed_type * information * universes - -val infexecute : - 'a unsafe_env -> constr -> unsafe_judgment * information * universes - -val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env - -val core_infmachine : 'a unsafe_env -> constr -> information -i*) diff --git a/kernel/machops.ml b/kernel/machops.ml deleted file mode 100644 index 23bac0b277..0000000000 --- a/kernel/machops.ml +++ /dev/null @@ -1,909 +0,0 @@ - -(* $Id$ *) - -open Pp -open Util -open Names -open Univ -open Generic -open Term -open Evd -open Constant -open Inductive -open Sign -open Environ -open Reduction -open Instantiate -open Type_errors - -let make_judge v tj = - { uj_val = v; - uj_type = tj.body; - uj_kind= DOP0 (Sort tj.typ) } - -let j_val_only j = j.uj_val -(* Faut-il caster ? *) -let j_val = j_val_only - -let j_val_cast j = mkCast j.uj_val j.uj_type - -let typed_type_of_judgment env j = - match whd_betadeltaiota env j.uj_type with - | DOP0(Sort s) -> { body = j.uj_val; typ = s } - | _ -> error_not_type CCI env j.uj_val - -let assumption_of_judgement env j = - match whd_betadeltaiota env j.uj_type with - | DOP0(Sort s) -> { body = j.uj_val; typ = s } - | _ -> error_assumption CCI env j.uj_val - -(* Type of a de Bruijn index. *) - -let relative env n = - try - let (_,typ) = lookup_rel n env in - { uj_val = Rel n; - uj_type = lift n typ.body; - uj_kind = DOP0 (Sort typ.typ) } - with Not_found -> - error_unbound_rel CCI env n - -(* Management of context of variables. *) - -(* Checks if a context of variable is included in another one. *) - -let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) = - let rec aux = function - | ([], [], _, _) -> true - | (_, _, [], []) -> false - | ((id1::idl1), (ty1::tyl1), idl2, tyl2) -> - let rec search = function - | ([], []) -> false - | ((id2::idl2), (ty2::tyl2)) -> - if id1 = id2 then - (is_conv env (body_of_type ty1) (body_of_type ty2)) - & aux (idl1,tyl1,idl2,tyl2) - else - search (idl2,tyl2) - | (_, _) -> invalid_arg "hyps_inclusion" - in - search (idl2,tyl2) - | (_, _, _, _) -> invalid_arg "hyps_inclusion" - in - aux (idl1,tyl1,idl2,tyl2) - -(* Checks if the given context of variables [hyps] is included in the - current context of [env]. *) - -let construct_reference id env hyps = - let hyps' = get_globals (context env) in - if hyps_inclusion env hyps hyps' then - Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) - else - error_reference_variables CCI env id - -let check_hyps id env hyps = - let hyps' = get_globals (context env) in - if not (hyps_inclusion env hyps hyps') then - error_reference_variables CCI env id - -(* Instantiation of terms on real arguments. *) - -let type_of_constant env c = - let (sp,args) = destConst c in - let cb = lookup_constant sp env in - let hyps = cb.const_hyps in - check_hyps (basename sp) env hyps; - instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) - -(* Existentials. *) - -let type_of_existential env c = - let (sp,args) = destConst c in - let info = Evd.map (evar_map env) sp in - let hyps = info.evar_hyps in - check_hyps (basename sp) env hyps; - instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args) - -(* Constants or existentials. *) - -let type_of_constant_or_existential env c = - if is_existential c then - type_of_existential env c - else - type_of_constant env c - -(* Inductive types. *) - -let instantiate_arity mis = - let ids = ids_of_sign mis.mis_mib.mind_hyps in - let args = Array.to_list mis.mis_args in - let arity = mis.mis_mip.mind_arity in - { body = instantiate_constr ids arity.body args; - typ = arity.typ } - -let type_of_inductive env i = - let mis = lookup_mind_specif i env in - let hyps = mis.mis_mib.mind_hyps in - check_hyps (basename mis.mis_sp) env hyps; - instantiate_arity mis - -(* Constructors. *) - -let instantiate_lc mis = - let hyps = mis.mis_mib.mind_hyps in - let lc = mis.mis_mip.mind_lc in - instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args) - -let type_of_constructor env c = - let (sp,i,j,args) = destMutConstruct c in - let mind = DOPN (MutInd (sp,i), args) in - let recmind = check_mrectype_spec env mind in - let mis = lookup_mind_specif recmind env in - check_hyps (basename mis.mis_sp) env (mis.mis_mib.mind_hyps); - let specif = instantiate_lc mis in - let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in - if j > mis_nconstr mis then - anomaly "type_of_constructor" - else - sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis)) - -(* gives the vector of constructors and of - types of constructors of an inductive definition - correctly instanciated *) - -let mis_type_mconstructs mis = - let specif = instantiate_lc mis - and ntypes = mis_ntypes mis - and nconstr = mis_nconstr mis in - let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) - and make_ck k = - DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args) - in - (Array.init nconstr make_ck, - sAPPVList specif (list_tabulate make_ik ntypes)) - -let type_mconstructs env mind = - let redmind = check_mrectype_spec env mind in - let mis = lookup_mind_specif redmind env in - mis_type_mconstructs mis - -(* Case. *) - -let rec sort_of_arity env c = - match whd_betadeltaiota env c with - | DOP0(Sort( _)) as c' -> c' - | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env c2 - | _ -> invalid_arg "sort_of_arity" - -let make_arity_dep env k = - let rec mrec c m = match whd_betadeltaiota env c with - | DOP0(Sort _) -> mkArrow m k - | DOP2(Prod,b,DLAM(n,c_0)) -> - prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1]))) - | _ -> invalid_arg "make_arity_dep" - in - mrec - -let make_arity_nodep env k = - let rec mrec c = match whd_betadeltaiota env c with - | DOP0(Sort _) -> k - | DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0)) - | _ -> invalid_arg "make_arity_nodep" - in - mrec - -let error_elim_expln env kp ki = - if is_info_sort env kp && not (is_info_sort env ki) then - "non-informative objects may not construct informative ones." - else - match (kp,ki) with - | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) -> - "strong elimination on non-small inductive types leads to paradoxes." - | _ -> "wrong arity" - -exception Arity of (constr * constr * string) option - -let is_correct_arity env kd kn (c,p) = - let rec srec ind (pt,t) = - try - (match whd_betadeltaiota env pt, whd_betadeltaiota env t with - | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) -> - if is_conv env a1 a1' then - srec (applist(lift 1 ind,[Rel 1])) (a2,a2') - else - raise (Arity None) - | DOP2(Prod,a1,DLAM(_,a2)), ki -> - let k = whd_betadeltaiota env a2 in - let ksort = (match k with DOP0(Sort s) -> s - | _ -> raise (Arity None)) in - if is_conv env a1 ind then - if List.exists (base_sort_cmp CONV ksort) kd then - (true,k) - else - raise (Arity (Some(k,ki,error_elim_expln env k ki))) - else - raise (Arity None) - | k, DOP2(Prod,_,_) -> - raise (Arity None) - | k, ki -> - let ksort = (match k with DOP0(Sort s) -> s - | _ -> raise (Arity None)) in - if List.exists (base_sort_cmp CONV ksort) kn then - false,k - else - raise (Arity (Some(k,ki,error_elim_expln env k ki)))) - with Arity kinds -> - let listarity = - (List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kd) - @(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kn) - in error_elim_arity CCI env ind listarity c p pt kinds - in srec - -let cast_instantiate_arity mis = - let tty = instantiate_arity mis in - DOP2 (Cast, tty.body, DOP0 (Sort tty.typ)) - -let find_case_dep_nparams env (c,p) (mind,largs) typP = - let mis = lookup_mind_specif mind env in - let nparams = mis_nparams mis - and kd = mis_kd mis - and kn = mis_kn mis - and t = cast_instantiate_arity mis in - let (globargs,la) = list_chop nparams largs in - let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in - let arity = applist(mind,globargs) in - let (dep,_) = is_correct_arity env kd kn (c,p) arity (typP,glob_t) in - (dep, (nparams, globargs,la)) - -let type_one_branch_dep (env,nparams,globargs,p) co t = - let rec typrec n c = - match whd_betadeltaiota env c with - | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2) - | x -> let lAV = destAppL (ensure_appl x) in - let (_,vargs) = array_chop (nparams+1) lAV in - applist - (appvect ((lift n p),vargs), - [applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))]) - in - typrec 0 (hnf_prod_applist env "type_case" t globargs) - -let type_one_branch_nodep (env,nparams,globargs,p) t = - let rec typrec n c = - match whd_betadeltaiota env c with - | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2)) - | x -> let lAV = destAppL(ensure_appl x) in - let (_,vargs) = array_chop (nparams+1) lAV in - appvect (lift n p,vargs) - in - typrec 0 (hnf_prod_applist env "type_case" t globargs) - -(* type_case_branches type un

Case c of ... end - ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc - pt = sorte de p - type_case_branches retourne (lb, lr); lb est le vecteur des types - attendus dans les branches du Case; lr est le type attendu du resultat - *) - -let type_case_branches env ct pt p c = - try - let ((mI,largs) as indt) = find_mrectype env ct in - let (dep,(nparams,globargs,la)) = - find_case_dep_nparams env (c,p) indt pt - in - let (lconstruct,ltypconstr) = type_mconstructs env mI in - if dep then - (mI, - array_map2 (type_one_branch_dep (env,nparams,globargs,p)) - lconstruct ltypconstr, - beta_applist (p,(la@[c]))) - else - (mI, - Array.map (type_one_branch_nodep (env,nparams,globargs,p)) - ltypconstr, - beta_applist (p,la)) - with Induc -> - error_case_not_inductive CCI env c ct - -let check_branches_message env (c,ct) (explft,lft) = - let n = Array.length explft - and expn = Array.length lft in - let rec check_conv i = - if not (i = n) then - if not (is_conv_leq env lft.(i) (explft.(i))) then - error_ill_formed_branch CCI env c i (nf_betaiota env lft.(i)) - (nf_betaiota env explft.(i)) - else - check_conv (i+1) - in - if n<>expn then error_number_branches CCI env c ct expn else check_conv 0 - -let type_of_case env pj cj lfj = - let lft = Array.map (fun j -> j.uj_type) lfj in - let (mind,bty,rslty) = - type_case_branches env cj.uj_type pj.uj_type pj.uj_val cj.uj_val in - let kind = sort_of_arity env pj.uj_type in - check_branches_message env (cj.uj_val,cj.uj_type) (bty,lft); - { uj_val = - mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj); - uj_type = rslty; - uj_kind = kind } - -(* Prop and Set *) - -let type_of_prop_or_set cts = - { uj_val = DOP0(Sort(Prop cts)); - uj_type = DOP0(Sort type_0); - uj_kind = DOP0(Sort type_1) } - -(* Type of Type(i). *) - -let type_of_type u g = - let (uu,g') = super u g in - let (uuu,g'') = super uu g' in - { uj_val = DOP0 (Sort (Type u)); - uj_type = DOP0 (Sort (Type uu)); - uj_kind = DOP0 (Sort (Type uuu)) }, - g'' - -let type_of_sort c g = - match c with - | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' - | DOP0 (Sort (Prop _)) -> mkType prop_univ, g - | DOP0 (Implicit) -> mkImplicit, g - | _ -> invalid_arg "type_of_sort" - -(* Type of a lambda-abstraction. *) - -let sort_of_product domsort rangsort g0 = - match rangsort with - (* Product rule (s,Prop,Prop) *) - | Prop _ -> rangsort, g0 - | Type u2 -> - (match domsort with - (* Product rule (Prop,Type_i,Type_i) *) - | Prop _ -> rangsort, g0 - (* Product rule (Type_i,Type_i,Type_i) *) - | Type u1 -> let (u12,g1) = sup u1 u2 g0 in Type u12, g1) - -let abs_rel env name var j = - let rngtyp = whd_betadeltaiota env j.uj_kind in - let cvar = incast_type var in - let (s,g) = sort_of_product var.typ (destSort rngtyp) (universes env) in - { uj_val = mkLambda name cvar (j_val j); - uj_type = mkProd name cvar j.uj_type; - uj_kind = mkSort s }, - g - -(* Type of a product. *) - -let gen_rel env name var j = - let jtyp = whd_betadeltaiota env j.uj_type in - let jkind = whd_betadeltaiota env j.uj_kind in - let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in - if isprop jkind then - error "Proof objects can only be abstracted" - else - match jtyp with - | DOP0(Sort s) -> - let (s',g) = sort_of_product var.typ s (universes env) in - let res_type = mkSort s' in - let (res_kind,g') = type_of_sort res_type g in - { uj_val = - mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j); - uj_type = res_type; - uj_kind = res_kind }, g' - | _ -> - error_generalization CCI env (name,var) j.uj_val - -(* Type of a cast. *) - -let cast_rel env cj tj = - if is_conv_leq env cj.uj_type tj.uj_val then - { uj_val = j_val_only cj; - uj_type = tj.uj_val; - uj_kind = whd_betadeltaiota env tj.uj_type } - else - error_actual_type CCI env cj tj - -(* Type of an application. *) - -let apply_rel_list env0 nocheck argjl funj = - let rec apply_rec env typ = function - | [] -> - { uj_val = applist (j_val_only funj, List.map j_val_only argjl); - uj_type = typ; - uj_kind = funj.uj_kind }, - universes env - | hj::restjl -> - match whd_betadeltaiota env typ with - | DOP2(Prod,c1,DLAM(_,c2)) -> - if nocheck then - apply_rec env (subst1 hj.uj_val c2) restjl - else - (match conv_leq env hj.uj_type c1 with - | Convertible g -> - let env' = set_universes g env in - apply_rec env' (subst1 hj.uj_val c2) restjl - | NotConvertible -> - error_cant_apply CCI env "Type Error" funj argjl) - | _ -> - error_cant_apply CCI env "Non-functional construction" funj argjl - in - apply_rec env0 funj.uj_type argjl - - -(* Fixpoints. *) - -(* Checking function for terms containing existential variables. - The function noccur_with_meta consideres the fact that - each existential variable (as well as each isevar) - in the term appears applied to its local context, - which may contain the CoFix variables. These occurrences of CoFix variables - are not considered *) - -let noccur_with_meta sigma n m term = - let rec occur_rec n = function - | Rel(p) -> if n<=p & p () - | DOPN(AppL,cl) -> - (match strip_outer_cast cl.(0) with - | DOP0 (Meta _) -> () - | _ -> Array.iter (occur_rec n) cl) - | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> () - | DOPN(op,cl) -> Array.iter (occur_rec n) cl - | DOPL(_,cl) -> List.iter (occur_rec n) cl - | DOP0(_) -> () - | DOP1(_,c) -> occur_rec n c - | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 - | DLAM(_,c) -> occur_rec (n+1) c - | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v - in - try (occur_rec n term; true) with Occur -> false - -(* Check if t is a subterm of Rel n, and gives its specification, - assuming lst already gives index of - subterms with corresponding specifications of recursive arguments *) - -(* A powerful notion of subterm *) - -let find_sorted_assoc p = - let rec findrec = function - | (a,ta)::l -> - if a < p then findrec l else if a = p then ta else raise Not_found - | _ -> raise Not_found - in - findrec - -let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) -let map_lift_fst = map_lift_fst_n 1 - -let rec instantiate_recarg sp lrc ra = - match ra with - | Mrec(j) -> Imbr(sp,j,lrc) - | Imbr(sp1,k,l) -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l) - | Norec -> Norec - | Param(k) -> List.nth lrc k - -(* propagate checking for F,incorporating recursive arguments *) -let check_term env mind_recvec f = - let rec crec n l (lrec,c) = - match (lrec,strip_outer_cast c) with - | (Param(_)::lr,DOP2(Lambda,_,DLAM(_,b))) -> - let l' = map_lift_fst l in - crec (n+1) l' (lr,b) - | (Norec::lr,DOP2(Lambda,_,DLAM(_,b))) -> - let l' = map_lift_fst l in - crec (n+1) l' (lr,b) - | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b))) -> - let l' = map_lift_fst l in - crec (n+1) ((1,mind_recvec.(i))::l') (lr,b) - | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> - let l' = map_lift_fst l in - let sprecargs = - mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in - let lc = - Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) - in - crec (n+1) ((1,lc)::l') (lr,b) - | _,f_0 -> f n l f_0 - in - crec - -let is_inst_var env k c = - match whd_betadeltaiota_stack env c [] with - | (Rel n,_) -> n=k - | _ -> false - -let is_subterm_specif env lcx mind_recvec = - let rec crec n lst c = - match whd_betadeltaiota_stack env c [] with - | ((Rel k),_) -> find_sorted_assoc k lst - | (DOPN(MutCase _,_) as x,_) -> - let ( _,_,c,br) = destCase x in - if Array.length br = 0 then - [||] - else - let lcv = - (try - if is_inst_var env n c then lcx else (crec n lst c) - with Not_found -> (Array.create (Array.length br) [])) - in - assert (Array.length br = Array.length lcv); - let stl = - array_map2 - (fun lc a -> - check_term env mind_recvec crec n lst (lc,a)) lcv br - in - stl.(0) - - | (DOPN(Fix(_),la) as mc,l) -> - let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in - let nbfix = List.length funnames in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let (gamma,strippedBody) = decompose_lam_n (decrArg+1) theBody in - let absTypes = List.map snd gamma in - let nbOfAbst = nbfix+decrArg+1 in - let newlst = - if List.length l < (decrArg+1) then - ((nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst)) - else - let theDecrArg = List.nth l decrArg in - let recArgsDecrArg = - try (crec n lst theDecrArg) - with Not_found -> Array.create 0 [] - in - if (Array.length recArgsDecrArg)=0 then - (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) - else - (1,recArgsDecrArg) :: - (nbOfAbst,lcx) :: - (map_lift_fst_n nbOfAbst lst) - in - crec (n+nbOfAbst) newlst strippedBody - - | (DOP2(Lambda,_,DLAM(_,b)),[]) -> - let lst' = map_lift_fst lst in - crec (n+1) lst' b - - (*** Experimental change *************************) - | (DOP0(Meta _),_) -> [||] - | _ -> raise Not_found - in - crec - -let is_subterm env lcx mind_recvec n lst c = - try - let _ = is_subterm_specif env lcx mind_recvec n lst c in true - with Not_found -> - false - -(* Auxiliary function: it checks a condition f depending on a deBrujin - index for a certain number of abstractions *) - -let rec check_subterm_rec_meta env vectn k def = - (k < 0) or - (let nfi = Array.length vectn in - (* check fi does not appear in the k+1 first abstractions, - gives the type of the k+1-eme abstraction *) - let rec check_occur n def = - (match strip_outer_cast def with - | DOP2(Lambda,a,DLAM(_,b)) -> - if noccur_with_meta (evar_map env) n nfi a then - if n = k+1 then (a,b) else check_occur (n+1) b - else - error "Bad occurrence of recursive call" - | _ -> error "Not enough abstractions in the definition") in - let (c,d) = check_occur 1 def in - let (mI, largs) = - (try find_minductype env c - with Induc -> error "Recursive definition on a non inductive type") in - let (sp,tyi,_) = destMutInd mI in - let mind_recvec = mis_recargs (lookup_mind_specif mI env) in - let lcx = mind_recvec.(tyi) in - (* n = decreasing argument in the definition; - lst = a mapping var |-> recargs - t = the term to be checked - *) - let rec check_rec_call n lst t = - (* n gives the index of the recursive variable *) - (noccur_with_meta (evar_map env) (n+k+1) nfi t) or - (* no recursive call in the term *) - (match whd_betadeltaiota_stack env t [] with - | (Rel p,l) -> - if n+k+1 <= p & p < n+k+nfi+1 then - (* recursive call *) - let glob = nfi+n+k-p in (* the index of the recursive call *) - let np = vectn.(glob) in (* the decreasing arg of the rec call *) - if List.length l > np then - (match list_chop np l with - (la,(z::lrest)) -> - if (is_subterm env lcx mind_recvec n lst z) - then List.for_all (check_rec_call n lst) (la@lrest) - else error "Recursive call applied to an illegal term" - | _ -> assert false) - else error "Not enough arguments for the recursive call" - else List.for_all (check_rec_call n lst) l - | (DOPN(MutCase _,_) as mc,l) -> - let (ci,p,c_0,lrest) = destCase mc in - let lc = - (try - if is_inst_var env n c_0 then - lcx - else - is_subterm_specif env lcx mind_recvec n lst c_0 - with Not_found -> - Array.create (Array.length lrest) []) - in - (array_for_all2 - (fun c_0 a -> - check_term env mind_recvec (check_rec_call) n lst (c_0,a)) - lc lrest) - && (List.for_all (check_rec_call n lst) (c_0::p::l)) - - (* Enables to traverse Fixpoint definitions in a more intelligent - way, ie, the rule : - - if - g = Fix g/1 := [y1:T1]...[yp:Tp]e & - - f is guarded with respect to the set of pattern variables S - in a1 ... am & - - f is guarded with respect to the set of pattern variables S - in T1 ... Tp & - - ap is a sub-term of the formal argument of f & - - f is guarded with respect to the set of pattern variables S+{yp} - in e - then f is guarded with respect to S in (g a1 ... am). - - Eduardo 7/9/98 *) - - | (DOPN(Fix(_),la) as mc,l) -> - (List.for_all (check_rec_call n lst) l) && - let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in - let nbfix = List.length funnames in - let decrArg = recindxs.(i) in - if (List.length l < (decrArg+1)) then - (array_for_all (check_rec_call n lst) la) - else - let theDecrArg = List.nth l decrArg in - let recArgsDecrArg = - try (is_subterm_specif env lcx mind_recvec n lst theDecrArg) - with Not_found -> Array.create 0 [] - in - if (Array.length recArgsDecrArg)=0 then - array_for_all (check_rec_call n lst) la - else - let theBody = bodies.(i) in - let (gamma,strippedBody) = - decompose_lam_n (decrArg+1) theBody in - let absTypes = List.map snd gamma in - let nbOfAbst = nbfix+decrArg+1 in - let newlst = - ((1,recArgsDecrArg)::(map_lift_fst_n nbOfAbst lst)) - in - ((array_for_all - (fun t -> check_rec_call n lst t) - typarray) && - (list_for_all_i (fun n -> check_rec_call n lst) n absTypes) & - (check_rec_call (n+nbOfAbst) newlst strippedBody)) - - - | (DOP2(_,a,b),l) -> - (check_rec_call n lst a) && - (check_rec_call n lst b) && - (List.for_all (check_rec_call n lst) l) - - | (DOPN(_,la),l) -> - (array_for_all (check_rec_call n lst) la) && - (List.for_all (check_rec_call n lst) l) - - | (DOP0 (Meta _),l) -> true - - | (DLAM(_,t),l) -> - (check_rec_call (n+1) (map_lift_fst lst) t) && - (List.for_all (check_rec_call n lst) l) - - | (DLAMV(_,vt),l) -> - (array_for_all (check_rec_call (n+1) (map_lift_fst lst)) vt) && - (List.for_all (check_rec_call n lst) l) - - | (_,l) -> List.for_all (check_rec_call n lst) l - ) - - in - check_rec_call 1 [] d) - -(* vargs is supposed to be built from A1;..Ak;[f1]..[fk][|d1;..;dk|] -and vdeft is [|t1;..;tk|] such that f1:A1,..,fk:Ak |- di:ti -nvect is [|n1;..;nk|] which gives for each recursive definition -the inductive-decreasing index -the function checks the convertibility of ti with Ai *) - -let check_fix env = function - | DOPN(Fix(nvect,j),vargs) -> - let nbfix = let nv = Array.length vargs in - if nv < 2 then error "Ill-formed recursive definition" else nv-1 in - let varit = Array.sub vargs 0 nbfix in - let ldef = array_last vargs in - let ln = Array.length nvect - and la = Array.length varit in - if ln <> la then - error "Ill-formed fix term" - else - let (lna,vdefs) = decomp_DLAMV_name ln ldef in - let vlna = Array.of_list lna in - let check_type i = - try - let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in () - with UserError (s,str) -> - error_ill_formed_rec_body CCI env str lna i vdefs - in - for i = 0 to ln-1 do check_type i done - - | _ -> assert false - -(* Co-fixpoints. *) - -let check_guard_rec_meta env nbfix def deftype = - let rec codomain_is_coind c = - match whd_betadeltaiota env (strip_outer_cast c) with - | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b - | b -> - (try find_mcoinductype env b - with - | Induc -> error "The codomain is not a coinductive type" - | _ -> error "Type of Cofix function not as expected") - in - let (mI, _) = codomain_is_coind deftype in - let (sp,tyi,_) = destMutInd mI in - let lvlra = (mis_recargs (lookup_mind_specif mI env)) in - let vlra = lvlra.(tyi) in - let evd = evar_map env in - let rec check_rec_call alreadygrd n vlra t = - if (noccur_with_meta evd n nbfix t) then - true - else - match whd_betadeltaiota_stack env t [] with - | (DOP0 (Meta _), l) -> true - - | (Rel p,l) -> - if n <= p && p < n+nbfix then - (* recursive call *) - if alreadygrd then - if List.for_all (noccur_with_meta evd n nbfix) l then - true - else - error "Nested recursive occurrences" - else - error "Unguarded recursive call" - else - error "check_guard_rec_meta: ???" - - | (DOPN ((MutConstruct((x,y),i)),l), args) -> - let lra =vlra.(i-1) in - let mI = DOPN(MutInd(x,y),l) in - let _,realargs = list_chop (mind_nparams env mI) args in - let rec process_args_of_constr l lra = - match l with - | [] -> true - | t::lr -> - (match lra with - | [] -> - anomalylabstrm "check_guard_rec_meta" - [< 'sTR "a constructor with an empty list"; - 'sTR "of recargs is being applied" >] - | (Mrec i)::lrar -> - let newvlra = lvlra.(i) in - (check_rec_call true n newvlra t) && - (process_args_of_constr lr lrar) - - | (Imbr(sp,i,lrc)::lrar) -> - let mis = - lookup_mind_specif (mkMutInd sp i [||]) env in - let sprecargs = mis_recargs mis in - let lc = (Array.map - (List.map - (instantiate_recarg sp lrc)) - sprecargs.(i)) - in (check_rec_call true n lc t) & - (process_args_of_constr lr lrar) - - | _::lrar -> - if (noccur_with_meta evd n nbfix t) - then (process_args_of_constr lr lrar) - else error "Recursive call inside a non-recursive argument of constructor") - in (process_args_of_constr realargs lra) - - - | (DOP2(Lambda,a,DLAM(_,b)),[]) -> - if (noccur_with_meta evd n nbfix a) then - check_rec_call alreadygrd (n+1) vlra b - else - error "Recursive call in the type of an abstraction" - - | (DOPN(CoFix(j),vargs),l) -> - let nbfix = let nv = Array.length vargs in - if nv < 2 then - error "Ill-formed recursive definition" - else - nv-1 - in - let varit = Array.sub vargs 0 nbfix in - let ldef = array_last vargs in - let la = Array.length varit in - let (lna,vdefs) = decomp_DLAMV_name la ldef in - let vlna = Array.of_list lna - in - if (array_for_all (noccur_with_meta evd n nbfix) varit) then - (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) - && - (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) - else - error "Recursive call in the type of a declaration" - - | (DOPN(MutCase _,_) as mc,l) -> - let (_,p,c,vrest) = destCase mc in - if (noccur_with_meta evd n nbfix p) then - if (noccur_with_meta evd n nbfix c) then - if (List.for_all (noccur_with_meta evd n nbfix) l) then - (array_for_all (check_rec_call alreadygrd n vlra) vrest) - else - error "Recursive call in the argument of a function defined by cases" - else - error "Recursive call in the argument of a case expression" - else - error "Recursive call in the type of a Case expression" - - | _ -> error "Definition not in guarded form" - - in - check_rec_call false 1 vlra def - -(* The function which checks that the whole block of definitions - satisfies the guarded condition *) - -let check_cofix env f = - match f with - | DOPN(CoFix(j),vargs) -> - let nbfix = let nv = Array.length vargs in - if nv < 2 then - error "Ill-formed recursive definition" - else - nv-1 - in - let varit = Array.sub vargs 0 nbfix in - let ldef = array_last vargs in - let la = Array.length varit in - let (lna,vdefs) = decomp_DLAMV_name la ldef in - let vlna = Array.of_list lna in - let check_type i = - (try - let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in () - with UserError (s,str) -> - error_ill_formed_rec_body CCI env str lna i vdefs) - in - for i = 0 to nbfix-1 do check_type i done - | _ -> assert false - -(* Checks the type of a (co)fixpoint. - Fix and CoFix are typed the same way; only the guard condition differs. *) - -exception IllBranch of int - -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in - assert (Array.length lar = lt); - try - let cv = - conv_forall2_i - (fun i e def ar -> - let c = conv_leq e def (lift lt ar) in - if c = NotConvertible then raise (IllBranch i) else c) - env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar) - in - begin match cv with - | Convertible g -> g - | NotConvertible -> assert false - end - with IllBranch i -> - error_ill_typed_rec_body CCI env i lna vdefj lar diff --git a/kernel/machops.mli b/kernel/machops.mli deleted file mode 100644 index 1a3b729c29..0000000000 --- a/kernel/machops.mli +++ /dev/null @@ -1,58 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Names -open Univ -open Term -open Environ -(*i*) - - -(* Base operations of the typing machine. *) - -val make_judge : constr -> typed_type -> unsafe_judgment - -val j_val_only : unsafe_judgment -> constr - -val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type - -val relative : 'a unsafe_env -> int -> unsafe_judgment - -val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type - -val type_of_inductive : 'a unsafe_env -> constr -> typed_type - -val type_of_constructor : 'a unsafe_env -> constr -> constr - -val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment - -> unsafe_judgment array -> unsafe_judgment - -val type_of_prop_or_set : contents -> unsafe_judgment - -val type_of_type : universe -> universes -> unsafe_judgment * universes - -val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type - -val abs_rel : - 'a unsafe_env -> name -> typed_type -> unsafe_judgment - -> unsafe_judgment * universes - -val gen_rel : - 'a unsafe_env -> name -> typed_type -> unsafe_judgment - -> unsafe_judgment * universes - -val cast_rel : - 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment - -val apply_rel_list : - 'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment - -> unsafe_judgment * universes - -val check_fix : 'a unsafe_env -> constr -> unit -val check_cofix : 'a unsafe_env -> constr -> unit - -val type_fixpoint : 'a unsafe_env -> name list -> typed_type array - -> unsafe_judgment array -> universes - - diff --git a/kernel/typeops.ml b/kernel/typeops.ml new file mode 100644 index 0000000000..23bac0b277 --- /dev/null +++ b/kernel/typeops.ml @@ -0,0 +1,909 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Evd +open Constant +open Inductive +open Sign +open Environ +open Reduction +open Instantiate +open Type_errors + +let make_judge v tj = + { uj_val = v; + uj_type = tj.body; + uj_kind= DOP0 (Sort tj.typ) } + +let j_val_only j = j.uj_val +(* Faut-il caster ? *) +let j_val = j_val_only + +let j_val_cast j = mkCast j.uj_val j.uj_type + +let typed_type_of_judgment env j = + match whd_betadeltaiota env j.uj_type with + | DOP0(Sort s) -> { body = j.uj_val; typ = s } + | _ -> error_not_type CCI env j.uj_val + +let assumption_of_judgement env j = + match whd_betadeltaiota env j.uj_type with + | DOP0(Sort s) -> { body = j.uj_val; typ = s } + | _ -> error_assumption CCI env j.uj_val + +(* Type of a de Bruijn index. *) + +let relative env n = + try + let (_,typ) = lookup_rel n env in + { uj_val = Rel n; + uj_type = lift n typ.body; + uj_kind = DOP0 (Sort typ.typ) } + with Not_found -> + error_unbound_rel CCI env n + +(* Management of context of variables. *) + +(* Checks if a context of variable is included in another one. *) + +let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) = + let rec aux = function + | ([], [], _, _) -> true + | (_, _, [], []) -> false + | ((id1::idl1), (ty1::tyl1), idl2, tyl2) -> + let rec search = function + | ([], []) -> false + | ((id2::idl2), (ty2::tyl2)) -> + if id1 = id2 then + (is_conv env (body_of_type ty1) (body_of_type ty2)) + & aux (idl1,tyl1,idl2,tyl2) + else + search (idl2,tyl2) + | (_, _) -> invalid_arg "hyps_inclusion" + in + search (idl2,tyl2) + | (_, _, _, _) -> invalid_arg "hyps_inclusion" + in + aux (idl1,tyl1,idl2,tyl2) + +(* Checks if the given context of variables [hyps] is included in the + current context of [env]. *) + +let construct_reference id env hyps = + let hyps' = get_globals (context env) in + if hyps_inclusion env hyps hyps' then + Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) + else + error_reference_variables CCI env id + +let check_hyps id env hyps = + let hyps' = get_globals (context env) in + if not (hyps_inclusion env hyps hyps') then + error_reference_variables CCI env id + +(* Instantiation of terms on real arguments. *) + +let type_of_constant env c = + let (sp,args) = destConst c in + let cb = lookup_constant sp env in + let hyps = cb.const_hyps in + check_hyps (basename sp) env hyps; + instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) + +(* Existentials. *) + +let type_of_existential env c = + let (sp,args) = destConst c in + let info = Evd.map (evar_map env) sp in + let hyps = info.evar_hyps in + check_hyps (basename sp) env hyps; + instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args) + +(* Constants or existentials. *) + +let type_of_constant_or_existential env c = + if is_existential c then + type_of_existential env c + else + type_of_constant env c + +(* Inductive types. *) + +let instantiate_arity mis = + let ids = ids_of_sign mis.mis_mib.mind_hyps in + let args = Array.to_list mis.mis_args in + let arity = mis.mis_mip.mind_arity in + { body = instantiate_constr ids arity.body args; + typ = arity.typ } + +let type_of_inductive env i = + let mis = lookup_mind_specif i env in + let hyps = mis.mis_mib.mind_hyps in + check_hyps (basename mis.mis_sp) env hyps; + instantiate_arity mis + +(* Constructors. *) + +let instantiate_lc mis = + let hyps = mis.mis_mib.mind_hyps in + let lc = mis.mis_mip.mind_lc in + instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args) + +let type_of_constructor env c = + let (sp,i,j,args) = destMutConstruct c in + let mind = DOPN (MutInd (sp,i), args) in + let recmind = check_mrectype_spec env mind in + let mis = lookup_mind_specif recmind env in + check_hyps (basename mis.mis_sp) env (mis.mis_mib.mind_hyps); + let specif = instantiate_lc mis in + let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in + if j > mis_nconstr mis then + anomaly "type_of_constructor" + else + sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis)) + +(* gives the vector of constructors and of + types of constructors of an inductive definition + correctly instanciated *) + +let mis_type_mconstructs mis = + let specif = instantiate_lc mis + and ntypes = mis_ntypes mis + and nconstr = mis_nconstr mis in + let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) + and make_ck k = + DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args) + in + (Array.init nconstr make_ck, + sAPPVList specif (list_tabulate make_ik ntypes)) + +let type_mconstructs env mind = + let redmind = check_mrectype_spec env mind in + let mis = lookup_mind_specif redmind env in + mis_type_mconstructs mis + +(* Case. *) + +let rec sort_of_arity env c = + match whd_betadeltaiota env c with + | DOP0(Sort( _)) as c' -> c' + | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env c2 + | _ -> invalid_arg "sort_of_arity" + +let make_arity_dep env k = + let rec mrec c m = match whd_betadeltaiota env c with + | DOP0(Sort _) -> mkArrow m k + | DOP2(Prod,b,DLAM(n,c_0)) -> + prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1]))) + | _ -> invalid_arg "make_arity_dep" + in + mrec + +let make_arity_nodep env k = + let rec mrec c = match whd_betadeltaiota env c with + | DOP0(Sort _) -> k + | DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0)) + | _ -> invalid_arg "make_arity_nodep" + in + mrec + +let error_elim_expln env kp ki = + if is_info_sort env kp && not (is_info_sort env ki) then + "non-informative objects may not construct informative ones." + else + match (kp,ki) with + | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) -> + "strong elimination on non-small inductive types leads to paradoxes." + | _ -> "wrong arity" + +exception Arity of (constr * constr * string) option + +let is_correct_arity env kd kn (c,p) = + let rec srec ind (pt,t) = + try + (match whd_betadeltaiota env pt, whd_betadeltaiota env t with + | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) -> + if is_conv env a1 a1' then + srec (applist(lift 1 ind,[Rel 1])) (a2,a2') + else + raise (Arity None) + | DOP2(Prod,a1,DLAM(_,a2)), ki -> + let k = whd_betadeltaiota env a2 in + let ksort = (match k with DOP0(Sort s) -> s + | _ -> raise (Arity None)) in + if is_conv env a1 ind then + if List.exists (base_sort_cmp CONV ksort) kd then + (true,k) + else + raise (Arity (Some(k,ki,error_elim_expln env k ki))) + else + raise (Arity None) + | k, DOP2(Prod,_,_) -> + raise (Arity None) + | k, ki -> + let ksort = (match k with DOP0(Sort s) -> s + | _ -> raise (Arity None)) in + if List.exists (base_sort_cmp CONV ksort) kn then + false,k + else + raise (Arity (Some(k,ki,error_elim_expln env k ki)))) + with Arity kinds -> + let listarity = + (List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kd) + @(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kn) + in error_elim_arity CCI env ind listarity c p pt kinds + in srec + +let cast_instantiate_arity mis = + let tty = instantiate_arity mis in + DOP2 (Cast, tty.body, DOP0 (Sort tty.typ)) + +let find_case_dep_nparams env (c,p) (mind,largs) typP = + let mis = lookup_mind_specif mind env in + let nparams = mis_nparams mis + and kd = mis_kd mis + and kn = mis_kn mis + and t = cast_instantiate_arity mis in + let (globargs,la) = list_chop nparams largs in + let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in + let arity = applist(mind,globargs) in + let (dep,_) = is_correct_arity env kd kn (c,p) arity (typP,glob_t) in + (dep, (nparams, globargs,la)) + +let type_one_branch_dep (env,nparams,globargs,p) co t = + let rec typrec n c = + match whd_betadeltaiota env c with + | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2) + | x -> let lAV = destAppL (ensure_appl x) in + let (_,vargs) = array_chop (nparams+1) lAV in + applist + (appvect ((lift n p),vargs), + [applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))]) + in + typrec 0 (hnf_prod_applist env "type_case" t globargs) + +let type_one_branch_nodep (env,nparams,globargs,p) t = + let rec typrec n c = + match whd_betadeltaiota env c with + | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2)) + | x -> let lAV = destAppL(ensure_appl x) in + let (_,vargs) = array_chop (nparams+1) lAV in + appvect (lift n p,vargs) + in + typrec 0 (hnf_prod_applist env "type_case" t globargs) + +(* type_case_branches type un

Case c of ... end + ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc + pt = sorte de p + type_case_branches retourne (lb, lr); lb est le vecteur des types + attendus dans les branches du Case; lr est le type attendu du resultat + *) + +let type_case_branches env ct pt p c = + try + let ((mI,largs) as indt) = find_mrectype env ct in + let (dep,(nparams,globargs,la)) = + find_case_dep_nparams env (c,p) indt pt + in + let (lconstruct,ltypconstr) = type_mconstructs env mI in + if dep then + (mI, + array_map2 (type_one_branch_dep (env,nparams,globargs,p)) + lconstruct ltypconstr, + beta_applist (p,(la@[c]))) + else + (mI, + Array.map (type_one_branch_nodep (env,nparams,globargs,p)) + ltypconstr, + beta_applist (p,la)) + with Induc -> + error_case_not_inductive CCI env c ct + +let check_branches_message env (c,ct) (explft,lft) = + let n = Array.length explft + and expn = Array.length lft in + let rec check_conv i = + if not (i = n) then + if not (is_conv_leq env lft.(i) (explft.(i))) then + error_ill_formed_branch CCI env c i (nf_betaiota env lft.(i)) + (nf_betaiota env explft.(i)) + else + check_conv (i+1) + in + if n<>expn then error_number_branches CCI env c ct expn else check_conv 0 + +let type_of_case env pj cj lfj = + let lft = Array.map (fun j -> j.uj_type) lfj in + let (mind,bty,rslty) = + type_case_branches env cj.uj_type pj.uj_type pj.uj_val cj.uj_val in + let kind = sort_of_arity env pj.uj_type in + check_branches_message env (cj.uj_val,cj.uj_type) (bty,lft); + { uj_val = + mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj); + uj_type = rslty; + uj_kind = kind } + +(* Prop and Set *) + +let type_of_prop_or_set cts = + { uj_val = DOP0(Sort(Prop cts)); + uj_type = DOP0(Sort type_0); + uj_kind = DOP0(Sort type_1) } + +(* Type of Type(i). *) + +let type_of_type u g = + let (uu,g') = super u g in + let (uuu,g'') = super uu g' in + { uj_val = DOP0 (Sort (Type u)); + uj_type = DOP0 (Sort (Type uu)); + uj_kind = DOP0 (Sort (Type uuu)) }, + g'' + +let type_of_sort c g = + match c with + | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' + | DOP0 (Sort (Prop _)) -> mkType prop_univ, g + | DOP0 (Implicit) -> mkImplicit, g + | _ -> invalid_arg "type_of_sort" + +(* Type of a lambda-abstraction. *) + +let sort_of_product domsort rangsort g0 = + match rangsort with + (* Product rule (s,Prop,Prop) *) + | Prop _ -> rangsort, g0 + | Type u2 -> + (match domsort with + (* Product rule (Prop,Type_i,Type_i) *) + | Prop _ -> rangsort, g0 + (* Product rule (Type_i,Type_i,Type_i) *) + | Type u1 -> let (u12,g1) = sup u1 u2 g0 in Type u12, g1) + +let abs_rel env name var j = + let rngtyp = whd_betadeltaiota env j.uj_kind in + let cvar = incast_type var in + let (s,g) = sort_of_product var.typ (destSort rngtyp) (universes env) in + { uj_val = mkLambda name cvar (j_val j); + uj_type = mkProd name cvar j.uj_type; + uj_kind = mkSort s }, + g + +(* Type of a product. *) + +let gen_rel env name var j = + let jtyp = whd_betadeltaiota env j.uj_type in + let jkind = whd_betadeltaiota env j.uj_kind in + let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in + if isprop jkind then + error "Proof objects can only be abstracted" + else + match jtyp with + | DOP0(Sort s) -> + let (s',g) = sort_of_product var.typ s (universes env) in + let res_type = mkSort s' in + let (res_kind,g') = type_of_sort res_type g in + { uj_val = + mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j); + uj_type = res_type; + uj_kind = res_kind }, g' + | _ -> + error_generalization CCI env (name,var) j.uj_val + +(* Type of a cast. *) + +let cast_rel env cj tj = + if is_conv_leq env cj.uj_type tj.uj_val then + { uj_val = j_val_only cj; + uj_type = tj.uj_val; + uj_kind = whd_betadeltaiota env tj.uj_type } + else + error_actual_type CCI env cj tj + +(* Type of an application. *) + +let apply_rel_list env0 nocheck argjl funj = + let rec apply_rec env typ = function + | [] -> + { uj_val = applist (j_val_only funj, List.map j_val_only argjl); + uj_type = typ; + uj_kind = funj.uj_kind }, + universes env + | hj::restjl -> + match whd_betadeltaiota env typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + if nocheck then + apply_rec env (subst1 hj.uj_val c2) restjl + else + (match conv_leq env hj.uj_type c1 with + | Convertible g -> + let env' = set_universes g env in + apply_rec env' (subst1 hj.uj_val c2) restjl + | NotConvertible -> + error_cant_apply CCI env "Type Error" funj argjl) + | _ -> + error_cant_apply CCI env "Non-functional construction" funj argjl + in + apply_rec env0 funj.uj_type argjl + + +(* Fixpoints. *) + +(* Checking function for terms containing existential variables. + The function noccur_with_meta consideres the fact that + each existential variable (as well as each isevar) + in the term appears applied to its local context, + which may contain the CoFix variables. These occurrences of CoFix variables + are not considered *) + +let noccur_with_meta sigma n m term = + let rec occur_rec n = function + | Rel(p) -> if n<=p & p () + | DOPN(AppL,cl) -> + (match strip_outer_cast cl.(0) with + | DOP0 (Meta _) -> () + | _ -> Array.iter (occur_rec n) cl) + | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> () + | DOPN(op,cl) -> Array.iter (occur_rec n) cl + | DOPL(_,cl) -> List.iter (occur_rec n) cl + | DOP0(_) -> () + | DOP1(_,c) -> occur_rec n c + | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 + | DLAM(_,c) -> occur_rec (n+1) c + | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v + in + try (occur_rec n term; true) with Occur -> false + +(* Check if t is a subterm of Rel n, and gives its specification, + assuming lst already gives index of + subterms with corresponding specifications of recursive arguments *) + +(* A powerful notion of subterm *) + +let find_sorted_assoc p = + let rec findrec = function + | (a,ta)::l -> + if a < p then findrec l else if a = p then ta else raise Not_found + | _ -> raise Not_found + in + findrec + +let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) +let map_lift_fst = map_lift_fst_n 1 + +let rec instantiate_recarg sp lrc ra = + match ra with + | Mrec(j) -> Imbr(sp,j,lrc) + | Imbr(sp1,k,l) -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l) + | Norec -> Norec + | Param(k) -> List.nth lrc k + +(* propagate checking for F,incorporating recursive arguments *) +let check_term env mind_recvec f = + let rec crec n l (lrec,c) = + match (lrec,strip_outer_cast c) with + | (Param(_)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) l' (lr,b) + | (Norec::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) l' (lr,b) + | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + crec (n+1) ((1,mind_recvec.(i))::l') (lr,b) + | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + let l' = map_lift_fst l in + let sprecargs = + mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in + let lc = + Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) + in + crec (n+1) ((1,lc)::l') (lr,b) + | _,f_0 -> f n l f_0 + in + crec + +let is_inst_var env k c = + match whd_betadeltaiota_stack env c [] with + | (Rel n,_) -> n=k + | _ -> false + +let is_subterm_specif env lcx mind_recvec = + let rec crec n lst c = + match whd_betadeltaiota_stack env c [] with + | ((Rel k),_) -> find_sorted_assoc k lst + | (DOPN(MutCase _,_) as x,_) -> + let ( _,_,c,br) = destCase x in + if Array.length br = 0 then + [||] + else + let lcv = + (try + if is_inst_var env n c then lcx else (crec n lst c) + with Not_found -> (Array.create (Array.length br) [])) + in + assert (Array.length br = Array.length lcv); + let stl = + array_map2 + (fun lc a -> + check_term env mind_recvec crec n lst (lc,a)) lcv br + in + stl.(0) + + | (DOPN(Fix(_),la) as mc,l) -> + let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in + let nbfix = List.length funnames in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let (gamma,strippedBody) = decompose_lam_n (decrArg+1) theBody in + let absTypes = List.map snd gamma in + let nbOfAbst = nbfix+decrArg+1 in + let newlst = + if List.length l < (decrArg+1) then + ((nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst)) + else + let theDecrArg = List.nth l decrArg in + let recArgsDecrArg = + try (crec n lst theDecrArg) + with Not_found -> Array.create 0 [] + in + if (Array.length recArgsDecrArg)=0 then + (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) + else + (1,recArgsDecrArg) :: + (nbOfAbst,lcx) :: + (map_lift_fst_n nbOfAbst lst) + in + crec (n+nbOfAbst) newlst strippedBody + + | (DOP2(Lambda,_,DLAM(_,b)),[]) -> + let lst' = map_lift_fst lst in + crec (n+1) lst' b + + (*** Experimental change *************************) + | (DOP0(Meta _),_) -> [||] + | _ -> raise Not_found + in + crec + +let is_subterm env lcx mind_recvec n lst c = + try + let _ = is_subterm_specif env lcx mind_recvec n lst c in true + with Not_found -> + false + +(* Auxiliary function: it checks a condition f depending on a deBrujin + index for a certain number of abstractions *) + +let rec check_subterm_rec_meta env vectn k def = + (k < 0) or + (let nfi = Array.length vectn in + (* check fi does not appear in the k+1 first abstractions, + gives the type of the k+1-eme abstraction *) + let rec check_occur n def = + (match strip_outer_cast def with + | DOP2(Lambda,a,DLAM(_,b)) -> + if noccur_with_meta (evar_map env) n nfi a then + if n = k+1 then (a,b) else check_occur (n+1) b + else + error "Bad occurrence of recursive call" + | _ -> error "Not enough abstractions in the definition") in + let (c,d) = check_occur 1 def in + let (mI, largs) = + (try find_minductype env c + with Induc -> error "Recursive definition on a non inductive type") in + let (sp,tyi,_) = destMutInd mI in + let mind_recvec = mis_recargs (lookup_mind_specif mI env) in + let lcx = mind_recvec.(tyi) in + (* n = decreasing argument in the definition; + lst = a mapping var |-> recargs + t = the term to be checked + *) + let rec check_rec_call n lst t = + (* n gives the index of the recursive variable *) + (noccur_with_meta (evar_map env) (n+k+1) nfi t) or + (* no recursive call in the term *) + (match whd_betadeltaiota_stack env t [] with + | (Rel p,l) -> + if n+k+1 <= p & p < n+k+nfi+1 then + (* recursive call *) + let glob = nfi+n+k-p in (* the index of the recursive call *) + let np = vectn.(glob) in (* the decreasing arg of the rec call *) + if List.length l > np then + (match list_chop np l with + (la,(z::lrest)) -> + if (is_subterm env lcx mind_recvec n lst z) + then List.for_all (check_rec_call n lst) (la@lrest) + else error "Recursive call applied to an illegal term" + | _ -> assert false) + else error "Not enough arguments for the recursive call" + else List.for_all (check_rec_call n lst) l + | (DOPN(MutCase _,_) as mc,l) -> + let (ci,p,c_0,lrest) = destCase mc in + let lc = + (try + if is_inst_var env n c_0 then + lcx + else + is_subterm_specif env lcx mind_recvec n lst c_0 + with Not_found -> + Array.create (Array.length lrest) []) + in + (array_for_all2 + (fun c_0 a -> + check_term env mind_recvec (check_rec_call) n lst (c_0,a)) + lc lrest) + && (List.for_all (check_rec_call n lst) (c_0::p::l)) + + (* Enables to traverse Fixpoint definitions in a more intelligent + way, ie, the rule : + + if - g = Fix g/1 := [y1:T1]...[yp:Tp]e & + - f is guarded with respect to the set of pattern variables S + in a1 ... am & + - f is guarded with respect to the set of pattern variables S + in T1 ... Tp & + - ap is a sub-term of the formal argument of f & + - f is guarded with respect to the set of pattern variables S+{yp} + in e + then f is guarded with respect to S in (g a1 ... am). + + Eduardo 7/9/98 *) + + | (DOPN(Fix(_),la) as mc,l) -> + (List.for_all (check_rec_call n lst) l) && + let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in + let nbfix = List.length funnames in + let decrArg = recindxs.(i) in + if (List.length l < (decrArg+1)) then + (array_for_all (check_rec_call n lst) la) + else + let theDecrArg = List.nth l decrArg in + let recArgsDecrArg = + try (is_subterm_specif env lcx mind_recvec n lst theDecrArg) + with Not_found -> Array.create 0 [] + in + if (Array.length recArgsDecrArg)=0 then + array_for_all (check_rec_call n lst) la + else + let theBody = bodies.(i) in + let (gamma,strippedBody) = + decompose_lam_n (decrArg+1) theBody in + let absTypes = List.map snd gamma in + let nbOfAbst = nbfix+decrArg+1 in + let newlst = + ((1,recArgsDecrArg)::(map_lift_fst_n nbOfAbst lst)) + in + ((array_for_all + (fun t -> check_rec_call n lst t) + typarray) && + (list_for_all_i (fun n -> check_rec_call n lst) n absTypes) & + (check_rec_call (n+nbOfAbst) newlst strippedBody)) + + + | (DOP2(_,a,b),l) -> + (check_rec_call n lst a) && + (check_rec_call n lst b) && + (List.for_all (check_rec_call n lst) l) + + | (DOPN(_,la),l) -> + (array_for_all (check_rec_call n lst) la) && + (List.for_all (check_rec_call n lst) l) + + | (DOP0 (Meta _),l) -> true + + | (DLAM(_,t),l) -> + (check_rec_call (n+1) (map_lift_fst lst) t) && + (List.for_all (check_rec_call n lst) l) + + | (DLAMV(_,vt),l) -> + (array_for_all (check_rec_call (n+1) (map_lift_fst lst)) vt) && + (List.for_all (check_rec_call n lst) l) + + | (_,l) -> List.for_all (check_rec_call n lst) l + ) + + in + check_rec_call 1 [] d) + +(* vargs is supposed to be built from A1;..Ak;[f1]..[fk][|d1;..;dk|] +and vdeft is [|t1;..;tk|] such that f1:A1,..,fk:Ak |- di:ti +nvect is [|n1;..;nk|] which gives for each recursive definition +the inductive-decreasing index +the function checks the convertibility of ti with Ai *) + +let check_fix env = function + | DOPN(Fix(nvect,j),vargs) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then error "Ill-formed recursive definition" else nv-1 in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let ln = Array.length nvect + and la = Array.length varit in + if ln <> la then + error "Ill-formed fix term" + else + let (lna,vdefs) = decomp_DLAMV_name ln ldef in + let vlna = Array.of_list lna in + let check_type i = + try + let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in () + with UserError (s,str) -> + error_ill_formed_rec_body CCI env str lna i vdefs + in + for i = 0 to ln-1 do check_type i done + + | _ -> assert false + +(* Co-fixpoints. *) + +let check_guard_rec_meta env nbfix def deftype = + let rec codomain_is_coind c = + match whd_betadeltaiota env (strip_outer_cast c) with + | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b + | b -> + (try find_mcoinductype env b + with + | Induc -> error "The codomain is not a coinductive type" + | _ -> error "Type of Cofix function not as expected") + in + let (mI, _) = codomain_is_coind deftype in + let (sp,tyi,_) = destMutInd mI in + let lvlra = (mis_recargs (lookup_mind_specif mI env)) in + let vlra = lvlra.(tyi) in + let evd = evar_map env in + let rec check_rec_call alreadygrd n vlra t = + if (noccur_with_meta evd n nbfix t) then + true + else + match whd_betadeltaiota_stack env t [] with + | (DOP0 (Meta _), l) -> true + + | (Rel p,l) -> + if n <= p && p < n+nbfix then + (* recursive call *) + if alreadygrd then + if List.for_all (noccur_with_meta evd n nbfix) l then + true + else + error "Nested recursive occurrences" + else + error "Unguarded recursive call" + else + error "check_guard_rec_meta: ???" + + | (DOPN ((MutConstruct((x,y),i)),l), args) -> + let lra =vlra.(i-1) in + let mI = DOPN(MutInd(x,y),l) in + let _,realargs = list_chop (mind_nparams env mI) args in + let rec process_args_of_constr l lra = + match l with + | [] -> true + | t::lr -> + (match lra with + | [] -> + anomalylabstrm "check_guard_rec_meta" + [< 'sTR "a constructor with an empty list"; + 'sTR "of recargs is being applied" >] + | (Mrec i)::lrar -> + let newvlra = lvlra.(i) in + (check_rec_call true n newvlra t) && + (process_args_of_constr lr lrar) + + | (Imbr(sp,i,lrc)::lrar) -> + let mis = + lookup_mind_specif (mkMutInd sp i [||]) env in + let sprecargs = mis_recargs mis in + let lc = (Array.map + (List.map + (instantiate_recarg sp lrc)) + sprecargs.(i)) + in (check_rec_call true n lc t) & + (process_args_of_constr lr lrar) + + | _::lrar -> + if (noccur_with_meta evd n nbfix t) + then (process_args_of_constr lr lrar) + else error "Recursive call inside a non-recursive argument of constructor") + in (process_args_of_constr realargs lra) + + + | (DOP2(Lambda,a,DLAM(_,b)),[]) -> + if (noccur_with_meta evd n nbfix a) then + check_rec_call alreadygrd (n+1) vlra b + else + error "Recursive call in the type of an abstraction" + + | (DOPN(CoFix(j),vargs),l) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then + error "Ill-formed recursive definition" + else + nv-1 + in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let la = Array.length varit in + let (lna,vdefs) = decomp_DLAMV_name la ldef in + let vlna = Array.of_list lna + in + if (array_for_all (noccur_with_meta evd n nbfix) varit) then + (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) + && + (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) + else + error "Recursive call in the type of a declaration" + + | (DOPN(MutCase _,_) as mc,l) -> + let (_,p,c,vrest) = destCase mc in + if (noccur_with_meta evd n nbfix p) then + if (noccur_with_meta evd n nbfix c) then + if (List.for_all (noccur_with_meta evd n nbfix) l) then + (array_for_all (check_rec_call alreadygrd n vlra) vrest) + else + error "Recursive call in the argument of a function defined by cases" + else + error "Recursive call in the argument of a case expression" + else + error "Recursive call in the type of a Case expression" + + | _ -> error "Definition not in guarded form" + + in + check_rec_call false 1 vlra def + +(* The function which checks that the whole block of definitions + satisfies the guarded condition *) + +let check_cofix env f = + match f with + | DOPN(CoFix(j),vargs) -> + let nbfix = let nv = Array.length vargs in + if nv < 2 then + error "Ill-formed recursive definition" + else + nv-1 + in + let varit = Array.sub vargs 0 nbfix in + let ldef = array_last vargs in + let la = Array.length varit in + let (lna,vdefs) = decomp_DLAMV_name la ldef in + let vlna = Array.of_list lna in + let check_type i = + (try + let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in () + with UserError (s,str) -> + error_ill_formed_rec_body CCI env str lna i vdefs) + in + for i = 0 to nbfix-1 do check_type i done + | _ -> assert false + +(* Checks the type of a (co)fixpoint. + Fix and CoFix are typed the same way; only the guard condition differs. *) + +exception IllBranch of int + +let type_fixpoint env lna lar vdefj = + let lt = Array.length vdefj in + assert (Array.length lar = lt); + try + let cv = + conv_forall2_i + (fun i e def ar -> + let c = conv_leq e def (lift lt ar) in + if c = NotConvertible then raise (IllBranch i) else c) + env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar) + in + begin match cv with + | Convertible g -> g + | NotConvertible -> assert false + end + with IllBranch i -> + error_ill_typed_rec_body CCI env i lna vdefj lar diff --git a/kernel/typeops.mli b/kernel/typeops.mli new file mode 100644 index 0000000000..1a3b729c29 --- /dev/null +++ b/kernel/typeops.mli @@ -0,0 +1,58 @@ + +(* $Id$ *) + +(*i*) +open Names +open Univ +open Term +open Environ +(*i*) + + +(* Base operations of the typing machine. *) + +val make_judge : constr -> typed_type -> unsafe_judgment + +val j_val_only : unsafe_judgment -> constr + +val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type + +val relative : 'a unsafe_env -> int -> unsafe_judgment + +val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type + +val type_of_inductive : 'a unsafe_env -> constr -> typed_type + +val type_of_constructor : 'a unsafe_env -> constr -> constr + +val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment + -> unsafe_judgment array -> unsafe_judgment + +val type_of_prop_or_set : contents -> unsafe_judgment + +val type_of_type : universe -> universes -> unsafe_judgment * universes + +val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type + +val abs_rel : + 'a unsafe_env -> name -> typed_type -> unsafe_judgment + -> unsafe_judgment * universes + +val gen_rel : + 'a unsafe_env -> name -> typed_type -> unsafe_judgment + -> unsafe_judgment * universes + +val cast_rel : + 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment + +val apply_rel_list : + 'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment + -> unsafe_judgment * universes + +val check_fix : 'a unsafe_env -> constr -> unit +val check_cofix : 'a unsafe_env -> constr -> unit + +val type_fixpoint : 'a unsafe_env -> name list -> typed_type array + -> unsafe_judgment array -> universes + + diff --git a/kernel/typing.ml b/kernel/typing.ml new file mode 100644 index 0000000000..2311fb9992 --- /dev/null +++ b/kernel/typing.ml @@ -0,0 +1,600 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Reduction +open Sign +open Environ +open Type_errors +open Machops + +(* Fonctions temporaires pour relier la forme castée de la forme jugement *) + +let tjudge_of_cast env = function + | DOP2 (Cast, b, t) -> + (match whd_betadeltaiota env t with + | DOP0 (Sort s) -> {body=b; typ=s} + | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]" + | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]") + | _ -> anomaly "Not casted (tjudge_of_cast)" + +let tjudge_of_judge env j = + { body = j.uj_val; + typ = match whd_betadeltaiota env j.uj_type with + (* Nécessaire pour ZFC *) + | DOP0 (Sort s) -> s + | DOP0 Implicit -> anomaly "Tiens, un implicit" + | _ -> anomaly "Not a type (tjudge_ofjudge)" } + +let vect_lift = Array.mapi lift +let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) + +(*s The machine flags. + [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$) + like [Acc_rec.fw]. + [nocheck] indicates if we can skip some verifications to accelerate + the type inference. *) + +type 'a mach_flags = { + fix : bool; + nocheck : bool } + +(* The typing machine without information. *) + +let rec execute mf env cstr = + let u0 = universes env in + match kind_of_term cstr with + | IsMeta n -> + let metaty = + try lookup_meta n env + with Not_found -> error "A variable remains non instanciated" + in + (match kind_of_term metaty with + | IsCast (typ,kind) -> + ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0) + | _ -> + let (jty,u1) = execute mf env metaty in + let k = hnf_constr env jty.uj_type in + ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1)) + + | IsRel n -> + (relative env n, u0) + + | IsVar id -> + (make_judge cstr (snd (lookup_var id env)), u0) + + | IsAbst _ -> + if evaluable_abst env cstr then + execute mf env (abst_value env cstr) + else + error "Cannot typecheck an unevaluable abstraction" + + | IsConst _ -> + (make_judge cstr (type_of_constant_or_existential env cstr), u0) + + | IsMutInd _ -> + (make_judge cstr (type_of_inductive env cstr), u0) + + | IsMutConstruct _ -> + let (typ,kind) = destCast (type_of_constructor env cstr) in + ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0) + + | IsMutCase (_,p,c,lf) -> + let (cj,u1) = execute mf env c in + let env1 = set_universes u1 env in + let (pj,u2) = execute mf env1 p in + let env2 = set_universes u2 env1 in + let (lfj,u3) = execute_array mf env2 lf in + let env3 = set_universes u3 env2 in + (type_of_case env3 pj cj lfj, u3) + + | IsFix (vn,i,lar,lfi,vdef) -> + if (not mf.fix) && array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in + let fix = mkFix vn i larv lfi vdefv in + check_fix env fix; + (make_judge fix larv.(i), u1) + + | IsCoFix (i,lar,lfi,vdef) -> + let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in + let cofix = mkCoFix i larv lfi vdefv in + check_cofix env cofix; + (make_judge cofix larv.(i), u1) + + | IsSort (Prop c) -> + (type_of_prop_or_set c, u0) + + | IsSort (Type u) -> + type_of_type u u0 + + | IsAppL a -> + let la = Array.length a in + if la = 0 then error_cant_execute CCI env cstr; + let hd = a.(0) + and tl = Array.to_list (Array.sub a 1 (la - 1)) in + let (j,u1) = execute mf env hd in + let env1 = set_universes u1 env in + let (jl,u2) = execute_list mf env1 tl in + let env2 = set_universes u2 env1 in + apply_rel_list env2 mf.nocheck jl j + + | IsLambda (name,c1,c2) -> + let (j,u1) = execute mf env c1 in + let var = assumption_of_judgement env j in + let env1 = push_rel (name,var) (set_universes u1 env) in + let (j',u2) = execute mf env1 c2 in + let env2 = set_universes u2 env1 in + abs_rel env2 name var j' + + | IsProd (name,c1,c2) -> + let (j,u1) = execute mf env c1 in + let var = assumption_of_judgement env j in + let env1 = push_rel (name,var) (set_universes u1 env) in + let (j',u2) = execute mf env1 c2 in + let env2 = set_universes u2 env1 in + gen_rel env2 name var j' + + | IsCast (c,t) -> + let (cj,u1) = execute mf env c in + let env1 = set_universes u1 env in + let (tj,u2) = execute mf env1 t in + let env2 = set_universes u2 env1 in + (cast_rel env2 cj tj, u2) + + | _ -> error_cant_execute CCI env cstr + +and execute_fix mf env lar lfi vdef = + let (larj,u1) = execute_array mf env lar in + let env1 = set_universes u1 env in + let lara = Array.map (assumption_of_judgement env1) larj in + let nlara = + List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in + let env2 = + List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in + let (vdefj,u2) = execute_array mf env2 vdef in + let env3 = set_universes u2 env2 in + let vdefv = Array.map j_val_only vdefj in + let u3 = type_fixpoint env3 lfi lara vdefj in + (lara,vdefv,u3) + +and execute_array mf env v = + let (jl,u1) = execute_list mf env (Array.to_list v) in + (Array.of_list jl, u1) + +and execute_list mf env = function + | [] -> ([], universes env) + | c::r -> + let (j,u') = execute mf env c in + let (jr,u'') = execute_list mf (set_universes u' env) r in + (j::jr, u'') + + +(* The typed type of a judgment. *) + +let execute_type mf env constr = + let (j,_) = execute mf env constr in + typed_type_of_judgment env j + + +(* Exported machines. First safe machines, with no general fixpoint + allowed (the flag [fix] is not set) and all verifications done (the + flag [nocheck] is not set). *) + +let safe_machine env constr = + let mf = { fix = false; nocheck = false } in + execute mf env constr + +let safe_machine_type env constr = + let mf = { fix = false; nocheck = false } in + execute_type mf env constr + +(* Machines with general fixpoint. *) + +let fix_machine env constr = + let mf = { fix = true; nocheck = false } in + execute mf env constr + +let fix_machine_type env constr = + let mf = { fix = true; nocheck = false } in + execute_type mf env constr + +(* Fast machines without any verification. *) + +let unsafe_machine env constr = + let mf = { fix = true; nocheck = true } in + execute mf env constr + +let unsafe_machine_type env constr = + let mf = { fix = true; nocheck = true } in + execute_type mf env constr + + +(* ``Type of'' machines. *) + +let type_of env c = + let (j,_) = safe_machine env c in nf_betaiota env j.uj_type + +let type_of_type env c = + let tt = safe_machine_type env c in DOP0 (Sort tt.typ) + +let unsafe_type_of env c = + let (j,_) = unsafe_machine env c in nf_betaiota env j.uj_type + +let unsafe_type_of_type env c = + let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) + + +(*s Machines with information. *) + +type information = Logic | Inf of unsafe_judgment + +(*i +let implicit_judgment = {body=mkImplicit;typ=implicit_sort} + +let add_inf_rel (na,inf) env = + match inf with + Logic -> add_rel (na,implicit_judgment) env + | Inf j -> add_rel (na,tjudge_of_judge j) env + + +let fw_mutind sigma fenv k = + let (sp,x,args) = destMutInd k in + let mis = mind_specif_of_mind k in + match mis_singl mis with + Some a -> Some (a,true) + | None -> + if is_info_cast_type sigma (mis_arity mis) then + let infK = + global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x))) + in Some (infK,false) + else None + +let inf_of_mind sigma fenv mind = + try + match fw_mutind sigma fenv mind with + Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK) + | None -> Logic + with + Not_found | Failure _ -> + anomaly "cannot convert an inductive to an finductive" + +let inf_mconstructor (sigma,metamap) fenv k = + let (sp,x,i,cl) = destMutConstruct k in + let mind = mkMutInd sp x cl in + (match fw_mutind sigma fenv mind with + None -> Logic + | Some(infi,singl) -> + (match mind_lamexp mind with + | Some clamexp -> + if singl + then Inf(cast_fmachine (sigma,[]) fenv clamexp) + else + let (infsp, infx, infcl) = destMutInd infi in + let infmconstructor = mkMutConstruct infsp infx i infcl in + let infval = subst1 infmconstructor clamexp in + Inf (cast_fmachine (sigma,fst metamap) fenv infval) + | _ -> assert false)) + + +exception DefinedExtraction + +(* when c is an evaluable constant with an extraction which + contains an implicit, gives the value of the c constant + otherwise raise DefinedExtraction +*) + +let value_implicit_const sigma c cinf = + match c with DOPN(Const(_),_) -> + if evaluable_const sigma c then + let cv = const_value sigma cinf in + if is_implicit cv (* or contains_implicit sigma cv *) + then const_value sigma c + else raise DefinedExtraction + else raise DefinedExtraction + | _ -> raise DefinedExtraction + +let unsafe_infmachine (sigma,metamap) env fenv c = + let rec infexec env fenv cstr = match cstr with + DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic + | DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic + | DOP2(Cast,c,_) -> infexec env fenv c + | DOP0(Meta n) -> + (match List.assoc n (snd metamap) with + Logic -> Logic + | Inf j -> Inf{uj_val=DOP0(Meta n); + uj_type=j.uj_val; + uj_kind = hnf_constr sigma j.uj_type}) + + | Rel n -> + inf_rel fenv + (contents_of_type sigma (snd (lookup_rel n env))) n + + | VAR str -> + inf_var fenv + (contents_of_type sigma (snd(lookup_glob str env))) str + + | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr + + | DOPN(Abst _,_) -> + if evaluable_abst cstr then infexec env fenv (abst_value cstr) + else error "cannot extract from an unevaluable abstraction" + + | DOP0(Sort s) -> inf_sort s + + | DOPN(AppL,tl) -> + let c1 = (hd_vect tl) + and cl = tl_vect tl in + let funinf = infexec env fenv c1 in + (match funinf with Logic -> Logic + | Inf(j) -> let cinf = j.uj_val in + (* try to expand constants corresponding + to non extractable terms *) + (try if is_extraction_expanded() then + let valcte = value_implicit_const sigma c1 cinf + in infexec env fenv (whd_betaiota (appvect(valcte,cl))) + else raise DefinedExtraction + with DefinedExtraction -> + let argsinf = Array.map (infexec env fenv) cl + in it_vect inf_apply funinf argsinf)) + + | DOP2(Lambda,c1,DLAM(name,c2)) -> + let varinf = infexec env fenv c1 in + let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env) + (add_inf_rel (name,varinf) fenv) c2 + in inf_abs_rel name bodyinf varinf + + | DOP2(Prod,c1,DLAM(name,c2)) -> + let c1inf = infexec env fenv c1 in + let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env) + (add_inf_rel (name,c1inf) fenv) c2 + in inf_gen_rel name c2inf c1inf + + | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr + + | DOPN(MutConstruct _,_) -> + inf_mconstructor (sigma,metamap) fenv cstr + + | DOPN(Fix(vn,i),cl) -> + let lar = Array.sub cl 0 ((Array.length cl) - 1) in + let inflar = Array.map (infexec env fenv) lar in + let infAi = inflar.(i) in + (match infAi with + Logic -> Logic + | Inf aij -> + let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in + let (new_env,new_fenv) = + it_vect2 + (fun (ne,nfe) fk ak -> + (add_rel (fk,tjudge_of_cast sigma ak) ne, + let infAk = infexec ne nfe ak + in (add_inf_rel (fk,infAk) nfe))) + (env,fenv) + (Array.of_list (List.rev lfi)) (vect_lift lar) in +(* a special function to localize the recursive index in the extracted term *) + let rec exec_def ne nfe n def = + (match hnf_constr sigma def with + DOP2(Lambda,c1,DLAM(name,c2)) -> + let varinf = infexec ne nfe c1 in + let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) + and nfe' = add_inf_rel (name,varinf) nfe in + if n = 0 then + let infc2 = infexec ne' nfe' c2 + in let infdef = inf_abs_rel name infc2 varinf + and index = + if varinf = Logic then -1 + (* the recursive call was on a non-informative term *) + else 0 in (infdef,index) + else + let bodyinf,countl = + exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) + (add_inf_rel (name,varinf) nfe) (n-1) c2 in + let (infabs,abs) = + inf_abs_rel_count name bodyinf varinf + in (infabs, + if abs = ERASE then countl + else if countl<0 then countl-1 + else countl+1) + | _ -> anomaly "exec_def : should be a lambda") in + let infdefs_ind = + map2_vect (exec_def new_env new_fenv) vn ldefs + in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind) + + | DOPN(CoFix i,cl) -> + let lar = Array.sub cl 0 ((Array.length cl) - 1) in + let inflar = Array.map (infexec env fenv) lar in + let infAi = inflar.(i) in + (match infAi with + Logic -> Logic + | Inf aij -> + let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in + let (new_env,new_fenv) = + it_vect2 (fun (ne,nfe) fk ak -> + (add_rel (fk,tjudge_of_cast sigma ak) ne, + let infAk = infexec ne nfe ak + in (add_inf_rel (fk,infAk) nfe))) + (env,fenv) + (Array.of_list (List.rev lfi)) (vect_lift lar) in + + let infdefs = Array.map (infexec new_env new_fenv) ldefs + in inf_cofix sigma i aij.uj_type lfi inflar infdefs) + + | DOPN(MutCase _,_) -> + let (ci,p,c,lf) = destCase cstr in + let pinf = infexec env fenv p in + (match pinf with + Logic -> Logic + | Inf pj -> + if is_extraction_expanded() then + let (d,l) = whd_betadeltaiota_stack sigma c [] in + (match d with (DOPN(MutConstruct(_,_),_)) -> + let cstr' = + DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf) + in infexec env fenv (whd_betaiota cstr') + | _ -> + let cinf = infexec env fenv c + and lfinf = Array.map (infexec env fenv) lf + in inf_mutcase fenv sigma pj ci cinf lfinf + ) + else let cinf = infexec env fenv c + and lfinf = Array.map (infexec env fenv) lf + in inf_mutcase fenv sigma pj ci cinf lfinf) + + | _ -> error "Cannot extract information" + in infexec env fenv c + + +let core_infmachine meta env fenv c = + try unsafe_infmachine meta env fenv c + with (UserError _ | Failure _) -> Logic + +(* WITH INFORMATION *) +(* does not check anymore that extracted terms are well-formed *) +let judgement_infmachine meta env fenv c ct = + try + match unsafe_infmachine meta env fenv c with + Inf infj -> + let inftyp = + try unsafe_infmachine meta env fenv ct + with (UserError _ | Failure _) -> + (warning "Failed to extract in type"; Logic) + in (match inftyp with + Inf infjt -> + Inf{uj_val=infj.uj_val; + uj_type=infjt.uj_val; + uj_kind=infj.uj_kind} + | Logic -> Inf infj) + | Logic -> Logic + with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic) + +let infmachine_type nocheck (sigma,metamap) env fenv constr = + let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in + let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in + let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in + let inf = + if is_info_type sigma t then (* Case the term is informative *) + let uniarc = get_uniarc () in + let infjt = + judgement_infmachine + (sigma,(constr_metamap,inf_metamap)) env fenv + t.body + (DOP0 (Sort t.typ)) in + let _ = set_uniarc uniarc in + infjt + else Logic + + in hash_jpair_type + ({body = strip_all_casts t.body; typ = t.typ}, + (inf_app (fun j -> {uj_val = nf_beta j.uj_val; + uj_type = nf_beta j.uj_type; + uj_kind = j.uj_kind }) inf)) + +let infmachine nocheck (sigma,metamap) env fenv constr = + let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in + let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in + let j = core_fmachine nocheck (sigma,constr_metamap) env constr in + let inf = + if is_info_judge sigma j then (* Case the term is informative *) + let uniarc = get_uniarc () in + let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in + let infjt = + judgement_infmachine + (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in + let _ = set_uniarc uniarc in + infjt + else Logic + + in hash_jpair + ({uj_val = strip_all_casts j.uj_val; + uj_type = strip_all_casts j.uj_type; + uj_kind = j.uj_kind}, + (inf_app (fun j -> {uj_val = nf_beta j.uj_val; + uj_type = nf_beta j.uj_type; + uj_kind = j.uj_kind }) inf)) + + +let jsign_of_sign sigma sign = + sign_it + (fun id a (sign,fsign) -> + let sign' = add_sign (id,a) sign in + let fsign' = + match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body + with + (_,Logic) -> fsign + | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign + in (sign',fsign')) + sign (([],[]),([],[])) + + +let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign) + +let infexemeta_type sigma metamap (env,fenv) c = + infmachine_type true (sigma,metamap) env fenv c + +let infexecute_rec_type sigma (env,fenv) c = + infmachine_type false (sigma,[]) env fenv c + +let infexecute_type sigma (sign,fsign) c = + infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c + +let infexemeta sigma metamap (env,fenv) c = + infmachine true (sigma,metamap) env fenv c + +let infexecute_rec sigma (env,fenv) c = + infmachine false (sigma,[]) env fenv c + +let infexecute sigma (sign,fsign) c = + infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c + +(* A adapter pour les nouveaux env +let fvar_type sigma (sign,fsign) v = + let na = destVar v in + let varty = (snd(lookup_sign na sign)) + in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with + Inf ft -> ft.uj_val + | Logic -> invalid_arg "Fvar with a non-informative type (1)!" + +*) + +(* MACHINE WITH UNIVERSES *) +(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab, + recuperer le graphe local, et restaurer l'acien graphe global *) + +let whd_instuni = function + DOP0(Sort(Type(u))) -> + let u = (if u = dummy_univ then new_univ() else u) + in DOP0(Sort(Type(u))) + | c -> c + +(* Instantiate universes: replace all dummy_univ by fresh universes. + This is already done by the machine. + Indtypes instantiates the universes itself, because in the case of + large constructor, additionnal constraints must be considered. *) +let instantiate_universes c = strong whd_instuni c + + +(* sp est le nom de la constante pour laquelle il faut que c soit bien type. + Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles + independamment. + Au lieu de sp, Lib.cwd() serait peut-etre suffisant. + Cela eviterai de donner un section-path quand on veut typer. *) +let fexecute_type_with_univ sigma sign sp c = + with_universes (fexecute_type sigma sign) (sp,initial_universes,c) + + +let fexecute_with_univ sigma sign sp c = + with_universes (fexecute sigma sign) (sp,initial_universes,c) + + +let infexecute_type_with_univ sigma psign sp c = + with_universes (infexecute_type sigma psign) (sp,initial_universes,c) + + +let infexecute_with_univ sigma psign sp c = + with_universes (infexecute sigma psign) (sp,initial_universes,c) +i*) diff --git a/kernel/typing.mli b/kernel/typing.mli new file mode 100644 index 0000000000..9e37c4c798 --- /dev/null +++ b/kernel/typing.mli @@ -0,0 +1,48 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Names +open Term +open Univ +open Environ +open Machops +(*i*) + +(*s Machines without information. *) + +val safe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes +val safe_machine_type : 'a unsafe_env -> constr -> typed_type + +val fix_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes +val fix_machine_type : 'a unsafe_env -> constr -> typed_type + +val unsafe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes +val unsafe_machine_type : 'a unsafe_env -> constr -> typed_type + +val type_of : 'a unsafe_env -> constr -> constr + +val type_of_type : 'a unsafe_env -> constr -> constr + +val unsafe_type_of : 'a unsafe_env -> constr -> constr + + +(*s Machine with information. *) + +type information = Logic | Inf of unsafe_judgment + +(*i +val infexemeta : + 'a unsafe_env -> constr -> unsafe_judgment * information * universes + +val infexecute_type : + 'a unsafe_env -> constr -> typed_type * information * universes + +val infexecute : + 'a unsafe_env -> constr -> unsafe_judgment * information * universes + +val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env + +val core_infmachine : 'a unsafe_env -> constr -> information +i*) -- cgit v1.2.3