diff options
Diffstat (limited to 'pretyping/term_dnet.ml')
| -rw-r--r-- | pretyping/term_dnet.ml | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 4c6c5e631..f47485780 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -20,9 +20,9 @@ open Pp (* debug *) (* Representation/approximation of terms to use in the dnet: - * + * * - no meta or evar (use ['a pattern] for that) - * + * * - [Rel]s and [Sort]s are not taken into account (that's why we need * a second pass of linear filterin on the results - it's not a perfect * term indexing structure) @@ -52,7 +52,7 @@ struct | DNil type dconstr = dconstr t - + (* debug *) let rec pr_dconstr f : 'a t -> std_ppcmds = function | DRel -> str "*" @@ -64,7 +64,7 @@ struct | DCase (_,t1,t2,ta) -> str "case" | DFix _ -> str "fix" | DCoFix _ -> str "cofix" - | DCons ((t,dopt),tl) -> f t ++ (match dopt with + | DCons ((t,dopt),tl) -> f t ++ (match dopt with Some t' -> str ":=" ++ f t' | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl | DNil -> str "[]" @@ -116,10 +116,10 @@ struct then invalid_arg "fold2:compare" else match c1,c2 with | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc - | (DCtx (c1,t1), DCtx (c2,t2) + | (DCtx (c1,t1), DCtx (c2,t2) | DApp (c1,t1), DApp (c2,t2) | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 - | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> + | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2 @@ -129,7 +129,7 @@ struct f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 | _ -> assert false - let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = + let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in if compare (head c1) (head c2) <> 0 then invalid_arg "map2_t:compare" else @@ -139,29 +139,29 @@ struct | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2) - | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> + | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2) | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) - | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> + | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) | _ -> assert false let terminal = function | (DRel | DSort | DNil | DRef _) -> true - | _ -> false + | _ -> false end - + (* * Terms discrimination nets * Uses the general dnet datatype on DTerm.t * (here you can restart reading) *) -(* - * Construction of the module +(* + * Construction of the module *) module type IDENT = @@ -185,7 +185,7 @@ struct module TDnet : Dnet.S with type ident=Ident.t and type 'a structure = 'a DTerm.t - and type meta = metavariable + and type meta = metavariable = Dnet.Make(DTerm)(Ident) (struct type t = metavariable @@ -193,20 +193,20 @@ struct end) type t = TDnet.t - + type ident = TDnet.ident - + type 'a pattern = 'a TDnet.pattern type term_pattern = term_pattern DTerm.t pattern - + type idset = TDnet.Idset.t type result = ident * (constr*existential_key) * Termops.subst open DTerm open TDnet - - let rec pat_of_constr c : term_pattern = + + let rec pat_of_constr c : term_pattern = match kind_of_term c with | Rel _ -> Term DRel | Sort _ -> Term DSort @@ -216,46 +216,46 @@ struct | Construct c -> Term (DRef (ConstructRef c)) | Term.Meta _ -> assert false | Evar (i,_) -> Meta i - | Case (ci,c1,c2,ca) -> + | Case (ci,c1,c2,ca) -> Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca)) - | Fix ((ia,i),(_,ta,ca)) -> + | Fix ((ia,i),(_,ta,ca)) -> Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca)) - | CoFix (i,(_,ta,ca)) -> + | CoFix (i,(_,ta,ca)) -> Term(DCoFix(i,Array.map pat_of_constr ta,Array.map pat_of_constr ca)) | Cast (c,_,_) -> pat_of_constr c | Lambda (_,t,c) -> Term(DLambda (pat_of_constr t, pat_of_constr c)) - | (Prod (_,_,_) | LetIn(_,_,_,_)) -> + | (Prod (_,_,_) | LetIn(_,_,_,_)) -> let (ctx,c) = ctx_of_constr (Term DNil) c in Term (DCtx (ctx,c)) - | App (f,ca) -> + | App (f,ca) -> Array.fold_left (fun c a -> Term (DApp (c,a))) (pat_of_constr f) (Array.map pat_of_constr ca) - and ctx_of_constr ctx c : term_pattern * term_pattern = + and ctx_of_constr ctx c : term_pattern * term_pattern = match kind_of_term c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c | _ -> ctx,pat_of_constr c - + let empty_ctx : term_pattern -> term_pattern = function | Meta _ as c -> c | Term (DCtx(_,_)) as c -> c | c -> Term (DCtx (Term DNil, c)) - - (* + + (* * Basic primitives *) let empty = TDnet.empty - - let subst s t = + + let subst s t = let sleaf id = Ident.subst s id in let snode = function | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr)) | n -> n in TDnet.map sleaf snode t - + let union = TDnet.union - + let add (c:constr) (id:Ident.t) (dn:t) = let c = Opt.reduce c in let c = empty_ctx (pat_of_constr c) in @@ -264,11 +264,11 @@ struct let new_meta_no = let ctr = ref 0 in fun () -> decr ctr; !ctr - + let new_meta_no = Evarutil.new_untyped_evar let neutral_meta = new_meta_no() - + let new_meta () = Meta (new_meta_no()) let new_evar () = mkEvar(new_meta_no(),[||]) @@ -292,19 +292,19 @@ struct let subst_evar i c = e_subst_evar i (fun _ -> c) (* debug *) - let rec pr_term_pattern p = - (fun pr_t -> function + let rec pr_term_pattern p = + (fun pr_t -> function | Term t -> pr_t t | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]" ) (pr_dconstr pr_term_pattern) p - let search_pat cpat dpat dn (up,plug) = + let search_pat cpat dpat dn (up,plug) = let whole_c = subst_evar plug cpat up in TDnet.Idset.fold - (fun id acc -> + (fun id acc -> let c_id = Opt.reduce (Ident.constr_of id) in - let (ctx,wc) = - try Termops.align_prod_letin whole_c c_id + let (ctx,wc) = + try Termops.align_prod_letin whole_c c_id with Invalid_argument _ -> [],c_id in let up = it_mkProd_or_LetIn up ctx in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in @@ -326,11 +326,11 @@ struct let fold_pattern_up f acc dpat cpat dn (up,plug) = fold_pattern_nonlin ( fun m dn acc -> - f dn (subst_evar plug (e_subst_evar neutral_meta new_evar cpat) up, m) acc + f dn (subst_evar plug (e_subst_evar neutral_meta new_evar cpat) up, m) acc ) acc dpat dn - let possibly_under pat k dn (up,plug) = - let rec aux fst dn (up,plug) acc = + let possibly_under pat k dn (up,plug) = + let rec aux fst dn (up,plug) acc = let cpat = pat() in let dpat = pat_of_constr cpat in let dpat = if fst then empty_ctx dpat else dpat in @@ -345,24 +345,24 @@ struct * High-level primitives describing specific search problems *) - let search_pattern dn pat = + let search_pattern dn pat = let pat = Opt.reduce pat in search_pat pat (empty_ctx (pat_of_constr pat)) dn init - + let search_concl dn pat = let pat = Opt.reduce pat in search_pat pat (under_prod (empty_ctx (pat_of_constr pat))) dn init - let search_eq_concl dn eq pat = + let search_eq_concl dn eq pat = let pat = Opt.reduce pat in let eq_pat = eq_pat eq () in let eq_dpat = under_prod (empty_ctx (pat_of_constr eq_pat)) in snd (fold_pattern_up - (fun dn up acc -> + (fun dn up acc -> search_pat pat (pat_of_constr pat) dn up @ acc ) [] eq_dpat eq_pat dn init) - - let search_head_concl dn pat = + + let search_head_concl dn pat = let pat = Opt.reduce pat in possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init @@ -370,12 +370,12 @@ struct let map f dn = TDnet.map f (fun x -> x) dn end - + module type S = sig type t type ident - + type result = ident * (constr*existential_key) * Termops.subst val empty : t |