| ListValue of value list
type value_type =
- | TermType
+ | TermType of (int * Gramext.g_assoc) option
| StringType
| NumType
| OptType of value_type
let declaration_of_var = function
| Ast.NumVar s -> s, NumType
| Ast.IdentVar s -> s, StringType
- | Ast.TermVar s -> s, TermType
+ | Ast.TermVar (s,l) -> s, TermType l
| _ -> assert false
let value_of_term = function
let rec well_typed ty value =
match ty, value with
- | TermType, TermValue _
+ | TermType _, TermValue _
| StringType, StringValue _
| OptType _, OptValue None
| NumType, NumValue _ -> true
| ListValue of value list
type value_type =
- | TermType
+ | TermType of (int * Gramext.g_assoc) option
| StringType
| NumType
| OptType of value_type
let pp_assoc =
function
- | Gramext.NonA -> "NonA"
- | Gramext.LeftA -> "LeftA"
- | Gramext.RightA -> "RightA"
+ | Gramext.NonA -> "N"
+ | Gramext.LeftA -> "L"
+ | Gramext.RightA -> "R"
let pp_pos =
function
and pp_variable = function
| Ast.NumVar s -> "number " ^ s
| Ast.IdentVar s -> "ident " ^ s
- | Ast.TermVar s -> "term " ^ s
+ | Ast.TermVar (s,None) -> s
+ | Ast.TermVar (s,Some (l,a)) -> "term " ^string_of_int l ^ " " ^ pp_assoc a ^ " " ^ s
| Ast.Ascription (t, n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
let rec pp_value_type =
function
- | Env.TermType -> "Term"
+ | Env.TermType None -> "Term"
+ | Env.TermType (Some (l,a)) -> "Term "^string_of_int l ^ " " ^ pp_assoc a
| 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 = 2
+let magic = 3
type term =
(* CIC AST *)
(* level 1 and 2 variables *)
| NumVar of string
| IdentVar of string
- | TermVar of string
+ | TermVar of string * (int * Gramext.g_assoc) option
(* level 1 variables *)
| Ascription of term * string
let aux = function
| Ast.NumVar s
| Ast.IdentVar s
- | Ast.TermVar s -> s
+ | Ast.TermVar (s,_) -> s
| _ -> assert false
in
List.map aux (variables_of_term t)
and aux_variable = function
| Ast.NumVar name -> add_name name
| Ast.IdentVar name -> add_name name
- | Ast.TermVar name -> add_name name
+ | Ast.TermVar (name,_) -> add_name name
| Ast.FreshVar _ -> ()
| Ast.Ascription _ -> assert false
and aux_magic = function
(** {2 Grammar extension} *)
+let level_of precedence associativity =
+ if precedence < min_precedence || precedence > max_precedence then
+ raise (Level_not_found precedence);
+ let assoc_string =
+ match associativity with
+ | Gramext.NonA -> "N"
+ | Gramext.LeftA -> "L"
+ | Gramext.RightA -> "R"
+ in
+ string_of_int precedence ^ assoc_string
+
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 = Gramext.Sself
+let gram_term = function
+ | None -> Gramext.Sself
+ | Some (precedence, associativity) ->
+ Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence associativity)
+;;
let gram_of_literal =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
(* LUCA: DEFCON 3 BEGIN *)
- | Binding (name, Env.TermType) :: tl ->
+ | Binding (name, Env.TermType l) :: tl ->
Gramext.action
(fun (v:Ast.term) ->
- aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+ aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
| Binding (name, Env.StringType) :: tl ->
Gramext.action
(fun (v:string) ->
and aux_variable =
function
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+ | Ast.TermVar (s,level) ->
+ [Binding (s, Env.TermType level), gram_term level]
| Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
in
aux pattern
-let level_of precedence associativity =
- if precedence < min_precedence || precedence > max_precedence then
- raise (Level_not_found 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 = Grammar.token Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
| "opt"; p = l1_simple_pattern -> Ast.Opt p
]
];
+ l1_associativity : [
+ [ IDENT "L" -> Gramext.LeftA
+ | IDENT "N" -> Gramext.NonA
+ | IDENT "R" -> Gramext.RightA
+ ]
+ ];
l1_pattern_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; assoc = l1_associativity ; id = IDENT ->
+ Ast.TermVar (id, Some (int_of_string precedence,assoc))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+ [ 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)
(* {{{ Grammar for ast magics, notation level 2 *)
EXTEND
GLOBAL: level2_meta;
+ l2_associativity : [
+ [ IDENT "L" -> Gramext.LeftA
+ | IDENT "N" -> Gramext.NonA
+ | IDENT "R" -> Gramext.RightA
+ ]
+ ];
l2_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; assoc = l2_associativity; id = IDENT ->
+ Ast.TermVar (id,Some (int_of_string precedence, assoc))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
| "fresh"; id = IDENT -> Ast.FreshVar id
- | "anonymous" -> Ast.TermVar "_"
- | id = IDENT -> Ast.TermVar id
+ | "anonymous" -> Ast.TermVar ("_",None)
+ | id = IDENT -> Ast.TermVar (id,None)
]
];
l2_magic: [
let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
+ | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
| _ -> failwith "Invalid bound name."
]
];
match meta with
| Ast.Variable (Ast.FreshVar _)
| Ast.Variable (Ast.IdentVar _) -> meta
- | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
| _ -> failwith "Invalid index name."
]
];
child_assoc = Gramext.RightA &&
child_pos <> `Right))
then begin (* parens should be added *)
-(* prerr_endline "adding parens!"; *)
+(* prerr_endline "adding parens!"; *)
match t with
| Mpresentation.Mobject (_, box) ->
mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
assert false
and aux_attributes xmlattrs mathonly xref pos prec t =
let reset = ref false in
- let new_level = ref None in
+ let inferred_level = ref None in
+ let expected_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
let new_pos = ref pos in
| `Raw _ -> ()
| `Level (-1, _) -> reset := true
| `Level (child_prec, child_assoc) ->
- new_level := Some (child_prec, child_assoc)
+ assert (!expected_level = None);
+ expected_level := !inferred_level;
+ inferred_level := Some (child_prec, child_assoc)
| `IdRef xref -> new_xref := xref :: !new_xref
| `ChildPos pos -> new_pos := pos
| `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
aux_attribute t
| t ->
- (match !new_level with
- | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
+ let prec =
+ match !expected_level with
+ | None -> prec
+ | Some (prec, _) -> prec
+ in
+ (match !inferred_level with
+ | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
| Some (child_prec, child_assoc) ->
let t' =
aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
- Ast.Variable (Ast.TermVar name)
+ Ast.Variable (Ast.TermVar (name,None))
in
let rec aux = function
| Ast.AttributedTerm (_, t) -> assert false
List.map2
(fun p t ->
match p, t with
- Ast.Variable (Ast.TermVar name), _ ->
- name, (Env.TermType, Env.TermValue t)
+ | Ast.Variable (Ast.TermVar (name,l)), _ ->
+ name, (Env.TermType l, Env.TermValue t)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
(* following assertion should be a conditional that makes this
* instantiation fail *)
assert (CicNotationEnv.well_typed expected_ty value);
- [ add_pos_info pos (CicNotationEnv.term_of_value value) ]
+ let value = CicNotationEnv.term_of_value value in
+ let value =
+ match expected_ty with
+ | Env.TermType (Some l) ->
+ Ast.AttributedTerm (`Level l,value)
+ | _ -> value
+ in
+ [ add_pos_info pos value ]
| Ast.Magic m -> subst_magic pos env m
| Ast.Literal l as t ->
let t = add_idrefs idrefs t in
new_name
in
let rec aux env term =
-(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
+(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
match term with
| Ast.AttributedTerm (_, term) -> aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
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 -> Env.lookup_term env name
+ | Ast.TermVar (name,None) ->
+ Env.lookup_term env name
+ | Ast.TermVar (name,Some 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
and aux_magic env = function
| Env.ListValue (_ :: _) ->
instantiate_fold_left
(let acc_binding =
- acc_name, (Env.TermType, Env.TermValue acc)
+ acc_name, (Env.TermType None, 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, Env.TermValue acc)
+ acc_name, (Env.TermType None, Env.TermValue acc)
in
aux (acc_binding :: head_names names env') rec_pattern
| Env.ListValue [] -> aux env base_pattern
projects / helm.git / commitdiff