| ListValue of value list
type value_type =
- | TermType of int option
+ | TermType of int
| StringType
| NumType
| OptType of value_type
let declaration_of_var = function
| Ast.NumVar s -> s, NumType
| Ast.IdentVar s -> s, StringType
- | Ast.TermVar (s,l) -> s, TermType l
+ | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l
| _ -> assert false
let value_of_term = function
| ListValue of value list
type value_type =
- | TermType of int option
+ | TermType of int (* the level of the expected term *)
| StringType
| NumType
| OptType of value_type
and pp_variable = function
| Ast.NumVar s -> "number " ^ s
| Ast.IdentVar s -> "ident " ^ s
- | Ast.TermVar (s,None) -> s
- | Ast.TermVar (s,Some l) -> "term " ^string_of_int l
+ | Ast.TermVar (s,Ast.Self _) -> s
+ | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l
| Ast.Ascription (t, n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
let rec pp_value_type =
function
- | Env.TermType None -> "Term"
- | Env.TermType (Some l) -> "Term "^string_of_int l
+ | Env.TermType l -> "Term "^string_of_int l
| Env.StringType -> "String"
| Env.NumType -> "Number"
| Env.OptType t -> "Maybe " ^ pp_value_type t
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 3
+let magic = 4
type term =
(* CIC AST *)
| Fail
| If of term * term * term (* test, pattern if true, pattern if false *)
+and term_level = Self of int | Level of int
+
and pattern_variable =
(* level 1 and 2 variables *)
| NumVar of string
| IdentVar of string
- | TermVar of string * int option
+ | TermVar of string * term_level
(* level 1 variables *)
| Ascription of term * string
-cicNotationPres.cmi: mpresentation.cmi box.cmi
+termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
+cicNotationPres.cmi: mpresentation.cmi box.cmi
content2pres.cmi: cicNotationPres.cmi
sequent2pres.cmi: cicNotationPres.cmi
renderingAttrs.cmo: renderingAttrs.cmi
content2presMatcher.cmo: content2presMatcher.cmi
content2presMatcher.cmx: content2presMatcher.cmi
termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
- termContentPres.cmi
+ cicNotationParser.cmi termContentPres.cmi
termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
- termContentPres.cmi
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
- cicNotationPres.cmi
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
- cicNotationPres.cmi
+ cicNotationParser.cmx termContentPres.cmi
boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
boxPp.cmi
boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
boxPp.cmi
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi boxPp.cmi box.cmi \
+ cicNotationPres.cmi
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx boxPp.cmx box.cmx \
+ cicNotationPres.cmi
content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
box.mli \
content2presMatcher.mli \
termContentPres.mli \
- cicNotationPres.mli \
boxPp.mli \
+ cicNotationPres.mli \
content2pres.mli \
sequent2pres.mli \
$(NULL)
s
else
match Utf8Macro.tex_of_unicode s with
- | Some s -> s ^ " "
- | None -> " " ^ s ^ " "
+ | s::_ -> s ^ " "
+ | [] -> " " ^ s ^ " "
end else
s
in
let level_of precedence =
if precedence < min_precedence || precedence > max_precedence then
raise (Level_not_found precedence);
- string_of_int precedence ^ "N"
+ string_of_int precedence
let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
let gram_ident s = Gramext.Stoken ("IDENT", s)
let gram_number s = Gramext.Stoken ("NUMBER", s)
let gram_keyword s = Gramext.Stoken ("", s)
let gram_term = function
- | None -> Gramext.Sself
- | Some (precedence) ->
- Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence)
+ | Ast.Self _ -> Gramext.Sself
+ | Ast.Level precedence ->
+ Gramext.Snterml
+ (Grammar.Entry.obj (term: 'a Grammar.Entry.e), level_of precedence)
;;
let gram_of_literal =
and aux_variable =
function
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar (s,level) ->
- [Binding (s, Env.TermType level), gram_term level]
+ | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) ->
+ [Binding (s, Env.TermType level), gram_term lv]
| Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
| Ast.Literal _ as l -> incr symbols; l
| Ast.Layout l -> Ast.Layout (aux_layout l)
| Ast.Magic m -> Ast.Magic (aux_magic m)
- | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | Ast.Variable v -> (aux_variable v)
| t -> assert false
and aux_layout = function
| Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
| _ -> assert false
and aux_variable =
function
- | Ast.NumVar _ as t -> t
- | Ast.TermVar (s,None) when associativity <> Gramext.NonA ->
+ | Ast.NumVar _ as t -> Ast.Variable t
+ | Ast.TermVar (s,Ast.Self _) when associativity <> Gramext.NonA ->
incr variables;
if !variables > 2 then
raise (Parse_error ("Exactly 2 variables must be specified in an "^
"associative notation"));
(match !variables, associativity with
- | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some
- (level-1)) *)
- | 1,Gramext.RightA -> Ast.TermVar (s, None)
- | 2,Gramext.LeftA ->Ast.TermVar (s, None)
- | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1))
+ | 1,Gramext.LeftA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self level))
+ | 1,Gramext.RightA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+ | 2,Gramext.LeftA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+ | 2,Gramext.RightA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Level (level-1)))
| _ -> assert false)
- | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA ->
+ | Ast.TermVar (s,Ast.Level _) when associativity <> Gramext.NonA ->
raise (Parse_error ("Variables can not be declared with a " ^
"precedence in an associative notation"))
- (* avoid camlp5 divergence due to non-Sself recursion at the same level *)
- | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 ->
- raise (Parse_error ("Left recursive rule with precedence not greater " ^
- "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
- | Ast.TermVar _ as t -> incr variables; t
- | Ast.IdentVar _ as t -> t
+ (*avoid camlp5 divergence due to non-Sself recursion at the same level *)
+ | Ast.TermVar (s,Ast.Level l) when l<=level && !variables=0 && !symbols=0->
+ raise(Parse_error("Left recursive rule with precedence not greater " ^
+ "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
+ | Ast.TermVar _ as t -> incr variables; Ast.Variable t
+ | Ast.IdentVar _ as t -> Ast.Variable t
| Ast.Ascription _ -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
in
if associativity <> Gramext.NonA && level = min_precedence then
raise (Parse_error ("You can not specify an associative notation " ^
"at level "^string_of_int min_precedence ^ "; increase it"));
- let cp = CL1P (aux level1_pattern, level) in
+ let cp = aux level1_pattern in
+(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *)
if !variables <> 2 && associativity <> Gramext.NonA then
raise (Parse_error ("Exactly 2 variables must be specified in an "^
"associative notation"));
- cp
+ CL1P (cp,level)
;;
let extend (CL1P (level1_pattern,precedence)) action =
(** {2 Grammar} *)
-let parse_level1_pattern_ref = ref (fun _ -> assert false)
+let parse_level1_pattern_ref = ref (fun _ _ -> assert false)
let parse_level2_ast_ref = ref (fun _ -> assert false)
let parse_level2_meta_ref = ref (fun _ -> assert false)
pt_names body
let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
+let return_term_of_level loc term l =
+ Ast.AttributedTerm (`Loc loc, term l)
(* create empty precedence level for "term" *)
let _ =
| i when i < first -> acc
| i ->
aux
- ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod)
+ ((Some (level_of i), Some Gramext.NonA, dummy_prod)
:: acc)
(i - 1)
in
EXTEND
GLOBAL: level1_pattern;
- level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ];
- l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
+ level1_pattern: [
+ [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ]
+ ];
+ l1_pattern: [
+ [ p = LIST1 l1_simple_pattern ->
+ fun l -> List.map (fun x -> x l) p ]
+ ];
literal: [
[ s = SYMBOL -> `Symbol s
| k = QKEYWORD -> `Keyword k
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
-(* row_sep: [ [ "rowsep"; sep = literal -> sep ] ];
- field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *)
l1_magic_pattern: [
- [ "list0"; p = l1_simple_pattern; sep = OPT sep -> Ast.List0 (p, sep)
- | "list1"; p = l1_simple_pattern; sep = OPT sep -> Ast.List1 (p, sep)
- | "opt"; p = l1_simple_pattern -> Ast.Opt p
+ [ "list0"; p = l1_simple_pattern; sep = OPT sep ->
+ fun l -> Ast.List0 (p l, sep)
+ | "list1"; p = l1_simple_pattern; sep = OPT sep ->
+ fun l -> Ast.List1 (p l, sep)
+ | "opt"; p = l1_simple_pattern -> fun l -> Ast.Opt (p l)
]
];
l1_pattern_variable: [
[ "term"; precedence = NUMBER; id = IDENT ->
- Ast.TermVar (id, Some (int_of_string precedence))
+ Ast.TermVar (id, Ast.Level (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
l1_simple_pattern:
[ "layout" LEFTA
[ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Sub (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Sup (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Below (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Above (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Over (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Atop (p1, p2)))
-(* | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
- return_term loc (Array (p, csep, rsep)) *)
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
| SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Frac (p1, p2)))
- | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Ast.Layout (Ast.Sqrt p))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
+ | SYMBOL "\\sqrt"; p = SELF ->
+ return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
| SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
- return_term loc (Ast.Layout (Ast.Root (arg, index)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.H, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.H, false, false), p l)))
| "vbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.V, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.V, false, false), p l)))
| "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.HV, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.HV, false, false), p l)))
| "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p)))
- | "break" -> return_term loc (Ast.Layout Ast.Break)
-(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
+ | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
| LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.group p)
+ return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None)))
- | m = l1_magic_pattern -> return_term loc (Ast.Magic m)
- | v = l1_pattern_variable -> return_term loc (Ast.Variable v)
- | l = literal -> return_term loc (Ast.Literal l)
+ [ i = IDENT ->
+ return_term_of_level loc
+ (fun l -> Ast.Variable (Ast.TermVar (i,Ast.Self l)))
+ | m = l1_magic_pattern ->
+ return_term_of_level loc (fun l -> Ast.Magic (m l))
+ | v = l1_pattern_variable ->
+ return_term_of_level loc (fun _ -> Ast.Variable v)
+ | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
]
];
END
GLOBAL: level2_meta;
l2_variable: [
[ "term"; precedence = NUMBER; id = IDENT ->
- Ast.TermVar (id,Some (int_of_string precedence))
+ Ast.TermVar (id,Ast.Level (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
| "fresh"; id = IDENT -> Ast.FreshVar id
- | "anonymous" -> Ast.TermVar ("_",None)
- | id = IDENT -> Ast.TermVar (id,None)
+ | "anonymous" -> Ast.TermVar ("_",Ast.Self 0) (* is the level relevant?*)
+ | id = IDENT -> Ast.TermVar (id,Ast.Self 0)
]
];
l2_magic: [
| vars = protected_binder_vars -> vars
]
];
- term: LEVEL "10N"
+ term: LEVEL "10"
[
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
- term: LEVEL "20N"
+ term: LEVEL "20"
[
- [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" ->
+ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
return_term loc (fold_cluster b vars typ body)
| SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"->
+ (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"->
return_term loc (fold_exists vars typ body)
]
];
- term: LEVEL "70N"
+ term: LEVEL "70"
[
- [ p1 = term; p2 = term LEVEL "71N" ->
+ [ p1 = term; p2 = term LEVEL "71" ->
let rec aux = function
| Ast.Appl (hd :: tl)
| Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
return_term loc (Ast.Appl (aux p1 @ [p2]))
]
];
- term: LEVEL "90N"
+ term: LEVEL "90"
[
[ id = IDENT -> return_term loc (Ast.Ident (id, None))
| id = IDENT; s = explicit_subst ->
| Stdpp.Exc_located (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
-let parse_level1_pattern lexbuf =
+let parse_level1_pattern precedence lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+ (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf) precedence)
let parse_level2_ast lexbuf =
exc_located_wrapper
(** {2 Parsing functions} *)
- (** concrete syntax pattern: notation level 1 *)
-val parse_level1_pattern: Ulexing.lexbuf -> CicNotationPt.term
+ (** concrete syntax pattern: notation level 1, the
+ * integer is the precedence *)
+val parse_level1_pattern: int -> Ulexing.lexbuf -> CicNotationPt.term
(** AST pattern: notation level 2 *)
val parse_level2_ast: Ulexing.lexbuf -> CicNotationPt.term
aux_mpres t
let add_parens child_prec curr_prec t =
-(* eprintf
- ("add_parens: " ^^
- "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!")
- child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
- curr_prec; *)
- if is_atomic t then t
-(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *)
- else if child_prec >= 0 && child_prec <= curr_prec then
- begin (* parens should be added *)
-(* prerr_endline "adding parens!"; *)
+ if is_atomic t then
+ ((*prerr_endline ("NOT adding parens around ATOMIC: "^
+ BoxPp.render_to_string (function x::_->x|_->assert false)
+ ~map_unicode_to_tex:false 80 t);*)t)
+ else if child_prec >= 0 && child_prec < curr_prec then
+ begin
+ (*prerr_endline ("adding parens around: "^
+ BoxPp.render_to_string (function x::_->x|_->assert false)
+ ~map_unicode_to_tex:false 80 t);*)
match t with
| Mpresentation.Mobject (_, box) ->
mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
| mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
end else
- t
+ ((*prerr_endline ("NOT adding parens around: "^
+ BoxPp.render_to_string (function x::_->x|_->assert false)
+ ~map_unicode_to_tex:false 80 t);*)t)
let render ids_to_uris ?(prec=(-1)) =
let module A = Ast in
let expected_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
-(* let reinit = ref false in *)
let rec aux_attribute =
function
| A.AttributedTerm (attr, t) ->
(match !inferred_level with
| None -> aux !new_xmlattrs mathonly new_xref prec t
| Some child_prec ->
- let t' =
- aux !new_xmlattrs mathonly new_xref child_prec t in
+ let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
+ (*prerr_endline
+ ("inferred: "^string_of_int child_prec^
+ " exp: "^string_of_int prec ^
+ " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
+ (function x::_->x|_->assert false) 80 t');*)
if !reset
- then t'
+ then ((*prerr_endline "reset";*)t')
else add_parens child_prec prec t')
in
+(* prerr_endline (CicNotationPp.pp_term t); *)
aux_attribute t
and aux_literal xmlattrs xref prec l =
let attrs = make_href xmlattrs xref in
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
- Ast.Variable (Ast.TermVar (name,None))
+ Ast.Variable (Ast.TermVar (name,Ast.Level 0))
in
let rec aux = function
| Ast.AttributedTerm (_, t) -> assert false
List.map2
(fun p t ->
match p, t with
- | Ast.Variable (Ast.TermVar (name,l)), _ ->
+ | Ast.Variable (Ast.TermVar (name,(Ast.Self l|Ast.Level l))), _ ->
name, (Env.TermType l, Env.TermValue t)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
let value = CicNotationEnv.term_of_value value in
let value =
match expected_ty with
- | Env.TermType (Some l) ->
- Ast.AttributedTerm (`Level l,value)
+ | Env.TermType l -> Ast.AttributedTerm (`Level l,value)
| _ -> value
in
[ value ]
aux [] env
let instantiate_level2 env term =
+(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
try
let rec aux env term =
(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
match term with
- | Ast.AttributedTerm (_, term) -> aux env term
+ | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
| Ast.Binder (binder, var, body) ->
Ast.Binder (binder, aux_capture_var env var, aux env body)
and aux_variable env = function
| Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
| Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
- | Ast.TermVar (name,None) ->
- Env.lookup_term env name
- | Ast.TermVar (name,Some l) ->
+ | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) ->
Ast.AttributedTerm (`Level l,Env.lookup_term env name)
| Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
| Ast.Ascription (term, name) -> assert false
| Env.ListValue (_ :: _) ->
instantiate_fold_left
(let acc_binding =
- acc_name, (Env.TermType None, Env.TermValue acc)
+ acc_name, (Env.TermType 0, Env.TermValue acc)
in
aux (acc_binding :: head_names names env') rec_pattern)
(tail_names names env')
| Env.ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
let acc_binding =
- acc_name, (Env.TermType None, Env.TermValue acc)
+ acc_name, (Env.TermType 0, Env.TermValue acc)
in
aux (acc_binding :: head_names names env') rec_pattern
| Env.ListValue [] -> aux env base_pattern
grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi
+print_grammar.cmo: print_grammar.cmi
+print_grammar.cmx: print_grammar.cmi
grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi
+print_grammar.cmo: print_grammar.cmi
+print_grammar.cmx: print_grammar.cmi
grafiteDisambiguator.mli \
grafiteDisambiguate.mli \
grafiteWalker.mli \
+ print_grammar.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
-all: test_parser print_grammar test_dep
+all: test_parser test_dep
clean: clean_tests
# <cross> cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
- tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
+ tactic_term: [ [ t = term LEVEL "90" -> t ] ];
new_name: [
[ id = IDENT -> Some id
| SYMBOL "_" -> None ]
in
let p1 =
add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern
+ (CicNotationParser.parse_level1_pattern prec
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
open Gramext
-let tex_of_unicode s =
-(*CSC: ??????? What's the meaning of this function?
- let contractions = ("\\Longrightarrow","=>") :: [] in
- if String.length s <= 1 then s
- else (* probably an extended unicode symbol *)
- let s = Utf8Macro.tex_of_unicode s in
- try List.assoc s contractions with Not_found -> s
-*) match Utf8Macro.tex_of_unicode s with
- Some s -> s
- | None -> s
+let rec flatten_tree = function
+ | DeadEnd -> []
+ | LocAct _ -> [[]]
+ | Node {node = n; brother = b; son = s} ->
+ List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
+
+let tex_of_unicode s = s
+
+let rec clean_dummy_desc = function
+ | Dlevels l -> Dlevels (clean_levels l)
+ | x -> x
+
+and clean_levels = function
+ | [] -> []
+ | l :: tl -> clean_level l @ clean_levels tl
+
+and clean_level = function
+ | x ->
+ let pref = clean_tree x.lprefix in
+ let suff = clean_tree x.lsuffix in
+ match pref,suff with
+ | DeadEnd, DeadEnd -> []
+ | _ -> [{x with lprefix = pref; lsuffix = suff}]
+
+and clean_tree = function
+ | Node n -> clean_node n
+ | x -> x
+
+and clean_node = function
+ | {node=node;son=son;brother=brother} ->
+ let bn = is_symbol_dummy node in
+ let bs = is_tree_dummy son in
+ let bb = is_tree_dummy brother in
+ let son = if bs then DeadEnd else son in
+ let brother = if bb then DeadEnd else brother in
+ if bb && bs && bn then
+ DeadEnd
+ else
+ if bn then
+ Node {node=Sself;son=son;brother=brother}
+ else
+ Node {node=node;son=son;brother=brother}
+
+and is_level_dummy = function
+ | {lsuffix=lsuffix;lprefix=lprefix} ->
+ is_tree_dummy lsuffix && is_tree_dummy lprefix
+
+and is_desc_dummy = function
+ | Dlevels l -> List.for_all is_level_dummy l
+ | Dparser _ -> true
+
+and is_entry_dummy = function
+ | {edesc=edesc} -> is_desc_dummy edesc
+
+and is_symbol_dummy = function
+ | Stoken ("DUMMY", _) -> true
+ | Stoken _ -> false
+ | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
+ | Snterm e | Snterml (e, _) -> is_entry_dummy e
+ | Slist1 x | Slist0 x -> is_symbol_dummy x
+ | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+ | Sopt x -> is_symbol_dummy x
+ | Sself | Snext -> false
+ | Stree t -> is_tree_dummy t
+ | _ -> assert false
+
+and is_tree_dummy = function
+ | Node {node=node} -> is_symbol_dummy node
+ | _ -> true
let needs_brackets t =
let rec count_brothers = function
count_brothers t > 1
let visit_description desc fmt self =
- let skip s = List.mem s [ ] in
+ let skip s = true in
let inline s = List.mem s [ "int" ] in
- let rec visit_entry e todo is_son nesting =
+ let rec visit_entry e todo is_son =
let { ename = ename; edesc = desc } = e in
if inline ename then
- visit_desc desc todo is_son nesting
+ visit_desc desc todo is_son
else
begin
Format.fprintf fmt "%s " ename;
todo @ [e]
end
- and visit_desc d todo is_son nesting =
+ and visit_desc d todo is_son =
match d with
- | Dlevels [] -> todo
- | Dlevels [lev] -> visit_level lev todo is_son nesting
- | Dlevels (lev::levels) ->
- let todo = visit_level lev todo is_son nesting in
+ | Dlevels l ->
List.fold_left
- (fun acc l ->
- Format.fprintf fmt "@ | ";
- visit_level l acc is_son nesting)
- todo levels;
- | _ -> todo
+ (fun acc l ->
+ Format.fprintf fmt "@ ";
+ visit_level l acc is_son )
+ todo l;
+ | Dparser _ -> todo
- and visit_level l todo is_son nesting =
- let { lsuffix = suff ; lprefix = pref } = l in
- let todo = visit_tree suff todo is_son nesting in
- visit_tree pref todo is_son nesting
+ and visit_level l todo is_son =
+ let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
+ visit_tree name
+ (List.map
+ (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
+ todo is_son
- and visit_tree t todo is_son nesting =
- match t with
- | Node node -> visit_node node todo is_son nesting
- | _ -> todo
-
- and visit_node n todo is_son nesting =
- let is_tree_printable t =
- match t with
- | Node _ -> true
- | _ -> false
- in
- let { node = symbol; son = son ; brother = brother } = n in
- let todo = visit_symbol symbol todo is_son nesting in
- let todo =
- if is_tree_printable son then
- begin
- let need_b = needs_brackets son in
- if not is_son then
- Format.fprintf fmt "@[<hov2>";
- if need_b then
- Format.fprintf fmt "( ";
- let todo = visit_tree son todo true nesting in
- if need_b then
- Format.fprintf fmt ")";
- if not is_son then
- Format.fprintf fmt "@]";
- todo
- end
- else
- todo
+ and visit_tree name t todo is_son =
+ if List.for_all (List.for_all is_symbol_dummy) t then todo else (
+ Format.fprintf fmt "@[<v>";
+ (match name with
+ |Some name -> Format.fprintf fmt "Precedence %s:@ " name
+ | None -> ());
+ Format.fprintf fmt "@[<v>";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ if List.for_all is_symbol_dummy x then todo else (
+ Format.fprintf fmt "@[<h> | ";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ let todo = visit_symbol x acc true in
+ Format.fprintf fmt "@ ";
+ todo)
+ acc x
+ in
+ Format.fprintf fmt "@]@ ";
+ todo))
+ todo t
in
- if is_tree_printable brother then
- begin
- Format.fprintf fmt "@ | ";
- visit_tree brother todo is_son nesting
- end
- else
- todo
+ Format.fprintf fmt "@]";
+ Format.fprintf fmt "@]";
+ todo)
- and visit_symbol s todo is_son nesting =
+ and visit_symbol s todo is_son =
match s with
| Smeta (name, sl, _) ->
Format.fprintf fmt "%s " name;
List.fold_left (
fun acc s ->
- let todo = visit_symbol s acc is_son nesting in
+ let todo = visit_symbol s acc is_son in
if is_son then
Format.fprintf fmt "@ ";
todo)
todo sl
- | Snterm entry -> visit_entry entry todo is_son nesting
- | Snterml (entry,_) -> visit_entry entry todo is_son nesting
+ | Snterm entry -> visit_entry entry todo is_son
+ | Snterml (entry,_) -> visit_entry entry todo is_son
| Slist0 symbol ->
Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting+1) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
| Slist0sep (symbol,sep) ->
Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol sep todo is_son (nesting + 2) in
+ let todo = visit_symbol sep todo is_son in
Format.fprintf fmt " ";
- let todo = visit_symbol symbol todo is_son (nesting + 2) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @]] @ ";
todo
| Slist1 symbol ->
Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]}+ @ ";
todo
| Slist1sep (symbol,sep) ->
- let todo = visit_symbol symbol todo is_son nesting in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol sep todo is_son (nesting + 1) in
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ let todo = visit_symbol sep todo is_son in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
| Sopt symbol ->
Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]] @ ";
todo
| Sself -> Format.fprintf fmt "%s " self; todo
| Stoken pattern ->
let constructor, keyword = pattern in
if keyword = "" then
- Format.fprintf fmt "`%s' " constructor
+ (if constructor <> "DUMMY" then
+ Format.fprintf fmt "`%s' " constructor)
else
- Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
+ Format.fprintf fmt "%s " (tex_of_unicode keyword);
todo
| Stree tree ->
- if needs_brackets tree then
- begin
- Format.fprintf fmt "@[<hov2>( ";
- let todo = visit_tree tree todo is_son (nesting + 1) in
- Format.fprintf fmt ")@] @ ";
- todo
- end
- else
- visit_tree tree todo is_son (nesting + 1)
+ visit_tree None (flatten_tree tree) todo is_son
+ | _ -> assert false
in
- visit_desc desc [] false 0
+ visit_desc desc [] false
;;
-let rec clean_dummy_desc = function
- | Dlevels l -> Dlevels (clean_levels l)
- | x -> x
-and clean_levels = function
- | [] -> []
- | l :: tl -> clean_level l @ clean_levels tl
-
-and clean_level = function
- | x ->
- let pref = clean_tree x.lprefix in
- let suff = clean_tree x.lsuffix in
- match pref,suff with
- | DeadEnd, DeadEnd -> []
- | _ -> [{x with lprefix = pref; lsuffix = suff}]
-
-and clean_tree = function
- | Node n -> clean_node n
- | x -> x
-
-and clean_node = function
- | {node=node;son=son;brother=brother} ->
- let bn = is_symbol_dummy node in
- let bs = is_tree_dummy son in
- let bb = is_tree_dummy brother in
- let son = if bs then DeadEnd else son in
- let brother = if bb then DeadEnd else brother in
- if bb && bs && bn then
- DeadEnd
- else
- if bn then
- Node {node=Sself;son=son;brother=brother}
- else
- Node {node=node;son=son;brother=brother}
-
-and is_level_dummy = function
- | {lsuffix=lsuffix;lprefix=lprefix} ->
- is_tree_dummy lsuffix && is_tree_dummy lprefix
-
-and is_desc_dummy = function
- | Dlevels l -> List.for_all is_level_dummy l
- | Dparser _ -> true
-
-and is_entry_dummy = function
- | {edesc=edesc} -> is_desc_dummy edesc
-
-and is_symbol_dummy = function
- | Stoken ("DUMMY", _) -> true
- | Stoken _ -> false
- | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
- | Snterm e | Snterml (e, _) -> is_entry_dummy e
- | Slist1 x | Slist0 x -> is_symbol_dummy x
- | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
- | Sopt x -> is_symbol_dummy x
- | Sself | Snext -> false
- | Stree t -> is_tree_dummy t
-
-and is_tree_dummy = function
- | Node {node=node} -> is_symbol_dummy node
- | _ -> true
-;;
-
-
-let rec visit_entries todo pped =
- let fmt = Format.std_formatter in
+let rec visit_entries fmt todo pped =
match todo with
| [] -> ()
| hd :: tl ->
if not (List.memq hd pped) then
begin
let { ename = ename; edesc = desc } = hd in
- Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
+ Format.fprintf fmt "@[<hv 2>%s ::= " ename;
let desc = clean_dummy_desc desc in
let todo = visit_description desc fmt ename @ todo in
- Format.fprintf fmt "@]";
- Format.pp_print_newline fmt ();
- Format.pp_print_newline fmt ();
+ Format.fprintf fmt "@]\n\n";
todo
end
else
pped
in
let todo,pped = clean_todo todo in
- visit_entries todo pped
+ visit_entries fmt todo pped
;;
-let _ =
- let g_entry = Grammar.Entry.obj GrafiteParser.statement in
- visit_entries [g_entry] []
+let ebnf_of_term () =
+ let g_entry = Grammar.Entry.obj CicNotationParser.term in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+ visit_entries fmt [g_entry] [];
+ Format.fprintf fmt "@?";
+ let s = Buffer.contents buff in
+ s
+;;
let tex_of_unicode s =
(*WARNING: the space below is a nbsp (0x00A0), not a normal space *)
- if s = " " then Some ""
+ if s = " " then [""]
else
try
- Some ("\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s)
- with Not_found -> None
+ let alt = Hashtbl.find_all Utf8MacroTable.utf82macro s in
+ List.sort
+ (fun x y -> Pervasives.compare (String.length x) (String.length y))
+ alt
+ with Not_found -> []
+let pp_table () =
+ let rec list_uniq ?(eq=(=)) = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when eq h1 h2 -> list_uniq ~eq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq ~eq tl
+ in
+ let l = ref [] in
+ Hashtbl.iter (fun k _ -> l := k :: !l) Utf8MacroTable.utf82macro;
+ l := list_uniq (List.sort compare !l);
+ List.map
+ (fun k ->
+ let vs = Hashtbl.find_all Utf8MacroTable.utf82macro k in
+ (k, List.map (fun x -> "\\"^x) vs))
+ !l
+;;
val unicode_of_tex: string -> string
(** ... the other way round *)
-val tex_of_unicode: string -> string option
+val tex_of_unicode: string -> string list
+
+val pp_table: unit -> (string * (string list)) list
List.iter
(fun (macro, utf8) ->
Hashtbl.replace macro2utf8 macro utf8;
- Hashtbl.replace utf82macro utf8 macro)
+ Hashtbl.add utf82macro utf8 macro)
data;;
</child>
</widget>
</child>
+ <child>
+ <widget class="GtkImageMenuItem" id="showTermGrammarMenuItem">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Displays the term grammar</property>
+ <property name="label" translatable="yes">Show term's grammar</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
</child>
</widget>
</child>
+ <child>
+ <widget class="GtkImageMenuItem" id="showUnicodeTable">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Displays the Tex/Unicode table</property>
+ <property name="label" translatable="yes">Show Tex/Unicode table</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
<child>
<widget class="GtkImageMenuItem" id="aboutMenuItem">
<property name="visible">True</property>
c#load (`About `Coercions));
connect_menu_item main#showAutoGuiMenuItem
(fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
+ connect_menu_item main#showTermGrammarMenuItem
+ (fun _ ->
+ let w = GWindow.window ~resizable:true
+ ~position:`CENTER_ON_PARENT
+ ~title:"Terms grammar" ~width:640 ~height:400 () in
+ w#set_transient_for (main#toplevel#as_window);
+ let s = GBin.scrolled_window () in
+ (w :> GContainer.container)#add (s :> GObj.widget);
+ let t = GText.view () in
+ t#buffer#insert (Print_grammar.ebnf_of_term ());
+ s#add (t:>GObj.widget);
+ w#show ());
+ connect_menu_item main#showUnicodeTable
+ (fun _ ->
+ let w = GWindow.window ~resizable:true
+ ~position:`CENTER_ON_PARENT
+ ~title:"Tex/UTF8 table" ~width:640 ~height:400 () in
+ w#set_transient_for (main#toplevel#as_window);
+ let s = GBin.scrolled_window () in
+ (w :> GContainer.container)#add (s :> GObj.widget);
+ let t = GTree.view () in
+ let m = new MatitaGtkMisc.multiStringListModel ~cols:2 t in
+ List.iter (fun (k,vs) ->
+ m#easy_mappend [k;String.concat " " vs])
+ (Utf8Macro.pp_table ());
+ s#add (t:>GObj.widget);
+ w#show ());
(* script monospace font stuff *)
self#updateFontSize ();
(* debug menu *)
projects / helm.git / commitdiff