diff options
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/linear/ccidpc.ml4 | 25 | ||||
-rwxr-xr-x | contrib/linear/lk_proofs.ml | 55 |
2 files changed, 52 insertions, 28 deletions
diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4 index 1e3ec39e4..1823b2d48 100755 --- a/contrib/linear/ccidpc.ml4 +++ b/contrib/linear/ccidpc.ml4 @@ -105,8 +105,9 @@ let ctr = ref 0 let gen_ident id = make_ident (atompart_of_id id) (incr ctr;Some !ctr) let gen_name a na = - let (Name id) = (named_hd Environ.empty_env a na) - in gen_ident id + match (named_hd Environ.empty_env a na) with + (Name id)->gen_ident id + | Anonymous->assert false let dpc_of_cci_term lid = let rec tradrec cciterm = @@ -140,6 +141,7 @@ let cci_of_dpc_term tradsign sign = | APP (t::dpcargs) -> let t' = tradrec t in Term.applist(t', List.map tradrec dpcargs) + | _-> assert false in tradrec @@ -160,13 +162,13 @@ let dpc_of_cci_fmla gls cciterm = (match match_with_forall_term cciterm with Some ((na,a,b) as trp)-> let id = gen_name a na in - let f=mkApp(mkLambda trp,[|mkVar id|]) in + 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=mkApp(mkLambda trp,[|mkVar id|]) 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 @@ -209,7 +211,8 @@ let forAllI gls=if is_forall_term (pf_concl gls) then let forAllE id t gls = let rgl=pf_whd_betadeltaiota gls (pf_type_of gls (mkVar id)) in if is_forall_term rgl then - generalize [mkApp (mkVar id,[|t|])] gls else tclFAIL 0 gls + tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls + else tclFAIL 0 gls let existE id gls = let (_,_,t)=lookup_named id (pf_hyps gls) in @@ -227,6 +230,11 @@ 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 + split (Rawterm.ImplicitBindings [t]) 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 @@ -340,8 +348,9 @@ 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) - ((onNthClause (fun (Some jid) -> - trad (kid::kspine) (jid::jspine) pf) + ((onNthClause (function (Some jid) -> + trad (kid::kspine) (jid::jspine) pf + | None-> assert false) (-2))))) gls | Proof2(_,_,RExists2(kid,kterm,f,pf)) -> @@ -368,4 +377,4 @@ and trad kspine jspine dpcpf gls = tradpf kspine jspine dpcpf gls -(* $Id$ *) + diff --git a/contrib/linear/lk_proofs.ml b/contrib/linear/lk_proofs.ml index e4ee29807..1360615a4 100755 --- a/contrib/linear/lk_proofs.ml +++ b/contrib/linear/lk_proofs.ml @@ -8,7 +8,7 @@ (*i $Id$ i*) -open Names +open Names open General open Dpctypes @@ -106,6 +106,7 @@ let sep_at at llt (lmu,_) = then ((Po a)::l1,l2) else (l1,(Po a)::l2) | [] -> ([],[]) + | _->assert false in sep_at_rec at let sep_nat nat llt (lmu,_) = @@ -117,6 +118,7 @@ let sep_nat nat llt (lmu,_) = then ((No a)::l1,l2) else (l1,(No a)::l2) | [] -> ([],[]) + | _->assert false in sep_nat_rec nat let sep_neg neg llt (lmu,_) = @@ -193,6 +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 in let (x0,l1,l2) = if all_X0=[] then failwith "Can't find X0 in sep_path ! (impossible case)" else find_X0 all_X0 @@ -206,7 +209,9 @@ let sep_path (at,nat,conj,rneg,lneg) p = in let litS1 = glue (List.map (fun x -> all_lit_sfla x) s1) in let (at1,at2) = sep_at at litS1 p and (nat1,nat2) = sep_nat nat litS1 p - in let neg = lneg @ (List.map (fun (Po (Neg f)) -> (No f)) rneg) + in let neg = lneg @ (List.map (function + (Po (Neg f)) -> (No f) + | _->assert false) 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 @@ -241,11 +246,15 @@ let rec rneg_case pr = function and sq2' = (Neg f)::sq2 in (Proof2(sq1',sq2',RNeg2(f,pr1))) | [] -> pr + | _->assert false -let lneg_case ((Proof2(sq1,sq2,_)) as pr) (No(Neg f)) = - let sq1' = (Neg f)::sq1 - and sq2' = substract sq2 [f] - in (Proof2(sq1',sq2',LNeg2(f,pr))) + +let lneg_case ((Proof2(sq1,sq2,_)) as pr) =function + (No(Neg f))-> + let sq1' = (Neg f)::sq1 + and sq2' = substract sq2 [f] + in (Proof2(sq1',sq2',LNeg2(f,pr))) + | _->assert false let find_lneg lneg = let rec is_negneg = function @@ -296,14 +305,18 @@ and cases (at,nat,conj,rneg,lneg) p = in rneg_case pr rneg else if rneg<>[] then - let s = at@nat@lneg@(List.map (fun (Po (Neg f)) -> (No f)) rneg) + let s = at@nat@lneg@(List.map (function + (Po (Neg f)) -> (No f) + | _->assert false) rneg) in let pr = proof_of_path s p in rneg_case pr rneg else - let (No (Neg f)) as g = find_lneg lneg - in let s = at@nat@(substract lneg [g])@[Po f] - in let pr = proof_of_path s p - in lneg_case pr g + match find_lneg lneg with + (No (Neg f)) as g -> + let s = at@nat@(substract lneg [g])@[Po f] in + let pr = proof_of_path s p in + lneg_case pr g + |_->assert false (* pi_formula : separated formula -> formula @@ -718,13 +731,15 @@ let int_quant f u pr = let qt = quant_var f in let un_qt = such_that qt (function (Universal _) -> true | _ -> false) and fr_var = free_var_formula f - in let un_var = List.map (fun (Universal(id,_,_)) -> id) un_qt - in let sk_var = un_var @ fr_var - in let u0 = unher_unif sk_var u - in let pr0 = pi_proof pr - in let pr1 = unher_proof sk_var pr0 - in let cst = make_constraints qt u0 - in let pog = make_pog qt cst - in let qpr = quant_proof cst pog pr1 - in witness_proof u0 qpr + in let un_var = List.map (function + (Universal(id,_,_)) -> id + | _ ->assert false) un_qt + in let sk_var = un_var @ fr_var + in let u0 = unher_unif sk_var u + in let pr0 = pi_proof pr + in let pr1 = unher_proof sk_var pr0 + in let cst = make_constraints qt u0 + in let pog = make_pog qt cst + in let qpr = quant_proof cst pog pr1 + in witness_proof u0 qpr |