open Printf
+module Ast = CicNotationPt
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
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;
| t -> t
let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t)
+
let add_keyword_attrs =
add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+
let box kind spacing indent content =
Ast.Layout (Ast.Box ((kind, spacing, indent), content))
+
let hbox = box Ast.H
let vbox = box Ast.V
let hvbox = box Ast.HV
let hovbox = box Ast.HOV
let break = Ast.Layout Ast.Break
-let reset_href t = Ast.AttributedTerm (`Href [], t)
-let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
-let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
+let builtin_symbol s = Ast.Literal (`Symbol s)
+let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
+
let number s =
- reset_href
- (add_xml_attrs (RenderingAttrs.number_attributes `MathML)
- (Ast.Literal (`Number s)))
+ add_xml_attrs (RenderingAttrs.number_attributes `MathML)
+ (Ast.Literal (`Number s))
+
let ident i =
add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+
+let ident_w_href href i =
+ match href with
+ | None -> ident i
+ | Some href -> Ast.AttributedTerm (`Href [href], ident i)
+
let binder_symbol s =
add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
(builtin_symbol s)
| `Type -> "Type"
let pp_ast0 t k =
- let rec aux = function
+ let rec aux =
+ function
| Ast.Appl ts ->
add_level_info Ast.apply_prec Ast.apply_assoc
(hovbox true true (CicNotationUtil.dress break (List.map k ts)))
let indty_box =
match indty_opt with
| None -> []
- | Some indty -> [ keyword "in"; ident indty ]
+ | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ]
in
let match_box =
hvbox false true [
hvbox false false ([ k what ] @ indty_box); break;
keyword "with" ]
in
- let mk_case_pattern (head, vars) =
- hbox true false (ident head :: List.map aux_var vars)
+ let mk_case_pattern (head, href, vars) =
+ hbox true false (ident_w_href href head :: List.map aux_var vars)
in
let patterns' =
List.map
hvbox false true [
aux_var var; builtin_symbol "\\def"; break; k s ];
break; keyword "in" ];
+ break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
let rec_op =
| Cic.AMutInd (id,uri,i,substs) as t ->
let name = name_of_inductive_type uri i in
let uri_str = UriManager.string_of_uri uri in
- let puri_str =
- uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")"
- in
+ let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in
register_uri id puri_str;
idref id (Ast.Ident (name, aux_substs substs))
| Cic.AMutConstruct (id,uri,i,j,substs) ->
idref id (Ast.Ident (name, aux_substs substs))
| Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
let name = name_of_inductive_type uri typeno in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
+ let ctor_puri j =
+ UriManager.uri_of_string
+ (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
+ in
+ let case_indty = name, Some (UriManager.uri_of_string puri_str) in
let constructors = constructors_of_inductive_type uri typeno in
let rec eat_branch ty pat =
match (ty, pat) with
(CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
| _, _ -> [], k pat
in
+ let j = ref 0 in
let patterns =
- List.map2
- (fun (name, ty) pat ->
- let (capture_variables, rhs) = eat_branch ty pat in
- ((name, capture_variables), rhs))
- constructors patterns
+ try
+ List.map2
+ (fun (name, ty) pat ->
+ incr j;
+ let (capture_variables, rhs) = eat_branch ty pat in
+ ((name, Some (ctor_puri !j), capture_variables), rhs))
+ constructors patterns
+ with Invalid_argument _ -> assert false
in
- idref id (Ast.Case (k te, Some name, Some (k ty), patterns))
+ idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))
| Cic.AFix (id, no, funs) ->
let defs =
List.map
let ty, value =
try
List.assoc name env
- with Not_found -> assert false
+ with Not_found ->
+ prerr_endline ("name " ^ name ^ " not found in environment");
+ assert false
in
assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
assert (CicNotationEnv.well_typed expected_ty value);
[ CicNotationEnv.term_of_value value ]
| Ast.Magic m -> subst_magic env m
- | Ast.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ]
- | Ast.Literal _ as t -> [ (*reset_href*) t ]
+ | Ast.Literal (`Keyword k) as t -> [ add_keyword_attrs t ]
+ | Ast.Literal _ as t -> [ t ]
| Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
| t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
and subst_magic env = function
instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list
- (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
+ let terms = subst env p in
+ instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
instantiate_list [] values
| Ast.Opt p ->
let ast_env_of_env env =
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
- match term with
- | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
- | _ ->
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
- let prec, assoc, l1 =
- try
- Hashtbl.find level1_patterns21 pid
- with Not_found -> assert false
- in
- add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
+ (match (get_compiled21 ()) term with
+ | None -> pp_ast0 term pp_ast1
+ | Some (env, pid) ->
+ let prec, assoc, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
| Ast.IdentArg (n, name) ->
let t = (try List.assoc name env with Not_found -> assert false) in
let rec count_lambda = function
+ | Ast.AttributedTerm (_, t) -> count_lambda t
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
| _ -> 0
in
set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
let ast_of_acic id_to_sort annterm =
+ debug_print (lazy ("ast_of_acic <- "
+ ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast = ast_of_acic1 term_info annterm in
+ debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
ast, term_info.uri
-let pp_ast term =
-(* prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *)
- pp_ast1 term
+let pp_ast ast =
+ debug_print (lazy "pp_ast <-");
+ let ast' = pp_ast1 ast in
+ debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
+ ast'
let fresh_id =
let counter = ref ~-1 in
projects / helm.git / blobdiff