diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 44c629484..29f295682 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -138,12 +138,12 @@ let find_q x (m,q) = else find (Id.Set.union l accs) (i::acc) itl in find Id.Set.empty [] q -let occur_vars_in_decl env hyps d = +let occur_vars_in_decl env sigma hyps d = if Id.Set.is_empty hyps then false else - let ohyps = global_vars_set_of_decl env d in + let ohyps = global_vars_set_of_decl env sigma d in Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps -let reorder_context env sign ord = +let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then error "Order list has duplicates"; @@ -152,13 +152,13 @@ let reorder_context env sign ord = | [] -> List.rev ctxt_tail @ ctxt_head | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in - if occur_vars_in_decl env h d then + if occur_vars_in_decl env sigma h d then user_err ~hdr:"reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ pr_sequence pr_id (Id.Set.elements (Id.Set.inter h - (global_vars_set_of_decl env d)))); + (global_vars_set_of_decl env sigma d)))); step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with @@ -173,16 +173,16 @@ let reorder_context env sign ord = ctxt (push_val x moved_hyps) (d::ctxt_tail)) in step ord ords sign mt_q [] -let reorder_val_context env sign ord = - val_of_named_context (reorder_context env (named_context_of_val sign) ord) +let reorder_val_context env sigma sign ord = + val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) -let check_decl_position env sign d = +let check_decl_position env sigma sign d = let x = NamedDecl.get_id d in - let needed = global_vars_set_of_decl env d in - let deps = dependency_closure env (named_context_of_val sign) needed in + let needed = global_vars_set_of_decl env sigma d in + let deps = dependency_closure env sigma (named_context_of_val sign) needed in if Id.List.mem x deps then user_err ~hdr:"Logic.check_decl_position" (str "Cannot create self-referring hypothesis " ++ pr_id x); @@ -233,12 +233,12 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,declfrom,right) hto = +let move_hyp sigma toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (NamedDecl.get_id d2) d - else occur_var_in_decl env (NamedDecl.get_id d) d2 + then occur_var_in_decl env sigma (NamedDecl.get_id d2) d + else occur_var_in_decl env sigma (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> @@ -278,10 +278,10 @@ let move_hyp toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context hfrom hto sign = +let move_hyp_in_named_context sigma hfrom hto sign = let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in - move_hyp toleft (left,declfrom,right) hto + move_hyp sigma toleft (left,declfrom,right) hto (**********************************************************************) @@ -320,10 +320,10 @@ let check_conv_leq_goal env sigma arg ty conclty = else sigma exception Stop of constr list -let meta_free_prefix a = +let meta_free_prefix sigma a = try let _ = Array.fold_left (fun acc a -> - if occur_meta a then raise (Stop acc) + if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc @@ -338,7 +338,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in - if (not !check) && not (occur_meta trm) then + if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) @@ -346,7 +346,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma conclty in - if !check && occur_meta conclty then + if !check && occur_meta sigma (EConstr.of_constr conclty) then raise (RefinerError (MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in gl::goalacc, conclty, sigma, ev @@ -367,10 +367,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f then + if is_template_polymorphic env sigma (EConstr.of_constr f) then let ty = (* Template sort-polymorphism of definition and inductive types *) - let firstmeta = Array.findi (fun i x -> occur_meta x) l in + let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma f args in @@ -406,7 +406,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (acc'',conclty',sigma, ans) | _ -> - if occur_meta trm then + if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm"); let t'ty = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in @@ -432,9 +432,9 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f + if is_template_polymorphic env sigma (EConstr.of_constr f) then - let l' = meta_free_prefix l in + let l' = meta_free_prefix sigma l in (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in @@ -464,7 +464,7 @@ and mk_hdgoals sigma goal goalacc trm = (acc',ty,sigma,c) | _ -> - if !check && occur_meta trm then + if !check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta"); goalacc, goal_type_of env sigma trm, sigma, trm @@ -511,9 +511,9 @@ let convert_hyp check sign sigma d = if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); - if check then reorder := check_decl_position env sign d; + if check then reorder := check_decl_position env sigma sign d; d) in - reorder_val_context env sign' !reorder + reorder_val_context env sigma sign' !reorder @@ -537,7 +537,7 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) + move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) nexthyp, t,cl,sigma else |