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
| 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
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)
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
| 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
| 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
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 ()
projects / helm.git / commitdiff