Quelle constrexpr_ops.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Libnames
open Glob_term
open Notationextern
open Constrexpr

(***********)
(* Universes *)

let expr_Type_sort = None, UAnonymous {rigid=UnivRigid}
let expr_SProp_sort = None, UNamed [CSProp, 0]
let expr_Prop_sort = None, UNamed [CProp, 0]
let expr_Set_sort = None, UNamed [CSet, 0]

let sort_name_expr_eq c1 c2 = match c1, c2 with
  | CSProp, CSProp
  | CProp, CProp
  | CSet, CSet -> true
  | CType q1, CType q2 -> Libnames.qualid_eq q1 q2
  | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2
  | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false

let qvar_expr_eq c1 c2 = match c1, c2 with
  | CQVar q1, CQVar q2 -> Libnames.qualid_eq q1 q2
  | CQAnon _, CQAnon _ -> true
  | CRawQVar q1, CRawQVar q2 -> Sorts.QVar.equal q1 q2
  | (CQVar _ | CQAnon _ | CRawQVar _), _ -> false

let quality_expr_eq q1 q2 = match q1, q2 with
  | CQConstant q1, CQConstant q2 -> Sorts.Quality.Constants.equal q1 q2
  | CQualVar q1, CQualVar q2 -> qvar_expr_eq q1 q2
  | (CQConstant _ | CQualVar _), _ -> false

let relevance_expr_eq a b = match a, b with
  | CRelevant, CRelevant | CIrrelevant, CIrrelevant -> true
  | CRelevanceVar q1, CRelevanceVar q2 -> qvar_expr_eq q1 q2
  | (CRelevant | CIrrelevant | CRelevanceVar _), _ -> false

let relevance_info_expr_eq = Option.equal relevance_expr_eq

let univ_level_expr_eq u1 u2 =
  Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2

let sort_expr_eq (q1, l1) (q2, l2) =
  Option.equal qvar_expr_eq q1 q2 &&
  Glob_ops.glob_sort_gen_eq
    (List.equal (fun (x,m) (y,n) ->
      sort_name_expr_eq x y
      && Int.equal m n))
    l1 l2

let instance_expr_eq (q1,u1) (q2,u2) =
  List.equal quality_expr_eq q1 q2 && List.equal univ_level_expr_eq u1 u2

(***********************)
(* For binders parsing *)

let binder_kind_eq b1 b2 = match b1, b2 with
| Default bk1, Default bk2 -> Glob_ops.binding_kind_eq bk1 bk2
| Generalized (ck1, b1), Generalized (ck2, b2) ->
  Glob_ops.binding_kind_eq ck1 ck2 &&
  (if b1 then b2 else not b2)
| (Default _ | Generalized _), _ -> false

let default_binder_kind = Default Explicit

let names_of_local_assums bl =
  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|_->[]) bl)

let names_of_local_binders bl =
  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|CLocalDef(l,_,_,_)->[l]|CLocalPattern _ -> assert false) bl)

(**********************************************************************)
(* Functions on constr_expr *)

(* Note: redundant Number representations, such as -0 and +0 (and others),
   are considered different here. *)

let prim_token_eq t1 t2 = match t1, t2 with
| Number n1, Number n2 -> NumTok.Signed.equal n1 n2
| String s1, String s2 -> String.equal s1 s2
| (Number _ | String _), _ -> false

let explicitation_eq pos1 pos2 = match pos1, pos2 with
| ExplByName id1, ExplByName id2 -> Id.equal id1 id2
| ExplByPos n1, ExplByPos n2 -> Int.equal n1 n2
| (ExplByName _ | ExplByPos _), _ -> false

let rec cases_pattern_expr_eq p1 p2 =
  if CAst.(p1.v == p2.v) then true
  else match CAst.(p1.v, p2.v) with
  | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
      CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
  | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
      qualid_eq c1 c2 &&
      Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
      List.equal cases_pattern_expr_eq b1 b2
  | CPatAtom(r1), CPatAtom(r2) ->
    Option.equal qualid_eq r1 r2
  | CPatOr a1, CPatOr a2 ->
    List.equal cases_pattern_expr_eq a1 a2
  | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) ->
    Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
    notation_eq n1 n2 &&
    cases_pattern_notation_substitution_eq s1 s2 &&
    List.equal cases_pattern_expr_eq l1 l2
  | CPatPrim i1, CPatPrim i2 ->
    prim_token_eq i1 i2
  | CPatRecord l1, CPatRecord l2 ->
    let equal (r1, e1) (r2, e2) =
      qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2
    in
    List.equal equal l1 l2
  | CPatDelimiters(depth1,s1,e1), CPatDelimiters(depth2,s2,e2) ->
    depth1 = depth2 && String.equal s1 s2 && cases_pattern_expr_eq e1 e2
  | _ -> false

and cases_pattern_notation_substitution_eq (s1, n1, b1) (s2, n2, b2) =
  List.equal cases_pattern_expr_eq s1 s2 &&
  List.equal (List.equal cases_pattern_expr_eq) n1 n2 &&
  List.equal (eq_pair cases_pattern_expr_eq Glob_ops.binding_kind_eq) b1 b2

let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) =
  cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2

(* We use a functor to avoid passing the recursion all over the place *)
module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end) = struct

  open A
  let args_eq (a1,e1) (a2,e2) =
    Option.equal (CAst.eq explicitation_eq) e1 e2 &&
    constr_expr_eq a1 a2

  let case_expr_eq (e1, n1, p1) (e2, n2, p2) =
    constr_expr_eq e1 e2 &&
    Option.equal (CAst.eq Name.equal) n1 n2 &&
    Option.equal cases_pattern_expr_eq p1 p2

  let branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
    List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
    constr_expr_eq e1 e2

  let recursion_order_expr_eq_r r1 r2 = match r1, r2 with
    | CStructRec i1, CStructRec i2 -> lident_eq i1 i2
    | CWfRec (i1,e1), CWfRec (i2,e2) ->
      constr_expr_eq e1 e2
    | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
      Option.equal lident_eq i1 i2 &&
      constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
    | _ -> false

  let recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2

  let local_binder_eq l1 l2 = match l1, l2 with
    | CLocalDef (n1, _, e1, t1), CLocalDef (n2, _, e2, t2) ->
      CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
    | CLocalAssum (n1, _, _, e1), CLocalAssum (n2, _, _, e2) ->
      (* Don't care about the metadata *)
      List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2
    | _ -> false

  let fix_expr_eq (id1,_,r1,bl1,a1,b1) (id2,_,r2,bl2,a2,b2) =
    (lident_eq id1 id2) &&
    Option.equal recursion_order_expr_eq r1 r2 &&
    List.equal local_binder_eq bl1 bl2 &&
    constr_expr_eq a1 a2 &&
    constr_expr_eq b1 b2

  let cofix_expr_eq (id1,_,bl1,a1,b1) (id2,_,bl2,a2,b2) =
    (lident_eq id1 id2) &&
    List.equal local_binder_eq bl1 bl2 &&
    constr_expr_eq a1 a2 &&
    constr_expr_eq b1 b2

  let constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
    List.equal constr_expr_eq e1 e2 &&
    List.equal (List.equal constr_expr_eq) el1 el2 &&
    List.equal kinded_cases_pattern_expr_eq b1 b2 &&
    List.equal (List.equal local_binder_eq) bl1 bl2

  let instance_eq (x1,c1) (x2,c2) =
    Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2

  let constr_expr_eq e1 e2 =
    if CAst.(e1.v == e2.v) then true
    else match CAst.(e1.v, e2.v) with
      | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && Option.equal instance_expr_eq u1 u2
      | CFix(id1,fl1), CFix(id2,fl2) ->
        lident_eq id1 id2 &&
        List.equal fix_expr_eq fl1 fl2
      | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
        lident_eq id1 id2 &&
        List.equal cofix_expr_eq fl1 fl2
      | CProdN(bl1,a1), CProdN(bl2,a2) ->
        List.equal local_binder_eq bl1 bl2 &&
        constr_expr_eq a1 a2
      | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
        List.equal local_binder_eq bl1 bl2 &&
        constr_expr_eq a1 a2
      | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
        CAst.eq Name.equal na1 na2 &&
        constr_expr_eq a1 a2 &&
        Option.equal constr_expr_eq t1 t2 &&
        constr_expr_eq b1 b2
      | CAppExpl((r1,u1),al1), CAppExpl((r2,u2),al2) ->
        qualid_eq r1 r2 &&
        Option.equal instance_expr_eq u1 u2 &&
        List.equal constr_expr_eq al1 al2
      | CApp(e1,al1), CApp(e2,al2) ->
        constr_expr_eq e1 e2 &&
        List.equal args_eq al1 al2
      | CProj(e1,(p1,u1),al1,c1), CProj(e2,(p2,u2),al2,c2) ->
        e1 = (e2:bool) &&
        qualid_eq p1 p2 &&
        Option.equal instance_expr_eq u1 u2 &&
        List.equal args_eq al1 al2 &&
        constr_expr_eq c1 c2
      | CRecord l1, CRecord l2 ->
        let field_eq (r1, e1) (r2, e2) =
          qualid_eq r1 r2 && constr_expr_eq e1 e2
        in
        List.equal field_eq l1 l2
      | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
        (* Don't care about the case_style *)
        Option.equal constr_expr_eq r1 r2 &&
        List.equal case_expr_eq a1 a2 &&
        List.equal branch_expr_eq brl1 brl2
      | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
        List.equal (CAst.eq Name.equal) n1 n2 &&
        Option.equal (CAst.eq Name.equal) m1 m2 &&
        Option.equal constr_expr_eq e1 e2 &&
        constr_expr_eq t1 t2 &&
        constr_expr_eq b1 b2
      | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
        constr_expr_eq e1 e2 &&
        Option.equal (CAst.eq Name.equal) n1 n2 &&
        Option.equal constr_expr_eq r1 r2 &&
        constr_expr_eq t1 t2 &&
        constr_expr_eq f1 f2
      | CHole _, CHole _ -> true
      | (CGenarg _ | CGenargGlob _), (CGenarg _ | CGenargGlob _) -> true
      | CPatVar i1, CPatVar i2 ->
        Id.equal i1 i2
      | CEvar (id1, c1), CEvar (id2, c2) ->
        Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
      | CSort s1, CSort s2 ->
        sort_expr_eq s1 s2
      | CCast(c1,k1,t1), CCast(c2,k2,t2) ->
        constr_expr_eq c1 c2 && Option.equal Glob_ops.cast_kind_eq k1 k2 && constr_expr_eq t1 t2
      | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
        Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
        notation_eq n1 n2 &&
        constr_notation_substitution_eq s1 s2
      | CPrim i1, CPrim i2 ->
        prim_token_eq i1 i2
      | CGeneralization (bk1, e1), CGeneralization (bk2, e2) ->
        Glob_ops.binding_kind_eq bk1 bk2 &&
        constr_expr_eq e1 e2
      | CDelimiters(depth1,s1,e1), CDelimiters(depth2,s2,e2) ->
        depth1 = depth2 &&
        String.equal s1 s2 &&
        constr_expr_eq e1 e2
      | CArray(u1,t1,def1,ty1), CArray(u2,t2,def2,ty2) ->
        Array.equal constr_expr_eq t1 t2 &&
        constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 &&
        Option.equal instance_expr_eq u1 u2
      | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
        | CApp _ | CProj _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
        | CGenarg _ | CGenargGlob _
        | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
        | CGeneralization _ | CDelimiters _ | CArray _), _ -> false

end

let constr_expr_eq_gen eq =
  let module Eq = EqGen(struct let constr_expr_eq = eq end) in
  Eq.constr_expr_eq

module Eq = EqGen(struct
    let rec constr_expr_eq c1 c2 = constr_expr_eq_gen constr_expr_eq c1 c2
  end)
include Eq

let constr_loc c = CAst.(c.loc)
let cases_pattern_expr_loc cp = CAst.(cp.loc)

let local_binder_loc = let open CAst in function
  | CLocalAssum ({ loc } ::_,_,_,t)
  | CLocalDef ( { loc },_,t,None) -> Loc.merge_opt loc (constr_loc t)
  | CLocalDef ( { loc },_,b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
  | CLocalAssum ([],_,_,_) -> assert false
  | CLocalPattern { loc } -> loc

let local_binders_loc bll = match bll with
  | []     -> None
  | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))

(** Folds and maps *)
let is_constructor id =
  match
    Smartlocate.global_of_extended_global
      (Nametab.locate_extended (qualid_of_ident id))
  with
  | exception Not_found -> false
  | None -> false
  | Some gref -> Globnames.isConstructRef gref

let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
  | CPatRecord l ->
    List.fold_left (fun nacc (r, cp) -> cases_pattern_fold_names f h nacc cp) nacc l
  | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right (fun na (n,acc) -> (f na n,acc)) na (cases_pattern_fold_names f h nacc pat)
  | CPatOr (patl) ->
    List.fold_left (cases_pattern_fold_names f h) nacc patl
  | CPatCstr (_,patl1,patl2) ->
    List.fold_left (cases_pattern_fold_names f h)
      (Option.fold_left (List.fold_left (cases_pattern_fold_names f h)) nacc patl1) patl2
  | CPatNotation (_,_,(patl,patll,binderl),patl') ->
    List.fold_left (cases_pattern_fold_names f h)
      (List.fold_left (cases_pattern_fold_names f h) nacc
         (patl@List.flatten patll@List.map fst binderl)) patl'
  | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f h nacc pat
  | CPatAtom (Some qid)
      when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
      let (n, acc) = nacc in
      (f (qualid_basename qid) n, acc)
  | CPatPrim _ | CPatAtom _ -> nacc
  | CPatCast (p,t) ->
      let (n, acc) = nacc in
      cases_pattern_fold_names f h (n, h acc t) p

let ids_of_pattern_list p =
  fst (List.fold_left
    (List.fold_left (cases_pattern_fold_names Id.Set.add (fun () _ -> ())))
    (Id.Set.empty,()) p)

let ids_of_cases_tomatch tms =
  List.fold_right
    (fun (_, ona, indnal) l ->
       Option.fold_right (fun t ids -> fst (cases_pattern_fold_names Id.Set.add (fun () _ -> ()) (ids,()) t))
         indnal
         (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
    tms Id.Set.empty

let rec fold_local_binders g f n acc b = let open CAst in function
  | CLocalAssum (nal,_,bk,t)::l ->
    let nal = List.(map (fun {v} -> v) nal) in
    let n' = List.fold_right (Name.fold_right g) nal n in
    f n (fold_local_binders g f n' acc b l) t
  | CLocalDef ( { v = na },_,c,t)::l ->
    Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
  | CLocalPattern pat :: l ->
    let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
    fold_local_binders g f n acc b l
  | [] ->
    f n acc b

let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
    | CAppExpl ((_,_),l) -> List.fold_left (f n) acc l
    | CApp (t,l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
    | CProj (e,_,l,t) -> f n (List.fold_left (f n) acc (List.map fst l)) t
    | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
    | CLetIn (na,a,t,b) ->
      f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
    | CCast (a,_,b) -> f n (f n acc a) b
    | CNotation (_,_,(l,ll,bl,bll)) ->
      (* The following is an approximation: we don't know exactly if
         an ident is binding nor to which subterms bindings apply *)
      let acc = List.fold_left (f n) acc (l@List.flatten ll) in
      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None)) bl) acc bll
    | CGeneralization (_,c) -> f n acc c
    | CDelimiters (_,_,a) -> f n acc a
    | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
    | CCases (sty,rtnpo,al,bl) ->
      let ids = ids_of_cases_tomatch al in
      let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
      let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
      List.fold_right (fun {CAst.v=(patl,rhs)} acc ->
          let ids = ids_of_pattern_list patl in
          f (Id.Set.fold g ids n) acc rhs) bl acc
    | CLetTuple (nal,(ona,po),b,c) ->
      let n' = List.fold_right (CAst.with_val (Name.fold_right g)) nal n in
      f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n') (f n acc b) c
    | CIf (c,(ona,po),b1,b2) ->
      let acc = f n (f n (f n acc b1) b2) c in
      Option.fold_left
        (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
    | CFix (_,l) ->
      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_,_) -> g id) l n in
      List.fold_right (fun (_,_,ro,lb,t,c) acc ->
          fold_local_binders g f n'
            (fold_local_binders g f n acc t lb) c lb) l acc
    | CCoFix (_,_) ->
      Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
    | CArray (_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
    | CHole _ | CGenarg _ | CGenargGlob _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
      acc
  )

let free_vars_of_constr_expr c =
  let rec aux bdvars l = function
    | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
      let id = qualid_basename qid in
      if Id.List.mem id bdvars then l else Id.Set.add id l
    | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
  in aux [] Id.Set.empty c

let names_of_constr_expr c =
  let vars = ref Id.Set.empty in
  let rec aux () () = function
    | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
      let id = qualid_basename qid in vars := Id.Set.add id !vars
    | c -> fold_constr_expr_with_binders (fun a () -> vars := Id.Set.add a !vars) aux () () c
  in aux () () c; !vars

let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)

let rec fold_map_cases_pattern f h acc (CAst.{v=pt;loc} as p) = match pt with
  | CPatRecord l ->
    let acc, l = List.fold_left_map (fun acc (r, cp) -> let acc, cp = fold_map_cases_pattern f h acc cp in acc, (r, cp)) acc l in
    acc, CAst.make ?loc (CPatRecord l)
  | CPatAlias (pat,({CAst.v=na} as lna)) ->
    let acc, p = fold_map_cases_pattern f h acc pat in
    let acc = Name.fold_right f na acc in
    acc, CAst.make ?loc (CPatAlias (pat,lna))
  | CPatOr patl ->
    let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
    acc, CAst.make ?loc (CPatOr patl)
  | CPatCstr (c,patl1,patl2) ->
    let acc, patl1 = Option.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patl1 in
    let acc, patl2 = List.fold_left_map (fold_map_cases_pattern f h) acc patl2 in
    acc, CAst.make ?loc (CPatCstr (c,patl1,patl2))
  | CPatNotation (sc,ntn,(patl,patll,binderl),patl') ->
    let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
    let acc, patll = List.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patll in
    let acc, binderl' = List.fold_left_map (fold_fst (fold_map_cases_pattern f h)) acc binderl in
    let acc, patl' = List.fold_left_map (fold_map_cases_pattern f h) acc patl' in
    acc, CAst.make ?loc (CPatNotation (sc,ntn,(patl,patll,binderl'),patl'))
  | CPatDelimiters (depth,d,pat) ->
    let acc, p = fold_map_cases_pattern f h acc pat in
    acc, CAst.make ?loc (CPatDelimiters (depth,d,pat))
  | CPatAtom (Some qid)
      when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
    f (qualid_basename qid) acc, p
  | CPatPrim _ | CPatAtom _ -> (acc,p)
  | CPatCast (pat,t) ->
    let acc, pat = fold_map_cases_pattern f h acc pat in
    let t = h acc t in
    acc, CAst.make ?loc (CPatCast (pat,t))

(* Used in correctness and interface *)
let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e

let fold_map_local_binders f g e bl =
  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
  let open CAst in
  let h (e,bl) = function
      CLocalAssum(nal,r,k,ty) ->
      (map_binder g e nal, CLocalAssum(nal,r,k,f e ty)::bl)
    | CLocalDef( { loc ; v = na } as cna ,r,c,ty) ->
      (Name.fold_right g na e, CLocalDef(cna,r,f e c,Option.map (f e) ty)::bl)
    | CLocalPattern pat ->
      let e, pat = fold_map_cases_pattern g f e pat in
      (e, CLocalPattern pat::bl) in
  let (e,rbl) = List.fold_left h (e,[]) bl in
  (e, List.rev rbl)

let map_constr_expr_with_binders g f e = CAst.map (function
    | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
    | CApp (a,l) ->
      CApp (f e a,List.map (fun (a,i) -> (f e a,i)) l)
    | CProj (expl,p,l,a) ->
      CProj (expl,p,List.map (fun (a,i) -> (f e a,i)) l,f e a)
    | CProdN (bl,b) ->
      let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
    | CLambdaN (bl,b) ->
      let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b)
    | CLetIn (na,a,t,b) ->
      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
    | CCast (a,k,c) -> CCast (f e a, k, f e c)
    | CNotation (inscope,n,(l,ll,bl,bll)) ->
      (* This is an approximation because we don't know what binds what *)
      CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
                    List.map (fun bl -> snd (fold_map_local_binders f g e bl)) bll))
    | CGeneralization (b,c) -> CGeneralization (b,f e c)
    | CDelimiters (depth,s,a) -> CDelimiters (depth,s,f e a)
    | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
    | CCases (sty,rtnpo,a,bl) ->
      let bl = List.map (fun {CAst.v=(patl,rhs);loc} ->
          let ids = ids_of_pattern_list patl in
          CAst.make ?loc (patl,f (Id.Set.fold g ids e) rhs)) bl in
      let ids = ids_of_cases_tomatch a in
      let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
      CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
    | CLetTuple (nal,(ona,po),b,c) ->
      let e' = List.fold_right (CAst.with_val (Name.fold_right g)) nal e in
      let e'' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
      CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
    | CIf (c,(ona,po),b1,b2) ->
      let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
      CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
    | CFix (id,dl) ->
      CFix (id,List.map (fun (id,r,n,bl,t,d) ->
          let (e',bl') = fold_map_local_binders f g e bl in
          let t' = f e' t in
          (* Note: fix names should be inserted before the arguments... *)
          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_,_) -> g id e) e' dl in
          let d' = f e'' d in
          (id,r,n,bl',t',d')) dl)
    | CCoFix (id,dl) ->
      CCoFix (id,List.map (fun (id,r,bl,t,d) ->
          let (e',bl') = fold_map_local_binders f g e bl in
          let t' = f e' t in
          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
          let d' = f e'' d in
          (id,r,bl',t',d')) dl)
    | CArray (u, t, def, ty) ->
      CArray (u, Array.map (f e) t, f e def, f e ty)
    | CHole _ | CGenarg _ | CGenargGlob _ | CEvar _ | CPatVar _ | CSort _
    | CPrim _ | CRef _ as x -> x
  )

(* Used in constrintern *)
let rec replace_vars_constr_expr l r =
  match r with
  | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid ->
    let id = qualid_basename qid in
    (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us)
     with Not_found -> x)
  | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn

(* Returns the ranges of locs of the notation that are not occupied by args  *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)

let locs_of_notation ?loc locs ntn =
  let unloc loc = Option.cata Loc.unloc (0,0) loc in
  let (bl, el) = unloc loc        in
  let locs =  List.map unloc locs in
  let rec aux pos = function
    | [] -> if Int.equal pos el then [] else [(pos,el)]
    | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l
  in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)

let ntn_loc ?loc (args,argslist,binders,binderslist) =
  locs_of_notation ?loc
    (List.map constr_loc (args@List.flatten argslist)@
     List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@
     List.map local_binders_loc binderslist)

let patntn_loc ?loc (args,argslist,binders) =
  locs_of_notation ?loc
    (List.map cases_pattern_expr_loc (args@List.flatten argslist@List.map fst binders))

let error_invalid_pattern_notation ?loc () =
  CErrors.user_err ?loc  (str "Invalid notation for pattern.")

(** Pseudo-constructors *)

let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)
let mkRefC r      = CAst.make @@ CRef (r,None)
let mkCastC (a,k,t) = CAst.make @@ CCast (a,k,t)
let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,None,bk,a)],b)
let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,None,bk,a)],b)

let mkAppC (f,l) =
  let l = List.map (fun x -> (x,None)) l in
  match CAst.(f.v) with
  | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
  | _           -> CAst.make @@ CApp (f, l)

let mkProdCN ?loc bll c =
  if bll = [] then c else
  CAst.make ?loc @@ CProdN (bll,c)

let mkLambdaCN ?loc bll c =
  if bll = [] then c else
  CAst.make ?loc @@ CLambdaN (bll,c)

let mkCProdN ?loc bll c =
  CAst.make ?loc @@ CProdN (bll,c)

let mkCLambdaN ?loc bll c =
  CAst.make ?loc @@ CLambdaN (bll,c)

let coerce_reference_to_id qid =
  if qualid_is_ident qid then qualid_basename qid
  else
    CErrors.user_err ?loc:qid.CAst.loc
      (str "This expression should be a simple identifier.")

let coerce_to_id = function
  | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
    CAst.make ?loc @@ qualid_basename qid
  | { CAst.loc; _ } -> CErrors.user_err ?loc
                         (str "This expression should be a simple identifier.")

let coerce_to_name = function
  | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
    CAst.make ?loc @@ Name (qualid_basename qid)
  | { CAst.loc; v = CHole (None) } -> CAst.make ?loc Anonymous
  | { CAst.loc; _ } -> CErrors.user_err ?loc
                         (str "This expression should be a name.")

let mkCPatOr ?loc = function
  | [pat] -> pat
  | disjpat -> CAst.make ?loc @@ (CPatOr disjpat)

let mkAppPattern ?loc p lp =
  if List.is_empty lp then p else
  let open CAst in
  make ?loc @@ (match p.v with
  | CPatAtom (Some r) -> CPatCstr (r, None, lp)
  | CPatCstr (r, None, l2) ->
     CErrors.user_err ?loc:p.loc
                      (Pp.str "Nested applications not supported.")
  | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
  | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp)
  | _ -> CErrors.user_err ?loc:p.loc (Pp.str "Such pattern cannot have arguments."))

let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
  | CRef (r,None) ->
     CPatAtom (Some r)
  | CHole (None) ->
     CPatAtom None
  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
      when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
      CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
  | CApp (p,args) when List.for_all (fun (_,e) -> e=None) args ->
     (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
  | CAppExpl ((r,i),args) ->
     CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
  | CNotation (inscope,ntn,(c,cl,b,[])) ->
     CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,
                                List.map (List.map coerce_to_cases_pattern_expr) cl,
                                b),[])
  | CPrim p ->
     CPatPrim p
  | CRecord l ->
     CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
  | CDelimiters (depth,s,p) ->
     CPatDelimiters (depth,s,coerce_to_cases_pattern_expr p)
  | CCast (p,Some Constr.DEFAULTcast, t) ->
    CPatCast (coerce_to_cases_pattern_expr p,t)
  | CLambdaN _ | CProdN _ | CSort _ | CLetIn _ | CGeneralization _
  | CRef (_, Some _) | CCast (_, (Some (VMcast|NATIVEcast) | None), _)
  | CFix _ | CCoFix _ | CApp _ | CProj _ | CCases _ | CLetTuple _ | CIf _
  | CPatVar _ | CEvar _
  | CNotation (_,_,(_,_,_,_::_))
  | CHole (Some _) | CGenarg _ | CGenargGlob _ ->
    CErrors.user_err ?loc
                      (str "This expression should be coercible to a pattern.")
  | CArray _ ->
    CErrors.user_err ?loc
                      (str "Arrays in patterns not supported.")) c

let isCSort a =
  match a.CAst.v with Constrexpr.CSort _ -> true | _ -> false

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.24Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.