X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=09fd55b0d4bae7c890c6eb98599fbf6d3e9aa034;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=b0529dd7a570d82d72f458189130fbb0dd7d845a;hpb=2e41c32bf536719437749de627c7e034f5852f83;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index b0529dd7a..09fd55b0d 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -33,6 +33,7 @@ let grammar = Grammar.gcreate CicNotationLexer.notation_lexer let level1_pattern = Grammar.Entry.create grammar "level1_pattern" let level2_pattern = Grammar.Entry.create grammar "level2_pattern" let level3_term = Grammar.Entry.create grammar "level3_term" +let l2_pattern = Grammar.Entry.create grammar "l2_pattern" let notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *) let interpretation = Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *) @@ -73,6 +74,7 @@ let return_term loc term = AttributedTerm (`Loc loc, term) EXTEND GLOBAL: level1_pattern level2_pattern level3_term + l2_pattern notation interpretation; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ]; @@ -140,7 +142,7 @@ EXTEND ]; (* }}} *) (* {{{ Grammar for ast patterns, notation level 2 *) - level2_pattern: [ [ p = l2_pattern -> p ] ]; + level2_pattern: [ [ p = l2_pattern; EOI -> p ] ]; sort: [ [ SYMBOL "\\PROP" -> `Prop | SYMBOL "\\SET" -> `Set @@ -276,12 +278,11 @@ EXTEND [ id = IDENT -> return_term loc (Ident (id, None)) | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s)) | u = URI -> return_term loc (Uri (u, None)) - | n = NUMBER -> return_term loc (Num (n, 0)) + | n = NUMBER -> prerr_endline "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_subst -> return_term loc (Meta (int_of_string m, s)) | s = sort -> return_term loc (Sort s) - | s = SYMBOL -> return_term loc (Symbol (s, 0)) | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ]; IDENT "match"; t = l2_pattern; indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; @@ -372,18 +373,66 @@ let term = Gramext.Sself type env_type = (string * (value_type * value)) list -let make_action action = +let rec pp_value = + function + | TermValue _ -> "@TERM@" + | 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)) + +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 + +let pp_env env = + String.concat "; " + (List.map + (fun (name, (ty, value)) -> + sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value)) + env) + +let make_action action bindings = let rec aux (vl : env_type) = function - [] -> Gramext.action (fun (loc: location) -> action vl loc) - | None :: tl -> Gramext.action (fun _ -> aux vl tl) - | Some (name, typ) :: tl -> - (* i tipi servono? Magari servono solo quando si verifica la - * correttezza della notazione? - *) - Gramext.action (fun (v: value) -> aux ((name, (typ, v))::vl) tl) + [] -> + prerr_endline "aux: make_action"; + Gramext.action (fun (loc: location) -> action vl loc) + | None :: tl -> + prerr_endline "aux: none"; + Gramext.action (fun _ -> aux vl tl) + (* LUCA: DEFCON 3 BEGIN *) + | Some (name, TermType) :: tl -> + prerr_endline "aux: term"; + Gramext.action + (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl) + | Some (name, StringType) :: tl -> + prerr_endline "aux: string"; + Gramext.action + (fun (v:string) -> + aux ((name, (StringType, (StringValue v))) :: vl) tl) + | Some (name, NumType) :: tl -> + prerr_endline "aux: num"; + Gramext.action + (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl) + | Some (name, OptType t) :: tl -> + prerr_endline "aux: opt"; + Gramext.action + (fun (v:'a option) -> + aux ((name, (OptType t, (OptValue v))) :: vl) tl) + | Some (name, ListType t) :: tl -> + prerr_endline "aux: list"; + Gramext.action + (fun (v:'a list) -> + aux ((name, (ListType t, (ListValue v))) :: vl) tl) + (* LUCA: DEFCON 3 END *) in - aux [] + aux [] (List.rev bindings) let flatten_opt = let rec aux acc = @@ -429,17 +478,21 @@ let extract_term_production pattern = (Gramext.srules [ p_atoms, (make_action - (fun (env : env_type) (loc : location) -> env) + (fun (env : env_type) (loc : location) -> + prerr_endline "inner opt action"; + env) p_bindings)])], Gramext.action (fun (env_opt : env_type option) (loc : location) -> match env_opt with Some env -> + prerr_endline "opt action (Some _)"; List.map (fun (name, (typ, v)) -> (name, (OptType typ, OptValue (Some v)))) env | None -> + prerr_endline "opt action (None)"; List.map (fun (name, typ) -> (name, (OptType typ, OptValue None))) @@ -460,7 +513,7 @@ let level_of_int precedence = raise (Level_not_found precedence); string_of_int precedence -type rule_id = term Grammar.Entry.e * Token.t Gramext.g_symbol list +type rule_id = Token.t Gramext.g_symbol list let extend level1_pattern ?(precedence = 0) ?associativity action = let p_bindings, p_atoms = @@ -468,23 +521,25 @@ let extend level1_pattern ?(precedence = 0) ?associativity action = in let level = level_of_int precedence in let p_names = flatten_opt p_bindings in - let entry = Grammar.Entry.obj (level2_pattern: 'a Grammar.Entry.e) in + let entry = Grammar.Entry.obj (l2_pattern: 'a Grammar.Entry.e) in let _ = + prerr_endline (string_of_int (List.length p_bindings)); Grammar.extend [ entry, Some (Gramext.Level level), [ Some level, (* TODO should we put None here? *) associativity, [ p_atoms, (make_action - (fun (env: env_type)(loc: location) -> TermValue (action env loc)) + (fun (env: env_type) (loc: location) -> (action env loc)) p_bindings) ]]] in - (level2_pattern, p_atoms) + p_atoms -let delete (entry, atoms) = Grammar.delete_rule entry atoms +let delete atoms = Grammar.delete_rule l2_pattern atoms -let print_level2_pattern () = - Grammar.print_entry Format.std_formatter (Grammar.Entry.obj level2_pattern); - Format.pp_print_flush Format.std_formatter () +let print_l2_pattern () = + Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern); + Format.pp_print_flush Format.std_formatter (); + flush stdout (* vim:set encoding=utf8 foldmethod=marker: *)