X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=6bc494cdc5801be74a740972c16abf665dd60c9d;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=c7cc77be0a5f37b0978cdd817f4e239c1e46ce52;hpb=9230a8085102cd39258c047949e87001be6ffcf0;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index c7cc77be0..6bc494cdc 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -77,42 +77,32 @@ type binding = | Env of (string * value_type) list let make_action action bindings = - let rec aux (vl : env_type) = + let rec aux (vl : CicNotationEnv.t) = function - [] -> - prerr_endline "aux: make_action"; - Gramext.action (fun (loc: location) -> action vl loc) - | NoBinding :: tl -> - prerr_endline "aux: none"; - Gramext.action (fun _ -> aux vl tl) - (* LUCA: DEFCON 2 BEGIN *) + [] -> Gramext.action (fun (loc: location) -> action vl loc) + | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) + (* LUCA: DEFCON 5 BEGIN *) | Binding (name, TermType) :: tl -> - prerr_endline "aux: term"; Gramext.action - (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl) + (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl) | Binding (name, StringType) :: tl -> - prerr_endline "aux: string"; Gramext.action (fun (v:string) -> - aux ((name, (StringType, (StringValue v))) :: vl) tl) + aux ((name, (StringType, StringValue v)) :: vl) tl) | Binding (name, NumType) :: tl -> - prerr_endline "aux: num"; Gramext.action - (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl) + (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl) | Binding (name, OptType t) :: tl -> - prerr_endline "aux: opt"; Gramext.action (fun (v:'a option) -> - aux ((name, (OptType t, (OptValue v))) :: vl) tl) + aux ((name, (OptType t, OptValue v)) :: vl) tl) | Binding (name, ListType t) :: tl -> - prerr_endline "aux: list"; Gramext.action (fun (v:'a list) -> - aux ((name, (ListType t, (ListValue v))) :: vl) tl) + aux ((name, (ListType t, ListValue v)) :: vl) tl) | Env _ :: tl -> - prerr_endline "aux: env"; - Gramext.action (fun (v:env_type) -> aux (v @ vl) tl) - (* LUCA: DEFCON 2 END *) + Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) + (* LUCA: DEFCON 5 END *) in aux [] (List.rev bindings) @@ -160,7 +150,7 @@ let extract_term_production pattern = match magic with | Opt p -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : env_type option) (loc : location) = + let action (env_opt : CicNotationEnv.t option) (loc : location) = match env_opt with | Some env -> List.map opt_binding_some env | None -> List.map opt_binding_of_name p_names @@ -172,9 +162,8 @@ let extract_term_production pattern = | List0 (p, _) | 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 env0 = List.map list_binding_of_name p_names in let grow_env_entry env n v = - prerr_endline "grow_env_entry"; List.map (function | (n', (ty, ListValue vl)) as entry -> @@ -183,14 +172,12 @@ let extract_term_production pattern = env in let grow_env env_i env = - prerr_endline "grow_env"; List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env env_i - in - let action (env_list : env_type list) (loc : location) = - prerr_endline "list action"; - List.fold_right grow_env env_list env0 + in *) + let action (env_list : CicNotationEnv.t list) (loc : location) = + CicNotationEnv.coalesce_env p_names env_list in let g_symbol s = match magic with @@ -217,7 +204,8 @@ let extract_term_production pattern = let p_names = flatten_opt p_bindings in let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in let action = - make_action (fun (env : env_type) (loc : location) -> prerr_endline "inner action"; env) p_bindings + make_action (fun (env : CicNotationEnv.t) (loc : location) -> env) + p_bindings in p_bindings, p_atoms, p_names, action in @@ -247,7 +235,7 @@ let extend level1_pattern ?(precedence = default_precedence) associativity, [ p_atoms, (make_action - (fun (env: env_type) (loc: location) -> (action env loc)) + (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc)) p_bindings) ]]] in p_atoms @@ -256,10 +244,6 @@ let delete atoms = Grammar.delete_rule l2_pattern atoms (** {2 Grammar} *) -let boxify = function - | [ a ] -> a - | l -> Layout (Box (H, l)) - let fold_binder binder pt_names body = let fold_cluster binder terms ty body = List.fold_right @@ -341,7 +325,7 @@ EXTEND return_term loc (Layout (Box (V, p))) | SYMBOL "\\BREAK" -> return_term loc (Layout Break) | DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (boxify p) + return_term loc (CicNotationUtil.boxify p) | p = SELF; SYMBOL "\\AS"; id = IDENT -> return_term loc (Variable (Ascription (p, id))) ] @@ -509,8 +493,9 @@ EXTEND [ "90" NONA [ 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 -> prerr_endline "number"; return_term loc (Num (n, 0)) + | n = NUMBER -> return_term loc (Num (n, 0)) | IMPLICIT -> return_term loc (Implicit) | m = META -> return_term loc (Meta (int_of_string m, [])) | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s)) @@ -536,15 +521,15 @@ EXTEND (* }}} *) (* {{{ Grammar for interpretation, notation level 3 *) argument: [ - [ id = IDENT -> IdentArg id - | SYMBOL <:unicode> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a) - | SYMBOL <:unicode> (* η *); id = IDENT; SYMBOL "."; a = SELF -> - EtaArg (Some id, a) + [ id = IDENT -> IdentArg (0, id) + | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; + SYMBOL "."; id = IDENT -> + IdentArg (List.length l, id) ] ]; level3_term: [ [ u = URI -> UriPattern u - | a = argument -> ArgPattern a + | id = IDENT -> VarPattern id | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> (match terms with | [] -> assert false @@ -564,25 +549,26 @@ EXTEND [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ - [ IDENT "notation"; - p1 = level1_pattern; + [ p1 = level1_pattern; assoc = OPT associativity; prec = OPT precedence; IDENT "for"; p2 = level2_pattern -> (p1, assoc, prec, p2) ] ]; interpretation: [ - [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as"; - t = level3_term -> - () + [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> + (s, args, t) ] ]; (* }}} *) (* {{{ Top-level phrases *) phrase: [ [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2 - | (l1, assoc, prec, l2) = notation; SYMBOL "." -> + | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." -> Notation (l1, assoc, prec, l2) + | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." -> + Interpretation ((symbol, args), l3) + | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u) ] ]; (* }}} *)