From: Stefano Zacchiroli Date: Mon, 5 Sep 2005 15:55:46 +0000 (+0000) Subject: use uniform naming for referencing cicNotation* modules X-Git-Tag: V_0_1_2_1~95 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git use uniform naming for referencing cicNotation* modules --- diff --git a/helm/ocaml/cic_notation/box.ml b/helm/ocaml/cic_notation/box.ml index 241214f9c..7c4026d81 100644 --- a/helm/ocaml/cic_notation/box.ml +++ b/helm/ocaml/cic_notation/box.ml @@ -1,4 +1,4 @@ -(* 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 diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index f914b01d2..9a4a8e20b 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -23,10 +23,10 @@ * 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 @@ -94,19 +94,19 @@ let opt_declaration (n, ty) = (n, OptType ty) 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 *) diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 4f17e8049..1c83c2c45 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -25,8 +25,8 @@ 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 *) @@ -100,7 +100,8 @@ let unopt_names names env = 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 *) @@ -112,7 +113,8 @@ let head_names names env = 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 *) @@ -124,8 +126,8 @@ let tail_names names env = 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 @@ -144,31 +146,34 @@ let instantiate_level2 env term = 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 @@ -185,25 +190,25 @@ let instantiate_level2 env term = 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) @@ -213,17 +218,19 @@ let instantiate_level2 env term = | [] -> 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) @@ -233,18 +240,20 @@ let instantiate_level2 env term = | [] -> 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 @@ -257,10 +266,10 @@ let instantiate_appl_pattern env appl_pattern = 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 diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index b9809335c..a10d0a8bd 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -25,9 +25,9 @@ open Printf -module Pp = CicNotationPp -module Pt = CicNotationPt +module Ast = CicNotationPt module Env = CicNotationEnv +module Pp = CicNotationPp module Util = CicNotationUtil type pattern_id = int @@ -193,14 +193,14 @@ module Matcher21 = 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 @@ -213,14 +213,14 @@ struct 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 @@ -230,11 +230,11 @@ struct 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 @@ -291,7 +291,7 @@ struct 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 @@ -321,7 +321,7 @@ struct | 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 @@ -331,7 +331,7 @@ struct | 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 @@ -345,7 +345,7 @@ struct | None -> None | Some (env', _) -> Some (env' @ env)) - | Pt.Fail -> (fun _ _ -> None) + | Ast.Fail -> (fun _ _ -> None) | _ -> assert false end @@ -374,23 +374,23 @@ struct 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) @@ -403,8 +403,8 @@ struct 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 diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 7c52560be..13817e248 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -25,8 +25,8 @@ 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 @@ -70,33 +70,35 @@ let gram_of_literal = 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 *) @@ -116,11 +118,11 @@ let flatten_opt = (* 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 @@ -132,35 +134,35 @@ let extract_term_production pattern = [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 = @@ -176,34 +178,34 @@ let extract_term_production pattern = (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 @@ -240,7 +242,8 @@ let extend level1_pattern ~precedence ~associativity 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 @@ -265,7 +268,7 @@ let parse_level2_meta_ref = ref (fun _ -> assert false) 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 = @@ -273,7 +276,7 @@ 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 = @@ -310,56 +313,56 @@ EXTEND (* 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 @@ -369,29 +372,30 @@ EXTEND 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) ] ]; @@ -448,23 +452,23 @@ EXTEND 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." ] ]; @@ -493,7 +497,7 @@ EXTEND 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 @@ -513,12 +517,12 @@ EXTEND 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) ] @@ -526,10 +530,10 @@ EXTEND term: LEVEL "10N" [ (* let in *) [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); 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 *) @@ -542,26 +546,28 @@ EXTEND [ [ 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 ]; @@ -572,9 +578,9 @@ EXTEND 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) ] diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 9118d1c11..d51d1a65e 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -25,8 +25,8 @@ 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. @@ -53,34 +53,34 @@ let pp_literal = function (* debugging version *) 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 " @@ -89,30 +89,30 @@ let rec pp_term ?(pp_parens = true) t = 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 @@ -139,43 +139,46 @@ and pp_capture_variable = function 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" @@ -186,29 +189,29 @@ and pp_sep_opt = function | 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 "; " diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index c66566613..8d548e1eb 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -23,9 +23,10 @@ * 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 @@ -104,22 +105,22 @@ let box_of mathonly spec attrs children = @ 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)) @@ -151,15 +152,15 @@ let pp_pos = 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 _ @@ -193,7 +194,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t = 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 @@ -227,20 +228,20 @@ let render ids_to_uris = (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 @@ -252,8 +253,8 @@ let render ids_to_uris = (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 ]) @@ -264,15 +265,15 @@ let render ids_to_uris = 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 *) @@ -318,23 +319,23 @@ let render ids_to_uris = 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 diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 28edd491c..3145981b4 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -25,12 +25,12 @@ 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; diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml index 37579c827..53ac5e2d1 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.ml +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -23,20 +23,20 @@ * 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 diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index e4145e118..a7d7e733d 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -23,105 +23,41 @@ * 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) @@ -135,27 +71,27 @@ let visit_ast ?(special_k = fun _ -> assert false) k = 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 @@ -164,29 +100,29 @@ let variables_of_term t = 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) @@ -195,14 +131,14 @@ let keywords_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) ; @@ -210,9 +146,9 @@ let keywords_of_term 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 @@ -224,33 +160,33 @@ let meta_names_of_term term = 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 @@ -268,21 +204,21 @@ let meta_names_of_term 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 + | 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 ; @@ -317,21 +253,21 @@ let string_of_literal = function 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 [] @@ -357,33 +293,35 @@ let dressn ~sep:sauces = 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 diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index fb654529b..82d904989 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -23,11 +23,13 @@ * 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 @@ -111,19 +113,19 @@ type alias_spec = | 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 @@ -138,12 +140,12 @@ type ('term,'obj) command = | 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 *) diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index 7d1f8c22e..0c63d2594 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -27,6 +27,8 @@ open Printf open GrafiteAst +module Ast = CicNotationPt + let tactical_terminator = "." let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator @@ -239,7 +241,7 @@ let pp_obj = function 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." @@ -247,10 +249,10 @@ let pp_argument_pattern = function 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 diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index c138fce27..ae7e5229d 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -25,12 +25,14 @@ 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 @@ -40,7 +42,7 @@ EXTEND 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) ] ]; @@ -63,12 +65,12 @@ EXTEND 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>; 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 @@ -86,12 +88,12 @@ EXTEND ] -> 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: [ @@ -349,10 +351,10 @@ EXTEND ] ]; argument: [ - [ id = IDENT -> CicNotationPt.IdentArg (0, id) + [ id = IDENT -> Ast.IdentArg (0, id) | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; SYMBOL "."; id = IDENT -> - CicNotationPt.IdentArg (List.length l, id) + Ast.IdentArg (List.length l, id) ] ]; associativity: [ @@ -394,14 +396,14 @@ EXTEND ] ]; 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: [ @@ -418,26 +420,26 @@ EXTEND typ = term; SYMBOL <:unicode> ; 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> (* ≝ *); body = term -> body ] -> GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body)) | flavour = theorem_flavour; name = IDENT; body = OPT [ SYMBOL <:unicode> (* ≝ *); 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)) @@ -449,9 +451,9 @@ EXTEND 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 ->