diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 182 |
1 files changed, 142 insertions, 40 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0c02c5dab..ff1fd929b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -369,7 +369,7 @@ let check_hidden_implicit_parameters id impls = errorlabstrm "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") -let push_name_env ?(global_level=false) lvar implargs env = +let push_name_env ?(global_level=false) ntnvars implargs env = function | loc,Anonymous -> if global_level then @@ -377,7 +377,6 @@ let push_name_env ?(global_level=false) lvar implargs env = env | loc,Name id -> check_hidden_implicit_parameters id env.impls ; - let (_,ntnvars) = lvar in if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var loc; set_var_scope loc id false env ntnvars; @@ -433,14 +432,72 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b +let obj_string x = + if Obj.is_block (Obj.repr x) then + "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) + else "int_val = " ^ string_of_int (Obj.magic x) + +let rec free_vars_of_pat il = + function + | CPatCstr (loc, c, l1, l2) -> + let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in + List.fold_left free_vars_of_pat il l2 + | CPatAtom (loc, ro) -> + begin match ro with + | Some (Ident (loc, i)) -> (loc, i) :: il + | Some _ | None -> il + end + | CPatNotation (loc, n, l1, l2) -> + let il = List.fold_left free_vars_of_pat il (fst l1) in + List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) + | _ -> anomaly (str "free_vars_of_pat") + +let intern_local_pattern intern lvar env p = + List.fold_left + (fun env (loc, i) -> + let bk = Default Implicit in + let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in + let n = Name i in + let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in + env) + env (free_vars_of_pat [] p) + +type binder_data = + | BDRawDef of (Loc.t * glob_binder) + | BDPattern of + (Loc.t * (cases_pattern * Id.t list) * + (bool ref * + (Notation_term.tmp_scope_name option * + Notation_term.tmp_scope_name list) + option ref * Notation_term.notation_var_internalization_type) + Names.Id.Map.t * + intern_env * constr_expr) + +let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") + let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function | LocalRawAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in + let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> let indef = intern env def in (push_name_env lvar (impls_term_list indef) env locna, - (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl) + (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + | LocalPattern (loc,p,ty) -> + let tyc = + match ty with + | Some ty -> ty + | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) + in + let env = intern_local_pattern intern lvar env p in + let cp = + match !intern_cases_pattern_fwd (None,env.scopes) p with + | (_, [(_, cp)]) -> cp + | _ -> assert false + in + let il = List.map snd (free_vars_of_pat [] p) in + (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -509,16 +566,36 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function in (renaming',env), Name id' -let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c)) - -let rec subordinate_letins letins = function +type letin_param = + | LPLetIn of Loc.t * (Name.t * glob_constr) + | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t + +let make_letins = + List.fold_right + (fun a c -> + match a with + | LPLetIn (loc,(na,b)) -> + GLetIn(loc,na,b,c) + | LPCases (loc,(cp,il),id) -> + let tt = (GVar(loc,id),(Name id,None)) in + GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)])) + +let rec subordinate_letins intern letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | (loc,(na,_,Some b,t))::l -> - subordinate_letins ((loc,(na,b,t))::letins) l - | (loc,(na,bk,None,t))::l -> - let letins',rest = subordinate_letins [] l in + | BDRawDef (loc,(na,_,Some b,t))::l -> + subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l + | BDRawDef (loc,(na,bk,None,t))::l -> + let letins',rest = subordinate_letins intern [] l in letins',((loc,(na,bk,t)),letins)::rest + | BDPattern (loc,u,lvar,env,tyc) :: l -> + let ienv = Id.Set.elements env.ids in + let id = Namegen.next_ident_away (Id.of_string "pat") ienv in + let na = (loc, Name id) in + let bk = Default Explicit in + let _, bl' = intern_assumption intern lvar env [na] bk tyc in + let bl' = List.map (fun a -> BDRawDef a) bl' in + subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l) | [] -> letins,[] @@ -526,7 +603,7 @@ let rec subst_iterator y t = function | GVar (_,id) as x -> if Id.equal id y then t else x | x -> map_glob_constr (subst_iterator y t) x -let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = +let instantiate_notation_constr loc intern ntnvars subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) @@ -585,8 +662,8 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in - let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in - let letins,bl = subordinate_letins [] bl in + let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in + let letins,bl = subordinate_letins intern [] bl in let termin = aux subst' (renaming,env) terminator in let res = List.fold_left (fun t binder -> subst_iterator ldots_var t @@ -596,11 +673,14 @@ let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> - let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in - GProd (loc,na,bk,t,make_letins letins (aux subst' infos c')) + let a,letins = snd (Option.get binderopt) in + let e = make_letins letins (aux subst' infos c') in + let (loc,(na,bk,t)) = a in + GProd (loc,na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> - let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in - GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c')) + let a,letins = snd (Option.get binderopt) in + let (loc,(na,bk,t)) = a in + GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c')) (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> @@ -775,10 +855,10 @@ let intern_non_secvar_qualid loc qid intern env lvar us args = | GRef (_, VarRef _, _),_,_ -> raise Not_found | r -> r -let intern_applied_reference intern env namedctx lvar us args = function +let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function | Qualid (loc, qid) -> let r,projapp,args2 = - try intern_qualid loc qid intern env lvar us args + try intern_qualid loc qid intern env ntnvars us args with Not_found -> error_global_not_found_loc loc qid in let x, imp, scopes, l = find_appl_head_data r in @@ -788,7 +868,7 @@ let intern_applied_reference intern env namedctx lvar us args = function with Not_found -> let qid = qualid_of_ident id in try - let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in + let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> @@ -1195,6 +1275,8 @@ let drop_notations_pattern looked_for = | CPatAtom (loc,None) -> RCPatAtom (loc,None) | CPatOr (loc, pl) -> RCPatOr (loc,List.map (in_pat top scopes) pl) + | CPatCast _ -> + assert false and in_pat_sc scopes x = in_pat false (x,snd scopes) and in_not top loc scopes (subst,substlist as fullsubst) args = function | NVar id -> @@ -1280,6 +1362,10 @@ let intern_cases_pattern genv scopes aliases pat = intern_pat genv aliases (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) +let _ = + intern_cases_pattern_fwd := + fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p + let intern_ind_pattern genv scopes pat = let no_not = try @@ -1362,7 +1448,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar lvar c = +let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let rec intern env = function | CRef (ref,us) as x -> let (c,imp,subscopes,l),_ = @@ -1383,10 +1469,11 @@ let internalize globalenv env allow_patvar lvar c = (fun (id,(n,order),bl,ty,_) -> let intern_ro_arg f = let before, after = split_at_annot bl n in - let (env',rbefore) = - List.fold_left intern_local_binder (env,[]) before in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in let ro = f (intern env') in let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in + let rbefore = List.map (fun a -> BDRawDef a) rbefore in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = @@ -1398,12 +1485,18 @@ let internalize globalenv env allow_patvar lvar c = | CMeasureRec (m,r) -> intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in - ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in + let bl = + List.rev_map + (function + | BDRawDef a -> a + | BDPattern (loc,_,_,_,_) -> + Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in + ((n, ro), bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (_,bli,tyi,_) = idl_temp.(i) in let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in - push_name_env lvar (impls_type_list ~args:fix_args tyi) + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) en (Loc.ghost, Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in GRec (loc,GFix @@ -1422,15 +1515,15 @@ let internalize globalenv env allow_patvar lvar c = in let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> - let (env',rbl) = - List.fold_left intern_local_binder (env,[]) bl in + let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in + let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in (List.rev rbl, intern_type env' ty,env')) dl in let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in - push_name_env lvar (impls_type_list ~args:cofix_args tyi) + push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (Loc.ghost, Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in GRec (loc,GCoFix n, @@ -1449,15 +1542,15 @@ let internalize globalenv env allow_patvar lvar c = | CLetIn (loc,na,c1,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in GLetIn (loc, snd na, inc1, - intern (push_name_env lvar (impls_term_list inc1) env na) c2) + intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) | CNotation (_,"( _ )",([a],[],[])) -> intern env a | CNotation (loc,ntn,args) -> - intern_notation intern env lvar loc ntn args + intern_notation intern env ntnvars loc ntn args | CGeneralization (loc,b,a,c) -> - intern_generalization intern env lvar loc b a c + intern_generalization intern env ntnvars loc b a c | CPrim (loc, p) -> fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes)) | CDelimiters (loc, key, e) -> @@ -1485,7 +1578,7 @@ let internalize globalenv env allow_patvar lvar c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref | CNotation (loc,ntn,([],[],[])) -> - let c = intern_notation intern env lvar loc ntn ([],[],[]) in + let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | x -> (intern env f,[],[],[]), args in @@ -1518,7 +1611,7 @@ let internalize globalenv env allow_patvar lvar c = (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) tms ([],Id.Set.empty,[]) in let env' = Id.Set.fold - (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var)) + (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = @@ -1552,16 +1645,16 @@ let internalize globalenv env allow_patvar lvar c = (* "in" is None so no match to add *) let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> - let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') + let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.ghost,na') in intern_type env'' u) po in GLetTuple (loc, List.map snd nal, (na', p'), b', - intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) + intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> - let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) + let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.ghost,na') in intern_type env'' p) po in GIf (loc, c', (na', p'), intern env b1, intern env b2) @@ -1606,7 +1699,7 @@ let internalize globalenv env allow_patvar lvar c = and intern_type env = intern (set_type_scope env) and intern_local_binder env bind = - intern_local_binder_aux intern lvar env bind + intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n (loc,pl) = @@ -1685,11 +1778,11 @@ let internalize globalenv env allow_patvar lvar c = (tm',(snd na,typ)), extra_id, match_td and iterate_prod loc2 env bk ty body nal = - let env, bl = intern_assumption intern lvar env nal bk ty in + let env, bl = intern_assumption intern ntnvars env nal bk ty in it_mkGProd loc2 bl (intern_type env body) and iterate_lam loc2 env bk ty body nal = - let env, bl = intern_assumption intern lvar env nal bk ty in + let env, bl = intern_assumption intern ntnvars env nal bk ty in it_mkGLambda loc2 bl (intern env body) and intern_impargs c env l subscopes args = @@ -1895,7 +1988,16 @@ let intern_context global_level env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left - (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar) + (fun (lenv, bl) b -> + let bl = List.map (fun a -> BDRawDef a) bl in + let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in + let bl = + List.map + (function + | BDRawDef a -> a + | BDPattern (loc,_,_,_,_) -> + Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in + (env, bl)) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in (lenv.impls, List.map snd bl) |