summaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml4803
1 files changed, 803 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
new file mode 100644
index 00000000..cda482af
--- /dev/null
+++ b/parsing/pcoq.ml4
@@ -0,0 +1,803 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: pcoq.ml4,v 1.80.2.1 2004/07/16 19:30:40 herbelin Exp $ i*)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Rawterm
+open Topconstr
+open Ast
+open Genarg
+open Tacexpr
+open Ppextend
+open Extend
+
+(* The lexer of Coq *)
+
+(* Note: removing a token.
+ We do nothing because [remove_token] is called only when removing a grammar
+ rule with [Grammar.delete_rule]. The latter command is called only when
+ unfreezing the state of the grammar entries (see GRAMMAR summary, file
+ env/metasyntax.ml). Therefore, instead of removing tokens one by one,
+ we unfreeze the state of the lexer. This restores the behaviour of the
+ lexer. B.B. *)
+
+let lexer = {
+ Token.func = Lexer.func;
+ Token.using = Lexer.add_token;
+ Token.removing = (fun _ -> ());
+ Token.tparse = Lexer.tparse;
+ Token.text = Lexer.token_text }
+
+module L =
+ struct
+ let lexer = lexer
+ end
+
+(* The parser of Coq *)
+
+module G = Grammar.Make(L)
+
+let grammar_delete e rls =
+ List.iter
+ (fun (_,_,lev) ->
+ List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+ (List.rev rls)
+
+(* grammar_object is the superclass of all grammar entry *)
+module type Gramobj =
+sig
+ type grammar_object
+ val weaken_entry : 'a G.Entry.e -> grammar_object G.Entry.e
+end
+
+module Gramobj : Gramobj =
+struct
+ type grammar_object = Obj.t
+ let weaken_entry e = Obj.magic e
+end
+
+type grammar_object = Gramobj.grammar_object
+type typed_entry = entry_type * grammar_object G.Entry.e
+let in_typed_entry t e = (t,Gramobj.weaken_entry e)
+let type_of_typed_entry (t,e) = t
+let object_of_typed_entry (t,e) = e
+let weaken_entry x = Gramobj.weaken_entry x
+
+module type Gramtypes =
+sig
+ open Decl_kinds
+ val inGramObj : 'a raw_abstract_argument_type -> 'a G.Entry.e -> typed_entry
+ val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.Entry.e
+end
+
+module Gramtypes : Gramtypes =
+struct
+ let inGramObj rawwit = in_typed_entry (unquote rawwit)
+ let outGramObj (a:'a raw_abstract_argument_type) o =
+ if type_of_typed_entry o <> unquote a
+ then anomaly "outGramObj: wrong type";
+ (* downcast from grammar_object *)
+ Obj.magic (object_of_typed_entry o)
+end
+
+open Gramtypes
+
+type ext_kind =
+ | ByGrammar of
+ grammar_object G.Entry.e * Gramext.position option *
+ (string option * Gramext.g_assoc option *
+ (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+ | ByGEXTEND of (unit -> unit) * (unit -> unit)
+
+let camlp4_state = ref []
+
+(* The apparent parser of Coq; encapsulate G to keep track of the
+ extensions. *)
+module Gram =
+ struct
+ include G
+ let extend e pos rls =
+ camlp4_state :=
+ (ByGEXTEND ((fun () -> grammar_delete e rls),
+ (fun () -> G.extend e pos rls)))
+ :: !camlp4_state;
+ G.extend e pos rls
+ let delete_rule e pil =
+ errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.")
+ end
+
+
+let camlp4_verbosity silent f x =
+ let a = !Gramext.warning_verbose in
+ Gramext.warning_verbose := silent;
+ f x;
+ Gramext.warning_verbose := a
+
+(* This extension command is used by the Grammar constr *)
+
+let grammar_extend te pos rls =
+ camlp4_state := ByGrammar (Gramobj.weaken_entry te,pos,rls) :: !camlp4_state;
+ camlp4_verbosity (Options.is_verbose ()) (G.extend te pos) rls
+
+(* n is the number of extended entries (not the number of Grammar commands!)
+ to remove. *)
+let rec remove_grammars n =
+ if n>0 then
+ (match !camlp4_state with
+ | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
+ | ByGrammar(g,_,rls)::t ->
+ grammar_delete g rls;
+ camlp4_state := t;
+ remove_grammars (n-1)
+ | ByGEXTEND (undo,redo)::t ->
+ undo();
+ camlp4_state := t;
+ remove_grammars n;
+ redo();
+ camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state)
+
+(* An entry that checks we reached the end of the input. *)
+let eoi_entry en =
+ let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_eoi") in
+ GEXTEND Gram
+ e: [ [ x = en; EOI -> x ] ]
+ ;
+ END;
+ e
+
+let map_entry f en =
+ let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_map") in
+ GEXTEND Gram
+ e: [ [ x = en -> f x ] ]
+ ;
+ END;
+ e
+
+(* Parse a string, does NOT check if the entire string was read
+ (use eoi_entry) *)
+
+let parse_string f x =
+ let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
+
+type gram_universe = (string, typed_entry) Hashtbl.t
+
+let trace = ref false
+
+(* The univ_tab is not part of the state. It contains all the grammar that
+ exist or have existed before in the session. *)
+
+let univ_tab = (Hashtbl.create 7 : (string, string * gram_universe) Hashtbl.t)
+
+let create_univ s =
+ let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+
+let uprim = create_univ "prim"
+let uconstr = create_univ "constr"
+let umodule = create_univ "module"
+let utactic = create_univ "tactic"
+let uvernac = create_univ "vernac"
+
+let create_univ_if_new s =
+ (* compatibilite *)
+ let s = if s = "command" then (warning "'command' grammar universe is obsolete; use name 'constr' instead"; "constr") else s in
+ try
+ Hashtbl.find univ_tab s
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating univ %s]\n" s; flush stderr; ()
+ end;
+ let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+
+let get_univ = create_univ_if_new
+
+let get_entry (u, utab) s =
+ try
+ Hashtbl.find utab s
+ with Not_found ->
+ errorlabstrm "Pcoq.get_entry"
+ (str "unknown grammar entry " ++ str u ++ str ":" ++ str s)
+
+let new_entry etyp (u, utab) s =
+ let ename = u ^ ":" ^ s in
+ let e = in_typed_entry etyp (Gram.Entry.create ename) in
+ Hashtbl.add utab s e; e
+
+let entry_type (u, utab) s =
+ try
+ let e = Hashtbl.find utab s in
+ Some (type_of_typed_entry e)
+ with Not_found -> None
+
+let get_entry_type (u,n) = type_of_typed_entry (get_entry (get_univ u) n)
+
+let create_entry_if_new (u, utab) s etyp =
+ try
+ if type_of_typed_entry (Hashtbl.find utab s) <> etyp then
+ failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type")
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
+ end;
+ let _ = new_entry etyp (u, utab) s in ()
+
+let create_entry (u, utab) s etyp =
+ try
+ let e = Hashtbl.find utab s in
+ if type_of_typed_entry e <> etyp then
+ failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
+ e
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
+ end;
+ new_entry etyp (u, utab) s
+
+let create_constr_entry u s =
+ outGramObj rawwit_constr (create_entry u s ConstrArgType)
+
+let create_generic_entry s wit =
+ let (u,utab) = utactic in
+ let etyp = unquote wit in
+ try
+ let e = Hashtbl.find utab s in
+ if type_of_typed_entry e <> etyp then
+ failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
+ outGramObj wit e
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
+ end;
+ let e = Gram.Entry.create s in
+ Hashtbl.add utab s (inGramObj wit e); e
+
+let get_generic_entry s =
+ let (u,utab) = utactic in
+ try
+ object_of_typed_entry (Hashtbl.find utab s)
+ with Not_found ->
+ error ("unknown grammar entry "^u^":"^s)
+
+let get_generic_entry_type (u,utab) s =
+ try type_of_typed_entry (Hashtbl.find utab s)
+ with Not_found ->
+ error ("unknown grammar entry "^u^":"^s)
+
+let force_entry_type (u, utab) s etyp =
+ try
+ let entry = Hashtbl.find utab s in
+ let extyp = type_of_typed_entry entry in
+ if etyp = extyp then
+ entry
+ else begin
+ prerr_endline
+ ("Grammar entry " ^ u ^ ":" ^ s ^
+ " redefined with another type;\n older entry hidden.");
+ Hashtbl.remove utab s;
+ new_entry etyp (u, utab) s
+ end
+ with Not_found ->
+ new_entry etyp (u, utab) s
+
+(* [make_gen_entry] builds entries extensible by giving its name (a string) *)
+(* For entries extensible only via the ML name, Gram.Entry.create is enough *)
+
+let make_gen_entry (u,univ) rawwit s =
+ let e = Gram.Entry.create (u ^ ":" ^ s) in
+ Hashtbl.add univ s (inGramObj rawwit e); e
+
+(* Grammar entries *)
+
+module Prim =
+ struct
+ let gec_gen x = make_gen_entry uprim x
+
+ (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ (* Typically for tactic or vernac extensions *)
+ let preident = gec_gen rawwit_pre_ident "preident"
+ let ident = gec_gen rawwit_ident "ident"
+ let natural = gec_gen rawwit_int "natural"
+ let integer = gec_gen rawwit_int "integer"
+ let bigint = Gram.Entry.create "Prim.bigint"
+ let string = gec_gen rawwit_string "string"
+ let reference = make_gen_entry uprim rawwit_ref "reference"
+
+ (* parsed like ident but interpreted as a term *)
+ let hyp = gec_gen rawwit_ident "hyp"
+
+ (* synonym of hyp/ident (before semantics split) for v7 compatibility *)
+ let var = gec_gen rawwit_ident "var"
+
+ let name = Gram.Entry.create "Prim.name"
+ let identref = Gram.Entry.create "Prim.identref"
+
+ (* A synonym of ident - maybe ident will be located one day *)
+ let base_ident = Gram.Entry.create "Prim.base_ident"
+
+ let qualid = Gram.Entry.create "Prim.qualid"
+ let dirpath = Gram.Entry.create "Prim.dirpath"
+
+ let ne_string = Gram.Entry.create "Prim.ne_string"
+
+ (* For old ast printer *)
+ let astpat = Gram.Entry.create "Prim.astpat"
+ let ast = Gram.Entry.create "Prim.ast"
+ let astlist = Gram.Entry.create "Prim.astlist"
+ let ast_eoi = eoi_entry ast
+ let astact = Gram.Entry.create "Prim.astact"
+ end
+
+
+module Constr =
+ struct
+ let gec_constr = make_gen_entry uconstr rawwit_constr
+ let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr)
+
+ (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ let constr = gec_constr "constr"
+ let operconstr = gec_constr "operconstr"
+ let constr_eoi = eoi_entry constr
+ let lconstr = gec_constr "lconstr"
+ let binder_constr = create_constr_entry uconstr "binder_constr"
+ let ident = make_gen_entry uconstr rawwit_ident "ident"
+ let global = make_gen_entry uconstr rawwit_ref "global"
+ let sort = make_gen_entry uconstr rawwit_sort "sort"
+ let pattern = Gram.Entry.create "constr:pattern"
+ let annot = Gram.Entry.create "constr:annot"
+ let constr_pattern = gec_constr "constr_pattern"
+ let lconstr_pattern = gec_constr "lconstr_pattern"
+ let binder = Gram.Entry.create "constr:binder"
+ let binder_let = Gram.Entry.create "constr:binder_let"
+ end
+
+module Module =
+ struct
+ let module_expr = Gram.Entry.create "module_expr"
+ let module_type = Gram.Entry.create "module_type"
+ end
+
+module Tactic =
+ struct
+ (* Main entry for extensions *)
+ let simple_tactic = Gram.Entry.create "tactic:simple_tactic"
+
+ (* Entries that can be refered via the string -> Gram.Entry.e table *)
+ (* Typically for tactic user extensions *)
+ let castedopenconstr =
+ make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
+ let constr_with_bindings =
+ make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
+ let bindings =
+ make_gen_entry utactic rawwit_bindings "bindings"
+ let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
+ let quantified_hypothesis =
+ make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
+ let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
+ let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr"
+ let simple_intropattern =
+ make_gen_entry utactic rawwit_intro_pattern "simple_intropattern"
+
+ (* Main entries for ltac *)
+ let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
+ let tactic = make_gen_entry utactic rawwit_tactic "tactic"
+
+ (* Main entry for quotations *)
+ let tactic_eoi = eoi_entry tactic
+ end
+
+
+module Vernac_ =
+ struct
+ let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
+
+ (* The different kinds of vernacular commands *)
+ let gallina = gec_vernac "gallina"
+ let gallina_ext = gec_vernac "gallina_ext"
+ let command = gec_vernac "command"
+ let syntax = gec_vernac "syntax_command"
+ let vernac = gec_vernac "Vernac_.vernac"
+
+ let vernac_eoi = eoi_entry vernac
+ end
+
+
+(* Prim is not re-initialized *)
+let reset_all_grammars () =
+ let f = Gram.Unsafe.clear_entry in
+ List.iter f
+ [Constr.constr;Constr.operconstr;Constr.lconstr;Constr.annot;
+ Constr.constr_pattern;Constr.lconstr_pattern];
+ f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern;
+ f Module.module_expr; f Module.module_type;
+ f Tactic.simple_tactic;
+ f Tactic.castedopenconstr;
+ f Tactic.constr_with_bindings;
+ f Tactic.bindings;
+ f Tactic.constrarg;
+ f Tactic.quantified_hypothesis;
+ f Tactic.int_or_var;
+ f Tactic.red_expr;
+ f Tactic.tactic_arg;
+ f Tactic.tactic;
+ f Vernac_.gallina;
+ f Vernac_.gallina_ext;
+ f Vernac_.command;
+ f Vernac_.syntax;
+ f Vernac_.vernac;
+ Lexer.init()
+
+let main_entry = Gram.Entry.create "vernac"
+
+GEXTEND Gram
+ main_entry:
+ [ [ a = Vernac_.vernac -> Some (loc,a) | EOI -> None ] ]
+ ;
+END
+
+(* Quotations *)
+
+open Prim
+open Constr
+open Tactic
+open Vernac_
+
+(* current file and toplevel/vernac.ml *)
+let globalizer = ref (fun x -> failwith "No globalizer")
+let set_globalizer f = globalizer := f
+
+let define_ast_quotation default s (e:Coqast.t G.Entry.e) =
+ (if default then
+ GEXTEND Gram
+ ast: [ [ "<<"; c = e; ">>" -> c ] ];
+ (* Uncomment this to keep compatibility with old grammar syntax
+ constr: [ [ "<<"; c = e; ">>" -> c ] ];
+ vernac: [ [ "<<"; c = e; ">>" -> c ] ];
+ tactic: [ [ "<<"; c = e; ">>" -> c ] ];
+ *)
+ END);
+ (GEXTEND Gram
+ GLOBAL: ast constr command tactic;
+ ast:
+ [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+ (* Uncomment this to keep compatibility with old grammar syntax
+ constr:
+ [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+ command:
+ [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+ tactic:
+ [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+ *)
+ END)
+
+(*
+let _ = define_ast_quotation false "ast" ast in ()
+*)
+
+let dynconstr = Gram.Entry.create "Constr.dynconstr"
+let dyncasespattern = Gram.Entry.create "Constr.dyncasespattern"
+
+GEXTEND Gram
+ dynconstr:
+ [ [ a = Constr.constr -> ConstrNode a
+ (* For compatibility *)
+ | "<<"; a = Constr.lconstr; ">>" -> ConstrNode a ] ]
+ ;
+ dyncasespattern: [ [ a = Constr.pattern -> CasesPatternNode a ] ];
+END
+
+(**********************************************************************)
+(* The following is to dynamically set the parser in Grammar actions *)
+(* and Syntax pattern, according to the universe of the rule defined *)
+
+type parser_type =
+ | ConstrParser
+ | CasesPatternParser
+
+let default_action_parser_ref = ref dynconstr
+
+let get_default_action_parser () = !default_action_parser_ref
+
+let entry_type_of_parser = function
+ | ConstrParser -> Some ConstrArgType
+ | CasesPatternParser -> failwith "entry_type_of_parser: cases_pattern, TODO"
+
+let parser_type_from_name = function
+ | "constr" -> ConstrParser
+ | "cases_pattern" -> CasesPatternParser
+ | "tactic" -> assert false
+ | "vernac" -> error "No longer supported"
+ | s -> ConstrParser
+
+let set_default_action_parser = function
+ | ConstrParser -> default_action_parser_ref := dynconstr
+ | CasesPatternParser -> default_action_parser_ref := dyncasespattern
+
+let default_action_parser =
+ Gram.Entry.of_parser "default_action_parser"
+ (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
+
+(**********************************************************************)
+(* This determines (depending on the associativity of the current
+ level and on the expected associativity) if a reference to constr_n is
+ a reference to the current level (to be translated into "SELF" on the
+ left border and into "constr LEVEL n" elsewhere), to the level below
+ (to be translated into "NEXT") or to an below wrt associativity (to be
+ translated in camlp4 into "constr" without level) or to another level
+ (to be translated into "constr LEVEL n") *)
+
+let assoc_level = function
+ | Some Gramext.LeftA when !Options.v7 -> "L"
+ | _ -> ""
+
+let constr_level = function
+ | n,assoc -> (string_of_int n)^(assoc_level assoc)
+
+let constr_level2 = function
+ | n,assoc -> (string_of_int n)^(assoc_level (Some assoc))
+
+let default_levels_v7 =
+ [10,Gramext.RightA;
+ 9,Gramext.RightA;
+ 8,Gramext.RightA;
+ 1,Gramext.RightA;
+ 0,Gramext.RightA]
+
+let default_levels_v8 =
+ [200,Gramext.RightA;
+ 100,Gramext.RightA;
+ 99,Gramext.RightA;
+ 90,Gramext.RightA;
+ 10,Gramext.RightA;
+ 9,Gramext.RightA;
+ 1,Gramext.LeftA;
+ 0,Gramext.RightA]
+
+let default_pattern_levels_v8 =
+ [10,Gramext.LeftA;
+ 0,Gramext.RightA]
+
+let level_stack =
+ ref
+ [if !Options.v7 then (default_levels_v7, default_levels_v7)
+ else (default_levels_v8, default_pattern_levels_v8)]
+
+(* At a same level, LeftA takes precedence over RightA and NoneA *)
+(* In case, several associativity exists for a level, we make two levels, *)
+(* first LeftA, then RightA and NoneA together *)
+exception Found of Gramext.g_assoc
+
+open Ppextend
+
+let admissible_assoc = function
+ | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
+ | Gramext.RightA, Some Gramext.LeftA -> false
+ | _ -> true
+
+let create_assoc = function
+ | None -> Gramext.RightA
+ | Some a -> a
+
+let error_level_assoc p current expected =
+ let pr_assoc = function
+ | Gramext.LeftA -> str "left"
+ | Gramext.RightA -> str "right"
+ | Gramext.NonA -> str "non" in
+ errorlabstrm ""
+ (str "Level " ++ int p ++ str " is already declared " ++
+ pr_assoc current ++ str " associative while it is now expected to be " ++
+ pr_assoc expected ++ str " associative")
+
+let find_position forpat other assoc lev =
+ let default = if !Options.v7 then Some (10,Gramext.RightA) else None in
+ let ccurrent,pcurrent as current = List.hd !level_stack in
+ match lev with
+ | None ->
+ level_stack := current :: !level_stack;
+ None, (if other then assoc else None), None
+ | Some n ->
+ if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then
+ error "Left associativity not allowed at level 8";
+ let after = ref default in
+ let rec add_level q = function
+ | (p,_ as pa)::l when p > n -> pa :: add_level (Some pa) l
+ | (p,a as pa)::l as l' when p = n ->
+ if admissible_assoc (a,assoc) then raise (Found a);
+ (* No duplication of levels in v8 *)
+ if not !Options.v7 then error_level_assoc p a (out_some assoc);
+ (* Maybe this was (p,Left) and p occurs a second time *)
+ if a = Gramext.LeftA then
+ match l with
+ | (p,a)::_ as l' when p = n -> raise (Found a)
+ | _ -> after := Some pa; pa::(n,create_assoc assoc)::l
+ else
+ (* This was not (p,LeftA) hence assoc is RightA *)
+ (after := q; (n,create_assoc assoc)::l')
+ | l ->
+ after := q; (n,create_assoc assoc)::l
+ in
+ try
+ (* Create the entry *)
+ let updated =
+ if forpat then (ccurrent, add_level default pcurrent)
+ else (add_level default ccurrent, pcurrent) in
+ level_stack := updated:: !level_stack;
+ let assoc = create_assoc assoc in
+ (if !after = None then Some Gramext.First
+ else Some (Gramext.After (constr_level2 (out_some !after)))),
+ Some assoc, Some (constr_level2 (n,assoc))
+ with
+ Found a ->
+ level_stack := current :: !level_stack;
+ (* Just inherit the existing associativity and name (None) *)
+ Some (Gramext.Level (constr_level2 (n,a))), None, None
+
+let remove_levels n =
+ level_stack := list_skipn n !level_stack
+
+(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
+let camlp4_assoc = function
+ | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA
+ | None | Some Gramext.LeftA -> Gramext.LeftA
+
+(* [adjust_level assoc from prod] where [assoc] and [from] are the name
+ and associativity of the level where to add the rule; the meaning of
+ the result is
+
+ None = SELF
+ Some None = NEXT
+ Some (Some (n,cur)) = constr LEVEL n
+ s.t. if [cur] is set then [n] is the same as the [from] level *)
+let adjust_level assoc from = function
+(* Associativity is None means force the level *)
+ | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
+(* Compute production name on the right side *)
+ (* If NonA or LeftA on the right-hand side, set to NEXT *)
+ | (NumLevel n,BorderProd (false,Some (Gramext.NonA|Gramext.LeftA))) ->
+ Some None
+ (* If RightA on the right-hand side, set to the explicit (current) level *)
+ | (NumLevel n,BorderProd (false,Some Gramext.RightA)) ->
+ Some (Some (n,true))
+(* Compute production name on the left side *)
+ (* If NonA on the left-hand side, adopt the current assoc ?? *)
+ | (NumLevel n,BorderProd (true,Some Gramext.NonA)) -> None
+ (* If the expected assoc is the current one, set to SELF *)
+ | (NumLevel n,BorderProd (true,Some a)) when a = camlp4_assoc assoc ->
+ None
+ (* Otherwise, force the level, n or n-1, according to expected assoc *)
+ | (NumLevel n,BorderProd (true,Some a)) ->
+ if a = Gramext.LeftA then Some (Some (n,true)) else Some None
+ (* None means NEXT *)
+ | (NextLevel,_) -> Some None
+(* Compute production name elsewhere *)
+ | (NumLevel n,InternalProd) ->
+ match from with
+ | ETConstr (p,()) when p = n+1 -> Some None
+ | ETConstr (p,()) -> Some (Some (n,n=p))
+ | _ -> Some (Some (n,false))
+
+(*
+ (* If NonA on the right-hand side, set to NEXT *)
+ | (n,BorderProd (false,Some Gramext.NonA)) -> Some None
+ (* If NonA on the left-hand side, adopt the current assoc ?? *)
+ | (n,BorderProd (true,Some Gramext.NonA)) -> None
+ (* Associativity is None means force the level *)
+ | (n,BorderProd (_,None)) -> Some (Some (n,true))
+ (* If left assoc at a left level, set NEXT on the right *)
+ | (n,BorderProd (false,Some (Gramext.LeftA as a)))
+ when Gramext.LeftA = camlp4_assoc assoc -> Some None
+ (* If right or none assoc expected is the current assoc, set explicit
+ level on the right side *)
+ | (n,BorderProd (false,Some a)) when a = camlp4_assoc assoc ->
+ Some (Some (n,true))
+ (* If the expected assoc is the current one, SELF on the left sides *)
+ | (n,BorderProd (true,Some a)) when a = camlp4_assoc assoc -> None
+ (* Otherwise, force the level, n or n-1, according to expected assoc *)
+ | (n,BorderProd (left,Some a)) ->
+ if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA)
+ then Some (Some (n,true)) else Some (Some (n-1,false))
+(* | (8,InternalProd) -> None (* Or (Some 8) for factorization ? *)*)
+ | (n,InternalProd) ->
+ match from with
+ | ETConstr (p,()) when p = n+1 -> Some None
+ | ETConstr (p,()) -> Some (Some (n,n=p))
+ | _ -> Some (Some (n,false))
+*)
+
+let compute_entry allow_create adjust forpat = function
+ | ETConstr (n,q) ->
+ (if forpat then weaken_entry Constr.pattern
+ else weaken_entry Constr.operconstr),
+ (if forpat & !Options.v7 then None else adjust (n,q)), false
+ | ETIdent -> weaken_entry Constr.ident, None, false
+ | ETBigint -> weaken_entry Prim.bigint, None, false
+ | ETReference -> weaken_entry Constr.global, None, false
+ | ETPattern -> weaken_entry Constr.pattern, None, false
+ | ETOther ("constr","annot") ->
+ weaken_entry Constr.annot, None, false
+ | ETConstrList _ -> error "List of entries cannot be registered"
+ | ETOther (u,n) ->
+ let u = get_univ u in
+ let e =
+ try get_entry u n
+ with e when allow_create -> create_entry u n ConstrArgType in
+ object_of_typed_entry e, None, true
+
+(* This computes the name of the level where to add a new rule *)
+let get_constr_entry forpat en =
+ match en with
+ ETConstr(200,()) when not !Options.v7 & not forpat ->
+ snd (get_entry (get_univ "constr") "binder_constr"),
+ None,
+ false
+ | _ -> compute_entry true (fun (n,()) -> Some n) forpat en
+
+(* This computes the name to give to a production knowing the name and
+ associativity of the level where it must be added *)
+let get_constr_production_entry ass from forpat en =
+ (* first 2 cases to help factorisation *)
+ match en with
+ | ETConstr (NumLevel 10,q) when !Options.v7 & not forpat ->
+ weaken_entry Constr.lconstr, None, false
+(*
+ | ETConstr (8,q) when !Options.v7 ->
+ weaken_entry Constr.constr, None, false
+*)
+ | _ -> compute_entry false (adjust_level ass from) forpat en
+
+let constr_prod_level assoc cur lev =
+ if !Options.v7 then
+ if cur then constr_level (lev,assoc) else
+ match lev with
+ | 4 when !Options.v7 -> "4L"
+ | n -> string_of_int n
+ else
+ (* No duplication L/R of levels in v8 *)
+ constr_level (lev,assoc)
+
+let is_self from e =
+ match from, e with
+ ETConstr(n,()), ETConstr(NumLevel n',
+ BorderProd(false, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false
+ | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(true,_)) -> n=n'
+ | (ETIdent,ETIdent | ETReference, ETReference | ETBigint,ETBigint
+ | ETPattern, ETPattern) -> true
+ | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2'
+ | _ -> false
+
+let is_binder_level from e =
+ match from, e with
+ ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
+ | _ -> false
+
+let rec symbol_of_production assoc from forpat typ =
+ if is_binder_level from typ then
+ let eobj = snd (get_entry (get_univ "constr") "operconstr") in
+ Gramext.Snterml (Gram.Entry.obj eobj,"200")
+ else if is_self from typ then Gramext.Sself
+ else
+ match typ with
+ | ETConstrList (typ',[]) ->
+ Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ'))
+ | ETConstrList (typ',tkl) ->
+ Gramext.Slist1sep
+ (symbol_of_production assoc from forpat (ETConstr typ'),
+ Gramext.srules
+ [List.map (fun x -> Gramext.Stoken x) tkl,
+ List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
+ (Gramext.action (fun loc -> ()))])
+ | _ ->
+ match get_constr_production_entry assoc from forpat typ with
+ | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
+ | (eobj,Some None,_) -> Gramext.Snext
+ | (eobj,Some (Some (lev,cur)),_) ->
+ Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev)
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 11:19:42 +0000