From b3e715c1dd3692cc79e8a83e99fdd35c0ffec392 Mon Sep 17 00:00:00 2001 From: corbinea Date: Fri, 21 Mar 2003 14:28:26 +0000 Subject: Fin de la résurrection de Linear. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3781 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/linear/ccidpc.ml4 | 59 ++++++++++++++++++++++----------------------- contrib/linear/lk_proofs.ml | 18 +++++++------- 2 files changed, 38 insertions(+), 39 deletions(-) (limited to 'contrib') diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4 index 1823b2d48..06b4aaa48 100755 --- a/contrib/linear/ccidpc.ml4 +++ b/contrib/linear/ccidpc.ml4 @@ -67,7 +67,7 @@ let is_forall_term t=op2bool (match_with_forall_term t) let constr_of_string s () = Libnames.constr_of_reference (Nametab.locate (Libnames.qualid_of_string s)) -let id_ex=constr_of_string "Coq.Init.Logic.ex" +let id_ex=constr_of_string "Logic.ex" let match_with_exist_term t= match kind_of_term t with @@ -75,15 +75,15 @@ let match_with_exist_term t= if t=id_ex () && (Array.length v)=2 then match kind_of_term v.(1) with Lambda(na,a,b)->Some(na,a,b) - |_->assert false + |_->raise Impossible_case else None | _->None let is_exist_term t=op2bool (match_with_exist_term t) -let id_not=constr_of_string "Coq.Init.Logic.not" +let id_not=constr_of_string "Logic.not" -let id_false=constr_of_string "Coq.Init.Logic.False" +let id_false=constr_of_string "Logic.False" let match_with_not_term t= match kind_of_term t with @@ -107,7 +107,7 @@ let gen_ident id = make_ident (atompart_of_id id) (incr ctr;Some !ctr) let gen_name a na = match (named_hd Environ.empty_env a na) with (Name id)->gen_ident id - | Anonymous->assert false + | Anonymous->raise Impossible_case let dpc_of_cci_term lid = let rec tradrec cciterm = @@ -141,13 +141,19 @@ let cci_of_dpc_term tradsign sign = | APP (t::dpcargs) -> let t' = tradrec t in Term.applist(t', List.map tradrec dpcargs) - | _-> assert false + | _-> raise Impossible_case in tradrec let dpc_of_cci_fmla gls cciterm = let rec tradrec lid cciterm = - match match_with_conjunction cciterm with + match match_with_exist_term cciterm with + Some ((na,a,b)as trp)-> + let id = gen_name a na in + let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in + Exists(id,tradrec (id::lid) f) + |_-> + (match match_with_conjunction cciterm with Some (_,[a;b])->Conj(tradrec lid a,tradrec lid b) |_-> (match match_with_disjunction cciterm with @@ -165,12 +171,6 @@ let dpc_of_cci_fmla gls cciterm = let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in ForAll(id,tradrec (id::lid) f) |_-> - (match match_with_exist_term cciterm with - Some ((na,a,b)as trp)-> - let id = gen_name a na in - let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in - Exists(id,tradrec (id::lid) f) - |_-> let (hd,args) = whd_betaiota_stack cciterm in let dpcargs = List.map (dpc_of_cci_term lid) args in (match kind_of_term hd with @@ -214,11 +214,11 @@ let forAllE id t gls = tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls else tclFAIL 0 gls -let existE id gls = +let existE id id2 gls = let (_,_,t)=lookup_named id (pf_hyps gls) in if is_exist_term t then ((tclTHEN (simplest_elim (mkVar id)) - (tclDO 2 (dImp None)))) gls + (tclTHEN (intro_using id2) (dImp None)))) gls else tclFAIL 0 gls let negE id gls = @@ -230,16 +230,16 @@ let negE id gls = (*t exist_intro_head = put_pat mmk "ex_intro"*) let existI t gls = -(* if is_exist_term (pf_concl gls) then + if is_exist_term (pf_concl gls) then split (Rawterm.ImplicitBindings [t]) gls - else tclFAIL 0 gls *) - + else tclFAIL 0 gls + (* let (wc,kONT) = Evar_refiner.startWalk gls in let clause = mk_clenv_hnf_constr_type_of wc (pf_concl gls) in let clause' = clenv_constrain_missing_args [t] clause in res_pf kONT clause' gls - + *) let rec alpha_fmla bl1 bl2 p_0 p_1 = match p_0,p_1 with @@ -273,16 +273,15 @@ let first_pred p = in firstrec -let find_fmla_left (kspine,f) (jspine,gl) = - let ids = pf_ids_of_hyps gl - and sign= pf_hyps gl in - first_pred - (fun id -> - let (_,_,t)=lookup_named id sign in - ( try alpha_eq (kspine,f) +let find_fmla_left (kspine,f) (jspine,gl) = + let sign= pf_hyps gl in + let (id,_,_)=first_pred + (fun (id,_,t) -> + ( try + alpha_eq (kspine,f) (jspine,dpc_of_cci_fmla gl t) with _ -> false) - ) ids + ) sign in id let onNthClause tac n gls = @@ -299,7 +298,7 @@ let rec tradpf kspine jspine dpcpf gls = Proof2(_,_,Axiom2 f) -> let id = find_fmla_left (kspine,f) (jspine,gls) - in exact_no_check (mkVar id) gls + in (*exact_check (mkVar id)*)assumption gls | Proof2(_,_,LWeakening2(_,pf)) -> trad kspine jspine pf gls @@ -347,10 +346,10 @@ let rec tradpf kspine jspine dpcpf gls = | Proof2(_,_,LExists2(kid,f,pf)) -> let id = find_fmla_left (kspine,Exists(kid,f)) (jspine,gls) - in ((tclTHEN (existE id) + in ((tclTHEN (existE id kid) ((onNthClause (function (Some jid) -> trad (kid::kspine) (jid::jspine) pf - | None-> assert false) + | None-> raise Impossible_case) (-2))))) gls | Proof2(_,_,RExists2(kid,kterm,f,pf)) -> diff --git a/contrib/linear/lk_proofs.ml b/contrib/linear/lk_proofs.ml index 1360615a4..5ca3338c5 100755 --- a/contrib/linear/lk_proofs.ml +++ b/contrib/linear/lk_proofs.ml @@ -106,7 +106,7 @@ let sep_at at llt (lmu,_) = then ((Po a)::l1,l2) else (l1,(Po a)::l2) | [] -> ([],[]) - | _->assert false + | _->raise Impossible_case in sep_at_rec at let sep_nat nat llt (lmu,_) = @@ -118,7 +118,7 @@ let sep_nat nat llt (lmu,_) = then ((No a)::l1,l2) else (l1,(No a)::l2) | [] -> ([],[]) - | _->assert false + | _->raise Impossible_case in sep_nat_rec nat let sep_neg neg llt (lmu,_) = @@ -195,7 +195,7 @@ let sep_path (at,nat,conj,rneg,lneg) p = [x] -> x | ((Po(Conj _),_,_) as c::_) -> c (** on recherche d'abord A/\B **) | _::ll -> find_X0 ll - | _->assert false + | _->raise Impossible_case in let (x0,l1,l2) = if all_X0=[] then failwith "Can't find X0 in sep_path ! (impossible case)" else find_X0 all_X0 @@ -211,7 +211,7 @@ let sep_path (at,nat,conj,rneg,lneg) p = and (nat1,nat2) = sep_nat nat litS1 p in let neg = lneg @ (List.map (function (Po (Neg f)) -> (No f) - | _->assert false) rneg) + | _->raise Impossible_case) rneg) in let (neg1,neg2) = sep_neg neg litS1 p in let lit_at1 = List.map proj at1 and lit_nat1 = List.map proj nat1 @@ -246,7 +246,7 @@ let rec rneg_case pr = function and sq2' = (Neg f)::sq2 in (Proof2(sq1',sq2',RNeg2(f,pr1))) | [] -> pr - | _->assert false + | _->raise Impossible_case let lneg_case ((Proof2(sq1,sq2,_)) as pr) =function @@ -254,7 +254,7 @@ let lneg_case ((Proof2(sq1,sq2,_)) as pr) =function let sq1' = (Neg f)::sq1 and sq2' = substract sq2 [f] in (Proof2(sq1',sq2',LNeg2(f,pr))) - | _->assert false + | _->raise Impossible_case let find_lneg lneg = let rec is_negneg = function @@ -307,7 +307,7 @@ and cases (at,nat,conj,rneg,lneg) p = if rneg<>[] then let s = at@nat@lneg@(List.map (function (Po (Neg f)) -> (No f) - | _->assert false) rneg) + | _->raise Impossible_case) rneg) in let pr = proof_of_path s p in rneg_case pr rneg else @@ -316,7 +316,7 @@ and cases (at,nat,conj,rneg,lneg) p = let s = at@nat@(substract lneg [g])@[Po f] in let pr = proof_of_path s p in lneg_case pr g - |_->assert false + |_->raise Impossible_case (* pi_formula : separated formula -> formula @@ -733,7 +733,7 @@ let int_quant f u pr = and fr_var = free_var_formula f in let un_var = List.map (function (Universal(id,_,_)) -> id - | _ ->assert false) un_qt + | _ ->raise Impossible_case) un_qt in let sk_var = un_var @ fr_var in let u0 = unher_unif sk_var u in let pr0 = pi_proof pr -- cgit v1.2.3