aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml130
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/symbols.ml61
-rw-r--r--interp/symbols.mli2
-rw-r--r--interp/topconstr.ml36
-rw-r--r--interp/topconstr.mli2
6 files changed, 156 insertions, 79 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9e792dc74..cda51446e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -111,13 +111,27 @@ let add_glob loc ref =
dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id)
(**********************************************************************)
+(* Remembering the parsing scope of variables in notations *)
+
+let set_var_scope loc id (_,_,scopes) (_,_,varscopes) =
+ try
+ let idscopes = List.assoc id varscopes in
+ if !idscopes <> None & !idscopes <> Some scopes then
+ user_err_loc (loc,"set_var_scope",
+ pr_id id ++ str " already occurs in a different scope")
+ else
+ idscopes := Some scopes
+ with Not_found ->
+ if_verbose warning ("Could not globalize " ^ (string_of_id id))
+
+(**********************************************************************)
(* Discriminating between bound variables and global references *)
(* [vars1] is a set of name to avoid (used for the tactic language);
[vars2] is the set of global variables, env is the set of variables
abstracted until this point *)
-let intern_var (env,impls,_) (vars1,vars2) loc id =
+let intern_var (env,impls,scopes) (vars1,vars2,_) loc id =
(* Is [id] bound in *)
if Idset.mem id env or List.mem id vars1
then
@@ -157,13 +171,13 @@ let intern_reference env lvar = function
with e ->
(* Extra allowance for grammars *)
if !interning_grammar then begin
- if_verbose warning ("Could not globalize " ^ (string_of_id id));
- RVar (loc, id), [], []
+ set_var_scope loc id env lvar;
+ RVar (loc,id), [], []
end
else raise e
let interp_reference vars r =
- let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[]) r in r
+ let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[],[]) r in r
let apply_scope_env (ids,impls,scopes as env) = function
| [] -> env, []
@@ -351,8 +365,8 @@ let rec subst_rawconstr loc interp subst (ids,impls,scopes as env) = function
(**********************************************************************)
(* Main loop *)
-let internalise sigma env allow_soapp lvar c =
- let rec intern (ids,impls,scopes as env) = function
+let internalise isarity sigma env allow_soapp lvar c =
+ let rec intern isarity (ids,impls,scopes as env) = function
| CRef ref as x ->
let (c,imp,subscopes) = intern_reference env lvar ref in
(match intern_impargs c env imp subscopes [] with
@@ -367,8 +381,9 @@ let internalise sigma env allow_soapp lvar c =
raise (InternalisationError (locid,UnboundFixName (false,iddef)))
in
let ids' = List.fold_right Idset.add lf ids in
- let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in
- let arityl = Array.of_list (List.map (intern env) lc) in
+ let defl =
+ Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
+ let arityl = Array.of_list (List.map (intern true env) lc) in
RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
| CCoFix (loc, (locid,iddef), ldecl) ->
let (lf,lc,lt) = intern_cofix ldecl in
@@ -379,30 +394,32 @@ let internalise sigma env allow_soapp lvar c =
raise (InternalisationError (locid,UnboundFixName (true,iddef)))
in
let ids' = List.fold_right Idset.add lf ids in
- let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in
- let arityl = Array.of_list (List.map (intern env) lc) in
+ let defl =
+ Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in
+ let arityl = Array.of_list (List.map (intern true env) lc) in
RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
| CArrow (loc,c1,c2) ->
- RProd (loc, Anonymous, intern env c1, intern env c2)
+ RProd (loc, Anonymous, intern true env c1, intern true env c2)
| CProdN (loc,[],c2) ->
- intern env c2
+ intern true env c2
| CProdN (loc,(nal,ty)::bll,c2) ->
iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
| CLambdaN (loc,[],c2) ->
- intern env c2
+ intern isarity env c2
| CLambdaN (loc,(nal,ty)::bll,c2) ->
- iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal
+ iterate_lam loc isarity env ty (CLambdaN (loc, bll, c2)) nal
| CLetIn (loc,(_,na),c1,c2) ->
- RLetIn (loc, na, intern env c1,
- intern (name_fold Idset.add na ids,impls,scopes) c2)
+ RLetIn (loc, na, intern false env c1,
+ intern false (name_fold Idset.add na ids,impls,scopes) c2)
| CNotation (loc,ntn,args) ->
+ let scopes = if isarity then Symbols.type_scope::scopes else scopes in
let (ids,c) = Symbols.interp_notation ntn scopes in
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- subst_rawconstr loc intern subst env c
+ subst_rawconstr loc (intern false) subst env c
| CNumeral (loc, n) ->
Symbols.interp_numeral loc n scopes
| CDelimiters (loc, key, e) ->
- intern (ids,impls,find_delimiters_scope loc key::scopes) e
+ intern isarity (ids,impls,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, ref, args) ->
let (f,_,args_scopes) = intern_reference env lvar ref in
RApp (loc, f, intern_args env args_scopes args)
@@ -410,16 +427,17 @@ let internalise sigma env allow_soapp lvar c =
let (c, impargs, args_scopes) =
match f with
| CRef ref -> intern_reference env lvar ref
- | _ -> (intern env f, [], [])
+ | _ -> (intern false env f, [], [])
in
RApp (loc, c, intern_impargs c env impargs args_scopes args)
| CCases (loc, po, tms, eqns) ->
- RCases (loc, option_app (intern env) po,
- List.map (intern env) tms,
+ RCases (loc, option_app (intern true env) po,
+ List.map (intern false env) tms,
List.map (intern_eqn (List.length tms) env) eqns)
| COrderedCase (loc, tag, po, c, cl) ->
- ROrderedCase (loc, tag, option_app (intern env) po, intern env c,
- Array.of_list (List.map (intern env) cl))
+ ROrderedCase (loc, tag, option_app (intern true env) po,
+ intern false env c,
+ Array.of_list (List.map (intern false env) cl))
| CHole loc ->
RHole (loc, QuestionMark)
| CMeta (loc, n) when n >=0 or allow_soapp ->
@@ -429,7 +447,7 @@ let internalise sigma env allow_soapp lvar c =
| CSort (loc, s) ->
RSort(loc,s)
| CCast (loc, c1, c2) ->
- RCast (loc,intern env c1,intern env c2)
+ RCast (loc,intern false env c1,intern true env c2)
| CDynamic (loc,d) -> RDynamic (loc,d)
@@ -446,24 +464,24 @@ let internalise sigma env allow_soapp lvar c =
let rhs = replace_vars_constr_expr subst rhs in
List.iter message_redundant_alias subst;
let env_ids = List.fold_right Idset.add eqn_ids ids in
- (loc, eqn_ids,pl,intern (env_ids,impls,scopes) rhs)
+ (loc, eqn_ids,pl,intern false (env_ids,impls,scopes) rhs)
and iterate_prod loc2 (ids,impls,scopes as env) ty body = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
let ids' = name_fold Idset.add na ids in
let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in
- RProd (join_loc loc1 loc2, na, intern env ty, body)
- | [] -> intern env body
+ RProd (join_loc loc1 loc2, na, intern true env ty, body)
+ | [] -> intern true env body
- and iterate_lam loc2 (ids,impls,scopes as env) ty body = function
+ and iterate_lam loc2 isarity (ids,impls,scopes as env) ty body = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
let ids' = name_fold Idset.add na ids in
- let body = iterate_lam loc2 (ids',impls,scopes) ty body nal in
- let ty = locate_if_isevar loc1 na (intern env ty) in
+ let body = iterate_lam loc2 isarity (ids',impls,scopes) ty body nal in
+ let ty = locate_if_isevar loc1 na (intern true env ty) in
RLambda (join_loc loc1 loc2, na, ty, body)
- | [] -> intern env body
+ | [] -> intern isarity env body
and intern_impargs c env l subscopes args =
let rec aux n l subscopes args =
@@ -472,7 +490,7 @@ let internalise sigma env allow_soapp lvar c =
| (imp::l', (a,Some j)::args') ->
if is_status_implicit imp & j>=n then
if j=n then
- (intern enva a)::(aux (n+1) l' subscopes' args')
+ (intern false enva a)::(aux (n+1) l' subscopes' args')
else
(RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
else
@@ -483,7 +501,7 @@ let internalise sigma env allow_soapp lvar c =
if is_status_implicit imp then
(RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
else
- (intern enva a)::(aux (n+1) l' subscopes' args')
+ (intern false enva a)::(aux (n+1) l' subscopes' args')
| ([],args) -> intern_tailargs env subscopes args
| (_::l',[]) ->
if List.for_all is_status_implicit l then
@@ -497,18 +515,18 @@ let internalise sigma env allow_soapp lvar c =
raise (InternalisationError (constr_loc a, WrongExplicitImplicit))
| (a,None)::args ->
let (enva,subscopes) = apply_scope_env env subscopes in
- (intern enva a) :: (intern_tailargs env subscopes args)
+ (intern false enva a) :: (intern_tailargs env subscopes args)
| [] -> []
and intern_args env subscopes = function
| [] -> []
| a::args ->
let (enva,subscopes) = apply_scope_env env subscopes in
- (intern enva a) :: (intern_args env subscopes args)
+ (intern false enva a) :: (intern_args env subscopes args)
in
try
- intern env c
+ intern isarity env c
with
InternalisationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalisation_error e)
@@ -522,21 +540,26 @@ let extract_ids env =
(Termops.ids_of_rel_context (Environ.rel_context env))
Idset.empty
-let interp_rawconstr_gen sigma env impls allow_soapp lvar c =
- internalise sigma (extract_ids env, impls, Symbols.current_scopes ())
- allow_soapp (lvar,Environ.named_context env) c
+let interp_rawconstr_gen isarity sigma env impls allow_soapp lvar c =
+ internalise isarity sigma (extract_ids env, impls, [])
+ allow_soapp (lvar,Environ.named_context env, []) c
let interp_rawconstr sigma env c =
- interp_rawconstr_gen sigma env [] false [] c
+ interp_rawconstr_gen false sigma env [] false [] c
+
+let interp_rawtype sigma env c =
+ interp_rawconstr_gen true sigma env [] false [] c
-let interp_rawconstr_with_implicits sigma env impls c =
- interp_rawconstr_gen sigma env impls false [] c
+let interp_rawtype_with_implicits sigma env impls c =
+ interp_rawconstr_gen true sigma env impls false [] c
+(*
(* The same as interp_rawconstr but with a list of variables which must not be
globalized *)
let interp_rawconstr_wo_glob sigma env lvar c =
interp_rawconstr_gen sigma env [] false lvar c
+*)
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -551,10 +574,10 @@ let interp_casted_openconstr sigma env c typ =
understand_gen_tcc sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
let interp_type sigma env c =
- understand_type sigma env (interp_rawconstr sigma env c)
+ understand_type sigma env (interp_rawtype sigma env c)
let interp_type_with_implicits sigma env impls c =
- understand_type sigma env (interp_rawconstr_with_implicits sigma env impls c)
+ understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
let judgment_of_rawconstr sigma env c =
understand_judgment sigma env (interp_rawconstr sigma env c)
@@ -574,14 +597,14 @@ let retype_list sigma env lst =
(* of instantiations (variables and metas) *)
(* Note: typ is retyped *)
let interp_constr_gen sigma env lvar lmeta c exptyp =
- let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c
+ let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
and rtype lst = retype_list sigma env lst in
understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;;
(*Interprets a casted constr according to two lists of instantiations
(variables and metas)*)
let interp_openconstr_gen sigma env lvar lmeta c exptyp =
- let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c
+ let c = interp_rawconstr_gen false sigma env [] false (List.map fst lvar) c
and rtype lst = retype_list sigma env lst in
understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
@@ -636,12 +659,21 @@ let pattern_of_rawconstr lvar c =
(!metas,p)
let interp_constrpattern_gen sigma env lvar c =
- let c = interp_rawconstr_gen sigma env [] true (List.map fst lvar) c in
+ let c = interp_rawconstr_gen false sigma env [] true (List.map fst lvar) c in
let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
pattern_of_rawconstr nlvar c
let interp_constrpattern sigma env c =
interp_constrpattern_gen sigma env [] c
-let interp_aconstr a =
- aconstr_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a)
+let interp_aconstr vars a =
+ let env = Global.env () in
+ (* [vl] is intended to remember the scope of the free variables of [a] *)
+ let vl = List.map (fun id -> (id,ref None)) vars in
+ let c = for_grammar (internalise false Evd.empty (extract_ids env, [], [])
+ false ([],Environ.named_context env,vl)) a in
+ (* Translate and check that [c] has all its free variables bound in [vars] *)
+ let a = aconstr_of_rawconstr vars c in
+ (* Returns [a] and the ordered list of variables with their scopes *)
+ (* Variables occuring in binders have no relevant scope since bound *)
+ List.map (fun (id,r) -> (id,match !r with None -> [] | Some l -> l)) vl, a
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 8666db633..4c185a788 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -36,7 +36,7 @@ type implicits_env = (identifier * Impargs.implicits_list) list
(* Interprets global names, including syntactic defs and section variables *)
val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr
-val interp_rawconstr_gen : evar_map -> env -> implicits_env ->
+val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env ->
bool -> identifier list -> constr_expr -> rawconstr
(*s Composing the translation with typing *)
@@ -83,7 +83,7 @@ val interp_constrpattern :
val interp_reference : identifier list -> reference -> rawconstr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : constr_expr -> aconstr
+val interp_aconstr : identifier list -> constr_expr -> interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 6fc3c93c0..6a02f284b 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -58,8 +58,9 @@ let empty_scope = {
let default_scope = "core_scope"
let type_scope = "type_scope"
-let _ = Stringmap.add default_scope empty_scope !scope_map
-let _ = Stringmap.add type_scope empty_scope !scope_map
+let init_scope_map () =
+ scope_map := Stringmap.add default_scope empty_scope !scope_map;
+ scope_map := Stringmap.add type_scope empty_scope !scope_map
(**********************************************************************)
(* The global stack of scopes *)
@@ -225,7 +226,7 @@ let rec find_interpretation f = function
let rec interp_notation ntn scopes =
let f scope = fst (Stringmap.find ntn scope.notations) in
- try find_interpretation f scopes
+ try find_interpretation f (scopes @ !scope_stack)
with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
let uninterp_notations c =
@@ -236,24 +237,22 @@ let availability_of_notation (ntn_scope,ntn) scopes =
Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
find_without_delimiters f ntn_scope scopes
-let rec interp_numeral loc n = function
+let rec interp_numeral_gen loc f n = function
| scope :: scopes ->
- (try fst (lookup_numeral_interpreter loc scope) loc n
- with Not_found -> interp_numeral loc n scopes)
+ (try f (lookup_numeral_interpreter loc scope)
+ with Not_found -> interp_numeral_gen loc f n scopes)
| [] ->
user_err_loc (loc,"interp_numeral",
str "No interpretation for numeral " ++ pr_bigint n)
-let rec interp_numeral_as_pattern loc n name = function
- | scope :: scopes ->
- (try
- match snd (lookup_numeral_interpreter loc scope) with
- | None -> raise Not_found
- | Some g -> g loc n name
- with Not_found -> interp_numeral_as_pattern loc n name scopes)
- | [] ->
- user_err_loc (loc,"interp_numeral_as_pattern",
- str "No interpretation for numeral " ++ pr_bigint n)
+let interp_numeral loc n scopes =
+ interp_numeral_gen loc (fun x -> fst x loc n) n (scopes@ !scope_stack)
+
+let interp_numeral_as_pattern loc n name scopes =
+ let f x = match snd x with
+ | None -> raise Not_found
+ | Some g -> g loc n name in
+ interp_numeral_gen loc f n (scopes@ !scope_stack)
let uninterp_numeral c =
try
@@ -365,6 +364,34 @@ let pr_scopes prraw =
(fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
!scope_map (mt ())
+let rec find_default ntn = function
+ | scope::_ when Stringmap.mem ntn (find_scope scope).notations -> scope
+ | _::scopes -> find_default ntn scopes
+ | [] -> raise Not_found
+
+let locate_notation prraw ntn =
+ let ntn = if String.contains ntn ' ' then ntn else "_ "^ntn^" _" in
+ let l =
+ Stringmap.fold
+ (fun scope_name sc l ->
+ try
+ let ((_,r),(_,df)) = Stringmap.find ntn sc.notations in
+ (scope_name,r,df)::l
+ with Not_found -> l) !scope_map []
+ in
+ if l = [] then
+ str "Unknown notation"
+ else
+ let scope = find_default ntn !scope_stack in
+ prlist
+ (fun (sc,r,df) ->
+ hov 0 (
+ pr_notation_info prraw df r ++ brk (1,2) ++
+ str ": " ++ str sc ++
+ (if sc = scope then str " (default interpretation)" else mt ()) ++
+ fnl ()))
+ l
+
(**********************************************************************)
(* Mapping notations to concrete syntax *)
@@ -397,8 +424,8 @@ let unfreeze (scm,scs,asc,dlm,fkm,pprules) =
printing_rules := pprules
let init () =
+ init_scope_map ();
(*
- scope_map := Stringmap.empty;
scope_stack := Stringmap.empty
arguments_scope := Refmap.empty
*)
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 17b99dbd4..c8c844312 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -33,6 +33,7 @@ type scope
type scopes = scope_name list
val default_scope : scope_name
+val type_scope : scope_name
val declare_scope : scope_name -> unit
(* Open scope *)
@@ -114,6 +115,7 @@ val find_arguments_scope : global_reference -> scope_name option list
(* Prints scopes (expect a pure aconstr printer *)
val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
+val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
(**********************************************************************)
(*s Printing rules for notations *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7c1e9aea5..aa78ec5e0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -136,15 +136,26 @@ let rec subst_aconstr subst raw =
if r1' == r1 && r2' == r2 then raw else
ACast (r1',r2')
-let rec aux = function
- | RVar (_,id) -> AVar id
+let add_name r = function
+ | Anonymous -> ()
+ | Name id -> r := id :: !r
+
+let aconstr_of_rawconstr vars a =
+ let found = ref [] in
+ let bound_binders = ref [] in
+ let rec aux = function
+ | RVar (_,id) ->
+ if not (List.mem id !bound_binders) then found := id::!found;
+ AVar id
| RApp (_,g,args) -> AApp (aux g, List.map aux args)
- | RLambda (_,na,ty,c) -> ALambda (na,aux ty,aux c)
- | RProd (_,na,ty,c) -> AProd (na,aux ty,aux c)
- | RLetIn (_,na,b,c) -> ALetIn (na,aux b,aux c)
+ | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
+ | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
+ | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
| RCases (_,tyopt,tml,eqnl) ->
- let eqnl = List.map (fun (_,idl,pat,rhs) -> (idl,pat,aux rhs)) eqnl in
- ACases (option_app aux tyopt,List.map aux tml, eqnl)
+ let f (_,idl,pat,rhs) =
+ bound_binders := idl@(!bound_binders);
+ (idl,pat,aux rhs) in
+ ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl)
| ROrderedCase (_,b,tyopt,tm,bv) ->
AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
| RCast (_,c,t) -> ACast (aux c,aux t)
@@ -153,10 +164,15 @@ let rec aux = function
| RRef (_,r) -> ARef r
| RMeta (_,n) -> AMeta n
| RDynamic _ | RRec _ | REvar _ ->
- error "Fixpoints, cofixpoints and existential variables are not \
+ error "Fixpoints, cofixpoints, existential variables and pattern-matching not \
allowed in abbreviatable expressions"
-
-let aconstr_of_rawconstr = aux
+ in
+ let a = aux a in
+ let check_type x =
+ if not (List.mem x !found or List.mem x !bound_binders) then
+ error ((string_of_id x)^" is unbound in the right-hand-side") in
+ List.iter check_type vars;
+ a
(* Pattern-matching rawconstr and aconstr *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 35f62478e..5c452b870 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -43,7 +43,7 @@ val map_aconstr_with_binders_loc : loc ->
val subst_aconstr : Names.substitution -> aconstr -> aconstr
-val aconstr_of_rawconstr : rawconstr -> aconstr
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
(* [match_aconstr metas] match a rawconstr against an aconstr with
metavariables in [metas]; it raises [No_match] if the matching fails *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 02:12:11 +0000