From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/cc/ccalgo.ml | 122 +++++++++++++++++++++++---------------------------- 1 file changed, 54 insertions(+), 68 deletions(-) (limited to 'plugins/cc/ccalgo.ml') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc53b113..8e53a044 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,24 +1,26 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* !cc_verbose); @@ -62,7 +63,7 @@ module ST=struct let enter t sign st= if IntPairTable.mem st.toterm sign then - anomaly ~label:"enter" (Pp.str "signature already entered") + anomaly ~label:"enter" (Pp.str "signature already entered.") else IntPairTable.replace st.toterm sign t; IntTable.replace st.tosign t sign @@ -136,7 +137,7 @@ let family_eq f1 f2 = match f1, f2 with type term= Symb of constr - | Product of sorts * sorts + | Product of Sorts.t * Sorts.t | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -155,7 +156,7 @@ let rec term_equal t1 t2 = open Hashset.Combine let rec hash_term = function - | Symb c -> combine 1 (hash_constr c) + | Symb c -> combine 1 (Constr.hash c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) @@ -216,7 +217,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -233,7 +234,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr let equal = eq_constr_nounivs - let hash = hash_constr + let hash = Constr.hash end) module Typehash = Constrhash @@ -270,7 +271,8 @@ type state = mutable rew_depth:int; mutable changed:bool; by_type: Int.Set.t Typehash.t; - mutable gls:Proof_type.goal Tacmach.sigma} + mutable env:Environ.env; + sigma:Evd.evar_map} let dummy_node = { @@ -305,7 +307,8 @@ let empty depth gls:state = rew_depth=depth; by_type=Constrhash.create init_size; changed=false; - gls=gls + env=pf_env gls; + sigma=project gls } let forest state = state.uf @@ -322,7 +325,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative.") let get_constructors uf i= uf.map.(i).constructors @@ -340,7 +343,7 @@ let rec find_oldest_pac uf i pac= let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor.") let size uf i= (get_representative uf i).weight @@ -385,7 +388,7 @@ let term uf i=uf.map.(i).term let subterms uf i= match uf.map.(i).vertex with Node(j,k) -> (j,k) - | _ -> anomaly ~label:"subterms" (Pp.str "not a node") + | _ -> anomaly ~label:"subterms" (Pp.str "not a node.") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -424,7 +427,7 @@ let cc_product s1 s2 = mkLambda(_B_,mkSort(s2),_body_)) let rec constr_of_term = function - Symb s-> applist_projection s [] + Symb s-> s | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id | Constructor cinfo -> mkConstructU cinfo.ci_constr @@ -432,37 +435,20 @@ let rec constr_of_term = function make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> - applist_proj other l -and applist_proj c l = - match c with - | Symb s -> applist_projection s l - | _ -> applistc (constr_of_term c) l -and applist_projection c l = - match kind_of_term c with - | Const c when Environ.is_projection (fst c) (Global.env()) -> - let p = Projection.make (fst c) false in - (match l with - | [] -> (* Expand the projection *) - let ty,_ = Typeops.type_of_constant (Global.env ()) c in - let pb = Environ.lookup_projection p (Global.env()) in - let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx - | hd :: tl -> - applistc (mkProj (p, hd)) tl) - | _ -> applistc c l - -let rec canonize_name c = - let func = canonize_name in - match kind_of_term c with + | other -> Term.applist (constr_of_term other,l) + +let rec canonize_name sigma c = + let c = EConstr.Unsafe.to_constr c in + let func c = canonize_name sigma (EConstr.of_constr c) in + match Constr.kind c with | Const (kn,u) -> - let canon_const = constant_of_kn (canonical_con kn) in + let canon_const = Constant.make1 (Constant.canonical kn) in (mkConstU (canon_const,u)) | Ind ((kn,i),u) -> - let canon_mind = mind_of_kn (canonical_mind kn) in + let canon_mind = MutInd.make1 (MutInd.canonical kn) in (mkIndU ((canon_mind,i),u)) | Construct (((kn,i),j),u) -> - let canon_mind = mind_of_kn (canonical_mind kn) in + let canon_mind = MutInd.make1 (MutInd.canonical kn) in mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> mkProd (na,func t, func ct) @@ -474,7 +460,7 @@ let rec canonize_name c = mkApp (func ct,Array.smartmap func l) | Proj(p,c) -> let p' = Projection.map (fun kn -> - constant_of_kn (canonical_con kn)) p in + Constant.make1 (Constant.canonical kn)) p in (mkProj (p', func c)) | _ -> c @@ -485,7 +471,7 @@ let build_subst uf subst = (fun i -> try term uf i with e when CErrors.noncritical e -> - anomaly (Pp.str "incomplete matching")) + anomaly (Pp.str "incomplete matching.")) subst let rec inst_pattern subst = function @@ -497,10 +483,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (constr_of_term (term uf i)) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (constr_of_term t) ++ str "]" + Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -508,8 +494,8 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_unsafe_type_of state.gls trm in - let typ = canonize_name typ in + let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in + let typ = canonize_name state.sigma typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -615,7 +601,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -623,7 +609,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr prf ++ str " : " ++ + (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end @@ -750,7 +736,7 @@ let process_constructor_mark t i rep pac state = state.combine; f (n-1) q1 q2 | _-> anomaly ~label:"add_pacs" - (Pp.str "weird error in injection subterms merge") + (Pp.str "weird error in injection subterms merge.") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> (* add_pac state.uf.map.(i) pac t; *) @@ -817,11 +803,10 @@ let one_step state = let __eps__ = Id.of_string "_eps_" let new_state_var typ state = - let id = pf_get_new_id __eps__ state.gls in - let {it=gl ; sigma=sigma} = state.gls in - let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in - state.gls<- gls; - id + let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in + let id = Namegen.next_ident_away __eps__ ids in + state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env; + id let complete_one_class state i= match (get_representative state.uf i).inductive_status with @@ -829,18 +814,19 @@ let complete_one_class state i= let rec app t typ n = if n<=0 then t else let _,etyp,rest= destProd typ in - let id = new_state_var etyp state in + let id = new_state_var (EConstr.of_constr etyp) state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_unsafe_type_of state.gls - (constr_of_term (term state.uf pac.cnode)) in + let _c = Typing.unsafe_type_of state.env state.sigma + (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let _c = EConstr.Unsafe.to_constr _c in let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in - let typ = prod_applist _c (List.rev _args) in + let typ = Term.prod_applist _c (List.rev _args) in let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) - | _ -> anomaly (Pp.str "wrong incomplete class") + | _ -> anomaly (Pp.str "wrong incomplete class.") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -980,7 +966,7 @@ let find_instances state = Control.check_for_interrupt (); do_match state res pb_stack done; - anomaly (Pp.str "get out of here !") + anomaly (Pp.str "get out of here!") with Stack.Empty -> () in !res -- cgit v1.2.3