From 078ef847d4a3a2087f2dc404e48bcef76ee4b4d5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 May 2005 11:42:22 +0000 Subject: [PATCH] snapshot - first commit with working list syntax --- helm/ocaml/cic_notation/cicNotationParser.ml | 114 +++++++++++++------ helm/ocaml/cic_notation/test_parser.ml | 39 ++++--- 2 files changed, 97 insertions(+), 56 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 0c4ae0220..ede5b6e66 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -371,15 +371,24 @@ let ident s = Gramext.Stoken ("IDENT", s) let number s = Gramext.Stoken ("NUMBER", s) let term = Gramext.Sself +let g_symbol_of_literal = + function + | `Symbol s -> symbol s + | `Keyword s -> ident s + | `Number s -> number s + type env_type = (string * (value_type * value)) list type binding = | NoBinding | Binding of string * value_type - | Env + | Env of (string * value_type) list let rec pp_value = function +(* | TermValue (CicNotationPt.AttributedTerm (_, CicNotationPt.Num (s, _))) + | TermValue (CicNotationPt.Num (s, _)) -> + sprintf "@TERM[%s]@" s *) | TermValue _ -> "@TERM@" | StringValue s -> sprintf "\"%s\"" s | NumValue n -> n @@ -411,7 +420,7 @@ let make_action action bindings = | NoBinding :: tl -> prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl) - (* LUCA: DEFCON 3 BEGIN *) + (* LUCA: DEFCON 2 BEGIN *) | Binding (name, TermType) :: tl -> prerr_endline "aux: term"; Gramext.action @@ -435,10 +444,10 @@ let make_action action bindings = Gramext.action (fun (v:'a list) -> aux ((name, (ListType t, (ListValue v))) :: vl) tl) - | Env :: tl -> + | Env _ :: tl -> prerr_endline "aux: env"; Gramext.action (fun (v:env_type) -> aux (v @ vl) tl) - (* LUCA: DEFCON 3 END *) + (* LUCA: DEFCON 2 END *) in aux [] (List.rev bindings) @@ -446,11 +455,21 @@ let flatten_opt = let rec aux acc = function [] -> List.rev acc - | (NoBinding | Env) :: tl -> aux acc tl + | NoBinding :: tl -> aux acc tl + | Env names :: tl -> aux (List.rev names @ acc) tl | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl in aux [] +let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) +let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) + +let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None)) +let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) + +let opt_name (n, ty) = (n, OptType ty) +let list_name (n, ty) = (n, ListType ty) + (* given a level 1 pattern computes the new RHS of "term" grammar entry *) let extract_term_production pattern = let rec aux = function @@ -478,39 +497,54 @@ let extract_term_production pattern = | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p | Break -> [] | Box (_, pl) -> List.flatten (List.map aux pl) - and aux_magic = function + and aux_magic magic = + match magic with | Opt p -> - let p_bindings, p_atoms = List.split (aux p) in - let p_names = flatten_opt p_bindings in - [ Env, + let p_bindings, p_atoms, p_names, p_action = inner_pattern p in + let action (env_opt : env_type option) (loc : location) = + match env_opt with + | Some env -> List.map opt_binding_some env + | None -> List.map opt_binding_of_name p_names + in + [ Env (List.map opt_name p_names), + Gramext.srules + [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ], + Gramext.action action ] ] + | List0 (p, _) + | List1 (p, _) -> + let p_bindings, p_atoms, p_names, p_action = inner_pattern p in + let env0 = List.map list_binding_of_name p_names in + let grow_env_entry env n v = + prerr_endline "grow_env_entry"; + List.map + (function + | (n', (ty, ListValue vl)) as entry -> + if n' = n then n', (ty, ListValue (v :: vl)) else entry + | _ -> assert false) + env + in + let grow_env env_i env = + prerr_endline "grow_env"; + List.fold_left + (fun env (n, (_, v)) -> grow_env_entry env n v) + env env_i + in + let action (env_list : env_type list) (loc : location) = + prerr_endline "list action"; + List.fold_right grow_env env_list env0 + in + let g_symbol s = + match magic with + | List0 (_, None) -> Gramext.Slist0 s + | List1 (_, None) -> Gramext.Slist1 s + | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l) + | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l) + | _ -> assert false + in + [ Env (List.map list_name p_names), Gramext.srules - [ [ Gramext.Sopt - (Gramext.srules - [ p_atoms, - (make_action - (fun (env : env_type) (loc : location) -> - prerr_endline "inner opt action"; - env) - 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)) -> - (name, (OptType typ, OptValue (Some v)))) - env - | None -> - prerr_endline "opt action (None)"; - List.map - (fun (name, typ) -> - (name, (OptType typ, OptValue None))) - p_names) ]] + [ [ g_symbol (Gramext.srules [ p_atoms, p_action ]) ], + Gramext.action action ] ] | _ -> assert false and aux_variable = function @@ -519,6 +553,14 @@ let extract_term_production pattern = | IdentVar s -> [Binding (s, StringType), ident ""] | Ascription (p, s) -> assert false (* TODO *) | FreshVar _ -> assert false + and inner_pattern p = + let p_bindings, p_atoms = List.split (aux p) in + let p_names = flatten_opt p_bindings in + let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in + let action = + make_action (fun (env : env_type) (loc : location) -> prerr_endline "inner action"; env) p_bindings + in + p_bindings, p_atoms, p_names, action in aux pattern diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index a8e2c45b0..6cbb0ef2d 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -40,33 +40,32 @@ let _ = let id = CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA (P.Layout (P.Box (P.H, - [ P.Literal (`Symbol "+"); + [ + P.Magic + (P.List0 + (P.Layout (P.Box (P.H, + [ P.Literal (`Symbol "|"); + P.Variable (P.TermVar "ugo"); + P.Magic (P.Opt (P.Layout (P.Box (P.H, + [ P.Literal (`Symbol ","); + P.Variable (P.TermVar "pino")])))); + P.Literal (`Symbol "|"); + ])), + Some (`Symbol ";"))); +(* P.Literal (`Symbol "+"); P.Magic (P.Opt (P.Layout (P.Box (P.H, - [ P.Variable (P.TermVar "ugo"); + [ + P.Variable (P.TermVar "ugo"); P.Literal (`Symbol "+"); P.Variable (P.TermVar "pino") - ])))); - ] -(* [ P.Variable (P.TermVar "a"); + ])))); *) +(* P.Variable (P.TermVar "a"); P.Literal (`Symbol "+"); - P.Variable (P.TermVar "b"); - ] *) - ))) + P.Variable (P.TermVar "b"); *) + ]))) (fun env _ -> - begin prerr_endline "reducing rule" ; prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env)); -(* match env with - [(_, (_, P.OptValue v))] -> - begin - match v with - | Some x -> - printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x); - flush stdout - | None -> prerr_endline "nooooo" - end - | _ -> assert false *) - end ; P.Sort `Prop) in CicNotationParser.print_l2_pattern () -- 2.39.2