TODO
-* gestione priorita'/associativita'
- - triplicare livelli nella grammatica?
* implementare type-checker per le trasformazioni
* prestazioni trasformazioni 3 => 2 e 2 => 1
* magic per gestione degli array?
-* gestione speciale dei numeri
+* gestione della notazione per i numeri
* sintassi concreta
- studiare/implementare sintassi con ... per i magic fold
* integrazione
- portare le trasformazioni al nuovo ast
- - salvare la notazione nei file .moo
- togliere file non piu' utilizzati (caterva di cvs remove)
+ - gestire i problemi di ridefinizione della stessa notazione?
DONE
+* gestione priorita'/associativita'
+ - triplicare livelli nella grammatica?
* implementare trasformazione 1 => 0
* implementare istanziazione dei magic a livello 1 (2 => 1)
* implementare compilazione dei default in 2 => 1
- porting della disambiguazione al nuovo ast
- refactoring: unico punto di accesso allo stato imperativo della notazione
- gestire cast
+ - salvare la notazione nei file .moo
let min_precedence = 0
let max_precedence = 100
-let default_precedence = 50
let level1_pattern =
Grammar.Entry.create level1_pattern_grammar "level1_pattern"
in
aux pattern
-let level_of_int precedence =
+let level_of precedence associativity =
if precedence < min_precedence || precedence > max_precedence then
raise (Level_not_found precedence);
- string_of_int precedence
+ let assoc_string =
+ match associativity with
+ | Gramext.NonA -> "N"
+ | Gramext.LeftA -> "L"
+ | Gramext.RightA -> "R"
+ in
+ string_of_int precedence ^ assoc_string
type rule_id = Token.t Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
let owned_keywords = Hashtbl.create 23
-let extend level1_pattern ?(precedence = default_precedence)
- ?associativity action
-=
+let extend level1_pattern ~precedence ~associativity action =
let p_bindings, p_atoms =
List.split (extract_term_production level1_pattern)
in
- let level = level_of_int precedence in
+ let level = level_of precedence associativity in
let p_names = flatten_opt p_bindings in
let _ =
Grammar.extend
[ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
Some (Gramext.Level level),
[ None,
- associativity,
+ Some associativity,
[ p_atoms,
(make_action
(fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
let mk_level_list first last =
let rec aux acc = function
| i when i < first -> acc
- | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
+ | i ->
+ aux
+ ((Some (string_of_int i ^ "N"), Some Gramext.NonA, [])
+ :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, [])
+ :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, [])
+ :: acc)
+ (i - 1)
in
aux [] last
in
END
(* }}} *)
-
+(* {{{ Grammar for ast magics, notation level 2 *)
EXTEND
GLOBAL: level2_meta;
l2_variable: [
]
];
END
+(* }}} *)
+(* {{{ Grammar for ast patterns, notation level 2 *)
EXTEND
GLOBAL: level2_ast term let_defs;
-(* {{{ Grammar for ast patterns, notation level 2 *)
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
RPAREN -> (vars, typ)
]
];
- term: LEVEL "10" (* let in *)
- [ "10" NONA
- [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
- p1 = term; "in"; p2 = term ->
- return_term loc (LetIn (var, p1, p2))
- | "let"; k = induction_kind; defs = let_defs; "in";
- body = term ->
- return_term loc (LetRec (k, defs, body))
- ]
- ];
- term: LEVEL "20" (* binder *)
- [ "20" RIGHTA
+ term: LEVEL "10N" [ (* let in *)
+ [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ p1 = term; "in"; p2 = term ->
+ return_term loc (LetIn (var, p1, p2))
+ | "let"; k = induction_kind; defs = let_defs; "in";
+ body = term ->
+ return_term loc (LetRec (k, defs, body))
+ ]
+ ];
+ term: LEVEL "20R" (* binder *)
+ [
[ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
return_term loc (fold_cluster b vars typ body)
]
];
- term: LEVEL "70" (* apply *)
- [ "70" LEFTA
+ term: LEVEL "70L" (* apply *)
+ [
[ p1 = term; p2 = term ->
let rec aux = function
| Appl (hd :: tl)
return_term loc (Appl (aux p1 @ [p2]))
]
];
- term: LEVEL "90" (* simple *)
- [ "90" NONA
+ term: LEVEL "90N" (* simple *)
+ [
[ id = IDENT -> return_term loc (Ident (id, None))
| id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
| s = CSYMBOL -> return_term loc (Symbol (s, 0))
| blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
]
];
-(* }}} *)
END
+(* }}} *)
(** {2 API implementation} *)
val extend:
CicNotationPt.term ->
- ?precedence:int ->
- ?associativity:Gramext.g_assoc ->
+ precedence:int ->
+ associativity:Gramext.g_assoc ->
(CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) ->
rule_id
sprintf "#[%s]" (pp_term term)
| AttributedTerm (_, term) when print_attributes ->
sprintf "@[%s]" (pp_term term) *)
- | AttributedTerm (`Raw (text, None), _) -> text
- | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text
- | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text
+ | AttributedTerm (`Raw text, _) -> text
| AttributedTerm (_, term) -> pp_term ~pp_parens:false term
| Appl terms ->
let (x, y) = loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
-type blob_context = [ `Ast | `Meta ]
-
type term_attribute =
[ `Loc of location (* source file location *)
| `IdRef of string (* ACic pointer *)
| `Level of int * Gramext.g_assoc (* precedence, associativity *)
| `XmlAttrs of (string option * string * string) list
(* list of XML attributes: namespace, name, value *)
- | `Raw of string * blob_context option (* unparsed version *)
+ | `Raw of string (* unparsed version *)
]
type literal =
type interpretation_id = pattern_id
type pretty_printer_id = pattern_id
-let default_prec = 50
-let default_assoc = Gramext.NonA
-
module Ast = CicNotationPt
type term_info =
!(Hashtbl.find interpretations symbol)
with Not_found -> raise Interpretation_not_found
-let add_pretty_printer
- ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
-=
+let add_pretty_printer ~precedence ~associativity l2 l1 =
let id = fresh_id () in
let l2' = CicNotationUtil.strip_attributes l2 in
Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
CicNotationPt.cic_appl_pattern) list
val add_pretty_printer:
- ?precedence:int ->
- ?associativity:Gramext.g_assoc ->
+ precedence:int ->
+ associativity:Gramext.g_assoc ->
CicNotationPt.term -> (* level 2 pattern *)
CicNotationPt.term -> (* level 1 pattern *)
pretty_printer_id
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+ | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int *
CicNotationPt.term
(* level 1 pattern, associativity, precedence, level 2 pattern *)
| Interpretation of loc *
let pp_l2_pattern = CicNotationPp.pp_term
let pp_associativity = function
- | Some Gramext.LeftA -> "left associative "
- | Some Gramext.RightA -> "right associative "
- | Some Gramext.NonA -> "non associative "
- | None -> ""
+ | Gramext.LeftA -> "left associative"
+ | Gramext.RightA -> "right associative"
+ | Gramext.NonA -> "non associative"
-let pp_precedence = function
- | Some i -> sprintf "with precedence %d " i
- | None -> ""
+let pp_precedence i = sprintf "with precedence %d" i
let pp_command = function
| Include (_,path) -> "include " ^ path
(String.concat " " (List.map pp_argument_pattern arg_patterns))
(pp_cic_appl_pattern cic_appl_pattern)
| Notation (_, l1_pattern, assoc, prec, l2_pattern) ->
- sprintf "notation \"%s\" %s%sfor %s"
+ sprintf "notation \"%s\" %s %s for %s"
(pp_l1_pattern l1_pattern)
(pp_associativity assoc)
(pp_precedence prec)
let term = CicNotationParser.term
let statement = Grammar.Entry.create grammar "statement"
-let add_raw_attribute ?context ~text term =
- CicNotationPt.AttributedTerm (`Raw (text, context), term)
+let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+
+let default_precedence = 50
+let default_associativity = Gramext.NonA
EXTEND
GLOBAL: term statement;
IDENT "for";
p2 =
[ blob = UNPARSED_AST ->
- add_raw_attribute ~context:`Ast ~text:blob
+ add_raw_attribute ~text:(sprintf "@{%s}" blob)
(CicNotationParser.parse_level2_ast (Stream.of_string blob))
| blob = UNPARSED_META ->
- add_raw_attribute ~context:`Meta ~text:blob
+ add_raw_attribute ~text:(sprintf "${%s}" blob)
(CicNotationParser.parse_level2_meta (Stream.of_string blob))
] ->
+ let assoc =
+ match assoc with
+ | None -> default_associativity
+ | Some assoc -> assoc
+ in
+ let prec =
+ match prec with
+ | None -> default_precedence
+ | Some prec -> prec
+ in
(add_raw_attribute ~text:s
(CicNotationParser.parse_level1_pattern (Stream.of_string s)),
assoc, prec, p2)
exit 2
end
+let pp_associativity = function
+ | Gramext.LeftA -> "left"
+ | Gramext.RightA -> "right"
+ | Gramext.NonA -> "non"
+
+let pp_precedence = string_of_int
+
let process_stream ?(ignore_exn = false) istream =
let char_count = ref 0 in
let module P = CicNotationPt in
char_count := y + !char_count;
match statement with
| G.Executable (_, G.Macro (_, G.Check (_, t))) ->
- prerr_endline "====";
- prerr_endline (CicNotationPp.pp_term t); flush stdout;
+ prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t));
let t' = CicNotationRew.pp_ast t in
- prerr_endline (CicNotationPp.pp_term t'); flush stdout;
- let tbl = Hashtbl.create 0 in
- dump_xml t' tbl "out.xml"
+ prerr_endline (sprintf "rendered ast: %s"
+ (CicNotationPp.pp_term t'));
+ let tbl = Hashtbl.create 0 in
+ dump_xml t' tbl "out.xml"
| G.Executable (_, G.Command (_,
G.Notation (_, l1, associativity, precedence, l2))) ->
- prerr_endline "Extending parser ..."; flush stdout;
- prerr_endline (CicNotationPp.pp_term l1) ;
- prerr_endline (CicNotationPp.pp_term l2) ;
- prerr_endline (sprintf "Found keywords: %s"
- (String.concat " " (CicNotationUtil.keywords_of_term l1)));
- let time1 = Unix.gettimeofday () in
- ignore (CicNotationParser.extend l1 ?precedence ?associativity
- (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
- let time2 = Unix.gettimeofday () in
- prerr_endline "Extending pretty printer ..."; flush stdout;
- let time3 = Unix.gettimeofday () in
- ignore (CicNotationRew.add_pretty_printer
- ?precedence ?associativity l2 l1);
- let time4 = Unix.gettimeofday () in
- printf ("done (extending parser took %f, " ^^
- "extending pretty printer took %f)\n")
- (time2 -. time1) (time4 -. time3);
- flush stdout
+ prerr_endline "notation";
+ prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1));
+ prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2));
+ prerr_endline (sprintf "prec: %s" (pp_precedence precedence));
+ prerr_endline (sprintf "assoc: %s" (pp_associativity associativity));
+ let keywords = CicNotationUtil.keywords_of_term l1 in
+ if keywords <> [] then
+ prerr_endline (sprintf "keywords: %s"
+ (String.concat " " keywords));
+ ignore (CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
+ ignore (CicNotationRew.add_pretty_printer
+ ?precedence ?associativity l2 l1)
| G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) ->
- prerr_endline "Adding interpretation ..."; flush stdout;
- let time1 = Unix.gettimeofday () in
- ignore (CicNotationRew.add_interpretation id l2 l3);
- let time2 = Unix.gettimeofday () in
- printf "done (patterns compilation took %f seconds)\n"
- (time2 -. time1);
- flush stdout
+ prerr_endline "interpretation";
+ prerr_endline (sprintf "dsc: %s" id);
+ ignore (CicNotationRew.add_interpretation id l2 l3);
+ flush stdout
| G.Executable (_, G.Command (_, G.Dump _)) ->
CicNotationParser.print_l2_pattern (); print_newline ()
| G.Executable (_, G.Command (_, G.Render (_, uri))) ->
| Cic.AVariable (_, _, _, ty, _, _) -> ty
| _ -> assert false
in
- let time1 = Unix.gettimeofday () in
let t, id_to_uri =
CicNotationRew.ast_of_acic id_to_sort annterm
in
- let time2 = Unix.gettimeofday () in
- prerr_endline (sprintf "ast creation took %f seconds\n"
- (time2 -. time1));
- prerr_endline "AST";
- prerr_endline (CicNotationPp.pp_term t);
- flush stdout;
- let time3 = Unix.gettimeofday () in
- let t' = CicNotationRew.pp_ast t in
- let time4 = Unix.gettimeofday () in
- prerr_endline (sprintf "pretty printing took %f seconds\n"
- (time4 -. time3));
- prerr_endline (CicNotationPp.pp_term t');
- dump_xml t' id_to_uri "out.xml"
- | _ ->
- prerr_endline "Unsupported statement"
+ prerr_endline "AST";
+ prerr_endline (CicNotationPp.pp_term t);
+ let t' = CicNotationRew.pp_ast t in
+ prerr_endline (CicNotationPp.pp_term t');
+ dump_xml t' id_to_uri "out.xml"
+ | _ -> prerr_endline "Unsupported statement"
with
| End_of_file -> raise End_of_file
| CicNotationParser.Parse_error (floc, msg) ->
let usage = "" in
Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
print_endline "Loading builtin notation ...";
- let ic = open_in (Helm_registry.get "notation.core_file") in
- process_stream ~ignore_exn:true (Stream.of_channel ic);
- close_in ic;
+ CicNotation.load_notation (Helm_registry.get "notation.core_file");
print_endline "done.";
flush stdout;
process_stream ~ignore_exn:false (Stream.of_channel stdin)
projects / helm.git / commitdiff