aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-14 18:37:54 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-14 18:37:54 +0000
commite88e0b2140bdd2d194a52bc09f8338b5667d0f92 (patch)
tree67ca22f77ddb98725456e5f9a0b5ad613ae28da5 /interp
parente4efb857fa9053c41e4c030256bd17de7e24542f (diff)
Réforme de l'interprétation des termes :
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml360
-rw-r--r--interp/constrextern.mli49
-rw-r--r--interp/constrintern.ml653
-rw-r--r--interp/constrintern.mli87
-rw-r--r--interp/coqlib.ml285
-rw-r--r--interp/coqlib.mli133
-rw-r--r--interp/genarg.ml185
-rw-r--r--interp/genarg.mli213
-rw-r--r--interp/modintern.ml103
-rw-r--r--interp/modintern.mli24
-rw-r--r--interp/ppextend.ml57
-rw-r--r--interp/ppextend.mli47
-rw-r--r--interp/symbols.ml331
-rw-r--r--interp/symbols.mli77
-rw-r--r--interp/syntax_def.ml72
-rw-r--r--interp/syntax_def.mli23
-rw-r--r--interp/topconstr.ml300
-rw-r--r--interp/topconstr.mli133
18 files changed, 3132 insertions, 0 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
new file mode 100644
index 000000000..b9f22ff00
--- /dev/null
+++ b/interp/constrextern.ml
@@ -0,0 +1,360 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Util
+open Univ
+open Names
+open Nameops
+open Term
+open Termops
+open Inductive
+open Sign
+open Environ
+open Libnames
+open Declare
+open Impargs
+open Topconstr
+open Rawterm
+open Pattern
+open Nametab
+(*i*)
+
+(* Translation from rawconstr to front constr *)
+
+(**********************************************************************)
+(* Parametrization *)
+
+(* This governs printing of local context of references *)
+let print_arguments = ref false
+
+(* If true, prints local context of evars, whatever print_arguments *)
+let print_evar_arguments = ref false
+
+(* This forces printing of cast nodes *)
+let print_casts = ref true
+
+(* This governs printing of implicit arguments. When
+ [print_implicits] is on then [print_implicits_explicit_args] tells
+ how implicit args are printed. If on, implicit args are printed
+ prefixed by "!" otherwise the function and not the arguments is
+ prefixed by "!" *)
+let print_implicits = ref false
+let print_implicits_explicit_args = ref false
+
+(* This forces printing of coercions *)
+let print_coercions = ref false
+
+(* This forces printing universe names of Type{.} *)
+let print_universes = ref false
+
+
+let with_option o f x =
+ let old = !o in o:=true;
+ try let r = f x in o := old; r
+ with e -> o := old; raise e
+
+let with_arguments f = with_option print_arguments f
+let with_casts f = with_option print_casts f
+let with_implicits f = with_option print_implicits f
+let with_coercions f = with_option print_coercions f
+let with_universes f = with_option print_universes f
+
+(**********************************************************************)
+(* conversion of references *)
+
+let ids_of_ctxt ctxt =
+ Array.to_list
+ (Array.map
+ (function c -> match kind_of_term c with
+ | Var id -> id
+ | _ ->
+ error
+ "Termast: arbitrary substitution of references not yet implemented")
+ ctxt)
+
+let idopt_of_name = function
+ | Name id -> Some id
+ | Anonymous -> None
+
+let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
+
+let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r)
+
+(**********************************************************************)
+(* conversion of patterns *)
+
+let rec extern_cases_pattern = function (* loc is thrown away for printing *)
+ | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
+ | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+ | PatCstr(loc,cstrsp,args,na) ->
+ let args = List.map extern_cases_pattern args in
+ let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in
+ (match na with
+ | Name id -> CPatAlias (loc,p,id)
+ | Anonymous -> p)
+
+let occur_name na aty =
+ match na with
+ | Name id -> occur_var_constr_expr id aty
+ | Anonymous -> false
+
+(* Implicit args indexes are in ascending order *)
+let explicitize impl f args =
+ let n = List.length args in
+ let rec exprec q = function
+ | a::args, imp::impl when is_status_implicit imp ->
+ let tail = exprec (q+1) (args,impl) in
+ let visible =
+ (!print_implicits & !print_implicits_explicit_args)
+ or not (is_inferable_implicit n imp) in
+ if visible then (a,Some q) :: tail else tail
+ | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
+ | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
+ | [], _ -> [] in
+ let args = exprec 1 (args,impl) in
+ if args = [] then f else CApp (dummy_loc, f, args)
+
+let rec skip_coercion dest_ref (f,args as app) =
+ if !print_coercions then app
+ else
+ try
+ match dest_ref f with
+ | Some r ->
+ (match Classops.hide_coercion r with
+ | Some n ->
+ if n >= List.length args then app
+ else (* We skip a coercion *)
+ let _,fargs = list_chop n args in
+ skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+ | None -> app)
+ | None -> app
+ with Not_found -> app
+
+let extern_app impl f args =
+ if !print_implicits & not !print_implicits_explicit_args then
+ CAppExpl (dummy_loc, f, args)
+ else
+ explicitize impl (CRef f) args
+
+let loc = dummy_loc
+
+let rec extern = function
+ | RRef (_,ref) -> CRef (extern_ref ref)
+
+ | RVar (_,id) -> CRef (Ident (loc,id))
+
+ | REvar (_,n) -> extern_evar loc n
+
+ | RMeta (_,n) -> CMeta (loc,n)
+
+ | RApp (_,f,args) ->
+ let (f,args) =
+ skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
+ let args = List.map extern args in
+ (match f with
+ | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
+ | RRef (loc,ref) ->
+ extern_app (implicits_of_global ref) (extern_ref ref) args
+ | _ -> explicitize [] (extern f) args)
+
+ | RProd (_,Anonymous,t,c) ->
+ (* Anonymous product are never factorized *)
+ CArrow (loc,extern t,extern c)
+
+ | RLetIn (_,na,t,c) ->
+ CLetIn (loc,(loc,na),extern t,extern c)
+
+ | RProd (_,na,t,c) ->
+ let t = extern t in
+ let (idl,c) = factorize_prod t c in
+ CProdN (loc,[(loc,na)::idl,t],c)
+
+ | RLambda (_,na,t,c) ->
+ let t = extern t in
+ let (idl,c) = factorize_lambda t c in
+ CLambdaN (loc,[(loc,na)::idl,t],c)
+
+ | RCases (_,typopt,tml,eqns) ->
+ let pred = option_app extern typopt in
+ let tml = List.map extern tml in
+ let eqns = List.map extern_eqn eqns in
+ CCases (loc,pred,tml,eqns)
+
+ | ROrderedCase (_,cs,typopt,tm,bv) ->
+ let bv = Array.to_list (Array.map extern bv) in
+ COrderedCase (loc,cs,option_app extern typopt,extern tm,bv)
+
+ | RRec (_,fk,idv,tyv,bv) ->
+ (match fk with
+ | RFix (nv,n) ->
+ let rec split_lambda binds = function
+ | (0, t) -> (List.rev binds,extern t)
+ | (n, RLambda (_,na,t,b)) ->
+ split_lambda (([loc,na],extern t)::binds) (n-1,b)
+ | _ -> anomaly "extern: ill-formed fixpoint body" in
+ let rec split_product = function
+ | (0, t) -> extern t
+ | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
+ | _ -> anomaly "extern: ill-formed fixpoint type" in
+ let listdecl =
+ Array.mapi
+ (fun i fi ->
+ let (lparams,def) = split_lambda [] (nv.(i)+1,bv.(i)) in
+ let typ = split_product (nv.(i)+1,tyv.(i)) in
+ (fi, lparams, typ, def))
+ idv
+ in
+ CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
+ | RCoFix n ->
+ let listdecl =
+ Array.mapi (fun i fi -> (fi,extern tyv.(i),extern bv.(i))) idv
+ in
+ CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
+
+ | RSort (_,s) ->
+ let s = match s with
+ | RProp _ -> s
+ | RType (Some _) when !print_universes -> s
+ | RType _ -> RType None in
+ CSort (loc,s)
+
+ | RHole (_,e) -> CHole loc
+
+ | RCast (_,c,t) -> CCast (loc,extern c,extern t)
+
+ | RDynamic (_,d) -> CDynamic (loc,d)
+
+and factorize_prod aty = function
+ | RProd (_,Name id,ty,c)
+ when aty = extern ty
+ & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
+ -> let (nal,c) = factorize_prod aty c in ((loc,Name id)::nal,c)
+ | c -> ([],extern c)
+
+and factorize_lambda aty = function
+ | RLambda (_,na,ty,c)
+ when aty = extern ty
+ & not (occur_name na aty) (* To avoid na in ty' escapes scope *)
+ -> let (nal,c) = factorize_lambda aty c in ((loc,na)::nal,c)
+ | c -> ([],extern c)
+
+and extern_eqn (loc,ids,pl,c) =
+ (loc,List.map extern_cases_pattern pl,extern c)
+(*
+and extern_numerals r =
+ on_numeral (fun p ->
+ match filter p r with
+ | Some f
+
+and extern_symbols r =
+*)
+
+let extern_rawconstr = extern
+
+(******************************************************************)
+(* Main translation function from constr -> constr_expr *)
+
+let extern_constr at_top env t =
+ let t' =
+ if !print_casts then t
+ else Reductionops.local_strong strip_outer_cast t in
+ let avoid = if at_top then ids_of_context env else [] in
+ extern (Detyping.detype env avoid (names_of_rel_context env) t')
+
+(******************************************************************)
+(* Main translation function from pattern -> constr_expr *)
+
+let rec extern_pattern tenv env = function
+ | PRef ref -> CRef (extern_ref ref)
+
+ | PVar id -> CRef (Ident (loc,id))
+
+ | PEvar n -> extern_evar loc n
+
+ | PRel n ->
+ CRef (Ident (loc,
+ try match lookup_name_of_rel n env with
+ | Name id -> id
+ | Anonymous ->
+ anomaly "ast_of_pattern: index to an anonymous variable"
+ with Not_found ->
+ id_of_string ("[REL "^(string_of_int n)^"]")))
+
+ | PMeta None -> CHole loc
+
+ | PMeta (Some n) -> CMeta (loc,n)
+
+ | PApp (f,args) ->
+ let (f,args) =
+ skip_coercion (function PRef r -> Some r | _ -> None)
+ (f,Array.to_list args) in
+ let args = List.map (extern_pattern tenv env) args in
+ (match f with
+ | PRef ref ->
+ extern_app (implicits_of_global ref) (extern_ref ref) args
+ | _ -> explicitize [] (extern_pattern tenv env f) args)
+
+ | PSoApp (n,args) ->
+ let args = List.map (extern_pattern tenv env) args in
+ (* [-n] is the trick to embed a so patten into a regular application *)
+ (* see constrintern.ml and g_constr.ml4 *)
+ explicitize [] (CMeta (loc,-n)) args
+
+ | PProd (Anonymous,t,c) ->
+ (* Anonymous product are never factorized *)
+ CArrow (loc,extern_pattern tenv env t,extern_pattern tenv env c)
+
+ | PLetIn (na,t,c) ->
+ CLetIn (loc,(loc,na),extern_pattern tenv env t,extern_pattern tenv env c)
+
+ | PProd (na,t,c) ->
+ let t = extern_pattern tenv env t in
+ let (idl,c) = factorize_prod_pattern tenv (add_name na env) t c in
+ CProdN (loc,[(loc,na)::idl,t],c)
+
+ | PLambda (na,t,c) ->
+ let t = extern_pattern tenv env t in
+ let (idl,c) = factorize_lambda_pattern tenv (add_name na env) t c in
+ CLambdaN (loc,[(loc,na)::idl,t],c)
+
+ | PCase (cs,typopt,tm,bv) ->
+ let bv = Array.to_list (Array.map (extern_pattern tenv env) bv) in
+ COrderedCase
+ (loc,cs,option_app (extern_pattern tenv env) typopt,
+ extern_pattern tenv env tm,bv)
+
+ | PFix f -> extern (Detyping.detype tenv [] env (mkFix f))
+
+ | PCoFix c -> extern (Detyping.detype tenv [] env (mkCoFix c))
+
+ | PSort s ->
+ let s = match s with
+ | RProp _ -> s
+ | RType (Some _) when !print_universes -> s
+ | RType _ -> RType None in
+ CSort (loc,s)
+
+and factorize_prod_pattern tenv env aty = function
+ | PProd (Name id as na,ty,c)
+ when aty = extern_pattern tenv env ty
+ & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
+ -> let (nal,c) = factorize_prod_pattern tenv (na::env) aty c in
+ ((loc,Name id)::nal,c)
+ | c -> ([],extern_pattern tenv env c)
+
+and factorize_lambda_pattern tenv env aty = function
+ | PLambda (na,ty,c)
+ when aty = extern_pattern tenv env ty
+ & not (occur_name na aty) (* To avoid na in ty' escapes scope *)
+ -> let (nal,c) = factorize_lambda_pattern tenv (add_name na env) aty c
+ in ((loc,na)::nal,c)
+ | c -> ([],extern_pattern tenv env c)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
new file mode 100644
index 000000000..cfa00c006
--- /dev/null
+++ b/interp/constrextern.mli
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Termops
+open Sign
+open Environ
+open Libnames
+open Nametab
+open Rawterm
+open Pattern
+open Topconstr
+(*i*)
+
+(* Translation of pattern, cases pattern, rawterm and term into syntax
+ trees for printing *)
+
+val extern_cases_pattern : cases_pattern -> cases_pattern_expr
+val extern_rawconstr : rawconstr -> constr_expr
+val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
+
+(* If [b=true] in [extern_constr b env c] then the variables in the first
+ level of quantification clashing with the variables in [env] are renamed *)
+
+val extern_constr : bool -> env -> constr -> constr_expr
+val extern_ref : global_reference -> reference
+
+(* For debugging *)
+val print_implicits : bool ref
+val print_casts : bool ref
+val print_arguments : bool ref
+val print_evar_arguments : bool ref
+val print_coercions : bool ref
+val print_universes : bool ref
+
+val with_casts : ('a -> 'b) -> 'a -> 'b
+val with_implicits : ('a -> 'b) -> 'a -> 'b
+val with_arguments : ('a -> 'b) -> 'a -> 'b
+val with_coercions : ('a -> 'b) -> 'a -> 'b
+val with_universes : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
new file mode 100644
index 000000000..2ce1a4db0
--- /dev/null
+++ b/interp/constrintern.ml
@@ -0,0 +1,653 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Options
+open Names
+open Nameops
+open Libnames
+open Impargs
+open Rawterm
+open Pattern
+open Pretyping
+open Topconstr
+open Nametab
+open Symbols
+
+type implicits_env = (identifier * Impargs.implicits_list) list
+
+let interning_grammar = ref false
+
+let for_grammar f x =
+ interning_grammar := true;
+ let a = f x in
+ interning_grammar := false;
+ a
+
+(**********************************************************************)
+(* Internalisation errors *)
+
+type internalisation_error =
+ | VariableCapture of identifier
+ | WrongExplicitImplicit
+ | NegativeMetavariable
+ | NotAConstructor of reference
+ | UnboundFixName of bool * identifier
+ | NonLinearPattern of identifier
+ | BadPatternsNumber of int * int
+ | BadExplicitationNumber of int * int option
+
+exception InternalisationError of loc * internalisation_error
+
+let explain_variable_capture id =
+ str "The variable " ++ pr_id id ++ str " occurs in its type"
+
+let explain_wrong_explicit_implicit =
+ str "Found an explicitely given implicit argument but was expecting" ++
+ fnl () ++ str "a regular one"
+
+let explain_negative_metavariable =
+ str "Metavariable numbers must be positive"
+
+let explain_not_a_constructor ref =
+ str "Unknown constructor: " ++ pr_reference ref
+
+let explain_unbound_fix_name is_cofix id =
+ str "The name" ++ spc () ++ pr_id id ++
+ spc () ++ str "is not bound in the corresponding" ++ spc () ++
+ str (if is_cofix then "co" else "") ++ str "fixpoint definition"
+
+let explain_non_linear_pattern id =
+ str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
+
+let explain_bad_patterns_number n1 n2 =
+ let s = if n1 > 1 then "s" else "" in
+ str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found "
+ ++ int n2
+
+let explain_bad_explicitation_number n po =
+ let s = match po with
+ | None -> "a regular argument"
+ | Some p -> string_of_int p in
+ str "Bad explicitation number: found " ++ int n ++
+ str" but was expecting " ++ str s
+
+let explain_internalisation_error = function
+ | VariableCapture id -> explain_variable_capture id
+ | WrongExplicitImplicit -> explain_wrong_explicit_implicit
+ | NegativeMetavariable -> explain_negative_metavariable
+ | NotAConstructor ref -> explain_not_a_constructor ref
+ | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
+ | NonLinearPattern id -> explain_non_linear_pattern id
+ | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
+ | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
+
+(**********************************************************************)
+(* Dump of globalization (to be used by coqdoc) *)
+
+let add_glob loc ref =
+(*i
+ let sp = Nametab.sp_of_global (Global.env ()) ref in
+ let dir,_ = repr_path sp in
+ let rec find_module d =
+ try
+ let qid = let dir,id = split_dirpath d in make_qualid dir id in
+ let _ = Nametab.locate_loaded_library qid in d
+ with Not_found -> find_module (dirpath_prefix d)
+ in
+ let s = string_of_dirpath (find_module dir) in
+ i*)
+ let sp = Nametab.sp_of_global None ref in
+ let id = let _,id = repr_path sp in string_of_id id in
+ let dp = string_of_dirpath (Declare.library_part ref) in
+ dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp 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 *)
+
+(* Is it a bound variables? *)
+let intern_var (env,impls,_) (vars1,vars2) loc id =
+ let imps, args_scopes =
+ (* Is [id] bound in *)
+ if Idset.mem id env or List.mem id vars1
+ then
+ try List.assoc id impls, []
+ with Not_found -> [], []
+ else
+ (* Is [id] a section variable *)
+ let _ = Sign.lookup_named id vars2 in
+ (* Car Fixpoint met les fns définies temporairement comme vars de sect *)
+ try
+ let ref = VarRef id in
+ implicits_of_global ref, find_arguments_scope ref
+ with _ -> [], []
+ in RVar (loc, id), imps, args_scopes
+
+(* Is it a global reference or a syntactic definition? *)
+let intern_qualid env vars loc qid =
+ try match Nametab.extended_locate qid with
+ | TrueGlobal ref ->
+ if !dump then add_glob loc ref;
+ RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref
+ | SyntacticDef sp ->
+ (Syntax_def.search_syntactic_definition loc sp),[],[]
+ with Not_found ->
+ error_global_not_found_loc loc qid
+
+let intern_reference env lvar = function
+ | Qualid (loc, qid) ->
+ intern_qualid env lvar loc qid
+ | Ident (loc, id) ->
+ (* For old ast syntax compatibility *)
+ if (string_of_id id).[0] = '$' then RVar (loc,id),[],[] else
+ (* End old ast syntax compatibility *)
+ try intern_var env lvar loc id
+ with Not_found ->
+ try intern_qualid env lvar loc (make_short_qualid id)
+ with e ->
+ (* Extra allowance for grammars *)
+ if !interning_grammar then begin
+ if_verbose warning ("Could not globalize " ^ (string_of_id id));
+ RVar (loc, id), [], []
+ end
+ else raise e
+
+let apply_scope_env (ids,impls,scopes as env) = function
+ | [] -> env, []
+ | (Some sc)::scl -> (ids,impls,sc::scopes), scl
+ | None::scl -> env, scl
+
+(**********************************************************************)
+(* Cases *)
+
+(* Check linearity of pattern-matching *)
+let rec has_duplicate = function
+ | [] -> None
+ | x::l -> if List.mem x l then (Some x) else has_duplicate l
+
+let loc_of_lhs lhs =
+ join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs))
+
+let check_linearity lhs ids =
+ match has_duplicate ids with
+ | Some id ->
+ raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id))
+ | None ->
+ ()
+
+(* Warns if some pattern variable starts with uppercase *)
+let check_uppercase loc ids =
+(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe
+ let is_uppercase_var v =
+ match (string_of_id v).[0] with 'A'..'Z' -> true | _ -> false
+ in
+ let warning_uppercase loc uplid =
+ let vars = h 0 (prlist_with_sep pr_coma pr_id uplid) in
+ let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
+ warn (str ("the variable"^s1) ++ vars ++
+ str (" start"^s2^"with an upper case letter in pattern")) in
+ let uplid = List.filter is_uppercase_var ids in
+ if uplid <> [] then warning_uppercase loc uplid
+*)
+ ()
+
+(* Match the number of pattern against the number of matched args *)
+let check_number_of_pattern loc n l =
+ let p = List.length l in
+ if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
+
+(* Manage multiple aliases *)
+
+ (* [merge_aliases] returns the sets of all aliases encountered at this
+ point and a substitution mapping extra aliases to the first one *)
+let merge_aliases (ids,subst as aliases) id =
+ ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
+
+let alias_of = function
+ | ([],_) -> Anonymous
+ | (id::_,_) -> Name id
+
+let message_redundant_alias (id1,id2) =
+ if_verbose warning
+ ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
+
+(* Differentiating between constructors and matching variables *)
+type pattern_qualid_kind =
+ | ConstrPat of constructor
+ | VarPat of identifier
+
+let find_constructor ref =
+ let (loc,qid) = qualid_of_reference ref in
+ try match extended_locate qid with
+ | SyntacticDef sp ->
+ (match Syntax_def.search_syntactic_definition loc sp with
+ | RRef (_,(ConstructRef c as x)) ->
+ if !dump then add_glob loc x;
+ c
+ | _ ->
+ raise (InternalisationError (loc,NotAConstructor ref)))
+ | TrueGlobal r ->
+ let rec unf = function
+ | ConstRef cst ->
+ (try
+ let v = Environ.constant_value (Global.env()) cst in
+ unf (reference_of_constr v)
+ with
+ Environ.NotEvaluableConst _ | Not_found ->
+ raise (InternalisationError (loc,NotAConstructor ref)))
+ | ConstructRef c ->
+ if !dump then add_glob loc r;
+ c
+ | _ -> raise (InternalisationError (loc,NotAConstructor ref))
+ in unf r
+ with Not_found ->
+ raise (InternalisationError (loc,NotAConstructor ref))
+
+let find_pattern_variable = function
+ | Ident (loc,id) -> id
+ | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
+
+let maybe_constructor ref =
+ try ConstrPat (find_constructor ref)
+ with InternalisationError _ -> VarPat (find_pattern_variable ref)
+
+let rec intern_cases_pattern scopes aliases = function
+ | CPatAlias (loc, p, id) ->
+ let aliases' = merge_aliases aliases id in
+ intern_cases_pattern scopes aliases' p
+ | CPatCstr (loc, head, pl) ->
+ let c = find_constructor head in
+ let (idsl,pl') =
+ List.split (List.map (intern_cases_pattern scopes ([],[])) pl)
+ in
+ (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases))
+ | CPatNumeral (loc, n) ->
+ ([aliases],
+ Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
+ | CPatDelimiters (_, sc, e) ->
+ intern_cases_pattern (sc::scopes) aliases e
+ | CPatAtom (loc, Some head) ->
+ (match maybe_constructor head with
+ | ConstrPat c ->
+ ([aliases], PatCstr (loc,c,[],alias_of aliases))
+ | VarPat id ->
+ let aliases = merge_aliases aliases id in
+ ([aliases], PatVar (loc,alias_of aliases)))
+ | CPatAtom (loc, None) ->
+ ([aliases], PatVar (loc,alias_of aliases))
+
+(**********************************************************************)
+(* Fix and CoFix *)
+
+let rec intern_fix = function
+ | [] -> ([],[],[],[])
+ | (fi, bl, c, t)::rest->
+ let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+ let (lf,ln,lc,lt) = intern_fix rest in
+ (fi::lf, ni::ln,
+ CProdN (dummy_loc, bl, c)::lc,
+ CLambdaN (dummy_loc, bl, t)::lt)
+
+let rec intern_cofix = function
+ | [] -> ([],[],[])
+ | (fi, c, t)::rest ->
+ let (lf,lc,lt) = intern_cofix rest in
+ (fi::lf, c::lc, t::lt)
+
+(**********************************************************************)
+(* Utilities for binders *)
+
+let check_capture loc ty = function
+ | Name id when occur_var_constr_expr id ty ->
+ raise (InternalisationError (loc,VariableCapture id))
+ | _ ->
+ ()
+
+let locate_if_isevar loc id = function
+ | RHole _ -> RHole (loc, AbstractionType id)
+ | x -> x
+
+(**********************************************************************)
+(* Utilities for application *)
+
+let set_hole_implicit i = function
+ | RRef (loc,r) -> (loc,ImplicitArg (r,i))
+ | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
+ | _ -> anomaly "Only refs have implicits"
+
+(**********************************************************************)
+(* Syntax extensions *)
+
+let coerce_to_id = function
+ | CRef (Ident (_,id)) -> id
+ | c ->
+ user_err_loc (constr_loc c, "subst_rawconstr",
+ str"This expression should be a simple identifier")
+
+let traverse_binder id (subst,(ids,impls,scopes as env)) =
+ try
+ let id' = coerce_to_id (List.assoc id subst) in
+ id', (subst,(Idset.add id' ids,impls,scopes))
+ with Not_found ->
+ id, (List.remove_assoc id subst,env)
+
+let rec subst_rawconstr loc interp (subst,env as senv) = function
+ | AVar id ->
+ let a = try List.assoc id subst
+ with Not_found -> CRef (Ident (dummy_loc,id)) in
+ interp env a
+ | t ->
+ map_aconstr_with_binders_loc loc traverse_binder
+ (subst_rawconstr loc interp) senv t
+
+(**********************************************************************)
+(* Main loop *)
+
+let internalise sigma env allow_soapp lvar c =
+ let rec intern (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
+ | [] -> c
+ | l -> RApp (constr_loc x, c, l))
+ | CFix (loc, (locid,iddef), ldecl) ->
+ let (lf,ln,lc,lt) = intern_fix ldecl in
+ let n =
+ try
+ (list_index iddef lf) -1
+ with Not_found ->
+ 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
+ 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
+ let n =
+ try
+ (list_index iddef lf) -1
+ with Not_found ->
+ 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
+ RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
+ | CArrow (loc,c1,c2) ->
+ RProd (loc, Anonymous, intern env c1, intern env c2)
+ | CProdN (loc,[],c2) ->
+ intern env c2
+ | CProdN (loc,(nal,ty)::bll,c2) ->
+ iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
+ | CLambdaN (loc,[],c2) ->
+ intern env c2
+ | CLambdaN (loc,(nal,ty)::bll,c2) ->
+ iterate_lam loc 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)
+ | CNotation (loc,ntn,args) ->
+ subst_rawconstr loc intern (args,env)
+ (Symbols.interp_notation ntn scopes)
+ | CNumeral (loc, n) ->
+ Symbols.interp_numeral loc n scopes
+ | CDelimiters (loc, sc, e) ->
+ intern (ids,impls,sc::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)
+ | CApp (loc, f, args) ->
+ let (c, impargs, args_scopes) =
+ match f with
+ | CRef ref -> intern_reference env lvar ref
+ | _ -> (intern 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,
+ 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))
+ | CHole loc ->
+ RHole (loc, QuestionMark)
+ | CMeta (loc, n) when n >=0 or allow_soapp ->
+ RMeta (loc, n)
+ | CMeta (loc, _) ->
+ raise (InternalisationError (loc,NegativeMetavariable))
+ | CSort (loc, s) ->
+ RSort(loc,s)
+ | CCast (loc, c1, c2) ->
+ RCast (loc,intern env c1,intern env c2)
+
+ | CGrammar (loc,c,subst) ->
+ subst_rawconstr loc intern (subst,env) c
+
+ | CDynamic (loc,d) -> RDynamic (loc,d)
+
+ and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) =
+ let (idsl_substl_list,pl) =
+ List.split (List.map (intern_cases_pattern scopes ([],[])) lhs) in
+ let idsl, substl = List.split (List.flatten idsl_substl_list) in
+ let eqn_ids = List.flatten idsl in
+ let subst = List.flatten substl in
+ (* Linearity implies the order in ids is irrelevant *)
+ check_linearity lhs eqn_ids;
+ check_uppercase loc eqn_ids;
+ check_number_of_pattern loc n pl;
+ 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)
+
+ 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
+
+ and iterate_lam 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_lam loc2 (ids',impls,scopes) ty body nal in
+ let ty = locate_if_isevar loc1 na (intern env ty) in
+ RLambda (join_loc loc1 loc2, na, ty, body)
+ | [] -> intern env body
+
+ and intern_impargs c env l subscopes args =
+ let rec aux n l subscopes args =
+ let (enva,subscopes') = apply_scope_env env subscopes in
+ match (l,args) with
+ | (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')
+ else
+ (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
+ else
+ let e = if is_status_implicit imp then Some n else None in
+ raise
+ (InternalisationError(constr_loc a,BadExplicitationNumber (j,e)))
+ | (imp::l',(a,None)::args') ->
+ 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')
+ | ([],args) -> intern_tailargs env subscopes args
+ | (_::l',[]) ->
+ if List.for_all is_status_implicit l then
+ (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes args)
+ else []
+ in
+ aux 1 l subscopes args
+
+ and intern_tailargs env subscopes = function
+ | (a,Some _)::args' ->
+ 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)
+ | [] -> []
+
+ 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)
+
+ in
+ try
+ intern env c
+ with
+ InternalisationError (loc,e) ->
+ user_err_loc (loc,"internalize",explain_internalisation_error e)
+
+(**************************************************************************)
+(* Functions to translate constr_expr into rawconstr *)
+(**************************************************************************)
+
+let extract_ids env =
+ List.fold_right Idset.add
+ (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 sigma env c =
+ interp_rawconstr_gen sigma env [] false [] c
+
+let interp_rawconstr_with_implicits sigma env impls c =
+ interp_rawconstr_gen 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 *)
+
+let interp_constr sigma env c =
+ understand sigma env (interp_rawconstr sigma env c)
+
+let interp_openconstr sigma env c =
+ understand_gen_tcc sigma env [] [] None (interp_rawconstr sigma env c)
+
+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)
+
+let interp_type_with_implicits sigma env impls c =
+ understand_type sigma env (interp_rawconstr_with_implicits sigma env impls c)
+
+let judgment_of_rawconstr sigma env c =
+ understand_judgment sigma env (interp_rawconstr sigma env c)
+
+let type_judgment_of_rawconstr sigma env c =
+ understand_type_judgment sigma env (interp_rawconstr sigma env c)
+
+(* To retype a list of key*constr with undefined key *)
+let retype_list sigma env lst =
+ List.fold_right (fun (x,csr) a ->
+ try (x,Retyping.get_judgment_of env sigma csr)::a with
+ | Anomaly _ -> a) lst []
+
+(* List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
+
+(* Interprets a constr according to two lists *)
+(* 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
+ 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
+ and rtype lst = retype_list sigma env lst in
+ understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;;
+
+let interp_casted_constr sigma env c typ =
+ understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c)
+
+(* To process patterns, we need a translation without typing at all. *)
+
+let rec pat_of_raw metas vars lvar = function
+ | RVar (_,id) ->
+ (try PRel (list_index (Name id) vars)
+ with Not_found ->
+ try List.assoc id lvar
+ with Not_found -> PVar id)
+ | RMeta (_,n) ->
+ metas := n::!metas; PMeta (Some n)
+ | RRef (_,r) ->
+ PRef r
+ (* Hack pour ne pas réécrire une interprétation complète des patterns*)
+ | RApp (_, RMeta (_,n), cl) when n<0 ->
+ PSoApp (- n, List.map (pat_of_raw metas vars lvar) cl)
+ | RApp (_,c,cl) ->
+ PApp (pat_of_raw metas vars lvar c,
+ Array.of_list (List.map (pat_of_raw metas vars lvar) cl))
+ | RLambda (_,na,c1,c2) ->
+ PLambda (na, pat_of_raw metas vars lvar c1,
+ pat_of_raw metas (na::vars) lvar c2)
+ | RProd (_,na,c1,c2) ->
+ PProd (na, pat_of_raw metas vars lvar c1,
+ pat_of_raw metas (na::vars) lvar c2)
+ | RLetIn (_,na,c1,c2) ->
+ PLetIn (na, pat_of_raw metas vars lvar c1,
+ pat_of_raw metas (na::vars) lvar c2)
+ | RSort (_,s) ->
+ PSort s
+ | RHole _ ->
+ PMeta None
+ | RCast (_,c,t) ->
+ if_verbose warning "Cast not taken into account in constr pattern";
+ pat_of_raw metas vars lvar c
+ | ROrderedCase (_,st,po,c,br) ->
+ PCase (st,option_app (pat_of_raw metas vars lvar) po,
+ pat_of_raw metas vars lvar c,
+ Array.map (pat_of_raw metas vars lvar) br)
+ | r ->
+ let loc = loc_of_rawconstr r in
+ user_err_loc (loc,"pattern_of_rawconstr", str "Not supported pattern")
+
+let pattern_of_rawconstr lvar c =
+ let metas = ref [] in
+ let p = pat_of_raw metas [] lvar c in
+ (!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 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)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
new file mode 100644
index 000000000..ce8c6f5ee
--- /dev/null
+++ b/interp/constrintern.mli
@@ -0,0 +1,87 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Evd
+open Environ
+open Libnames
+open Rawterm
+open Pattern
+open Coqast
+open Topconstr
+(*i*)
+
+(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
+
+ The translation performs:
+
+ - resolution of names :
+ - check all variables are bound
+ - make absolute the references to global objets
+ - resolution of symbolic notations using scopes
+ - insert existential variables for implicit arguments
+*)
+
+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 ->
+ bool -> identifier list -> constr_expr -> rawconstr
+
+(*s Composing the translation with typing *)
+val interp_constr : evar_map -> env -> constr_expr -> constr
+val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
+val interp_type : evar_map -> env -> constr_expr -> types
+val interp_openconstr : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_casted_openconstr :
+ evar_map -> env -> constr_expr -> constr -> evar_map * constr
+
+(* [interp_type_with_implicits] extends [interp_type] by allowing
+ implicits arguments in the ``rel'' part of [env]; the extra
+ argument associates a list of implicit positions to identifiers
+ declared in the rel_context of [env] *)
+val interp_type_with_implicits :
+ evar_map -> env -> implicits_env -> constr_expr -> types
+
+(*s Build a judgement from *)
+val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
+val type_judgment_of_rawconstr :
+ evar_map -> env -> constr_expr -> unsafe_type_judgment
+
+(* Interprets a constr according to two lists of instantiations (variables and
+ metas), possibly casting it*)
+val interp_constr_gen :
+ evar_map -> env -> (identifier * constr) list ->
+ (int * constr) list -> constr_expr -> constr option -> constr
+
+(* Interprets a constr according to two lists of instantiations (variables and
+ metas), possibly casting it, and turning unresolved evar into metas*)
+val interp_openconstr_gen :
+ evar_map -> env -> (identifier * constr) list ->
+ (int * constr) list -> constr_expr -> constr option -> evar_map * constr
+
+(* Interprets constr patterns according to a list of instantiations
+ (variables)*)
+val interp_constrpattern_gen :
+ evar_map -> env -> (identifier * constr) list -> constr_expr ->
+ int list * constr_pattern
+
+val interp_constrpattern :
+ evar_map -> env -> constr_expr -> int list * constr_pattern
+
+(* Interprets into a abbreviatable constr *)
+val interp_aconstr : constr_expr -> aconstr
+
+(* Globalization leak for Grammar *)
+val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
new file mode 100644
index 000000000..d06f6ac52
--- /dev/null
+++ b/interp/coqlib.ml
@@ -0,0 +1,285 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Libnames
+open Declare
+open Pattern
+open Nametab
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let coq_id = id_of_string "Coq"
+let init_id = id_of_string "Init"
+let arith_id = id_of_string "Arith"
+let datatypes_id = id_of_string "Datatypes"
+
+let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
+let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
+let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let nat_path = make_path datatypes_module (id_of_string "nat")
+
+let glob_nat = IndRef (nat_path,0)
+
+let path_of_O = ((nat_path,0),1)
+let path_of_S = ((nat_path,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+let eq_path = make_path logic_module (id_of_string "eq")
+let eqT_path = make_path logic_type_module (id_of_string "eqT")
+
+let glob_eq = IndRef (eq_path,0)
+let glob_eqT = IndRef (eqT_path,0)
+
+let reference dir s =
+ let dir = make_dir ("Coq"::"Init"::[dir]) in
+ let id = id_of_string s in
+ try
+ Nametab.absolute_reference (Libnames.make_path dir id)
+ with Not_found ->
+ anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id)))
+
+let constant dir s = constr_of_reference (reference dir s)
+
+type coq_sigma_data = {
+ proj1 : constr;
+ proj2 : constr;
+ elim : constr;
+ intro : constr;
+ typ : constr }
+
+type 'a delayed = unit -> 'a
+
+let build_sigma_set () =
+ { proj1 = constant "Specif" "projS1";
+ proj2 = constant "Specif" "projS2";
+ elim = constant "Specif" "sigS_rec";
+ intro = constant "Specif" "existS";
+ typ = constant "Specif" "sigS" }
+
+let build_sigma_type () =
+ { proj1 = constant "Specif" "projT1";
+ proj2 = constant "Specif" "projT2";
+ elim = constant "Specif" "sigT_rec";
+ intro = constant "Specif" "existT";
+ typ = constant "Specif" "sigT" }
+
+(* Equalities *)
+type coq_leibniz_eq_data = {
+ eq : constr delayed;
+ ind : constr delayed;
+ rrec : constr delayed option;
+ rect : constr delayed option;
+ congr: constr delayed;
+ sym : constr delayed }
+
+let constant dir id = lazy (constant dir id)
+
+(* Equality on Set *)
+let coq_eq_eq = constant "Logic" "eq"
+let coq_eq_ind = constant "Logic" "eq_ind"
+let coq_eq_rec = constant "Logic" "eq_rec"
+let coq_eq_rect = constant "Logic" "eq_rect"
+let coq_eq_congr = constant "Logic" "f_equal"
+let coq_eq_sym = constant "Logic" "sym_eq"
+let coq_f_equal2 = constant "Logic" "f_equal2"
+
+let build_coq_eq_data = {
+ eq = (fun () -> Lazy.force coq_eq_eq);
+ ind = (fun () -> Lazy.force coq_eq_ind);
+ rrec = Some (fun () -> Lazy.force coq_eq_rec);
+ rect = Some (fun () -> Lazy.force coq_eq_rect);
+ congr = (fun () -> Lazy.force coq_eq_congr);
+ sym = (fun () -> Lazy.force coq_eq_sym) }
+
+let build_coq_eq = build_coq_eq_data.eq
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+(* Specif *)
+let coq_sumbool = constant "Specif" "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type *)
+let coq_eqT_eq = constant "Logic_Type" "eqT"
+let coq_eqT_ind = constant "Logic_Type" "eqT_ind"
+let coq_eqT_congr =constant "Logic_Type" "congr_eqT"
+let coq_eqT_sym = constant "Logic_Type" "sym_eqT"
+
+let build_coq_eqT_data = {
+ eq = (fun () -> Lazy.force coq_eqT_eq);
+ ind = (fun () -> Lazy.force coq_eqT_ind);
+ rrec = None;
+ rect = None;
+ congr = (fun () -> Lazy.force coq_eqT_congr);
+ sym = (fun () -> Lazy.force coq_eqT_sym) }
+
+let build_coq_eqT = build_coq_eqT_data.eq
+let build_coq_sym_eqT = build_coq_eqT_data.sym
+
+(* Equality on Type as a Type *)
+let coq_idT_eq = constant "Logic_Type" "identityT"
+let coq_idT_ind = constant "Logic_Type" "identityT_ind"
+let coq_idT_rec = constant "Logic_Type" "identityT_rec"
+let coq_idT_rect = constant "Logic_Type" "identityT_rect"
+let coq_idT_congr = constant "Logic_Type" "congr_idT"
+let coq_idT_sym = constant "Logic_Type" "sym_idT"
+
+let build_coq_idT_data = {
+ eq = (fun () -> Lazy.force coq_idT_eq);
+ ind = (fun () -> Lazy.force coq_idT_ind);
+ rrec = Some (fun () -> Lazy.force coq_idT_rec);
+ rect = Some (fun () -> Lazy.force coq_idT_rect);
+ congr = (fun () -> Lazy.force coq_idT_congr);
+ sym = (fun () -> Lazy.force coq_idT_sym) }
+
+(* Empty Type *)
+let coq_EmptyT = constant "Logic_Type" "EmptyT"
+
+(* Unit Type and its unique inhabitant *)
+let coq_UnitT = constant "Logic_Type" "UnitT"
+let coq_IT = constant "Logic_Type" "IT"
+
+(* The False proposition *)
+let coq_False = constant "Logic" "False"
+
+(* The True proposition and its unique proof *)
+let coq_True = constant "Logic" "True"
+let coq_I = constant "Logic" "I"
+
+(* Connectives *)
+let coq_not = constant "Logic" "not"
+let coq_and = constant "Logic" "and"
+let coq_or = constant "Logic" "or"
+let coq_ex = constant "Logic" "ex"
+
+(* Runtime part *)
+let build_coq_EmptyT () = Lazy.force coq_EmptyT
+let build_coq_UnitT () = Lazy.force coq_UnitT
+let build_coq_IT () = Lazy.force coq_IT
+
+let build_coq_True () = Lazy.force coq_True
+let build_coq_I () = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not () = Lazy.force coq_not
+let build_coq_and () = Lazy.force coq_and
+let build_coq_or () = Lazy.force coq_or
+let build_coq_ex () = Lazy.force coq_ex
+
+(****************************************************************************)
+(* Patterns *)
+(* This needs to have interp_constrpattern available ...
+let parse_astconstr s =
+ try
+ Pcoq.parse_string Pcoq.Constr.constr_eoi s
+ with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+ error "Syntax error : not a construction"
+
+let parse_pattern s =
+ Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
+
+let coq_eq_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
+let coq_eqT_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Logic_Type.eqT ?1 ?2 ?3)"))
+let coq_idT_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
+let coq_existS_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
+let coq_existT_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Specif.existT ?1 ?2 ?3 ?4)"))
+let coq_not_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)"))
+let coq_imp_False_pattern =
+ lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_imp_False_pattern =
+ lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_eqdec_partial_pattern
+ lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
+let coq_eqdec_pattern
+ lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
+*)
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref = lazy (reference "Logic" "eq")
+let coq_eqT_ref = lazy (reference "Logic_Type" "eqT")
+let coq_idT_ref = lazy (reference "Logic_Type" "identityT")
+let coq_existS_ref = lazy (reference "Specif" "existS")
+let coq_existT_ref = lazy (reference "Specif" "existT")
+let coq_not_ref = lazy (reference "Logic" "not")
+let coq_False_ref = lazy (reference "Logic" "False")
+let coq_sumbool_ref = lazy (reference "Specif" "sumbool")
+let coq_sig_ref = lazy (reference "Specif" "sig")
+
+(* Pattern "(sig ?1 ?2)" *)
+let coq_sig_pattern =
+ lazy (PApp (PRef (Lazy.force coq_sig_ref),
+ [| PMeta (Some 1); PMeta (Some 2) |]))
+
+(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *)
+let coq_eq_pattern_gen eq =
+ lazy (PApp(PRef (Lazy.force eq), Array.init 3 (fun i -> PMeta (Some (i+1)))))
+let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
+let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref
+let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref
+
+(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
+let coq_ex_pattern_gen ex =
+ lazy (PApp(PRef (Lazy.force ex), Array.init 4 (fun i -> PMeta (Some (i+1)))))
+let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
+let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
+
+(* Patterns "~ ?" and "? -> False" *)
+let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|]))
+let imp a b = PProd (Anonymous, a, b)
+let coq_imp_False_pattern =
+ lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref)))
+
+(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *)
+let coq_eqdec_partial_pattern =
+ lazy
+ (PApp
+ (PRef (Lazy.force coq_sumbool_ref),
+ [| Lazy.force coq_eq_pattern; PMeta (Some 4) |]))
+
+(* The expected form of the goal for the tactic Decide Equality *)
+
+(* Pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" *)
+(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
+let x = Name (id_of_string "x")
+let y = Name (id_of_string "y")
+let coq_eqdec_pattern =
+ lazy
+ (PProd (x, PMeta (Some 1), PProd (y, PMeta (Some 1),
+ PApp (PRef (Lazy.force coq_sumbool_ref),
+ [| PApp (PRef (Lazy.force coq_eq_ref),
+ [| PMeta (Some 1); PRel 2; PRel 1 |]);
+ PApp (PRef (Lazy.force coq_not_ref),
+ [|PApp (PRef (Lazy.force coq_eq_ref),
+ [| PMeta (Some 1); PRel 2; PRel 1 |])|]) |]))))
+
+let build_coq_eq_pattern () = Lazy.force coq_eq_pattern
+let build_coq_eqT_pattern () = Lazy.force coq_eqT_pattern
+let build_coq_idT_pattern () = Lazy.force coq_idT_pattern
+let build_coq_existS_pattern () = Lazy.force coq_existS_pattern
+let build_coq_existT_pattern () = Lazy.force coq_existT_pattern
+let build_coq_not_pattern () = Lazy.force coq_not_pattern
+let build_coq_imp_False_pattern () = Lazy.force coq_imp_False_pattern
+let build_coq_eqdec_partial_pattern () = Lazy.force coq_eqdec_partial_pattern
+let build_coq_eqdec_pattern () = Lazy.force coq_eqdec_pattern
+let build_coq_sig_pattern () = Lazy.force coq_sig_pattern
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
new file mode 100644
index 000000000..dbe99e399
--- /dev/null
+++ b/interp/coqlib.mli
@@ -0,0 +1,133 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Libnames
+open Nametab
+open Term
+open Pattern
+(*i*)
+
+(*s This module collects the global references, constructions and
+ patterns of the standard library used in ocaml files *)
+
+(*s Global references *)
+
+(* Modules *)
+val logic_module : dir_path
+val logic_type_module : dir_path
+
+(* Natural numbers *)
+val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
+val glob_O : global_reference
+val glob_S : global_reference
+
+(* Equality *)
+val glob_eq : global_reference
+val glob_eqT : global_reference
+
+(*s Constructions and patterns related to Coq initial state are unknown
+ at compile time. Therefore, we can only provide methods to build
+ them at runtime. This is the purpose of the [constr delayed] and
+ [constr_pattern delayed] types. Objects of this time needs to be
+ applied to [()] to get the actual constr or pattern at runtime *)
+
+type 'a delayed = unit -> 'a
+
+(*s For Equality tactics *)
+type coq_sigma_data = {
+ proj1 : constr;
+ proj2 : constr;
+ elim : constr;
+ intro : constr;
+ typ : constr }
+
+val build_sigma_set : unit -> coq_sigma_data
+val build_sigma_type : unit -> coq_sigma_data
+
+type coq_leibniz_eq_data = {
+ eq : constr delayed;
+ ind : constr delayed;
+ rrec : constr delayed option;
+ rect : constr delayed option;
+ congr: constr delayed;
+ sym : constr delayed }
+
+val build_coq_eq_data : coq_leibniz_eq_data
+val build_coq_eqT_data : coq_leibniz_eq_data
+val build_coq_idT_data : coq_leibniz_eq_data
+
+val build_coq_f_equal2 : constr delayed
+val build_coq_eqT : constr delayed
+val build_coq_sym_eqT : constr delayed
+
+(* Empty Type *)
+val build_coq_EmptyT : constr delayed
+
+(* Unit Type and its unique inhabitant *)
+val build_coq_UnitT : constr delayed
+val build_coq_IT : constr delayed
+
+(* Specif *)
+val build_coq_sumbool : constr delayed
+
+(*s Connectives *)
+(* The False proposition *)
+val build_coq_False : constr delayed
+
+(* The True proposition and its unique proof *)
+val build_coq_True : constr delayed
+val build_coq_I : constr delayed
+
+(* Negation *)
+val build_coq_not : constr delayed
+
+(* Conjunction *)
+val build_coq_and : constr delayed
+
+(* Disjunction *)
+val build_coq_or : constr delayed
+
+(* Existential quantifier *)
+val build_coq_ex : constr delayed
+
+(**************************** Patterns ************************************)
+(* ["(eq ?1 ?2 ?3)"] *)
+val build_coq_eq_pattern : constr_pattern delayed
+
+(* ["(eqT ?1 ?2 ?3)"] *)
+val build_coq_eqT_pattern : constr_pattern delayed
+
+(* ["(identityT ?1 ?2 ?3)"] *)
+val build_coq_idT_pattern : constr_pattern delayed
+
+(* ["(existS ?1 ?2 ?3 ?4)"] *)
+val build_coq_existS_pattern : constr_pattern delayed
+
+(* ["(existT ?1 ?2 ?3 ?4)"] *)
+val build_coq_existT_pattern : constr_pattern delayed
+
+(* ["(not ?)"] *)
+val build_coq_not_pattern : constr_pattern delayed
+
+(* ["? -> False"] *)
+val build_coq_imp_False_pattern : constr_pattern delayed
+
+(* ["(sumbool (eq ?1 ?2 ?3) ?4)"] *)
+val build_coq_eqdec_partial_pattern : constr_pattern delayed
+
+(* ["! (x,y:?1). (sumbool (eq ?1 x y) ~(eq ?1 x y))"] *)
+val build_coq_eqdec_pattern : constr_pattern delayed
+
+(* ["(sig ?1 ?2)"] *)
+val build_coq_sig_pattern : constr_pattern delayed
diff --git a/interp/genarg.ml b/interp/genarg.ml
new file mode 100644
index 000000000..b25908b42
--- /dev/null
+++ b/interp/genarg.ml
@@ -0,0 +1,185 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Nametab
+open Rawterm
+open Topconstr
+
+type argument_type =
+ (* Basic types *)
+ | BoolArgType
+ | IntArgType
+ | IntOrVarArgType
+ | StringArgType
+ | PreIdentArgType
+ | IdentArgType
+ | RefArgType
+ (* Specific types *)
+ | SortArgType
+ | ConstrArgType
+ | ConstrMayEvalArgType
+ | QuantHypArgType
+ | TacticArgType
+ | CastedOpenConstrArgType
+ | ConstrWithBindingsArgType
+ | RedExprArgType
+ | List0ArgType of argument_type
+ | List1ArgType of argument_type
+ | OptArgType of argument_type
+ | PairArgType of argument_type * argument_type
+ | ExtraArgType of string
+
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+(* Dynamics but tagged by a type expression *)
+
+type ('a,'b) generic_argument = argument_type * Obj.t
+
+let dyntab = ref ([] : string list)
+
+type ('a,'b,'c) abstract_argument_type = argument_type
+
+let create_arg s =
+ if List.mem s !dyntab then
+ anomaly ("Genarg.create: already declared generic argument " ^ s);
+ dyntab := s :: !dyntab;
+ let t = ExtraArgType s in
+ (t,t)
+
+let exists_argtype s = List.mem s !dyntab
+
+type open_constr = Evd.evar_map * Term.constr
+(*type open_rawconstr = Coqast.t*)
+type open_rawconstr = constr_expr
+
+let rawwit_bool = BoolArgType
+let wit_bool = BoolArgType
+
+let rawwit_int = IntArgType
+let wit_int = IntArgType
+
+let rawwit_int_or_var = IntOrVarArgType
+let wit_int_or_var = IntOrVarArgType
+
+let rawwit_string = StringArgType
+let wit_string = StringArgType
+
+let rawwit_ident = IdentArgType
+let wit_ident = IdentArgType
+
+let rawwit_pre_ident = PreIdentArgType
+let wit_pre_ident = PreIdentArgType
+
+let rawwit_ref = RefArgType
+let wit_ref = RefArgType
+
+let rawwit_quant_hyp = QuantHypArgType
+let wit_quant_hyp = QuantHypArgType
+
+let rawwit_sort = SortArgType
+let wit_sort = SortArgType
+
+let rawwit_constr = ConstrArgType
+let wit_constr = ConstrArgType
+
+let rawwit_constr_may_eval = ConstrMayEvalArgType
+let wit_constr_may_eval = ConstrMayEvalArgType
+
+let rawwit_tactic = TacticArgType
+let wit_tactic = TacticArgType
+
+let rawwit_casted_open_constr = CastedOpenConstrArgType
+let wit_casted_open_constr = CastedOpenConstrArgType
+
+let rawwit_constr_with_bindings = ConstrWithBindingsArgType
+let wit_constr_with_bindings = ConstrWithBindingsArgType
+
+let rawwit_red_expr = RedExprArgType
+let wit_red_expr = RedExprArgType
+
+let wit_list0 t = List0ArgType t
+
+let wit_list1 t = List1ArgType t
+
+let wit_opt t = OptArgType t
+
+let wit_pair t1 t2 = PairArgType (t1,t2)
+
+let in_gen t o = (t,Obj.repr o)
+let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
+let genarg_tag (s,_) = s
+
+let fold_list0 f = function
+ | (List0ArgType t as u, l) ->
+ List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
+ | _ -> failwith "Genarg: not a list0"
+
+let fold_list1 f = function
+ | (List1ArgType t as u, l) ->
+ List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
+ | _ -> failwith "Genarg: not a list1"
+
+let fold_opt f a = function
+ | (OptArgType t as u, l) ->
+ (match Obj.magic l with
+ | None -> a
+ | Some x -> f (in_gen t x))
+ | _ -> failwith "Genarg: not a opt"
+
+let fold_pair f = function
+ | (PairArgType (t1,t2) as u, l) ->
+ let (x1,x2) = Obj.magic l in
+ f (in_gen t1 x1) (in_gen t2 x2)
+ | _ -> failwith "Genarg: not a pair"
+
+let app_list0 f = function
+ | (List0ArgType t as u, l) ->
+ let o = Obj.magic l in
+ (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
+ | _ -> failwith "Genarg: not a list0"
+
+let app_list1 f = function
+ | (List1ArgType t as u, l) ->
+ let o = Obj.magic l in
+ (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
+ | _ -> failwith "Genarg: not a list1"
+
+let app_opt f = function
+ | (OptArgType t as u, l) ->
+ let o = Obj.magic l in
+ (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o))
+ | _ -> failwith "Genarg: not an opt"
+
+let app_pair f1 f2 = function
+ | (PairArgType (t1,t2) as u, l) ->
+ let (o1,o2) = Obj.magic l in
+ let o1 = out_gen t1 (f1 (in_gen t1 o1)) in
+ let o2 = out_gen t2 (f2 (in_gen t2 o2)) in
+ (u, Obj.repr (o1,o2))
+ | _ -> failwith "Genarg: not a pair"
+
+let or_var_app f = function
+ | ArgArg x -> ArgArg (f x)
+ | ArgVar _ as x -> x
+
+let smash_var_app t f g = function
+ | ArgArg x -> f x
+ | ArgVar (_,id) ->
+ let (u, _ as x) = g id in
+ if t <> u then failwith "Genarg: a variable bound to a wrong type";
+ x
+
+let unquote x = x
+
+type an_arg_of_this_type = Obj.t
+
+let in_generic t x = (t, Obj.repr x)
diff --git a/interp/genarg.mli b/interp/genarg.mli
new file mode 100644
index 000000000..f1246b2cc
--- /dev/null
+++ b/interp/genarg.mli
@@ -0,0 +1,213 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Libnames
+open Rawterm
+open Topconstr
+
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type open_constr = Evd.evar_map * Term.constr
+type open_rawconstr = constr_expr
+
+
+(* The route of a generic argument, from parsing to evaluation
+
+ parsing in_raw out_raw
+ char stream ----> rawtype ----> rawconstr generic_argument ---->
+ |
+ | interp
+ V
+ type <---- constr generic_argument <----
+ out in
+
+To distinguish between the uninterpreted (raw) and the interpreted
+worlds, we annotate the type generic_argument by a phantom argument
+which is either constr_expr or constr (actually we add also a second
+argument raw_tactic_expr and tactic, but this is only for technical
+reasons, because these types are undefined at the type of compilation
+of Genarg).
+
+Transformation for each type :
+tag f raw open type cooked closed type
+
+BoolArgType bool bool
+IntArgType int int
+IntOrVarArgType int or_var int
+StringArgType string (parsed w/ "") string
+IdentArgType identifier identifier
+PreIdentArgType string (parsed w/o "") string
+RefArgType reference global_reference
+ConstrArgType constr_expr constr
+ConstrMayEvalArgType constr_expr may_eval constr
+QuantHypArgType quantified_hypothesis quantified_hypothesis
+TacticArgType raw_tactic_expr tactic
+CastedOpenConstrArgType constr_expr open_constr
+ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings
+List0ArgType of argument_type
+List1ArgType of argument_type
+OptArgType of argument_type
+ExtraArgType of string '_a '_b
+*)
+
+type ('a,'co,'ta) abstract_argument_type
+
+val rawwit_bool : (bool,'co,'ta) abstract_argument_type
+val wit_bool : (bool,'co,'ta) abstract_argument_type
+
+val rawwit_int : (int,'co,'ta) abstract_argument_type
+val wit_int : (int,'co,'ta) abstract_argument_type
+
+val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+
+val rawwit_string : (string,'co,'ta) abstract_argument_type
+val wit_string : (string,'co,'ta) abstract_argument_type
+
+val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
+val wit_ident : (identifier,'co,'ta) abstract_argument_type
+
+val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
+val wit_pre_ident : (string,'co,'ta) abstract_argument_type
+
+val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
+val wit_ref : (global_reference,constr,'ta) abstract_argument_type
+
+val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+
+val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type
+val wit_sort : (sorts,constr,'ta) abstract_argument_type
+
+val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
+val wit_constr : (constr,constr,'ta) abstract_argument_type
+
+val rawwit_constr_may_eval : (constr_expr may_eval,constr_expr,'ta) abstract_argument_type
+val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
+
+val rawwit_casted_open_constr : (open_rawconstr,constr_expr,'ta) abstract_argument_type
+val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
+
+val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
+
+val rawwit_red_expr : ((constr_expr,reference or_metanum) red_expr_gen,constr_expr,'ta) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
+
+(* TODO: transformer tactic en extra arg *)
+val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type
+val wit_tactic : ('ta,constr,'ta) abstract_argument_type
+
+val wit_list0 :
+ ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+
+val wit_list1 :
+ ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+
+val wit_opt :
+ ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type
+
+val wit_pair :
+ ('a,'co,'ta) abstract_argument_type ->
+ ('b,'co,'ta) abstract_argument_type ->
+ ('a * 'b,'co,'ta) abstract_argument_type
+
+(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *)
+type ('a,'b) generic_argument
+
+val fold_list0 :
+ (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+
+val fold_list1 :
+ (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+
+val fold_opt :
+ (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c
+
+val fold_pair :
+ (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) ->
+ ('a,'b) generic_argument -> 'c
+
+(* [app_list0] fails if applied to an argument not of tag [List0 t]
+ for some [t]; it's the responsability of the caller to ensure it *)
+
+val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_pair :
+ (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
+ (('a,'b) generic_argument -> ('c,'d) generic_argument)
+ -> ('a,'b) generic_argument -> ('c,'d) generic_argument
+
+(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
+ polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
+ de create *)
+val create_arg : string ->
+ ('rawa,'rawco,'rawta) abstract_argument_type
+ * ('a,'co,'ta) abstract_argument_type
+
+val exists_argtype : string -> bool
+
+type argument_type =
+ (* Basic types *)
+ | BoolArgType
+ | IntArgType
+ | IntOrVarArgType
+ | StringArgType
+ | PreIdentArgType
+ | IdentArgType
+ | RefArgType
+ (* Specific types *)
+ | SortArgType
+ | ConstrArgType
+ | ConstrMayEvalArgType
+ | QuantHypArgType
+ | TacticArgType
+ | CastedOpenConstrArgType
+ | ConstrWithBindingsArgType
+ | RedExprArgType
+ | List0ArgType of argument_type
+ | List1ArgType of argument_type
+ | OptArgType of argument_type
+ | PairArgType of argument_type * argument_type
+ | ExtraArgType of string
+
+val genarg_tag : ('a,'b) generic_argument -> argument_type
+
+val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
+
+(* We'd like
+
+ [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]
+
+ with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
+
+ in_generic is not typable; we replace the second argument by an absurd
+ type (with no introduction rule)
+*)
+type an_arg_of_this_type
+
+val in_generic :
+ argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument
+
+val in_gen :
+ ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
+val out_gen :
+ ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
new file mode 100644
index 000000000..8a0c8e545
--- /dev/null
+++ b/interp/modintern.ml
@@ -0,0 +1,103 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Entries
+open Libnames
+open Topconstr
+open Constrintern
+
+let rec make_mp mp = function
+ [] -> mp
+ | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
+
+(*
+(* Since module components are not put in the nametab we try to locate
+the module prefix *)
+exception BadRef
+
+let lookup_qualid (modtype:bool) qid =
+ let rec make_mp mp = function
+ [] -> mp
+ | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
+ in
+ let rec find_module_prefix dir n =
+ if n<0 then raise Not_found;
+ let dir',dir'' = list_chop n dir in
+ let id',dir''' =
+ match dir'' with
+ | hd::tl -> hd,tl
+ | _ -> anomaly "This list should not be empty!"
+ in
+ let qid' = make_qualid dir' id' in
+ try
+ match Nametab.locate qid' with
+ | ModRef mp -> mp,dir'''
+ | _ -> raise BadRef
+ with
+ Not_found -> find_module_prefix dir (pred n)
+ in
+ try Nametab.locate qid
+ with Not_found ->
+ let (dir,id) = repr_qualid qid in
+ let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
+ let mp =
+ List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
+ in
+ if modtype then
+ ModTypeRef (make_ln mp (label_of_id id))
+ else
+ ModRef (MPdot (mp,label_of_id id))
+
+*)
+
+(* Search for the head of [qid] in [binders].
+ If found, returns the module_path/kernel_name created from the dirpath
+ and the basename. Searches Nametab otherwise.
+*)
+
+let lookup_module (loc,qid) =
+ try
+ Nametab.locate_module qid
+ with
+ | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
+
+let lookup_modtype (loc,qid) =
+ try
+ Nametab.locate_modtype qid
+ with
+ | Not_found ->
+ Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
+
+let transl_with_decl env = function
+ | CWith_Module (id,qid) ->
+ With_Module (id,lookup_module qid)
+ | CWith_Definition (id,c) ->
+ With_Definition (id,interp_constr Evd.empty env c)
+
+let rec interp_modtype env = function
+ | CMTEident qid ->
+ MTEident (lookup_modtype qid)
+ | CMTEwith (mty,decl) ->
+ let mty = interp_modtype env mty in
+ let decl = transl_with_decl env decl in
+ MTEwith(mty,decl)
+
+
+let rec interp_modexpr env = function
+ | CMEident qid ->
+ MEident (lookup_module qid)
+ | CMEapply (me1,me2) ->
+ let me1 = interp_modexpr env me1 in
+ let me2 = interp_modexpr env me2 in
+ MEapply(me1,me2)
+
diff --git a/interp/modintern.mli b/interp/modintern.mli
new file mode 100644
index 000000000..2f9935674
--- /dev/null
+++ b/interp/modintern.mli
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Declarations
+open Environ
+open Entries
+open Topconstr
+(*i*)
+
+(* Module expressions and module types are interpreted relatively to
+ eventual functor or funsig arguments. *)
+
+val interp_modtype : env -> module_type_ast -> module_type_entry
+
+val interp_modexpr : env -> module_ast -> module_expr
+
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
new file mode 100644
index 000000000..e2e60dc15
--- /dev/null
+++ b/interp/ppextend.ml
@@ -0,0 +1,57 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+(*i*)
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int
+
+type parenRelation = L | E | Any | Prec of precedence
+
+type tolerability = precedence * parenRelation
+
+type ppbox =
+ | PpHB of int
+ | PpHOVB of int
+ | PpHVB of int
+ | PpVB of int
+ | PpTB
+
+type ppcut =
+ | PpBrk of int * int
+ | PpTbrk of int * int
+ | PpTab
+ | PpFnl
+
+let ppcmd_of_box = function
+ | PpHB n -> h n
+ | PpHOVB n -> hov n
+ | PpHVB n -> hv n
+ | PpVB n -> v n
+ | PpTB -> t
+
+let ppcmd_of_cut = function
+ | PpTab -> tab ()
+ | PpFnl -> fnl ()
+ | PpBrk(n1,n2) -> brk(n1,n2)
+ | PpTbrk(n1,n2) -> tbrk(n1,n2)
+
+type unparsing =
+ | UnpMetaVar of identifier * tolerability
+ | UnpTerminal of string
+ | UnpBox of ppbox * unparsing list
+ | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
new file mode 100644
index 000000000..890422de8
--- /dev/null
+++ b/interp/ppextend.mli
@@ -0,0 +1,47 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Pp
+open Names
+(*i*)
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int
+
+type parenRelation = L | E | Any | Prec of precedence
+
+type tolerability = precedence * parenRelation
+
+type ppbox =
+ | PpHB of int
+ | PpHOVB of int
+ | PpHVB of int
+ | PpVB of int
+ | PpTB
+
+type ppcut =
+ | PpBrk of int * int
+ | PpTbrk of int * int
+ | PpTab
+ | PpFnl
+
+val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
+
+val ppcmd_of_cut : ppcut -> std_ppcmds
+
+type unparsing =
+ | UnpMetaVar of identifier * tolerability
+ | UnpTerminal of string
+ | UnpBox of ppbox * unparsing list
+ | UnpCut of ppcut
diff --git a/interp/symbols.ml b/interp/symbols.ml
new file mode 100644
index 000000000..c6eff9ab9
--- /dev/null
+++ b/interp/symbols.ml
@@ -0,0 +1,331 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Summary
+open Rawterm
+open Topconstr
+open Ppextend
+(*i*)
+
+(*s A scope is a set of notations; it includes
+
+ - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
+ negative numbers (e.g. -0, -2, -13, ...). These interpreters may
+ fail if a number has no interpretation in the scope (e.g. there is
+ no interpretation for negative numbers in [nat]); interpreters both for
+ terms and patterns can be set; these interpreters are in permanent table
+ [numeral_interpreter_tab]
+ - a set of ML printers for expressions denoting numbers parsable in
+ this scope (permanently declared in [Esyntax.primitive_printer_tab])
+ - a set of interpretations for infix (more generally distfix) notations
+ - an optional pair of delimiters which, when occurring in a syntactic
+ expression, set this scope to be the current scope
+*)
+
+(**********************************************************************)
+(* Scope of symbols *)
+
+type level = precedence * precedence list
+type delimiters = string * string
+type scope = {
+ notations: (aconstr * level) Stringmap.t;
+ delimiters: delimiters option
+}
+type scopes = scope_name list
+
+(* Scopes table: scope_name -> symbol_interpretation *)
+let scope_map = ref Stringmap.empty
+
+let empty_scope = {
+ notations = Stringmap.empty;
+ delimiters = None
+}
+
+let default_scope = "core_scope"
+
+let _ = Stringmap.add default_scope empty_scope !scope_map
+
+let scope_stack = ref [default_scope]
+
+let current_scopes () = !scope_stack
+
+(* TODO: push nat_scope, z_scope, ... in scopes summary *)
+
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects) *)
+
+type numeral_interpreter_name = string
+type numeral_interpreter =
+ (loc -> bigint -> rawconstr)
+ * (loc -> bigint -> name -> cases_pattern) option
+
+let numeral_interpreter_tab =
+ (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t)
+
+let declare_numeral_interpreter sc t =
+ Hashtbl.add numeral_interpreter_tab sc t
+
+let lookup_numeral_interpreter s =
+ try
+ Hashtbl.find numeral_interpreter_tab s
+ with Not_found ->
+ error ("No interpretation for numerals in scope "^s)
+
+(* For loading without opening *)
+let declare_scope scope =
+ try let _ = Stringmap.find scope !scope_map in ()
+ with Not_found ->
+(* Options.if_verbose message ("Creating scope "^scope);*)
+ scope_map := Stringmap.add scope empty_scope !scope_map
+
+let find_scope scope =
+ try Stringmap.find scope !scope_map
+ with Not_found -> error ("Scope "^scope^" is not declared")
+
+let check_scope sc = let _ = find_scope sc in ()
+
+let declare_delimiters scope dlm =
+ let sc = find_scope scope in
+ if sc.delimiters <> None && Options.is_verbose () then
+ warning ("Overwriting previous delimiters in "^scope);
+ let sc = { sc with delimiters = Some dlm } in
+ scope_map := Stringmap.add scope sc !scope_map
+
+(* The mapping between notations and production *)
+
+let declare_notation nt scope (c,prec as info) =
+ let sc = find_scope scope in
+ if Stringmap.mem nt sc.notations && Options.is_verbose () then
+ warning ("Notation "^nt^" is already used in scope "^scope);
+ let sc = { sc with notations = Stringmap.add nt info sc.notations } in
+ scope_map := Stringmap.add scope sc !scope_map
+
+let rec find_interpretation f = function
+ | scope::scopes ->
+ (try f (find_scope scope)
+ with Not_found -> find_interpretation f scopes)
+ | [] -> raise Not_found
+
+let rec interp_notation ntn scopes =
+ let f scope = fst (Stringmap.find ntn scope.notations) in
+ try find_interpretation f scopes
+ with Not_found -> anomaly ("Unknown interpretation for notation "^ntn)
+
+let find_notation_with_delimiters scope =
+ match (Stringmap.find scope !scope_map).delimiters with
+ | Some dlm -> Some (Some dlm)
+ | None -> None
+
+let rec find_notation_without_delimiters ntn_scope ntn = function
+ | scope::scopes ->
+ (* Is the expected printer attached to the most recently open scope? *)
+ if scope = ntn_scope then
+ Some None
+ else
+ (* If the most recently open scope has a printer for this pattern
+ but not the expected one then we need delimiters *)
+ if Stringmap.mem ntn (Stringmap.find scope !scope_map).notations then
+ find_notation_with_delimiters ntn_scope
+ else
+ find_notation_without_delimiters ntn_scope ntn scopes
+ | [] ->
+ find_notation_with_delimiters ntn_scope
+
+let find_notation ntn_scope ntn scopes =
+ match
+ find_notation_without_delimiters ntn_scope ntn scopes
+ with
+ | None -> None
+ | Some None -> Some (None,scopes)
+ | Some x -> Some (x,ntn_scope::scopes)
+
+let exists_notation_in_scope scope prec ntn r =
+ try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = (r,prec)
+ with Not_found -> false
+
+let exists_notation_prec prec nt sc =
+ try snd (Stringmap.find nt sc.notations) = prec with Not_found -> false
+
+let exists_notation prec nt =
+ Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc)
+ !scope_map false
+
+(* We have to print delimiters; look for the more recent defined one *)
+(* Do we need to print delimiters? To know it, we look for a numeral *)
+(* printer available in the current stack of scopes *)
+let find_numeral_with_delimiters scope =
+ match (Stringmap.find scope !scope_map).delimiters with
+ | Some dlm -> Some (Some dlm)
+ | None -> None
+
+let rec find_numeral_without_delimiters printer_scope = function
+ | scope :: scopes ->
+ (* Is the expected printer attached to the most recently open scope? *)
+ if scope = printer_scope then
+ Some None
+ else
+ (* If the most recently open scope has a printer for numerals
+ but not the expected one then we need delimiters *)
+ if not (Hashtbl.mem numeral_interpreter_tab scope) then
+ find_numeral_without_delimiters printer_scope scopes
+ else
+ find_numeral_with_delimiters printer_scope
+ | [] ->
+ (* Can we switch to [scope]? Yes if it has defined delimiters *)
+ find_numeral_with_delimiters printer_scope
+
+let find_numeral_printer printer_scope scopes =
+ match
+ find_numeral_without_delimiters printer_scope scopes
+ with
+ | None -> None
+ | Some None -> Some (None,scopes)
+ | Some x -> Some (x,printer_scope::scopes)
+
+(* This is the map associating the scope a numeral printer belongs to *)
+(*
+let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t)
+*)
+
+let rec interp_numeral loc n = function
+ | scope :: scopes ->
+ (try fst (lookup_numeral_interpreter scope) loc n
+ with Not_found -> interp_numeral loc 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 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)
+
+(* Exportation of scopes *)
+let cache_scope (_,sc) =
+ check_scope sc;
+ scope_stack := sc :: !scope_stack
+
+let subst_scope (_,subst,sc) = sc
+
+open Libobject
+
+let (inScope,outScope) =
+ declare_object {(default_object "SCOPE") with
+ cache_function = cache_scope;
+ open_function = (fun i o -> if i=1 then cache_scope o);
+ subst_function = subst_scope;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x) }
+
+let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
+
+
+(* Special scopes associated to arguments of a global reference *)
+
+open Libnames
+
+module RefOrdered =
+ struct
+ type t = global_reference
+ let compare = Pervasives.compare
+ end
+
+module Refmap = Map.Make(RefOrdered)
+
+let arguments_scope = ref Refmap.empty
+
+let cache_arguments_scope (_,(r,scl)) =
+ List.iter (option_iter check_scope) scl;
+ arguments_scope := Refmap.add r scl !arguments_scope
+
+let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
+
+let (inArgumentsScope,outArgumentsScope) =
+ declare_object {(default_object "ARGUMENTS-SCOPE") with
+ cache_function = cache_arguments_scope;
+ open_function = (fun i o -> if i=1 then cache_arguments_scope o);
+ subst_function = subst_arguments_scope;
+ classify_function = (fun (_,o) -> Substitute o);
+ export_function = (fun x -> Some x) }
+
+let declare_arguments_scope r scl =
+ Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+
+let find_arguments_scope r =
+ try Refmap.find r !arguments_scope
+ with Not_found -> []
+
+(* Printing *)
+
+let pr_delimiters = function
+ | None -> str "No delimiters"
+ | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r
+
+let pr_notation prraw ntn r =
+ str ntn ++ str " stands for " ++ prraw r
+
+let pr_named_scope prraw scope sc =
+ str "Scope " ++ str scope ++ fnl ()
+ ++ pr_delimiters sc.delimiters ++ fnl ()
+ ++ Stringmap.fold
+ (fun ntn (r,_) strm -> pr_notation prraw ntn r ++ fnl () ++ strm)
+ sc.notations (mt ())
+
+let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+
+let pr_scopes prraw =
+ Stringmap.fold
+ (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+ !scope_map (mt ())
+
+(* Synchronisation with reset *)
+
+let freeze () = (!scope_map, !scope_stack, !arguments_scope)
+
+let unfreeze (scm,scs,asc) =
+ scope_map := scm;
+ scope_stack := scs;
+ arguments_scope := asc
+
+let init () = ()
+(*
+ scope_map := Strinmap.empty;
+ scope_stack := Stringmap.empty
+*)
+
+let _ =
+ declare_summary "symbols"
+ { freeze_function = freeze;
+ unfreeze_function = unfreeze;
+ init_function = init;
+ survive_section = false }
+
+
+let printing_rules =
+ ref (Stringmap.empty : (unparsing list * precedence) Stringmap.t)
+
+let declare_printing_rule ntn unpl =
+ printing_rules := Stringmap.add ntn unpl !printing_rules
+
+let find_notation_printing_rule ntn =
+ try Stringmap.find ntn !printing_rules
+ with Not_found -> anomaly ("No printing rule found for "^ntn)
diff --git a/interp/symbols.mli b/interp/symbols.mli
new file mode 100644
index 000000000..3c082b2ce
--- /dev/null
+++ b/interp/symbols.mli
@@ -0,0 +1,77 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Rawterm
+open Topconstr
+open Ppextend
+(*i*)
+
+(*s A numeral interpreter is the pair of an interpreter for _integer_
+ numbers in terms and an optional interpreter in pattern, if
+ negative numbers are not supported, the interpreter must fail with
+ an appropriate error message *)
+
+type numeral_interpreter_name = string
+type numeral_interpreter =
+ (loc -> bigint -> rawconstr)
+ * (loc -> bigint -> name -> cases_pattern) option
+
+(* A scope is a set of interpreters for symbols + optional
+ interpreter and printers for integers + optional delimiters *)
+
+type level = precedence * precedence list
+type delimiters = string * string
+type scope
+type scopes = scope_name list
+
+val default_scope : scope_name
+val current_scopes : unit -> scopes
+val open_scope : scope_name -> unit
+val declare_scope : scope_name -> unit
+
+(* Declare delimiters for printing *)
+val declare_delimiters : scope_name -> delimiters -> unit
+
+(* Declare, interpret, and look for a printer for numeral *)
+val declare_numeral_interpreter :
+ numeral_interpreter_name -> numeral_interpreter -> unit
+val interp_numeral : loc -> bigint -> scopes -> rawconstr
+val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern
+val find_numeral_printer : string -> scopes ->
+ (delimiters option * scopes) option
+
+(* Declare, interpret, and look for a printer for symbolic notations *)
+val declare_notation : notation -> scope_name -> aconstr * level -> unit
+val interp_notation : notation -> scopes -> aconstr
+val find_notation : scope_name -> notation -> scopes ->
+ (delimiters option * scopes) option
+val exists_notation_in_scope :
+ scope_name -> level -> notation -> aconstr -> bool
+val exists_notation : level -> notation -> bool
+
+(* Declare and look for scopes associated to arguments of a global ref *)
+open Libnames
+val declare_arguments_scope: global_reference -> scope_name option list -> unit
+val find_arguments_scope : global_reference -> scope_name option list
+
+(* Printing scopes *)
+val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds
+
+
+val declare_printing_rule : notation -> unparsing list * precedence -> unit
+val find_notation_printing_rule : notation -> unparsing list * precedence
+
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
new file mode 100644
index 000000000..a49352da3
--- /dev/null
+++ b/interp/syntax_def.ml
@@ -0,0 +1,72 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Names
+open Libnames
+open Topconstr
+open Libobject
+open Lib
+open Nameops
+
+(* Syntactic definitions. *)
+
+let syntax_table = ref (KNmap.empty : aconstr KNmap.t)
+
+let _ = Summary.declare_summary
+ "SYNTAXCONSTANT"
+ { Summary.freeze_function = (fun () -> !syntax_table);
+ Summary.unfreeze_function = (fun ft -> syntax_table := ft);
+ Summary.init_function = (fun () -> syntax_table := KNmap.empty);
+ Summary.survive_section = false }
+
+let add_syntax_constant kn c =
+ syntax_table := KNmap.add kn c !syntax_table
+
+let cache_syntax_constant ((sp,kn),c) =
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_syntax_constant"
+ (pr_id (basename sp) ++ str " already exists");
+ add_syntax_constant kn c;
+ Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
+
+let load_syntax_constant i ((sp,kn),c) =
+ if Nametab.exists_cci sp then
+ errorlabstrm "cache_syntax_constant"
+ (pr_id (basename sp) ++ str " already exists");
+ add_syntax_constant kn c;
+ Nametab.push_syntactic_definition (Nametab.Until i) sp kn
+
+let open_syntax_constant i ((sp,kn),c) =
+ Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
+
+let subst_syntax_constant ((sp,kn),subst,c) =
+ subst_aconstr subst c
+
+let classify_syntax_constant (_,c) = Substitute c
+
+let (in_syntax_constant, out_syntax_constant) =
+ declare_object {(default_object "SYNTAXCONSTANT") with
+ cache_function = cache_syntax_constant;
+ load_function = load_syntax_constant;
+ open_function = open_syntax_constant;
+ subst_function = subst_syntax_constant;
+ classify_function = classify_syntax_constant;
+ export_function = (fun x -> Some x) }
+
+let declare_syntactic_definition id c =
+ let _ = add_leaf id (in_syntax_constant c) in ()
+
+let rec set_loc loc _ a =
+ map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a
+
+let search_syntactic_definition loc kn =
+ set_loc loc () (KNmap.find kn !syntax_table)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
new file mode 100644
index 000000000..f4600d8db
--- /dev/null
+++ b/interp/syntax_def.mli
@@ -0,0 +1,23 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Names
+open Topconstr
+open Rawterm
+(*i*)
+
+(* Syntactic definitions. *)
+
+val declare_syntactic_definition : identifier -> aconstr -> unit
+
+val search_syntactic_definition : loc -> kernel_name -> rawconstr
+
+
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
new file mode 100644
index 000000000..8569c414b
--- /dev/null
+++ b/interp/topconstr.ml
@@ -0,0 +1,300 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Nameops
+open Libnames
+open Rawterm
+open Term
+(*i*)
+
+
+(* This is the subtype of rawconstr allowed in syntactic extensions *)
+type aconstr =
+ | ARef of global_reference
+ | AVar of identifier
+ | AApp of aconstr * aconstr list
+ | ALambda of name * aconstr * aconstr
+ | AProd of name * aconstr * aconstr
+ | ALetIn of name * aconstr * aconstr
+ | AOldCase of case_style * aconstr option * aconstr * aconstr array
+ | ASort of rawsort
+ | AHole of hole_kind
+ | AMeta of int
+ | ACast of aconstr * aconstr
+
+let name_app f e = function
+ | Name id -> let (id, e) = f id e in (Name id, e)
+ | Anonymous -> Anonymous, e
+
+let map_aconstr_with_binders_loc loc g f e = function
+ | AVar (id) -> RVar (loc,id)
+ | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args)
+ | ALambda (na,ty,c) ->
+ let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
+ | AProd (na,ty,c) ->
+ let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
+ | ALetIn (na,b,c) ->
+ let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
+ | AOldCase (b,tyopt,tm,bv) ->
+ ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
+ | ACast (c,t) -> RCast (loc,f e c,f e t)
+ | ASort x -> RSort (loc,x)
+ | AHole x -> RHole (loc,x)
+ | AMeta n -> RMeta (loc,n)
+ | ARef x -> RRef (loc,x)
+
+let rec subst_aconstr subst raw =
+ match raw with
+ | ARef ref ->
+ let ref' = subst_global subst ref in
+ if ref' == ref then raw else
+ ARef ref'
+
+ | AVar _ -> raw
+
+ | AApp (r,rl) ->
+ let r' = subst_aconstr subst r
+ and rl' = list_smartmap (subst_aconstr subst) rl in
+ if r' == r && rl' == rl then raw else
+ AApp(r',rl')
+
+ | ALambda (n,r1,r2) ->
+ let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ALambda (n,r1',r2')
+
+ | AProd (n,r1,r2) ->
+ let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ AProd (n,r1',r2')
+
+ | ALetIn (n,r1,r2) ->
+ let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ALetIn (n,r1',r2')
+
+ | AOldCase (b,ro,r,ra) ->
+ let ro' = option_smartmap (subst_aconstr subst) ro
+ and r' = subst_aconstr subst r
+ and ra' = array_smartmap (subst_aconstr subst) ra in
+ if ro' == ro && r' == r && ra' == ra then raw else
+ AOldCase (b,ro',r',ra')
+
+ | AMeta _ | ASort _ -> raw
+
+ | AHole (ImplicitArg (ref,i)) ->
+ let ref' = subst_global subst ref in
+ if ref' == ref then raw else
+ AHole (ImplicitArg (ref',i))
+ | AHole ( (AbstractionType _ | QuestionMark | CasesType |
+ InternalHole | TomatchTypeParameter _)) -> raw
+
+ | ACast (r1,r2) ->
+ let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+ if r1' == r1 && r2' == r2 then raw else
+ ACast (r1',r2')
+
+let rec aux = function
+ | RVar (_,id) -> 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)
+ | ROrderedCase (_,b,tyopt,tm,bv) ->
+ AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+ | RCast (_,c,t) -> ACast (aux c,aux t)
+ | RSort (_,s) -> ASort s
+ | RHole (_,w) -> AHole w
+ | RRef (_,r) -> ARef r
+ | RMeta (_,n) -> AMeta n
+ | RDynamic _ | RRec _ | RCases _ | REvar _ ->
+ error "Fixpoints, cofixpoints, existential variables and pattern-matching not \
+allowed in abbreviatable expressions"
+
+let aconstr_of_rawconstr = aux
+
+(*s Concrete syntax for terms *)
+
+type scope_name = string
+
+type notation = string
+
+type explicitation = int
+
+type cases_pattern_expr =
+ | CPatAlias of loc * cases_pattern_expr * identifier
+ | CPatCstr of loc * reference * cases_pattern_expr list
+ | CPatAtom of loc * reference option
+ | CPatNumeral of loc * Bignat.bigint
+ | CPatDelimiters of loc * scope_name * cases_pattern_expr
+
+type constr_expr =
+ | CRef of reference
+ | CFix of loc * identifier located * fixpoint_expr list
+ | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CArrow of loc * constr_expr * constr_expr
+ | CProdN of loc * (name located list * constr_expr) list * constr_expr
+ | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+ | CLetIn of loc * name located * constr_expr * constr_expr
+ | CAppExpl of loc * reference * constr_expr list
+ | CApp of loc * constr_expr * (constr_expr * explicitation option) list
+ | CCases of loc * constr_expr option * constr_expr list *
+ (loc * cases_pattern_expr list * constr_expr) list
+ | COrderedCase of loc * case_style * constr_expr option * constr_expr
+ * constr_expr list
+ | CHole of loc
+ | CMeta of loc * int
+ | CSort of loc * rawsort
+ | CCast of loc * constr_expr * constr_expr
+ | CNotation of loc * notation * (identifier * constr_expr) list
+ | CGrammar of loc * aconstr * (identifier * constr_expr) list
+ | CNumeral of loc * Bignat.bigint
+ | CDelimiters of loc * scope_name * constr_expr
+ | CDynamic of loc * Dyn.t
+
+and fixpoint_binder = name located list * constr_expr
+
+and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr = identifier * constr_expr * constr_expr
+
+let constr_loc = function
+ | CRef (Ident (loc,_)) -> loc
+ | CRef (Qualid (loc,_)) -> loc
+ | CFix (loc,_,_) -> loc
+ | CCoFix (loc,_,_) -> loc
+ | CArrow (loc,_,_) -> loc
+ | CProdN (loc,_,_) -> loc
+ | CLambdaN (loc,_,_) -> loc
+ | CLetIn (loc,_,_,_) -> loc
+ | CAppExpl (loc,_,_) -> loc
+ | CApp (loc,_,_) -> loc
+ | CCases (loc,_,_,_) -> loc
+ | COrderedCase (loc,_,_,_,_) -> loc
+ | CHole loc -> loc
+ | CMeta (loc,_) -> loc
+ | CSort (loc,_) -> loc
+ | CCast (loc,_,_) -> loc
+ | CNotation (loc,_,_) -> loc
+ | CGrammar (loc,_,_) -> loc
+ | CNumeral (loc,_) -> loc
+ | CDelimiters (loc,_,_) -> loc
+ | CDynamic _ -> dummy_loc
+
+let cases_pattern_loc = function
+ | CPatAlias (loc,_,_) -> loc
+ | CPatCstr (loc,_,_) -> loc
+ | CPatAtom (loc,_) -> loc
+ | CPatNumeral (loc,_) -> loc
+ | CPatDelimiters (loc,_,_) -> loc
+
+let replace_vars_constr_expr l t =
+ if l = [] then t else failwith "replace_constr_expr: TODO"
+
+let occur_var_constr_ref id = function
+ | Ident (loc,id') -> id = id'
+ | Qualid _ -> false
+
+let rec occur_var_constr_expr id = function
+ | CRef r -> occur_var_constr_ref id r
+ | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+ | CAppExpl (loc,r,l) ->
+ occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l
+ | CApp (loc,f,l) ->
+ occur_var_constr_expr id f or
+ List.exists (fun (a,_) -> occur_var_constr_expr id a) l
+ | CProdN (_,l,b) -> occur_var_binders id b l
+ | CLambdaN (_,l,b) -> occur_var_binders id b l
+ | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
+ | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+ | CNotation (_,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x) l
+ | CGrammar (loc,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x)l
+ | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
+ | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false
+ | CCases (loc,_,_,_)
+ | COrderedCase (loc,_,_,_,_)
+ | CFix (loc,_,_)
+ | CCoFix (loc,_,_) ->
+ Pp.warning "Capture check in multiple binders not done"; false
+
+and occur_var_binders id b = function
+ | (idl,a)::l ->
+ occur_var_constr_expr id a or
+ (not (List.mem (Name id) (snd (List.split idl)))
+ & occur_var_binders id b l)
+ | [] -> occur_var_constr_expr id b
+
+let mkIdentC id = CRef (Ident (dummy_loc, id))
+let mkRefC r = CRef r
+let mkAppC (f,l) = CApp (dummy_loc, f, List.map (fun x -> (x,None)) l)
+let mkCastC (a,b) = CCast (dummy_loc,a,b)
+let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
+let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
+let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b)
+
+(* Used in correctness and interface *)
+
+let map_binders f g e bl =
+ (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+ let h (nal,t) (e,bl) =
+ (List.fold_right (fun (_,na) -> name_fold g na) nal e,(nal,f e t)::bl) in
+ List.fold_right h bl (e,[])
+
+let map_constr_expr_with_binders f g e = function
+ | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
+ | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
+ | CApp (loc,a,l) -> CApp (loc,f e a,List.map (fun (a,i) -> (f e a,i)) l)
+ | CProdN (loc,bl,b) ->
+ let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
+ | CLambdaN (loc,bl,b) ->
+ let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
+ | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
+ | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
+ | CNotation (loc,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,f e t)) l)
+ | CGrammar (loc,r,l) -> CGrammar (loc,r,List.map (fun (x,t) ->(x,f e t)) l)
+ | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
+ | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x
+ | CCases (loc,po,a,bl) ->
+ (* TODO: apply g on the binding variables in pat... *)
+ (* hard because no syntactic diff between a constructor and a var *)
+ let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+ CCases (loc,option_app (f e) po,List.map (f e) a,bl)
+ | COrderedCase (loc,s,po,a,bl) ->
+ COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
+ | CFix (loc,id,dl) ->
+ let k (id,bl,t,d) =
+ let (e,bl) = map_binders f g e bl in (id,bl,f e t,f e d) in
+ CFix (loc,id,List.map k dl)
+ | CCoFix (loc,id,dl) ->
+ CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
+
+(* For binders parsing *)
+
+type local_binder =
+ | LocalRawDef of name located * constr_expr
+ | LocalRawAssum of name located list * constr_expr
+
+(* Concrete syntax for modules and modules types *)
+
+type with_declaration_ast =
+ | CWith_Module of identifier * qualid located
+ | CWith_Definition of identifier * constr_expr
+
+type module_type_ast =
+ | CMTEident of qualid located
+ | CMTEwith of module_type_ast * with_declaration_ast
+
+type module_ast =
+ | CMEident of qualid located
+ | CMEapply of module_ast * module_ast
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
new file mode 100644
index 000000000..72845f896
--- /dev/null
+++ b/interp/topconstr.mli
@@ -0,0 +1,133 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Libnames
+open Rawterm
+open Term
+(*i*)
+
+(*s This is the subtype of rawconstr allowed in syntactic extensions *)
+(* No location since intended to be substituted at any place of a text *)
+(* Complex expressions such as fixpoints, cofixpoints and pattern-matching *)
+(* are excluded; non global expressions such as existential variables also *)
+
+type aconstr =
+ | ARef of global_reference
+ | AVar of identifier
+ | AApp of aconstr * aconstr list
+ | ALambda of name * aconstr * aconstr
+ | AProd of name * aconstr * aconstr
+ | ALetIn of name * aconstr * aconstr
+ | AOldCase of case_style * aconstr option * aconstr * aconstr array
+ | ASort of rawsort
+ | AHole of hole_kind
+ | AMeta of int
+ | ACast of aconstr * aconstr
+
+val map_aconstr_with_binders_loc : loc ->
+ (identifier -> 'a -> identifier * 'a) ->
+ ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
+
+val subst_aconstr : Names.substitution -> aconstr -> aconstr
+
+val aconstr_of_rawconstr : rawconstr -> aconstr
+
+(*s Concrete syntax for terms *)
+
+type scope_name = string
+
+type notation = string
+
+type explicitation = int
+
+type cases_pattern_expr =
+ | CPatAlias of loc * cases_pattern_expr * identifier
+ | CPatCstr of loc * reference * cases_pattern_expr list
+ | CPatAtom of loc * reference option
+ | CPatNumeral of loc * Bignat.bigint
+ | CPatDelimiters of loc * scope_name * cases_pattern_expr
+
+type constr_expr =
+ | CRef of reference
+ | CFix of loc * identifier located * fixpoint_expr list
+ | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CArrow of loc * constr_expr * constr_expr
+ | CProdN of loc * (name located list * constr_expr) list * constr_expr
+ | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+ | CLetIn of loc * name located * constr_expr * constr_expr
+ | CAppExpl of loc * reference * constr_expr list
+ | CApp of loc * constr_expr * (constr_expr * explicitation option) list
+ | CCases of loc * constr_expr option * constr_expr list *
+ (loc * cases_pattern_expr list * constr_expr) list
+ | COrderedCase of loc * case_style * constr_expr option * constr_expr
+ * constr_expr list
+ | CHole of loc
+ | CMeta of loc * int
+ | CSort of loc * rawsort
+ | CCast of loc * constr_expr * constr_expr
+ | CNotation of loc * notation * (identifier * constr_expr) list
+ | CGrammar of loc * aconstr * (identifier * constr_expr) list
+ | CNumeral of loc * Bignat.bigint
+ | CDelimiters of loc * scope_name * constr_expr
+ | CDynamic of loc * Dyn.t
+
+and fixpoint_binder = name located list * constr_expr
+
+and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr = identifier * constr_expr * constr_expr
+
+val constr_loc : constr_expr -> loc
+
+val cases_pattern_loc : cases_pattern_expr -> loc
+
+val replace_vars_constr_expr :
+ (identifier * identifier) list -> constr_expr -> constr_expr
+
+val occur_var_constr_expr : identifier -> constr_expr -> bool
+
+val mkIdentC : identifier -> constr_expr
+val mkRefC : reference -> constr_expr
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+val mkCastC : constr_expr * constr_expr -> constr_expr
+val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
+val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+
+(* Used in correctness and interface; absence of var capture not guaranteed *)
+(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+
+val map_constr_expr_with_binders :
+ ('a -> constr_expr -> constr_expr) ->
+ (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
+
+(* For binders parsing *)
+
+type local_binder =
+ | LocalRawDef of name located * constr_expr
+ | LocalRawAssum of name located list * constr_expr
+
+(* Concrete syntax for modules and modules types *)
+
+type with_declaration_ast =
+ | CWith_Module of identifier * qualid located
+ | CWith_Definition of identifier * constr_expr
+
+type module_type_ast =
+ | CMTEident of qualid located
+ | CMTEwith of module_type_ast * with_declaration_ast
+
+type module_ast =
+ | CMEident of qualid located
+ | CMEapply of module_ast * module_ast
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 20:43:21 +0000