-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* http://helm.cs.unibo.it/
*)
-open CicNotationPt
+module Ast = CicNotationPt
type value =
- | TermValue of term
+ | TermValue of Ast.term
| StringValue of string
| NumValue of string
| OptValue of value option
let list_declaration (n, ty) = (n, ListType ty)
let declaration_of_var = function
- | NumVar s -> s, NumType
- | IdentVar s -> s, StringType
- | TermVar s -> s, TermType
+ | Ast.NumVar s -> s, NumType
+ | Ast.IdentVar s -> s, StringType
+ | Ast.TermVar s -> s, TermType
| _ -> assert false
let value_of_term = function
- | Num (s, _) -> NumValue s
- | Ident (s, None) -> StringValue s
+ | Ast.Num (s, _) -> NumValue s
+ | Ast.Ident (s, None) -> StringValue s
| t -> TermValue t
let term_of_value = function
- | NumValue s -> Num (s, 0)
- | StringValue s -> Ident (s, None)
+ | NumValue s -> Ast.Num (s, 0)
+ | StringValue s -> Ast.Ident (s, None)
| TermValue t -> t
| _ -> assert false (* TO BE UNDERSTOOD *)
open Printf
-open CicNotationEnv
-open CicNotationPt
+module Ast = CicNotationPt
+module Env = CicNotationEnv
(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
* be removes as soon as we believe implementation are equivalent *)
let rec aux acc = function
| (name, (ty, v)) :: tl when List.mem name names ->
(match ty, v with
- | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType ty, Env.OptValue (Some v) ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* some pattern may contain only meta names, thus we trash all others *)
let rec aux acc = function
| (name, (ty, v)) :: tl when List.mem name names ->
(match ty, v with
- | ListType ty, ListValue (v :: _) -> aux ((name, (ty, v)) :: acc) tl
+ | Env.ListType ty, Env.ListValue (v :: _) ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
let rec aux acc = function
| (name, (ty, v)) :: tl when List.mem name names ->
(match ty, v with
- | ListType ty, ListValue (_ :: vtl) ->
- aux ((name, (ListType ty, ListValue vtl)) :: acc) tl
+ | Env.ListType ty, Env.ListValue (_ :: vtl) ->
+ aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
| _ -> assert false)
| binding :: tl -> aux (binding :: acc) tl
| [] -> acc
in
let rec aux env term =
match term with
- | AttributedTerm (_, term) -> aux env term
- | Appl terms -> Appl (List.map (aux env) terms)
- | Binder (binder, var, body) ->
- Binder (binder, aux_capture_var env var, aux env body)
- | Case (term, indty, outty_opt, patterns) ->
- Case (aux env term, indty, aux_opt env outty_opt,
+ | Ast.AttributedTerm (_, term) -> 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)
+ | Ast.Case (term, indty, outty_opt, patterns) ->
+ Ast.Case (aux env term, indty, aux_opt env outty_opt,
List.map (aux_branch env) patterns)
- | LetIn (var, t1, t2) ->
- LetIn (aux_capture_var env var, aux env t1, aux env t2)
- | LetRec (kind, definitions, body) ->
- LetRec (kind, List.map (aux_definition env) definitions, aux env body)
- | Uri (name, None) -> Uri (name, None)
- | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs))
- | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs))
- | Meta (index, substs) -> Meta (index, aux_meta_substs env substs)
+ | Ast.LetIn (var, t1, t2) ->
+ Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
+ | Ast.LetRec (kind, definitions, body) ->
+ Ast.LetRec (kind, List.map (aux_definition env) definitions,
+ aux env body)
+ | Ast.Uri (name, None) -> Ast.Uri (name, None)
+ | Ast.Uri (name, Some substs) ->
+ Ast.Uri (name, Some (aux_substs env substs))
+ | Ast.Ident (name, Some substs) ->
+ Ast.Ident (name, Some (aux_substs env substs))
+ | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Implicit
- | Ident _
- | Num _
- | Sort _
- | Symbol _
- | UserInput -> term
+ | Ast.Implicit
+ | Ast.Ident _
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.UserInput -> term
- | Magic magic -> aux_magic env magic
- | Variable var -> aux_variable env var
+ | Ast.Magic magic -> aux_magic env magic
+ | Ast.Variable var -> aux_variable env var
| _ -> assert false
and aux_opt env = function
List.map (fun (name, term) -> (name, aux env term)) substs
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
and aux_variable env = function
- | NumVar name -> Num (lookup_num env name, 0)
- | IdentVar name -> Ident (lookup_string env name, None)
- | TermVar name -> lookup_term env name
- | FreshVar name -> Ident (lookup_fresh_name name, None)
- | Ascription (term, name) -> assert false
+ | 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.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+ | Ast.Ascription (term, name) -> assert false
and aux_magic env = function
- | Default (some_pattern, none_pattern) ->
+ | Ast.Default (some_pattern, none_pattern) ->
(match CicNotationUtil.names_of_term some_pattern with
| [] -> assert false (* some pattern must contain at least 1 name *)
| (name :: _) as names ->
- (match lookup_value env name with
- | OptValue (Some _) ->
+ (match Env.lookup_value env name with
+ | Env.OptValue (Some _) ->
(* assumption: if "name" above is bound to Some _, then all
* names returned by "meta_names_of" are bound to Some _ as well
*)
aux (unopt_names names env) some_pattern
- | OptValue None -> aux env none_pattern
+ | Env.OptValue None -> aux env none_pattern
| _ -> assert false))
- | Fold (`Left, base_pattern, names, rec_pattern) ->
+ | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
List.filter ((<>) acc_name)
| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_left acc env' =
- match lookup_value env' name with
- | ListValue (_ :: _) ->
+ match Env.lookup_value env' name with
+ | Env.ListValue (_ :: _) ->
instantiate_fold_left
- (let acc_binding = acc_name, (TermType, TermValue acc) in
+ (let acc_binding =
+ acc_name, (Env.TermType, Env.TermValue acc)
+ in
aux (acc_binding :: head_names names env') rec_pattern)
(tail_names names env')
- | ListValue [] -> acc
+ | Env.ListValue [] -> acc
| _ -> assert false
in
instantiate_fold_left (aux env base_pattern) env)
- | Fold (`Right, base_pattern, names, rec_pattern) ->
+ | Ast.Fold (`Right, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
List.filter ((<>) acc_name)
| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_right env' =
- match lookup_value env' name with
- | ListValue (_ :: _) ->
+ match Env.lookup_value env' name with
+ | Env.ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
- let acc_binding = acc_name, (TermType, TermValue acc) in
+ let acc_binding =
+ acc_name, (Env.TermType, Env.TermValue acc)
+ in
aux (acc_binding :: head_names names env') rec_pattern
- | ListValue [] -> aux env base_pattern
+ | Env.ListValue [] -> aux env base_pattern
| _ -> assert false
in
instantiate_fold_right env)
- | If (_, p_true, p_false) as t ->
- aux env (CicNotationUtil.find_branch (Magic t))
- | Fail -> assert false
+ | Ast.If (_, p_true, p_false) as t ->
+ aux env (CicNotationUtil.find_branch (Ast.Magic t))
+ | Ast.Fail -> assert false
| _ -> assert false
in
aux env term
assert false
in
let rec aux = function
- | UriPattern uri -> CicUtil.term_of_uri uri
- | ImplicitPattern -> Cic.Implicit None
- | VarPattern name -> lookup name
- | ApplPattern terms -> Cic.Appl (List.map aux terms)
+ | Ast.UriPattern uri -> CicUtil.term_of_uri uri
+ | Ast.ImplicitPattern -> Cic.Implicit None
+ | Ast.VarPattern name -> lookup name
+ | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
in
aux appl_pattern
open Printf
-module Pp = CicNotationPp
-module Pt = CicNotationPt
+module Ast = CicNotationPt
module Env = CicNotationEnv
+module Pp = CicNotationPp
module Util = CicNotationUtil
type pattern_id = int
struct
module Pattern21 =
struct
- type pattern_t = Pt.term
- type term_t = Pt.term
+ type pattern_t = Ast.term
+ type term_t = Ast.term
let rec classify = function
- | Pt.AttributedTerm (_, t) -> classify t
- | Pt.Variable _ -> Variable
- | Pt.Magic _
- | Pt.Layout _
- | Pt.Literal _ as t -> assert false
+ | Ast.AttributedTerm (_, t) -> classify t
+ | Ast.Variable _ -> Variable
+ | Ast.Magic _
+ | Ast.Layout _
+ | Ast.Literal _ as t -> assert false
| _ -> Constructor
let tag_of_pattern = CicNotationTag.get_tag
let tag_of_term = CicNotationTag.get_tag
let add_magic m =
let name = Util.fresh_name () in
magic_map := (name, m) :: !magic_map;
- Pt.Variable (Pt.TermVar name)
+ Ast.Variable (Ast.TermVar name)
in
let rec aux = function
- | Pt.AttributedTerm (_, t) -> assert false
- | Pt.Literal _
- | Pt.Layout _ -> assert false
- | Pt.Variable v -> Pt.Variable v
- | Pt.Magic m -> add_magic m
+ | Ast.AttributedTerm (_, t) -> assert false
+ | Ast.Literal _
+ | Ast.Layout _ -> assert false
+ | Ast.Variable v -> Ast.Variable v
+ | Ast.Magic m -> add_magic m
| t -> Util.visit_ast aux t
in
let term' = aux term in
List.map2
(fun p t ->
match p, t with
- Pt.Variable (Pt.TermVar name), _ ->
+ Ast.Variable (Ast.TermVar name), _ ->
name, (Env.TermType, Env.TermValue t)
- | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
+ | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
- | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
+ | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
name, (Env.StringType, Env.StringValue s)
| _ -> assert false)
pl tl
M.compiler rows' match_cb (fun _ -> None)
and compile_magic = function
- | Pt.Fold (kind, p_base, names, p_rec) ->
+ | Ast.Fold (kind, p_base, names, p_rec) ->
let p_rec_decls = Env.declarations_of_term p_rec in
(* LUCA: p_rec_decls should not contain "names" *)
let acc_name = try List.hd names with Failure _ -> assert false in
| Some (base_env, rec_envl) ->
Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *)
- | Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
+ | Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
let p_some_decls = Env.declarations_of_term p_some in
let none_env = List.map Env.opt_binding_of_name p_some_decls in
let compiled = compiler [p_some, 0] in
| Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
| _ -> assert false)
- | Pt.If (p_test, p_true, p_false) ->
+ | Ast.If (p_test, p_true, p_false) ->
let compiled_test = compiler [p_test, 0]
and compiled_true = compiler [p_true, 0]
and compiled_false = compiler [p_false, 0] in
| None -> None
| Some (env', _) -> Some (env' @ env))
- | Pt.Fail -> (fun _ _ -> None)
+ | Ast.Fail -> (fun _ _ -> None)
| _ -> assert false
end
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
- | Pt.UriPattern uri -> Uri uri, []
- | Pt.ImplicitPattern
- | Pt.VarPattern _ -> Blob, []
- | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
+ | Ast.UriPattern uri -> Uri uri, []
+ | Ast.ImplicitPattern
+ | Ast.VarPattern _ -> Blob, []
+ | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
let tag_of_pattern p =
let mask, pl = mask_of_appl_pattern p in
Hashtbl.hash mask, pl
- type pattern_t = Pt.cic_appl_pattern
+ type pattern_t = Ast.cic_appl_pattern
type term_t = Cic.annterm
let classify = function
- | Pt.ImplicitPattern
- | Pt.VarPattern _ -> Variable
- | Pt.UriPattern _
- | Pt.ApplPattern _ -> Constructor
+ | Ast.ImplicitPattern
+ | Ast.VarPattern _ -> Variable
+ | Ast.UriPattern _
+ | Ast.ApplPattern _ -> Constructor
end
module M = Matcher (Pattern32)
List.map2
(fun p t ->
match p with
- | Pt.ImplicitPattern -> Util.fresh_name (), t
- | Pt.VarPattern name -> name, t
+ | Ast.ImplicitPattern -> Util.fresh_name (), t
+ | Ast.VarPattern name -> name, t
| _ -> assert false)
pl matched_terms
in
open Printf
-open CicNotationEnv
-open CicNotationPt
+module Ast = CicNotationPt
+module Env = CicNotationEnv
exception Parse_error of Token.flocation * string
exception Level_not_found of int
type binding =
| NoBinding
- | Binding of string * value_type
- | Env of (string * value_type) list
+ | Binding of string * Env.value_type
+ | Env of (string * Env.value_type) list
let make_action action bindings =
let rec aux (vl : CicNotationEnv.t) =
function
- [] -> Gramext.action (fun (loc: location) -> action vl loc)
+ [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
(* LUCA: DEFCON 5 BEGIN *)
- | Binding (name, TermType) :: tl ->
+ | Binding (name, Env.TermType) :: tl ->
Gramext.action
- (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
- | Binding (name, StringType) :: tl ->
+ (fun (v:Ast.term) ->
+ aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+ | Binding (name, Env.StringType) :: tl ->
Gramext.action
(fun (v:string) ->
- aux ((name, (StringType, StringValue v)) :: vl) tl)
- | Binding (name, NumType) :: tl ->
+ aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
+ | Binding (name, Env.NumType) :: tl ->
Gramext.action
- (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
- | Binding (name, OptType t) :: tl ->
+ (fun (v:string) ->
+ aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
+ | Binding (name, Env.OptType t) :: tl ->
Gramext.action
(fun (v:'a option) ->
- aux ((name, (OptType t, OptValue v)) :: vl) tl)
- | Binding (name, ListType t) :: tl ->
+ aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
+ | Binding (name, Env.ListType t) :: tl ->
Gramext.action
(fun (v:'a list) ->
- aux ((name, (ListType t, ListValue v)) :: vl) tl)
+ aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
| Env _ :: tl ->
Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
(* LUCA: DEFCON 5 END *)
(* given a level 1 pattern computes the new RHS of "term" grammar entry *)
let extract_term_production pattern =
let rec aux = function
- | AttributedTerm (_, t) -> aux t
- | Literal l -> aux_literal l
- | Layout l -> aux_layout l
- | Magic m -> aux_magic m
- | Variable v -> aux_variable v
+ | Ast.AttributedTerm (_, t) -> aux t
+ | Ast.Literal l -> aux_literal l
+ | Ast.Layout l -> aux_layout l
+ | Ast.Magic m -> aux_magic m
+ | Ast.Variable v -> aux_variable v
| t ->
prerr_endline (CicNotationPp.pp_term t);
assert false
[NoBinding, gram_keyword s]
| `Number s -> [NoBinding, gram_number s]
and aux_layout = function
- | Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
- | Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
- | Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
- | Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
- | Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
- | Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
- | Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
- | Root (p1, p2) ->
+ | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
+ | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+ | Ast.Root (p1, p2) ->
[NoBinding, gram_symbol "\\root"] @ aux p2
@ [NoBinding, gram_symbol "\\of"] @ aux p1
- | Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
- | Break -> []
- | Box (_, pl) -> List.flatten (List.map aux pl)
- | Group pl -> List.flatten (List.map aux pl)
+ | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+ | Ast.Break -> []
+ | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
+ | Ast.Group pl -> List.flatten (List.map aux pl)
and aux_magic magic =
match magic with
- | Opt p ->
+ | Ast.Opt p ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
- let action (env_opt : CicNotationEnv.t option) (loc : location) =
+ let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
match env_opt with
- | Some env -> List.map opt_binding_some env
- | None -> List.map opt_binding_of_name p_names
+ | Some env -> List.map Env.opt_binding_some env
+ | None -> List.map Env.opt_binding_of_name p_names
in
- [ Env (List.map opt_declaration p_names),
+ [ Env (List.map Env.opt_declaration p_names),
Gramext.srules
[ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
Gramext.action action ] ]
- | List0 (p, _)
- | List1 (p, _) ->
+ | Ast.List0 (p, _)
+ | Ast.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 =
(fun env (n, (_, v)) -> grow_env_entry env n v)
env env_i
in *)
- let action (env_list : CicNotationEnv.t list) (loc : location) =
+ let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
CicNotationEnv.coalesce_env p_names env_list
in
let gram_of_list s =
match magic with
- | List0 (_, None) -> Gramext.Slist0 s
- | List1 (_, None) -> Gramext.Slist1 s
- | List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, None) -> Gramext.Slist0 s
+ | Ast.List1 (_, None) -> Gramext.Slist1 s
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
| _ -> assert false
in
- [ Env (List.map list_declaration p_names),
+ [ Env (List.map Env.list_declaration p_names),
Gramext.srules
[ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
Gramext.action action ] ]
| _ -> assert false
and aux_variable =
function
- | NumVar s -> [Binding (s, NumType), gram_number ""]
- | TermVar s -> [Binding (s, TermType), gram_term]
- | IdentVar s -> [Binding (s, StringType), gram_ident ""]
- | Ascription (p, s) -> assert false (* TODO *)
- | FreshVar _ -> assert false
+ | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
+ | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+ | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
+ | Ast.Ascription (p, s) -> assert false (* TODO *)
+ | Ast.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 action =
- make_action (fun (env : CicNotationEnv.t) (loc : location) -> env)
+ make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
p_bindings
in
p_bindings, p_atoms, p_names, action
Some associativity,
[ p_atoms,
(make_action
- (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
+ (fun (env: CicNotationEnv.t) (loc: Ast.location) ->
+ (action env loc))
p_bindings) ]]]
in
let keywords = CicNotationUtil.keywords_of_term level1_pattern in
let fold_cluster binder terms ty body =
List.fold_right
- (fun term body -> Binder (binder, (term, ty), body))
+ (fun term body -> Ast.Binder (binder, (term, ty), body))
terms body (* terms are names: either Ident or FreshVar *)
let fold_binder binder pt_names body =
(fun (names, ty) body -> fold_cluster binder names ty body)
pt_names body
-let return_term loc term = AttributedTerm (`Loc loc, term)
+let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
let _ = (* create empty precedence level for "term" *)
let mk_level_list first last =
(* row_sep: [ [ "rowsep"; sep = literal -> sep ] ];
field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *)
l1_magic_pattern: [
- [ "list0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep)
- | "list1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep)
- | "opt"; p = l1_simple_pattern -> Opt p
+ [ "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
]
];
l1_pattern_variable: [
- [ "term"; id = IDENT -> TermVar id
- | "number"; id = IDENT -> NumVar id
- | "ident"; id = IDENT -> IdentVar id
+ [ "term"; id = IDENT -> Ast.TermVar id
+ | "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 (Layout (Sub (p1, p2)))
+ return_term loc (Ast.Layout (Ast.Sub (p1, p2)))
| p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
- return_term loc (Layout (Sup (p1, p2)))
+ return_term loc (Ast.Layout (Ast.Sup (p1, p2)))
| p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
- return_term loc (Layout (Below (p1, p2)))
+ return_term loc (Ast.Layout (Ast.Below (p1, p2)))
| p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
- return_term loc (Layout (Above (p1, p2)))
+ return_term loc (Ast.Layout (Ast.Above (p1, p2)))
| p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
- return_term loc (Layout (Over (p1, p2)))
+ return_term loc (Ast.Layout (Ast.Over (p1, p2)))
| p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
- return_term loc (Layout (Atop (p1, p2)))
+ 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)) *)
| SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
- return_term loc (Layout (Frac (p1, p2)))
- | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Layout (Sqrt p))
+ return_term loc (Ast.Layout (Ast.Frac (p1, p2)))
+ | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Ast.Layout (Ast.Sqrt p))
| SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
- return_term loc (Layout (Root (arg, index)))
+ return_term loc (Ast.Layout (Ast.Root (arg, index)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Layout (Box ((H, false, false), p)))
+ return_term loc (Ast.Layout (Ast.Box ((Ast.H, false, false), p)))
| "vbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Layout (Box ((V, false, false), p)))
+ return_term loc (Ast.Layout (Ast.Box ((Ast.V, false, false), p)))
| "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Layout (Box ((HV, false, false), p)))
+ return_term loc (Ast.Layout (Ast.Box ((Ast.HV, false, false), p)))
| "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Layout (Box ((HOV, false, false), p)))
- | "break" -> return_term loc (Layout Break)
+ 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) *)
| LPAREN; p = l1_pattern; RPAREN ->
return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Variable (TermVar i))
- | m = l1_magic_pattern -> return_term loc (Magic m)
- | v = l1_pattern_variable -> return_term loc (Variable v)
- | l = literal -> return_term loc (Literal l)
+ [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+ | 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)
]
];
END
EXTEND
GLOBAL: level2_meta;
l2_variable: [
- [ "term"; id = IDENT -> TermVar id
- | "number"; id = IDENT -> NumVar id
- | "ident"; id = IDENT -> IdentVar id
- | "fresh"; id = IDENT -> FreshVar id
- | "anonymous" -> TermVar "_"
- | id = IDENT -> TermVar id
+ [ "term"; id = IDENT -> Ast.TermVar id
+ | "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
]
];
l2_magic: [
[ "fold"; kind = [ "left" -> `Left | "right" -> `Right ];
base = level2_meta; "rec"; id = IDENT; recursive = level2_meta ->
- Fold (kind, base, [id], recursive)
- | "default"; some = level2_meta; none = level2_meta -> Default (some, none)
+ Ast.Fold (kind, base, [id], recursive)
+ | "default"; some = level2_meta; none = level2_meta ->
+ Ast.Default (some, none)
| "if"; p_test = level2_meta;
"then"; p_true = level2_meta;
"else"; p_false = level2_meta ->
- If (p_test, p_true, p_false)
- | "fail" -> Fail
+ Ast.If (p_test, p_true, p_false)
+ | "fail" -> Ast.Fail
]
];
level2_meta: [
- [ magic = l2_magic -> Magic magic
- | var = l2_variable -> Variable var
+ [ magic = l2_magic -> Ast.Magic magic
+ | var = l2_variable -> Ast.Variable var
| blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
]
];
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
- List.map (fun n -> Ident (n, None)) names, Some ty
- | name = IDENT -> [Ident (name, None)], None
+ List.map (fun n -> Ast.Ident (n, None)) names, Some ty
+ | name = IDENT -> [Ast.Ident (name, None)], None
| blob = UNPARSED_META ->
let meta = !parse_level2_meta_ref (Stream.of_string blob) in
match meta with
- | Variable (FreshVar _) -> [meta], None
- | Variable (TermVar "_") -> [Ident ("_", None)], None
+ | Ast.Variable (Ast.FreshVar _) -> [meta], None
+ | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
| _ -> failwith "Invalid bound name."
]
];
single_arg: [
- [ name = IDENT -> Ident (name, None)
+ [ name = IDENT -> Ast.Ident (name, None)
| blob = UNPARSED_META ->
let meta = !parse_level2_meta_ref (Stream.of_string blob) in
match meta with
- | Variable (FreshVar _) -> meta
- | Variable (TermVar "_") -> Ident ("_", None)
+ | Ast.Variable (Ast.FreshVar _) -> meta
+ | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
| _ -> failwith "Invalid index name."
]
];
in
let rec find_arg name n = function
| [] ->
- fail loc (sprintf "Argument %s not found"
+ Ast.fail loc (sprintf "Argument %s not found"
(CicNotationPp.pp_term name))
| (l,_) :: tl ->
(match position_of name 0 l with
binder_vars: [
[ vars = [
l = LIST1 single_arg SEP SYMBOL "," -> l
- | SYMBOL "_" -> [Ident ("_", None)] ];
+ | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
| LPAREN;
vars = [
l = LIST1 single_arg SEP SYMBOL "," -> l
- | SYMBOL "_" -> [Ident ("_", None)] ];
+ | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
typ = OPT [ SYMBOL ":"; t = term -> t ];
RPAREN -> (vars, typ)
]
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))
+ return_term loc (Ast.LetIn (var, p1, p2))
| "let"; k = induction_kind; defs = let_defs; "in";
body = term ->
- return_term loc (LetRec (k, defs, body))
+ return_term loc (Ast.LetRec (k, defs, body))
]
];
term: LEVEL "20R" (* binder *)
[
[ p1 = term; p2 = term ->
let rec aux = function
- | Appl (hd :: tl)
- | AttributedTerm (_, Appl (hd :: tl)) ->
+ | Ast.Appl (hd :: tl)
+ | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
aux hd @ tl
| term -> [term]
in
- return_term loc (Appl (aux p1 @ [p2]))
+ return_term loc (Ast.Appl (aux p1 @ [p2]))
]
];
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))
- | u = URI -> return_term loc (Uri (u, None))
- | n = NUMBER -> return_term loc (Num (n, 0))
- | IMPLICIT -> return_term loc (Implicit)
- | PLACEHOLDER -> return_term loc UserInput
- | m = META -> return_term loc (Meta (int_of_string m, []))
- | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
- | s = sort -> return_term loc (Sort s)
+ [ id = IDENT -> return_term loc (Ast.Ident (id, None))
+ | id = IDENT; s = explicit_subst ->
+ return_term loc (Ast.Ident (id, Some s))
+ | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
+ | u = URI -> return_term loc (Ast.Uri (u, None))
+ | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+ | IMPLICIT -> return_term loc (Ast.Implicit)
+ | PLACEHOLDER -> return_term loc Ast.UserInput
+ | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
+ | m = META; s = meta_substs ->
+ return_term loc (Ast.Meta (int_of_string m, s))
+ | s = sort -> return_term loc (Ast.Sort s)
| outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
"match"; t = term;
indty_ident = OPT [ "in"; id = IDENT -> id ];
lhs, rhs
] SEP SYMBOL "|";
SYMBOL "]" ->
- return_term loc (Case (t, indty_ident, outtyp, patterns))
+ return_term loc (Ast.Case (t, indty_ident, outtyp, patterns))
| LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
- return_term loc (Cast (p1, p2))
+ return_term loc (Ast.Cast (p1, p2))
| LPAREN; p = term; RPAREN -> p
| blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
]
open Printf
-open CicNotationEnv
-open CicNotationPt
+module Ast = CicNotationPt
+module Env = CicNotationEnv
(* when set to true debugging information, not in sync with input syntax, will
* be added to the output of pp_term.
let rec pp_term ?(pp_parens = true) t =
let t_pp =
match t with
- | AttributedTerm (`Href _, term) when debug_printing ->
+ | Ast.AttributedTerm (`Href _, term) when debug_printing ->
sprintf "#[%s]" (pp_term ~pp_parens:false term)
- | AttributedTerm (`IdRef id, term) when debug_printing ->
+ | Ast.AttributedTerm (`IdRef id, term) when debug_printing ->
sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
- | AttributedTerm (_, term) when debug_printing ->
+ | Ast.AttributedTerm (_, term) when debug_printing ->
sprintf "@[%s]" (pp_term ~pp_parens:false term)
- | AttributedTerm (`Raw text, _) -> text
- | AttributedTerm (_, term) -> pp_term ~pp_parens:false term
+ | Ast.AttributedTerm (`Raw text, _) -> text
+ | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
- | Appl terms ->
+ | Ast.Appl terms ->
sprintf "%s" (String.concat " " (List.map pp_term terms))
- | Binder (`Forall, (Ident ("_", None), typ), body)
- | Binder (`Pi, (Ident ("_", None), typ), body) ->
+ | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
sprintf "%s \\to %s"
(match typ with None -> "?" | Some typ -> pp_term typ)
(pp_term body)
- | Binder (kind, var, body) ->
+ | Ast.Binder (kind, var, body) ->
sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
(pp_term body)
- | Case (term, indtype, typ, patterns) ->
+ | Ast.Case (term, indtype, typ, patterns) ->
sprintf "%smatch %s with %s"
(match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t))
(pp_term term) (pp_patterns patterns)
- | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
- | LetIn (var, t1, t2) ->
+ | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
+ | Ast.LetIn (var, t1, t2) ->
sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
(pp_term t2)
- | LetRec (kind, definitions, term) ->
+ | Ast.LetRec (kind, definitions, term) ->
sprintf "let %s %s in %s"
(match kind with `Inductive -> "rec" | `CoInductive -> "corec")
(String.concat " and "
sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
definitions))
(pp_term term)
- | Ident (name, Some []) | Ident (name, None)
- | Uri (name, Some []) | Uri (name, None) ->
+ | Ast.Ident (name, Some []) | Ast.Ident (name, None)
+ | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
name
- | Ident (name, Some substs)
- | Uri (name, Some substs) ->
+ | Ast.Ident (name, Some substs)
+ | Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
- | Implicit -> "?"
- | Meta (index, substs) ->
+ | Ast.Implicit -> "?"
+ | Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
(List.map (function None -> "_" | Some t -> pp_term t) substs))
- | Num (num, _) -> num
- | Sort `Set -> "Set"
- | Sort `Prop -> "Prop"
- | Sort `Type -> "Type"
- | Sort `CProp -> "CProp"
- | Symbol (name, _) -> "'" ^ name
-
- | UserInput -> ""
-
- | Literal l -> pp_literal l
- | Layout l -> pp_layout l
- | Magic m -> pp_magic m
- | Variable v -> pp_variable v
+ | Ast.Num (num, _) -> num
+ | Ast.Sort `Set -> "Set"
+ | Ast.Sort `Prop -> "Prop"
+ | Ast.Sort `Type -> "Type"
+ | Ast.Sort `CProp -> "CProp"
+ | Ast.Symbol (name, _) -> "'" ^ name
+
+ | Ast.UserInput -> ""
+
+ | Ast.Literal l -> pp_literal l
+ | Ast.Layout l -> pp_layout l
+ | Ast.Magic m -> pp_magic m
+ | Ast.Variable v -> pp_variable v
in
if pp_parens then sprintf "(%s)" t_pp
else t_pp
and pp_box_spec (kind, spacing, indent) =
let int_of_bool b = if b then 1 else 0 in
let kind_string =
- match kind with H -> "H" | V -> "V" | HV -> "HV" | HOV -> "HOV"
+ match kind with
+ Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV"
in
sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
and pp_layout = function
- | Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
- | Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
- | Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
- | Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2)
- | Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
- | Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
- | Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
- | Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
- | Root (arg, index) ->
+ | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
+ | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
+ | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
+ | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2)
+ | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
+ | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
+ | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
+ | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
+ | Ast.Root (arg, index) ->
sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
- | Break -> "\\BREAK"
+ | Ast.Break -> "\\BREAK"
(* | Space -> "\\SPACE" *)
- | Box (box_spec, terms) ->
+ | Ast.Box (box_spec, terms) ->
sprintf "\\%s [%s]" (pp_box_spec box_spec)
(String.concat " " (List.map pp_term terms))
- | Group terms ->
+ | Ast.Group terms ->
sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms))
and pp_magic = function
- | List0 (t, sep_opt) -> sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | List1 (t, sep_opt) -> sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | Opt t -> sprintf "opt %s" (pp_term t)
- | Fold (kind, p_base, names, p_rec) ->
+ | Ast.List0 (t, sep_opt) ->
+ sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | Ast.List1 (t, sep_opt) ->
+ sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | Ast.Opt t -> sprintf "opt %s" (pp_term t)
+ | Ast.Fold (kind, p_base, names, p_rec) ->
let acc = match names with acc :: _ -> acc | _ -> assert false in
sprintf "fold %s %s rec %s %s"
(pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec)
- | Default (p_some, p_none) ->
+ | Ast.Default (p_some, p_none) ->
sprintf "default %s %s" (pp_term p_some) (pp_term p_none)
- | If (p_test, p_true, p_false) ->
+ | Ast.If (p_test, p_true, p_false) ->
sprintf "if %s then %s else %s"
(pp_term p_test) (pp_term p_true) (pp_term p_false)
- | Fail -> "fail"
+ | Ast.Fail -> "fail"
and pp_fold_kind = function
| `Left -> "left"
| Some sep -> sprintf " sep %s" (pp_literal sep)
and pp_variable = function
- | NumVar s -> "number " ^ s
- | IdentVar s -> "ident " ^ s
- | TermVar s -> "term " ^ s
- | Ascription (t, n) -> assert false
- | FreshVar n -> "fresh " ^ n
+ | Ast.NumVar s -> "number " ^ s
+ | Ast.IdentVar s -> "ident " ^ s
+ | Ast.TermVar s -> "term " ^ s
+ | Ast.Ascription (t, n) -> assert false
+ | Ast.FreshVar n -> "fresh " ^ n
let pp_term t = pp_term ~pp_parens:false t
let rec pp_value = function
- | TermValue t -> sprintf "$%s$" (pp_term t)
- | StringValue s -> sprintf "\"%s\"" s
- | NumValue n -> n
- | OptValue (Some v) -> "Some " ^ pp_value v
- | OptValue None -> "None"
- | ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
+ | Env.TermValue t -> sprintf "$%s$" (pp_term t)
+ | Env.StringValue s -> sprintf "\"%s\"" s
+ | Env.NumValue n -> n
+ | Env.OptValue (Some v) -> "Some " ^ pp_value v
+ | Env.OptValue None -> "None"
+ | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
let rec pp_value_type =
function
- | TermType -> "Term"
- | StringType -> "String"
- | NumType -> "Number"
- | OptType t -> "Maybe " ^ pp_value_type t
- | ListType l -> "List " ^ pp_value_type l
+ | Env.TermType -> "Term"
+ | Env.StringType -> "String"
+ | Env.NumType -> "Number"
+ | Env.OptType t -> "Maybe " ^ pp_value_type t
+ | Env.ListType l -> "List " ^ pp_value_type l
let pp_env env =
String.concat "; "
* http://helm.cs.unibo.it/
*)
-module P = Mpresentation
+module Ast = CicNotationPt
+module Mpres = Mpresentation
-type mathml_markup = boxml_markup Mpresentation.mpres
+type mathml_markup = boxml_markup Mpres.mpres
and boxml_markup = mathml_markup Box.box
type markup = mathml_markup
@ attrs
in
match kind with
- | CicNotationPt.H ->
+ | Ast.H ->
if List.for_all eligible_math children then
Mpresentation.Mrow (attrs',
dress (List.map promote_to_math children))
else
mpres_of_box (Box.H (attrs',
List.map box_of_mpres children))
-(* | CicNotationPt.H when List.for_all genuine_math children ->
+(* | Ast.H when List.for_all genuine_math children ->
Mpresentation.Mrow (attrs', dress children) *)
- | CicNotationPt.V ->
+ | Ast.V ->
mpres_of_box (Box.V (attrs',
List.map box_of_mpres children))
- | CicNotationPt.HV ->
+ | Ast.HV ->
mpres_of_box (Box.HV (attrs',
List.map box_of_mpres children))
- | CicNotationPt.HOV ->
+ | Ast.HOV ->
mpres_of_box (Box.HOV (attrs',
List.map box_of_mpres children))
let is_atomic t =
let rec aux_mpres = function
- | P.Mi _
- | P.Mo _
- | P.Mn _
- | P.Ms _
- | P.Mtext _
- | P.Mspace _ -> true
- | P.Mobject (_, box) -> aux_box box
- | P.Maction (_, [mpres])
- | P.Mrow (_, [mpres]) -> aux_mpres mpres
+ | Mpres.Mi _
+ | Mpres.Mo _
+ | Mpres.Mn _
+ | Mpres.Ms _
+ | Mpres.Mtext _
+ | Mpres.Mspace _ -> true
+ | Mpres.Mobject (_, box) -> aux_box box
+ | Mpres.Maction (_, [mpres])
+ | Mpres.Mrow (_, [mpres]) -> aux_mpres mpres
| _ -> false
and aux_box = function
| Box.Space _
t
let render ids_to_uris =
- let module A = CicNotationPt in
+ let module A = Ast in
let module P = Mpresentation in
let use_unicode = true in
let lookup_uri = function
(RenderingAttrs.number_attributes `MathML)
@ make_href xmlattrs xref uris
in
- P.Mn (attrs, literal)
+ Mpres.Mn (attrs, literal)
| A.Symbol (literal, _) ->
let attrs =
(RenderingAttrs.symbol_attributes `MathML)
@ make_href xmlattrs xref uris
in
- P.Mo (attrs, to_unicode literal)
+ Mpres.Mo (attrs, to_unicode literal)
| A.Ident (literal, subst)
| A.Uri (literal, subst) ->
let attrs =
(RenderingAttrs.ident_attributes `MathML)
@ make_href xmlattrs xref (ref [])
in
- let name = P.Mi (attrs, to_unicode literal) in
+ let name = Mpres.Mi (attrs, to_unicode literal) in
(match subst with
| Some []
| None -> name
(List.map
(fun (name, t) ->
box_of mathonly (A.H, false, false) [] [
- P.Mi ([], name);
- P.Mo ([], to_unicode "\\def");
+ Mpres.Mi ([], name);
+ Mpres.Mo ([], to_unicode "\\def");
aux [] mathonly xref pos prec uris t ])
substs))
@ [ closed_brace ])
let var_name = UriManager.name_of_uri var_uri in
let href_attr = Some "xlink", "href", var in
box_of mathonly (A.H, false, false) [] [
- P.Mi ([href_attr], var_name);
- P.Mo ([], to_unicode "\\def");
+ Mpres.Mi ([href_attr], var_name);
+ Mpres.Mo ([], to_unicode "\\def");
aux [] mathonly xref pos prec uris t ])
substs)) *)
in
let substs_maction = toggle_action [ hidden_substs; substs' ] in
box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
| A.Literal l -> aux_literal xmlattrs xref prec uris l
- | A.UserInput -> P.Mtext ([], "%")
+ | A.UserInput -> Mpres.Mtext ([], "%")
| A.Layout l -> aux_layout mathonly xref pos prec uris l
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
and aux_literal xmlattrs xref prec uris l =
let attrs = make_href xmlattrs xref uris in
(match l with
- | `Symbol s -> P.Mo (attrs, to_unicode s)
- | `Keyword s -> P.Mo (attrs, to_unicode s)
- | `Number s -> P.Mn (attrs, to_unicode s))
+ | `Symbol s -> Mpres.Mo (attrs, to_unicode s)
+ | `Keyword s -> Mpres.Mo (attrs, to_unicode s)
+ | `Number s -> Mpres.Mn (attrs, to_unicode s))
and aux_layout mathonly xref pos prec uris l =
let attrs = make_xref xref in
let invoke' t = aux [] true (ref None) pos prec uris t in
match l with
- | A.Sub (t1, t2) -> P.Msub (attrs, invoke' t1, invoke' t2)
- | A.Sup (t1, t2) -> P.Msup (attrs, invoke' t1, invoke' t2)
- | A.Below (t1, t2) -> P.Munder (attrs, invoke' t1, invoke' t2)
- | A.Above (t1, t2) -> P.Mover (attrs, invoke' t1, invoke' t2)
+ | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke' t2)
+ | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke' t2)
+ | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke' t2)
+ | A.Above (t1, t2) -> Mpres.Mover (attrs, invoke' t1, invoke' t2)
| A.Frac (t1, t2)
- | A.Over (t1, t2) -> P.Mfrac (attrs, invoke' t1, invoke' t2)
+ | A.Over (t1, t2) -> Mpres.Mfrac (attrs, invoke' t1, invoke' t2)
| A.Atop (t1, t2) ->
- P.Mfrac (atop_attributes @ attrs, invoke' t1, invoke' t2)
- | A.Sqrt t -> P.Msqrt (attrs, invoke' t)
- | A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2)
+ Mpres.Mfrac (atop_attributes @ attrs, invoke' t1, invoke' t2)
+ | A.Sqrt t -> Mpres.Msqrt (attrs, invoke' t)
+ | A.Root (t1, t2) -> Mpres.Mroot (attrs, invoke' t1, invoke' t2)
| A.Box ((_, spacing, _) as kind, terms) ->
let children =
aux_children mathonly spacing xref pos prec uris
open Printf
+module Ast = CicNotationPt
+
type pattern_id = int
type interpretation_id = pattern_id
type pretty_printer_id = pattern_id
-module Ast = CicNotationPt
-
type term_info =
{ sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
uri: (Cic.id, string) Hashtbl.t;
* http://helm.cs.unibo.it/
*)
-open CicNotationPt
+module Ast = CicNotationPt
type tag = int
-type pattern_t = CicNotationPt.term
+type pattern_t = Ast.term
let get_tag term0 =
let subterms = ref [] in
let map_term t =
subterms := t :: !subterms ;
- Implicit
+ Ast.Implicit
in
let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
and special_k = function
- | AttributedTerm (_, t) -> aux t
+ | Ast.AttributedTerm (_, t) -> aux t
| _ -> assert false
in
let term_mask = aux term0 in
* http://helm.cs.unibo.it/
*)
-open CicNotationPt
-
-(* let meta_names_of term = *)
-(* let rec names = ref [] in *)
-(* let add_name n = *)
-(* if List.mem n !names then () *)
-(* else names := n :: !names *)
-(* in *)
-(* let rec aux = function *)
-(* | AttributedTerm (_, term) -> aux term *)
-(* | Appl terms -> List.iter aux terms *)
-(* | Binder (_, _, body) -> aux body *)
-(* | Case (term, indty, outty_opt, patterns) -> *)
-(* aux term ; *)
-(* aux_opt outty_opt ; *)
-(* List.iter aux_branch patterns *)
-(* | LetIn (_, t1, t2) -> *)
-(* aux t1 ; *)
-(* aux t2 *)
-(* | LetRec (_, definitions, body) -> *)
-(* List.iter aux_definition definitions ; *)
-(* aux body *)
-(* | Uri (_, Some substs) -> aux_substs substs *)
-(* | Ident (_, Some substs) -> aux_substs substs *)
-(* | Meta (_, substs) -> aux_meta_substs substs *)
-
-(* | Implicit *)
-(* | Ident _ *)
-(* | Num _ *)
-(* | Sort _ *)
-(* | Symbol _ *)
-(* | Uri _ *)
-(* | UserInput -> () *)
-
-(* | Magic magic -> aux_magic magic *)
-(* | Variable var -> aux_variable var *)
-
-(* | _ -> assert false *)
-(* and aux_opt = function *)
-(* | Some term -> aux term *)
-(* | None -> () *)
-(* and aux_capture_var (_, ty_opt) = aux_opt ty_opt *)
-(* and aux_branch (pattern, term) = *)
-(* aux_pattern pattern ; *)
-(* aux term *)
-(* and aux_pattern (head, vars) = *)
-(* List.iter aux_capture_var vars *)
-(* and aux_definition (var, term, i) = *)
-(* aux_capture_var var ; *)
-(* aux term *)
-(* and aux_substs substs = List.iter (fun (_, term) -> aux term) substs *)
-(* and aux_meta_substs meta_substs = List.iter aux_opt meta_substs *)
-(* and aux_variable = function *)
-(* | NumVar name -> add_name name *)
-(* | IdentVar name -> add_name name *)
-(* | TermVar name -> add_name name *)
-(* | FreshVar _ -> () *)
-(* | Ascription _ -> assert false *)
-(* and aux_magic = function *)
-(* | Default (t1, t2) *)
-(* | Fold (_, t1, _, t2) -> *)
-(* aux t1 ; *)
-(* aux t2 *)
-(* | _ -> assert false *)
-(* in *)
-(* aux term ; *)
-(* !names *)
+module Ast = CicNotationPt
let visit_ast ?(special_k = fun _ -> assert false) k =
let rec aux = function
- | Appl terms -> Appl (List.map k terms)
- | Binder (kind, var, body) ->
- Binder (kind, aux_capture_variable var, k body)
- | Case (term, indtype, typ, patterns) ->
- Case (k term, indtype, aux_opt typ, aux_patterns patterns)
- | Cast (t1, t2) -> Cast (k t1, k t2)
- | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
- | LetRec (kind, definitions, term) ->
+ | Ast.Appl terms -> Ast.Appl (List.map k terms)
+ | Ast.Binder (kind, var, body) ->
+ Ast.Binder (kind, aux_capture_variable var, k body)
+ | Ast.Case (term, indtype, typ, patterns) ->
+ Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+ | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
+ | Ast.LetIn (var, t1, t2) ->
+ Ast.LetIn (aux_capture_variable var, k t1, k t2)
+ | Ast.LetRec (kind, definitions, term) ->
let definitions =
List.map
(fun (var, ty, n) -> aux_capture_variable var, k ty, n)
definitions
in
- LetRec (kind, definitions, k term)
- | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
- | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
- | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
- | (AttributedTerm _
- | Layout _
- | Literal _
- | Magic _
- | Variable _) as t -> special_k t
- | (Ident _
- | Implicit
- | Num _
- | Sort _
- | Symbol _
- | Uri _
- | UserInput) as t -> t
+ Ast.LetRec (kind, definitions, k term)
+ | Ast.Ident (name, Some substs) ->
+ Ast.Ident (name, Some (aux_substs substs))
+ | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
+ | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
+ | (Ast.AttributedTerm _
+ | Ast.Layout _
+ | Ast.Literal _
+ | Ast.Magic _
+ | Ast.Variable _) as t -> special_k t
+ | (Ast.Ident _
+ | Ast.Implicit
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.Uri _
+ | Ast.UserInput) as t -> t
and aux_opt = function
| None -> None
| Some term -> Some (k term)
aux
let visit_layout k = function
- | Sub (t1, t2) -> Sub (k t1, k t2)
- | Sup (t1, t2) -> Sup (k t1, k t2)
- | Below (t1, t2) -> Below (k t1, k t2)
- | Above (t1, t2) -> Above (k t1, k t2)
- | Over (t1, t2) -> Over (k t1, k t2)
- | Atop (t1, t2) -> Atop (k t1, k t2)
- | Frac (t1, t2) -> Frac (k t1, k t2)
- | Sqrt t -> Sqrt (k t)
- | Root (arg, index) -> Root (k arg, k index)
- | Break -> Break
- | Box (kind, terms) -> Box (kind, List.map k terms)
- | Group terms -> Group (List.map k terms)
+ | Ast.Sub (t1, t2) -> Ast.Sub (k t1, k t2)
+ | Ast.Sup (t1, t2) -> Ast.Sup (k t1, k t2)
+ | Ast.Below (t1, t2) -> Ast.Below (k t1, k t2)
+ | Ast.Above (t1, t2) -> Ast.Above (k t1, k t2)
+ | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
+ | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
+ | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+ | Ast.Sqrt t -> Ast.Sqrt (k t)
+ | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
+ | Ast.Break -> Ast.Break
+ | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
+ | Ast.Group terms -> Ast.Group (List.map k terms)
let visit_magic k = function
- | List0 (t, l) -> List0 (k t, l)
- | List1 (t, l) -> List1 (k t, l)
- | Opt t -> Opt (k t)
- | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
- | Default (t1, t2) -> Default (k t1, k t2)
- | If (t1, t2, t3) -> If (k t1, k t2, k t3)
- | Fail -> Fail
+ | Ast.List0 (t, l) -> Ast.List0 (k t, l)
+ | Ast.List1 (t, l) -> Ast.List1 (k t, l)
+ | Ast.Opt t -> Ast.Opt (k t)
+ | Ast.Fold (kind, t1, names, t2) -> Ast.Fold (kind, k t1, names, k t2)
+ | Ast.Default (t1, t2) -> Ast.Default (k t1, k t2)
+ | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3)
+ | Ast.Fail -> Ast.Fail
let variables_of_term t =
let rec vars = ref [] in
else vars := v :: !vars
in
let rec aux = function
- | Magic m -> Magic (visit_magic aux m)
- | Layout l -> Layout (visit_layout aux l)
- | Variable v -> Variable (aux_variable v)
- | Literal _ as t -> t
- | AttributedTerm (_, t) -> aux t
+ | Ast.Magic m -> Ast.Magic (visit_magic aux m)
+ | Ast.Layout l -> Ast.Layout (visit_layout aux l)
+ | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | Ast.Literal _ as t -> t
+ | Ast.AttributedTerm (_, t) -> aux t
| t -> visit_ast aux t
and aux_variable = function
- | (NumVar _
- | IdentVar _
- | TermVar _) as t ->
+ | (Ast.NumVar _
+ | Ast.IdentVar _
+ | Ast.TermVar _) as t ->
add_variable t ;
t
- | FreshVar _ as t -> t
- | Ascription _ -> assert false
+ | Ast.FreshVar _ as t -> t
+ | Ast.Ascription _ -> assert false
in
ignore (aux t) ;
!vars
let names_of_term t =
let aux = function
- | NumVar s
- | IdentVar s
- | TermVar s -> s
+ | Ast.NumVar s
+ | Ast.IdentVar s
+ | Ast.TermVar s -> s
| _ -> assert false
in
List.map aux (variables_of_term t)
let rec keywords = ref [] in
let add_keyword k = keywords := k :: !keywords in
let rec aux = function
- | AttributedTerm (_, t) -> aux t
- | Layout l -> Layout (visit_layout aux l)
- | Literal (`Keyword k) as t ->
+ | Ast.AttributedTerm (_, t) -> aux t
+ | Ast.Layout l -> Ast.Layout (visit_layout aux l)
+ | Ast.Literal (`Keyword k) as t ->
add_keyword k;
t
- | Literal _ as t -> t
- | Magic m -> Magic (visit_magic aux m)
- | Variable _ as v -> v
+ | Ast.Literal _ as t -> t
+ | Ast.Magic m -> Ast.Magic (visit_magic aux m)
+ | Ast.Variable _ as v -> v
| t -> visit_ast aux t
in
ignore (aux t) ;
let rec strip_attributes t =
let special_k = function
- | AttributedTerm (_, term) -> strip_attributes term
- | Magic m -> Magic (visit_magic strip_attributes m)
- | Variable _ as t -> t
+ | Ast.AttributedTerm (_, term) -> strip_attributes term
+ | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m)
+ | Ast.Variable _ as t -> t
| t -> assert false
in
visit_ast ~special_k strip_attributes t
else names := n :: !names
in
let rec aux = function
- | AttributedTerm (_, term) -> aux term
- | Appl terms -> List.iter aux terms
- | Binder (_, _, body) -> aux body
- | Case (term, indty, outty_opt, patterns) ->
+ | Ast.AttributedTerm (_, term) -> aux term
+ | Ast.Appl terms -> List.iter aux terms
+ | Ast.Binder (_, _, body) -> aux body
+ | Ast.Case (term, indty, outty_opt, patterns) ->
aux term ;
aux_opt outty_opt ;
List.iter aux_branch patterns
- | LetIn (_, t1, t2) ->
+ | Ast.LetIn (_, t1, t2) ->
aux t1 ;
aux t2
- | LetRec (_, definitions, body) ->
+ | Ast.LetRec (_, definitions, body) ->
List.iter aux_definition definitions ;
aux body
- | Uri (_, Some substs) -> aux_substs substs
- | Ident (_, Some substs) -> aux_substs substs
- | Meta (_, substs) -> aux_meta_substs substs
+ | Ast.Uri (_, Some substs) -> aux_substs substs
+ | Ast.Ident (_, Some substs) -> aux_substs substs
+ | Ast.Meta (_, substs) -> aux_meta_substs substs
- | Implicit
- | Ident _
- | Num _
- | Sort _
- | Symbol _
- | Uri _
- | UserInput -> ()
+ | Ast.Implicit
+ | Ast.Ident _
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.Uri _
+ | Ast.UserInput -> ()
- | Magic magic -> aux_magic magic
- | Variable var -> aux_variable var
+ | Ast.Magic magic -> aux_magic magic
+ | Ast.Variable var -> aux_variable var
| _ -> assert false
and aux_opt = function
and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
and aux_variable = function
- | NumVar name -> add_name name
- | IdentVar name -> add_name name
- | TermVar name -> add_name name
- | FreshVar _ -> ()
- | Ascription _ -> assert false
+ | Ast.NumVar name -> add_name name
+ | Ast.IdentVar name -> add_name name
+ | Ast.TermVar name -> add_name name
+ | Ast.FreshVar _ -> ()
+ | Ast.Ascription _ -> assert false
and aux_magic = function
- | Default (t1, t2)
- | Fold (_, t1, _, t2) ->
+ | Ast.Default (t1, t2)
+ | Ast.Fold (_, t1, _, t2) ->
aux t1 ;
aux t2
- | If (t1, t2, t3) ->
+ | Ast.If (t1, t2, t3) ->
aux t1 ;
aux t2 ;
aux t3
- | Fail -> ()
+ | Ast.Fail -> ()
| _ -> assert false
in
aux term ;
let boxify = function
| [ a ] -> a
- | l -> Layout (Box ((H, false, false), l))
+ | l -> Ast.Layout (Ast.Box ((Ast.H, false, false), l))
let unboxify = function
- | Layout (Box ((H, false, false), [ a ])) -> a
+ | Ast.Layout (Ast.Box ((Ast.H, false, false), [ a ])) -> a
| l -> l
let group = function
| [ a ] -> a
- | l -> Layout (Group l)
+ | l -> Ast.Layout (Ast.Group l)
let ungroup =
let rec aux acc =
function
[] -> List.rev acc
- | Layout (Group terms) :: terms' -> aux acc (terms @ terms')
+ | Ast.Layout (Ast.Group terms) :: terms' -> aux acc (terms @ terms')
| term :: terms -> aux (term :: acc) terms
in
aux []
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | UriPattern uri ->
+ | Ast.UriPattern uri ->
(try
ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
acc
with Not_found -> uri :: acc)
- | ImplicitPattern
- | VarPattern _ -> acc
- | ApplPattern apl -> List.fold_left aux acc apl
+ | Ast.ImplicitPattern
+ | Ast.VarPattern _ -> acc
+ | Ast.ApplPattern apl -> List.fold_left aux acc apl
in
aux [] ap
let rec find_branch =
function
- Magic (If (_, Magic Fail, t)) -> find_branch t
- | Magic (If (_, t, _)) -> find_branch t
+ Ast.Magic (Ast.If (_, Ast.Magic Ast.Fail, t)) -> find_branch t
+ | Ast.Magic (Ast.If (_, t, _)) -> find_branch t
| t -> t
let cic_name_of_name = function
- | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
- | CicNotationPt.Ident (name, None) -> Cic.Name name
+ | Ast.Ident ("_", None) -> Cic.Anonymous
+ | Ast.Ident (name, None) -> Cic.Name name
| _ -> assert false
let name_of_cic_name =
- let add_dummy_xref t = CicNotationPt.AttributedTerm (`IdRef "", t) in
+(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *)
+ (* ZACK why we used to generate dummy xrefs? *)
+ let add_dummy_xref t = t in
function
- | Cic.Name s -> add_dummy_xref (CicNotationPt.Ident (s, None))
- | Cic.Anonymous -> add_dummy_xref (CicNotationPt.Ident ("_", None))
+ | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None))
+ | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None))
let fresh_index = ref ~-1
* http://helm.cs.unibo.it/
*)
+module Ast = CicNotationPt
+
type direction = [ `LeftToRight | `RightToLeft ]
type 'term reduction_kind =
[ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
-type loc = CicNotationPt.location
+type loc = Ast.location
type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
| Number_alias of int * string (* instance no, description *)
type obj =
- | Inductive of (string * CicNotationPt.term) list *
- CicNotationPt.term inductive_type list
+ | Inductive of (string * Ast.term) list *
+ Ast.term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of thm_flavour * string * CicNotationPt.term *
- CicNotationPt.term option
+ | Theorem of thm_flavour * string * Ast.term *
+ Ast.term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
- | Record of (string * CicNotationPt.term) list * string * CicNotationPt.term *
- (string * CicNotationPt.term) list
+ | Record of (string * Ast.term) list * string * Ast.term *
+ (string * Ast.term) list
type ('term,'obj) command =
| Default of loc * string * UriManager.uri list
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
- int * CicNotationPt.term
+ | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
+ int * Ast.term
(* direction, l1 pattern, associativity, precedence, l2 pattern *)
| Interpretation of loc *
- string * (string * CicNotationPt.argument_pattern list) *
- CicNotationPt.cic_appl_pattern
+ string * (string * Ast.argument_pattern list) *
+ Ast.cic_appl_pattern
(* description (i.e. id), symbol, arg pattern, appl pattern *)
(* DEBUGGING *)
open GrafiteAst
+module Ast = CicNotationPt
+
let tactical_terminator = "."
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
pp_fields fields ^ "}"
let pp_argument_pattern = function
- | CicNotationPt.IdentArg (eta_depth, name) ->
+ | Ast.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in
for i = 1 to eta_depth do
Buffer.add_string eta_buf "\\eta."
sprintf "%s%s" (Buffer.contents eta_buf) name
let rec pp_cic_appl_pattern = function
- | CicNotationPt.UriPattern uri -> UriManager.string_of_uri uri
- | CicNotationPt.VarPattern name -> name
- | CicNotationPt.ImplicitPattern -> "_"
- | CicNotationPt.ApplPattern aps ->
+ | Ast.UriPattern uri -> UriManager.string_of_uri uri
+ | Ast.VarPattern name -> name
+ | Ast.ImplicitPattern -> "_"
+ | Ast.ApplPattern aps ->
sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))
let pp_l1_pattern = CicNotationPp.pp_term
open Printf
+module Ast = CicNotationPt
+
let grammar = CicNotationParser.level2_ast_grammar
let term = CicNotationParser.term
let statement = Grammar.Entry.create grammar "statement"
-let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
let default_precedence = 50
let default_associativity = Gramext.NonA
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN -> names,ty
- | name = IDENT -> [name],CicNotationPt.Implicit
+ | name = IDENT -> [name],Ast.Implicit
]
];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
LIST0
[ id = IDENT ;
path = OPT [SYMBOL ":" ; path = term -> path ] ->
- (id,match path with Some p -> p | None -> CicNotationPt.UserInput) ]
+ (id,match path with Some p -> p | None -> Ast.UserInput) ]
SEP SYMBOL ";";
goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
let goal_path =
match goal_path with
- None -> CicNotationPt.UserInput
+ None -> Ast.UserInput
| Some goal_path -> goal_path
in
hyp_paths,goal_path
] ->
let wanted,hyp_paths,goal_path =
match wanted_and_sps with
- wanted,None -> wanted, [], CicNotationPt.UserInput
+ wanted,None -> wanted, [], Ast.UserInput
| wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
in
wanted, hyp_paths, goal_path ] ->
match res with
- None -> None,[],CicNotationPt.UserInput
+ None -> None,[],Ast.UserInput
| Some ps -> ps]
];
direction: [
]
];
argument: [
- [ id = IDENT -> CicNotationPt.IdentArg (0, id)
+ [ id = IDENT -> Ast.IdentArg (0, id)
| l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
SYMBOL "."; id = IDENT ->
- CicNotationPt.IdentArg (List.length l, id)
+ Ast.IdentArg (List.length l, id)
]
];
associativity: [
]
];
level3_term: [
- [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
- | id = IDENT -> CicNotationPt.VarPattern id
- | SYMBOL "_" -> CicNotationPt.ImplicitPattern
+ [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
+ | id = IDENT -> Ast.VarPattern id
+ | SYMBOL "_" -> Ast.ImplicitPattern
| LPAREN; terms = LIST1 SELF; RPAREN ->
(match terms with
| [] -> assert false
| [term] -> term
- | terms -> CicNotationPt.ApplPattern terms)
+ | terms -> Ast.ApplPattern terms)
]
];
interpretation: [
typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
GrafiteAst.Obj (loc,
GrafiteAst.Theorem
- (`Variant,name,typ,Some (CicNotationPt.Ident (newname, None))))
+ (`Variant,name,typ,Some (Ast.Ident (newname, None))))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
| flavour = theorem_flavour; name = IDENT;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
GrafiteAst.Obj (loc,
- GrafiteAst.Theorem (flavour, name, CicNotationPt.Implicit, body))
+ GrafiteAst.Theorem (flavour, name, Ast.Implicit, body))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
defs = CicNotationParser.let_defs ->
let name,ty =
match defs with
- | ((CicNotationPt.Ident (name, None), Some ty),_,_) :: _ -> name,ty
- | ((CicNotationPt.Ident (name, None), None),_,_) :: _ ->
- name, CicNotationPt.Implicit
+ | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
+ | ((Ast.Ident (name, None), None),_,_) :: _ ->
+ name, Ast.Implicit
| _ -> assert false
in
- let body = CicNotationPt.Ident (name,None) in
+ let body = Ast.Ident (name,None) in
GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty,
- Some (CicNotationPt.LetRec (ind_kind, defs, body))))
+ Some (Ast.LetRec (ind_kind, defs, body))))
| [ IDENT "inductive" ]; spec = inductive_spec ->
let (params, ind_types) = spec in
GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
in
GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
| IDENT "coercion" ; name = IDENT ->
- GrafiteAst.Coercion (loc, CicNotationPt.Ident (name,Some []))
+ GrafiteAst.Coercion (loc, Ast.Ident (name,Some []))
| IDENT "coercion" ; name = URI ->
- GrafiteAst.Coercion (loc, CicNotationPt.Uri (name,Some []))
+ GrafiteAst.Coercion (loc, Ast.Uri (name,Some []))
| IDENT "alias" ; spec = alias_spec ->
GrafiteAst.Alias (loc, spec)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
projects / helm.git / commitdiff