summaryrefslogtreecommitdiff
path: root/parsing/egrammar.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /parsing/egrammar.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'parsing/egrammar.ml')
-rw-r--r--parsing/egrammar.ml48
1 files changed, 23 insertions, 25 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 825d1af0..43836dbb 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: egrammar.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
open Pp
open Util
@@ -52,58 +52,56 @@ type prod_item =
| NonTerm of constr_production_entry *
(Names.identifier * constr_production_entry) option
-type 'a action_env = (identifier * 'a) list
+type 'a action_env = 'a list * 'a list list
let make_constr_action
(f : loc -> constr_expr action_env -> constr_expr) pil =
- let rec make (env : constr_expr action_env) = function
+ let rec make (env,envlist as fullenv : constr_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *)
- Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
- Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
+ Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+ make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
- Gramext.action (fun (v:constr_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl)
+ Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
| Some (p, ETPattern) :: tl ->
failwith "Unexpected entry of type cases pattern" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_cases_pattern_action
(f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
- let rec make (env : cases_pattern_expr action_env) = function
+ let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
| [] ->
- Gramext.action (fun loc -> f loc env)
+ Gramext.action (fun loc -> f loc fullenv)
| None :: tl -> (* parse a non-binding item *)
- Gramext.action (fun _ -> make env tl)
+ Gramext.action (fun _ -> make fullenv tl)
| Some (p, ETConstr _) :: tl -> (* pattern non-terminal *)
- Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl)
+ Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
| Some (p, ETReference) :: tl -> (* non-terminal *)
Gramext.action (fun (v:reference) ->
- make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+ make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
| Some (p, ETIdent) :: tl -> (* non-terminal *)
Gramext.action (fun (v:identifier) ->
- make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl)
+ make
+ (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
| Some (p, ETBigint) :: tl -> (* non-terminal *)
Gramext.action (fun (v:Bigint.bigint) ->
- make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl)
+ make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
| Some (p, ETConstrList _) :: tl ->
Gramext.action (fun (v:cases_pattern_expr list) ->
- let dummyid = Ident (dummy_loc,id_of_string "_") in
- make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl)
+ make (env, v :: envlist) tl)
| Some (p, (ETPattern | ETOther _)) :: tl ->
failwith "Unexpected entry of type cases pattern or other" in
- make [] (List.rev pil)
+ make ([],[]) (List.rev pil)
let make_constr_prod_item univ assoc from forpat = function
| Term tok -> (Gramext.Stoken tok, None)
@@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt =
let extend_constr_notation (n,assoc,ntn,rule) =
(* Add the notation in constr *)
- let mkact loc env = CNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CNotation (loc,ntn,env) in
let e = get_constr_entry false (ETConstr (n,())) in
extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
(* Add the notation in cases_pattern *)
- let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
+ let mkact loc env = CPatNotation (loc,ntn,env) in
let e = get_constr_entry true (ETConstr (n,())) in
extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
true rule