From 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 10 Sep 2000 07:19:28 +0000 Subject: Ajout d'un LetIn primitif. Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/omega/coq_omega.ml | 161 +++++++++++++++++++++++---------------------- 1 file changed, 83 insertions(+), 78 deletions(-) (limited to 'contrib/omega') diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 4375ef2a4..a8ecf4cd1 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -14,7 +14,6 @@ open Reduction open Proof_type open Ast open Names -open Generic open Term open Sign open Inductive @@ -83,22 +82,29 @@ let resolve_with_bindings_tac (c,lbind) gl = res_pf kONT clause gl let reduce_to_mind gl t = - let rec elimrec t l = match whd_castapp_stack t [] with - | (DOPN(MutInd (x0,x1),_) as mind,_) -> (mind,prod_it t l) - | (DOPN(Const _,_),_) -> + let rec elimrec t l = + let c, args = whd_castapp_stack t [] in + match kind_of_term c, args with + | (IsMutInd _,_) -> (c,Environ.it_mkProd_or_LetIn t l) + | (IsConst _,_) -> (try let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l with e when catchable_exception e -> errorlabstrm "tactics__reduce_to_mind" [< 'sTR"Not an inductive product" >]) - | (DOPN(MutCase _,_),_) -> + | (IsMutCase _,_) -> (try let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l with e when catchable_exception e -> errorlabstrm "tactics__reduce_to_mind" [< 'sTR"Not an inductive product" >]) - | (DOP2(Cast,c,_),[]) -> elimrec c l - | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l) + | (IsCast (c,_),[]) -> elimrec c l + | (IsProd (n,ty,t'),[]) -> + let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in + elimrec t' ((n,None,ty')::l) + | (IsLetIn (n,b,ty,t'),[]) -> + let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in + elimrec t' ((n,Some b,ty')::l) | _ -> error "Not an inductive product" in elimrec t [] @@ -115,7 +121,7 @@ let constructor_tac nconstropt i lbind gl = error "Not the expected number of constructors" | _ -> ()); if i > nconstr then error "Not enough Constructors"; - let c = DOPN(MutConstruct((x0,x1),i),args) in + let c = mkMutConstruct (((x0,x1),i),args) in let resolve_tac = resolve_with_bindings_tac (c,lbind) in (tclTHEN (tclTHEN (change_in_concl redcl) intros) resolve_tac) gl @@ -149,16 +155,7 @@ let hide_constr,find_constr,clear_tables,dump_tables = (fun () -> l := []), (fun () -> !l) -let get_applist = - let rec loop accu = function - | DOPN(AppL,cl) -> - begin match Array.to_list cl with - | h :: l -> loop (l @ accu) h - | [] -> failwith "get_applist" end - | DOP2(Cast,c,t) -> loop accu c - | t -> t,accu - in - loop [] +let get_applist c = whd_stack c [] exception Destruct @@ -175,14 +172,18 @@ type result = | Kimp of constr * constr | Kufo -let destructurate t = - match get_applist t with - | DOPN ((Const _ | MutConstruct _ | MutInd _) as c,_),args -> - Kapp (string_of_id (Global.id_of_global c),args) - | VAR id,[] -> Kvar(string_of_id id) - | DOP2(Prod,typ,DLAM(Anonymous,body)),[] -> Kimp(typ,body) - | DOP2(Prod,_,DLAM(Name _,_)),[] -> - error "Omega: Not a quantifier-free goal" +let destructurate t = + let c, args = get_applist t in + match kind_of_term c, args with + | IsConst (sp,_), args -> + Kapp (string_of_id (Global.id_of_global (Const sp)),args) + | IsMutConstruct (csp,_) , args -> + Kapp (string_of_id (Global.id_of_global (MutConstruct csp)),args) + | IsMutInd (isp,_), args -> + Kapp (string_of_id (Global.id_of_global (MutInd isp)),args) + | IsVar id,[] -> Kvar(string_of_id id) + | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body) + | IsProd (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" | _ -> Kufo let recognize_number t = @@ -425,58 +426,58 @@ type constr_path = | P_ARG let context operation path (t : constr) = - let rec loop i p0 p1 = - match (p0,p1) with - | (p, (DOP2(Cast,c,t))) -> DOP2(Cast,loop i p c,t) - | ([], t) -> operation i t - | (p, (DLAM(n,t))) -> DLAM(n,loop (i+1) p t) - | ((P_APP n :: p), (DOPN(AppL,v) as t)) -> + let rec loop i p0 t = + match (p0,kind_of_term t) with + | (p, IsCast (c,t)) -> mkCast (loop i p c,t) + | ([], _) -> operation i t + | ((P_APP n :: p), IsAppL _) -> let f,l = get_applist t in let v' = Array.of_list (f::l) in - v'.(n) <- loop i p v'.(n); (DOPN(AppL,v')) - | ((P_BRANCH n :: p), (DOPN(MutCase _,_) as t)) -> - let (_,_,_,v) = destCase t in - v.(n) <- loop i p v.(n); (DOPN(AppL,v)) - | ((P_ARITY :: p), (DOPN(AppL,v))) -> - let v' = Array.copy v in - v'.(0) <- loop i p v.(0); (DOPN(AppL,v')) - | ((P_ARG :: p), (DOPN(AppL,v))) -> - let v' = Array.copy v in - v'.(1) <- loop i p v.(1); (DOPN(AppL,v')) - | (p, (DOPN(Fix(_,n) as f,v))) -> - let v' = Array.copy v in - let l = Array.length v - 1 in - v'.(l) <- loop i (P_BRANCH n :: p) v.(l); (DOPN(f,v')) - | ((P_BRANCH n :: p), (DLAMV(name,v))) -> + v'.(n) <- loop i p v'.(n); (mkAppL v') + | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> + v.(n) <- loop i p v.(n); (mkAppL v) (* Not Mutcase ?? *) + | ((P_ARITY :: p), IsAppL (f,l)) -> + applist (loop i p f,l) + | ((P_ARG :: p), IsAppL (f,a::l)) -> + applist (f,(loop i p a)::l) + | (p, IsFix ((_,n as ln),(tys,lna,v))) -> + let l = Array.length v in let v' = Array.copy v in - v'.(n) <- loop (i+1) p v.(n); DLAMV(name,v') - | ((P_BODY :: p), (DOP2((Prod | Lambda) as k, t,c))) -> - (DOP2(k,t,loop i p c)) - | ((P_TYPE :: p), (DOP2((Prod | Lambda) as k, term,c))) -> - (DOP2(k,loop i p term, c)) - | (p, t) -> + v'.(n) <- loop (i+l) p v.(n); (mkFix (ln,(tys,lna,v'))) + | ((P_BODY :: p), IsProd (n,t,c)) -> + (mkProd (n,t,loop (i+1) p c)) + | ((P_BODY :: p), IsLambda (n,t,c)) -> + (mkLambda (n,t,loop (i+1) p c)) + | ((P_BODY :: p), IsLetIn (n,b,t,c)) -> + (mkLetIn (n,b,t,loop (i+1) p c)) + | ((P_TYPE :: p), IsProd (n,t,c)) -> + (mkProd (n,loop i p t,c)) + | ((P_TYPE :: p), IsLambda (n,t,c)) -> + (mkLambda (n,loop i p t,c)) + | ((P_TYPE :: p), IsLetIn (n,b,t,c)) -> + (mkLetIn (n,b,loop i p t,c)) + | (p, _) -> pPNL []; failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t let occurence path (t : constr) = - let rec loop p0 p1 = match (p0,p1) with - | (p, (DOP2(Cast,c,t))) -> loop p c - | ([], t) -> t - | (p, (DLAM(n,t))) -> loop p t - | ((P_APP n :: p), (DOPN(AppL,v) as t)) -> - let f,l = get_applist t in loop p v.(n) - | ((P_BRANCH n :: p), (DOPN(MutCase _,_) as t)) -> - let (_,_,_,v) = destCase t in loop p v.(n) - | ((P_ARITY :: p), (DOPN(AppL,v))) -> loop p v.(0) - | ((P_ARG :: p), (DOPN(AppL,v))) -> loop p v.(1) - | (p, (DOPN(Fix(_,n) as f,v))) -> - let l = Array.length v - 1 in loop (P_BRANCH n :: p) v.(l) - | ((P_BRANCH n :: p), (DLAMV(name,v))) -> loop p v.(n) - | ((P_BODY :: p), (DOP2((Prod | Lambda) as k, t,c))) -> loop p c - | ((P_TYPE :: p), (DOP2((Prod | Lambda) as k, term,c))) -> loop p term - | (p, t) -> + let rec loop p0 t = match (p0,kind_of_term t) with + | (p, IsCast (c,t)) -> loop p c + | ([], _) -> t + | ((P_APP n :: p), IsAppL (f,l)) -> loop p (List.nth l (n-1)) + | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> loop p v.(n) + | ((P_ARITY :: p), IsAppL (f,_)) -> loop p f + | ((P_ARG :: p), IsAppL (f,a::l)) -> loop p a + | (p, IsFix((_,n) ,(_,_,v))) -> loop p v.(n) + | ((P_BODY :: p), IsProd (n,t,c)) -> loop p c + | ((P_BODY :: p), IsLambda (n,t,c)) -> loop p c + | ((P_BODY :: p), IsLetIn (n,b,t,c)) -> loop p c + | ((P_TYPE :: p), IsProd (n,term,c)) -> loop p term + | ((P_TYPE :: p), IsLambda (n,term,c)) -> loop p term + | ((P_TYPE :: p), IsLetIn (n,b,term,c)) -> loop p term + | (p, _) -> pPNL []; failwith ("occurence " ^ string_of_int(List.length p)) in @@ -485,7 +486,7 @@ let occurence path (t : constr) = let abstract_path typ path t = let term_occur = ref (Rel 0) in let abstract = context (fun i t -> term_occur:= t; Rel i) path t in - mkLambda (Name (id_of_string "x")) typ abstract, !term_occur + mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in @@ -554,12 +555,14 @@ let clever_rewrite_base_poly typ p result theorem gl = let (abstracted,occ) = abstract_path typ (List.rev p) full in let t = applist - ((mkLambda (Name (id_of_string "P")) - (mkArrow typ mkProp) - (mkLambda (Name (id_of_string "H")) - (applist (Rel 1,[result])) - (mkAppL [| Lazy.force coq_eq_ind_r; - typ; result; Rel 2; Rel 1; occ; theorem |]))), + (mkLambda + (Name (id_of_string "P"), + mkArrow typ mkProp, + mkLambda + (Name (id_of_string "H"), + applist (Rel 1,[result]), + mkAppL [| Lazy.force coq_eq_ind_r; + typ; result; Rel 2; Rel 1; occ; theorem |])), [abstracted]) in exact (applist(t,[mkNewMeta()])) gl @@ -1206,8 +1209,10 @@ let replay_history tactic_normalisation = let theorem = mkAppL [| Lazy.force coq_ex; Lazy.force coq_Z; - mkLambda (Name(id_of_string v)) (Lazy.force coq_Z) - (mk_eq (Rel 1) eq1) |] + mkLambda + (Name(id_of_string v), + Lazy.force coq_Z, + mk_eq (Rel 1) eq1) |] in let mm = mk_integer m in let p_initial = [P_APP 2;P_TYPE] in -- cgit v1.2.3