From: Stefano Zacchiroli Date: Wed, 25 May 2005 16:41:30 +0000 (+0000) Subject: multiple bindings inside OPT supported X-Git-Tag: PRE_INDEX_1~122 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=29aacd800408d16b9cb58dd58e603e31aa2ad511;p=helm.git multiple bindings inside OPT supported --- diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 09fd55b0d..0c4ae0220 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -373,6 +373,11 @@ let term = Gramext.Sself type env_type = (string * (value_type * value)) list +type binding = + | NoBinding + | Binding of string * value_type + | Env + let rec pp_value = function | TermValue _ -> "@TERM@" @@ -403,33 +408,36 @@ let make_action action bindings = [] -> prerr_endline "aux: make_action"; Gramext.action (fun (loc: location) -> action vl loc) - | None :: tl -> + | NoBinding :: tl -> prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl) (* LUCA: DEFCON 3 BEGIN *) - | Some (name, TermType) :: tl -> + | Binding (name, TermType) :: tl -> prerr_endline "aux: term"; Gramext.action (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl) - | Some (name, StringType) :: tl -> + | Binding (name, StringType) :: tl -> prerr_endline "aux: string"; Gramext.action (fun (v:string) -> aux ((name, (StringType, (StringValue v))) :: vl) tl) - | Some (name, NumType) :: tl -> + | Binding (name, NumType) :: tl -> prerr_endline "aux: num"; Gramext.action (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl) - | Some (name, OptType t) :: tl -> + | Binding (name, OptType t) :: tl -> prerr_endline "aux: opt"; Gramext.action (fun (v:'a option) -> aux ((name, (OptType t, (OptValue v))) :: vl) tl) - | Some (name, ListType t) :: tl -> + | Binding (name, ListType t) :: tl -> prerr_endline "aux: list"; Gramext.action (fun (v:'a list) -> aux ((name, (ListType t, (ListValue v))) :: vl) tl) + | Env :: tl -> + prerr_endline "aux: env"; + Gramext.action (fun (v:env_type) -> aux (v @ vl) tl) (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -438,8 +446,8 @@ let flatten_opt = let rec aux acc = function [] -> List.rev acc - | None::tl -> aux acc tl - | Some hd::tl -> aux (hd::acc) tl + | (NoBinding | Env) :: tl -> aux acc tl + | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl in aux [] @@ -451,28 +459,30 @@ let extract_term_production pattern = | Magic m -> aux_magic m | Variable v -> aux_variable v | _ -> assert false - and aux_literal = function - | `Symbol s -> [None, symbol s] - | `Keyword s -> [None, ident s] - | `Number s -> [None, number s] + and aux_literal = + function + | `Symbol s -> [NoBinding, symbol s] + | `Keyword s -> [NoBinding, ident s] + | `Number s -> [NoBinding, number s] and aux_layout = function - | Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2 - | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2 - | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2 - | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2 - | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2 - | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2 - | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2 + | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2 + | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2 + | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2 + | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2 + | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2 + | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2 + | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2 | Root (p1, p2) -> - [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1 - | Sqrt p -> [None, symbol "\\SQRT"] @ aux p + [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] + @ aux p1 + | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p | Break -> [] | Box (_, pl) -> List.flatten (List.map aux pl) and aux_magic = function | Opt p -> let p_bindings, p_atoms = List.split (aux p) in let p_names = flatten_opt p_bindings in - [ None, + [ Env, Gramext.srules [ [ Gramext.Sopt (Gramext.srules @@ -484,8 +494,12 @@ let extract_term_production pattern = p_bindings)])], Gramext.action (fun (env_opt : env_type option) (loc : location) -> + Printf.printf "|p_names|=%d\n" (List.length p_names) ; + flush stdout ; match env_opt with Some env -> + Printf.printf "|env|=%d\n" (List.length env) ; + flush stdout ; prerr_endline "opt action (Some _)"; List.map (fun (name, (typ, v)) -> @@ -498,10 +512,11 @@ let extract_term_production pattern = (name, (OptType typ, OptValue None))) p_names) ]] | _ -> assert false - and aux_variable = function - | NumVar s -> [Some (s, NumType), number ""] - | TermVar s -> [Some (s, TermType), term] - | IdentVar s -> [Some (s, StringType), ident ""] + and aux_variable = + function + | NumVar s -> [Binding (s, NumType), number ""] + | TermVar s -> [Binding (s, TermType), term] + | IdentVar s -> [Binding (s, StringType), ident ""] | Ascription (p, s) -> assert false (* TODO *) | FreshVar _ -> assert false in diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 32ba0a318..ef6aa482c 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -55,6 +55,8 @@ val delete: rule_id -> unit (** {2 Debugging} *) val pp_env: env_type -> string +val pp_value: CicNotationPt.value -> string +val pp_value_type: CicNotationPt.value_type -> string (** print "level2_pattern" entry on stdout, flushing afterwards *) val print_l2_pattern: unit -> unit diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index c068491a3..a8e2c45b0 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -41,7 +41,12 @@ let _ = CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA (P.Layout (P.Box (P.H, [ P.Literal (`Symbol "+"); - P.Magic (P.Opt (P.Variable (P.TermVar "ugo"))) ] + P.Magic (P.Opt (P.Layout (P.Box (P.H, + [ P.Variable (P.TermVar "ugo"); + P.Literal (`Symbol "+"); + P.Variable (P.TermVar "pino") + ])))); + ] (* [ P.Variable (P.TermVar "a"); P.Literal (`Symbol "+"); P.Variable (P.TermVar "b"); @@ -52,10 +57,12 @@ let _ = prerr_endline "reducing rule" ; prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env)); (* match env with - [(x, (_, P.OptValue v))] -> + [(_, (_, P.OptValue v))] -> begin match v with - Some _ -> Printf.printf "Ugo c'e'? %s\n" x; flush stdout + | Some x -> + printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x); + flush stdout | None -> prerr_endline "nooooo" end | _ -> assert false *)