From 66685cf7c01806a0b5f7ed80ecee3d5cd5cff90d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Nov 2010 17:13:17 +0000 Subject: [PATCH] Implementation of proof irrelevance finished. --- .../grafite_engine/grafiteEngine.ml | 56 +++++++++++++++++++ .../components/ng_kernel/nCicTypeChecker.ml | 30 +++++----- .../components/ng_refiner/nCicUnification.ml | 11 ++-- 3 files changed, 77 insertions(+), 20 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 58904b833..0420c8119 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -396,6 +396,61 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; +let is_proof_irrelevant context ty = + match + NCicReduction.whd ~subst:[] context + (NCicTypeChecker.typeof ~subst:[] ~metasenv:[] context ty) + with + NCic.Sort NCic.Prop -> true + | NCic.Sort _ -> false + | _ -> assert false +;; + +let rec relevance_of ?(context=[]) ty = + match NCicReduction.whd ~subst:[] context ty with + NCic.Prod (n,s,t) -> + not (is_proof_irrelevant context s) :: + relevance_of ~context:((n,NCic.Decl s)::context) t + | _ -> [] +;; + +let compute_relevance uri = + function + NCic.Constant (_,name,bo,ty,attrs) -> + let relevance = relevance_of ty in + NCic.Constant (relevance,name,bo,ty,attrs) + | NCic.Fixpoint (ind,funs,attrs) -> + let funs = + List.map + (fun (_,name,recno,ty,bo) -> + let relevance = relevance_of ty in + relevance,name,recno,ty,bo + ) funs + in + NCic.Fixpoint (ind,funs,attrs) + | NCic.Inductive (ind,leftno,tys,attrs) -> + let context = + List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in + let tysno = List.length tys in + let tys = + List.map + (fun (_,name,arity,cons) -> + let relevance = relevance_of arity in + let cons = + List.map + (fun (_,name,ty) -> + let dety = + NCicTypeChecker.debruijn uri tysno ~subst:[] [] ty in + let relevance = relevance_of ~context dety in + relevance,name,ty + ) cons + in + (relevance,name,arity,cons) + ) tys + in + NCic.Inductive (ind,leftno,tys,attrs) +;; + let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = match cmd with @@ -448,6 +503,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = NCicUntrusted.map_obj_kind (fix ()) obj_kind | _ -> obj_kind in + let obj_kind = compute_relevance uri obj_kind in let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml index ccbebc271..4a89e9d12 100644 --- a/matita/components/ng_kernel/nCicTypeChecker.ml +++ b/matita/components/ng_kernel/nCicTypeChecker.ml @@ -762,7 +762,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in List.iter (fun (k_relev,_,te) -> - let k_relev = + let k_relev = try snd (HExtlib.split_nth leftno k_relev) with Failure _ -> k_relev in let te = debruijn uri len [] ~subst te in @@ -815,11 +815,11 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = raise (TypeCheckerFailure (lazy ("Non positive occurence in "^NUri.string_of_uri - uri))) - else check_relevance ~subst ~metasenv context k_relev te) + uri))) + else check_relevance ~subst ~metasenv context k_relev te) cl; check_relevance ~subst ~metasenv [] it_relev ty; - i+1) + i+1) tyl 1) and check_relevance ~subst ~metasenv context relevance ty = @@ -834,10 +834,10 @@ and check_relevance ~subst ~metasenv context relevance ty = | C.Prod (name,so,de) -> let sort = typeof ~subst ~metasenv context so in (match (relevance,R.whd ~subst context sort) with - | [],_ -> () + | [],_ -> () | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de - | true::_,C.Sort C.Prop - | false::_,C.Sort _ + | true::_,C.Sort C.Prop + | false::_,C.Sort _ | false::_,C.Meta _ -> error context ty | true::tl,C.Sort _ | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de @@ -1124,18 +1124,18 @@ and get_relevance ~metasenv ~subst context t args = let sort = typeof ~subst ~metasenv context so in let new_ty = S.subst ~avoid_beta_redexes:true arg de in (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[] - ~context so); + ~context so); prerr_endline ("sort: " ^ PP.ppterm ~subst ~metasenv:[] - ~context sort);*) - (match R.whd ~subst context sort with + ~context sort);*) + (match R.whd ~subst context sort with | C.Sort C.Prop -> false::(aux context new_ty tl) | C.Sort _ - | C.Meta _ -> true::(aux context new_ty tl) + | C.Meta _ -> true::(aux context new_ty tl) | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf - "Prod: the type %s of the source of %s is not a sort" - (PP.ppterm ~subst ~metasenv ~context sort) - (PP.ppterm ~subst ~metasenv ~context so))))) + "Prod: the type %s of the source of %s is not a sort" + (PP.ppterm ~subst ~metasenv ~context sort) + (PP.ppterm ~subst ~metasenv ~context so))))) | _ -> raise (TypeCheckerFailure @@ -1280,7 +1280,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = List.fold_left (fun (types,kl) (relevance,name,k,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in - check_relevance ~subst ~metasenv [] relevance ty; + check_relevance ~subst ~metasenv [] relevance ty; ((name,C.Decl ty)::types, k::kl) ) ([],[]) fl in diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index dd1e4b80c..9227289c6 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -823,10 +823,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = ppterm ~metasenv ~subst ~context (NCicReduction.unwind (k2,e2,t2,s2)))); pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); - let relevance = [] (* TO BE UNDERSTOOD + let relevance = match t1 with | C.Const r -> NCicEnvironment.get_relevance r - | _ -> [] *) in + | _ -> [] in let unif_from_stack (metasenv, subst) (t1, t2, b) = try let t1 = NCicReduction.from_stack ~delta:max_int t1 in @@ -839,7 +839,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = match l1,l2,r with | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo) | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo) - | l1, l2, _ -> + | l1, l2, _ -> NCicReduction.unwind (k1,e1,t1,List.rev l1), NCicReduction.unwind (k2,e2,t2,List.rev l2), todo @@ -848,10 +848,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = match t1, t2 with | NCic.Meta _, _ | _, NCic.Meta _ -> (NCicReduction.unwind (k1,e1,t1,s1)), - (NCicReduction.unwind (k2,e2,t2,s2)),[] + (NCicReduction.unwind (k2,e2,t2,s2)),[] | _ -> check_stack l1 l2 r [] in - let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in + let hh1,hh2,todo = + check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in try fo_unif_heads_and_cont_or_unwind_and_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) -- 2.39.2