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
| Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t)
| t -> t
-let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t)
+let add_xml_attrs attrs t =
+ if attrs = [] then t else 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 reset_href t = 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 ->
+ let href = UriManager.string_of_uri href in
+ add_xml_attrs [Some "xlink", "href", href] (ident i)
+
let binder_symbol s =
add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
(builtin_symbol s)
| `Prop -> "Prop"
| `Set -> "Set"
| `CProp -> "CProp"
- | `Type -> "Type"
+ | `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 =
let ast_of_acic0 term_info acic k =
let k = k term_info in
- let register_uri id uri = Hashtbl.add term_info.uri id uri in
+ let id_to_uris = term_info.uri in
+ let register_uri id uri = Hashtbl.add id_to_uris id uri in
let sort_of_id id =
try
Hashtbl.find term_info.sort id
with Not_found ->
prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
- `Type
+ `Type (CicUniv.fresh ())
in
let aux_substs substs =
Some
| Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
- | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
+ | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
| Cic.AImplicit _ -> assert false
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
- | `Set | `Type -> `Pi
+ | `Set | `Type _ -> `Pi
| `Prop | `CProp -> `Forall
in
idref id (Ast.Binder (binder_kind,
| 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 set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
-let instantiate21 env (* precedence associativity *) l1 =
- let rec subst_singleton env t =
- CicNotationUtil.group (subst env t)
+let add_idrefs =
+ List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+
+let instantiate21 idrefs env l1 =
+ let rec subst_singleton env =
+ function
+ Ast.AttributedTerm (attr, t) ->
+ Ast.AttributedTerm (attr, subst_singleton env t)
+ | t -> CicNotationUtil.group (subst env t)
and subst env = function
- | Ast.AttributedTerm (_, t) -> subst env t
+ | Ast.AttributedTerm (attr, t) as term ->
+ subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
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 l as t ->
+ let t = add_idrefs idrefs t in
+ (match l with
+ | `Keyword k -> [ add_keyword_attrs 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
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
match term with
- | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
+ | Ast.AttributedTerm (attrs, term') ->
+ Ast.AttributedTerm (attrs, pp_ast1 term')
| _ ->
(match (get_compiled21 ()) term with
| None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
+ | Some (env, ctors, pid) ->
+ let idrefs =
+ List.flatten (List.map CicNotationUtil.get_idrefs ctors)
+ in
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))
+ add_level_info prec assoc
+ (instantiate21 idrefs (ast_env_of_env env) l1))
-let instantiate32 term_info env symbol args =
+let instantiate32 term_info idrefs 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
in
add_lambda t (n - count_lambda t)
in
- let head = Ast.Symbol (symbol, 0) in
- match args with
- | [] -> head
- | _ -> Ast.Appl (head :: List.map instantiate_arg args)
+ let head =
+ let symbol = Ast.Symbol (symbol, 0) in
+ add_idrefs idrefs symbol
+ in
+ if args = [] then head
+ else Ast.Appl (head :: List.map instantiate_arg args)
let rec ast_of_acic1 term_info annterm =
+ let id_to_uris = term_info.uri in
+ let register_uri id uri = Hashtbl.add id_to_uris id uri in
match (get_compiled32 ()) annterm with
| None -> ast_of_acic0 term_info annterm ast_of_acic1
- | Some (env, pid) ->
+ | Some (env, ctors, pid) ->
+ let idrefs =
+ List.map
+ (fun annterm ->
+ let idref = CicUtil.id_of_annterm annterm in
+ (try
+ register_uri idref
+ (UriManager.string_of_uri
+ (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)))
+ with Invalid_argument _ -> ());
+ idref)
+ ctors
+ in
let env' =
List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
in
- let _, symbol, args, _, uris =
+ let _, symbol, args, _ =
try
Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
in
- let ast = instantiate32 term_info env' symbol args in
- Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm),
- (match uris with
- | [] -> ast
- | _ -> Ast.AttributedTerm (`Href uris, ast)))
+ let ast = instantiate32 term_info idrefs env' symbol args in
+ Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast)
let load_patterns32 t =
set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
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
let add_interpretation dsc (symbol, args) appl_pattern =
let id = fresh_id () in
- let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
- Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris);
+ Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern);
pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
load_patterns32 !pattern32_matrix;
(try
(List.sort Pervasives.compare
(List.map
(fun id ->
- let (dsc, _, args, appl_pattern, _) =
+ let (dsc, _, args, appl_pattern) =
try
Hashtbl.find level2_patterns32 id
with Not_found -> assert false
let remove_interpretation id =
(try
- let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in
+ let _, symbol, _, _ = Hashtbl.find level2_patterns32 id in
let ids = Hashtbl.find interpretations symbol in
ids := List.filter ((<>) id) !ids;
Hashtbl.remove level2_patterns32 id;
projects / helm.git / blobdiff