-module Ast = CicNotationPt
-module Env = CicNotationEnv
-module Pp = CicNotationPp
-module Util = CicNotationUtil
+module Ast = NotationPt
+module Env = NotationEnv
+module Pp = NotationPp
+module Util = NotationUtil
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
| _ -> PatternMatcher.Constructor
let tag_of_pattern = get_tag
let tag_of_term t = get_tag t
| _ -> PatternMatcher.Constructor
let tag_of_pattern = get_tag
let tag_of_term t = get_tag t
- let string_of_term = CicNotationPp.pp_term
- let string_of_pattern = CicNotationPp.pp_term
+
+ (* Debugging only *)
+ (*CSC: new NCicPp.status is the best I can do now *)
+ let string_of_term = NotationPp.pp_term (new NCicPp.status)
+ let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
| Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
- name, (Env.StringType, Env.StringValue s)
- | _ -> assert false)
+ name, (Env.StringType, Env.StringValue (Env.Ident s))
+ | _ -> assert false (* activate the DEBUGGING CODE below *))
and compile_magic = function
| Ast.Fold (kind, p_base, names, p_rec) ->
and compile_magic = function
| Ast.Fold (kind, p_base, names, p_rec) ->